Merge pull request #28 from Villetaneuse/more_structure_in_index

More structure in index
coq · Jul 5, 2024 · 2003cbc · 2003cbc
2 parents 85fe471 + 6488b8a
commit 2003cbc
Show file tree

Hide file tree

Showing 5 changed files with 95 additions and 17 deletions.
diff --git a/src/images/coq-community-logo.ico b/src/images/coq-community-logo.ico
diff --git a/src/images/coq-community-logo.png b/src/images/coq-community-logo.png
diff --git a/src/images/github-mark.png b/src/images/github-mark.png
diff --git a/src/index.html b/src/index.html
@@ -1,27 +1,71 @@
 <!DOCTYPE html>
 <html>
-<head>
+  <head>
     <title>Coq Platform Docs - Demo</title>
-</head>
-<body>
+    <meta charset="utf8"/>
+    <link rel="stylesheet" href="style.css"/>
+    <link rel="shortcut icon" href="images/coq-community-logo.ico" type="image/x-icon">
+  </head>
+  <body>
     <h1>Coq Platform Docs - Demo</h1>
+
+    <div style="text-align:left">
+        <img src="images/github-mark.png" height="25" style="border:0px">
+        <a href="https://github.com/Zimmi48/platform-docs">
+            View Coq-Platform-Doc
+        </a>
+        <img src="images/github-mark.png" height="25" style="border:0px">
+    </div>
+
+    <h2 id="about">About</h2>
+    <p><a href="https://coq.inria.fr"><img src="images/coq-community-logo.png" align="right" width="100"></a></p>
     <p>
-        This is a demo page for the Coq Platform Docs.
+    This is a demo page for the Coq Platform Docs.
+    These tutorials are meant to become part of Rocq's next website and the
+    github repository should be part of the Coq organization.
     </p>
     <p>
-        List of available tutorials:
+    The interactive versions can be run in a web browser, for the source code,
+    one needs a text editor able to interact with Coq (e.g. CoqIDE, emacs with
+    Proof General, vim with CoqTail, vscode with vscoq).
     </p>
+
+    <h2 id="coq-tut">Coq Tutorials</h2>
     <ul>
-        <li><a href="RequireImportTutorial.html">Require/Import Tutorial (interactive version)</a></li>
-        <li><a href="RequireImportTutorial.v">Require/Import Tutorial (source code)</a></li>
-        <li><a href="SearchTutorial.html">Search Tutorial (interactive version)</a></li>
-        <li><a href="SearchTutorial.v">Search Tutorial (source code)</a></li>
-        <li><a href="Tutorial_Equations_basics.html">Equations Tutorial : basics (interactive version)</a></li>
-        <li><a href="Tutorial_Equations_basics.v">Equations Tutorial : basics (source code)</a></li>
-        <li><a href="Tutorial_Equations_Obligations.html">Equations Tutorial : obligations (interactive version)</a></li>
-        <li><a href="Tutorial_Equations_Obligations.v">Equations Tutorial : obligations (source code)</a></li>
-        <li><a href="Tutorial_Equations_wf.html">Equations Tutorial : well-founded recursion (interactive version)</a></li>
-        <li><a href="Tutorial_Equations_wf.v">Equations Tutorial : well-founded recursion (source code)</a></li>
+      <li>
+        Search Tutorial:
+        <a href="SearchTutorial.html">interactive version</a>
+        and
+        <a href="SearchTutorial.v">source code</a>
+      </li>
+      <li>
+        Basic library files and module management:
+        <a href="RequireImportTutorial.html">interactive version</a>
+        and
+        <a href="RequireImportTutorial.v">source code</a>
+      </li>
     </ul>
-</body>
-</html>
+
+    <h2 id=eq-tut>Equations tutorials</h2>
+    <ul>
+      <li>
+        Basics:
+        <a href="Tutorial_Equations_basics.html">interactive version</a>
+        and
+        <a href="Tutorial_Equations_basics.v">source code</a>
+      </li>
+      <li>
+        Obligations:
+        <a href="Tutorial_Equations_Obligations.html">interactive version</a>
+        and
+        <a href="Tutorial_Equations_Obligations.v">source code</a>
+      </li>
+      <li>
+        Well-founded recursion:
+        <a href="Tutorial_Equations_wf.html">interactive version</a>
+        and
+        <a href="Tutorial_Equations_wf.v">source code</a>
+      </li>
+    </ul>
+  </body>
+</html>
diff --git a/src/style.css b/src/style.css
@@ -0,0 +1,34 @@
+/* shamelessly taken from the Coq-community website */
+code {
+	white-space: pre-wrap;
+}
+span.smallcaps {
+	font-variant: small-caps;
+}
+span.underline {
+	text-decoration: underline;
+}
+div.column {
+	display: inline-block; vertical-align: top; width: 50%;
+}
+div.hanging-indent {
+	margin-left: 1.5em; text-indent: -1.5em;
+}
+ul.task-list {
+	list-style: none;
+}
+body {
+	font-family: Arial, Helvetica; margin-left: 5em; font-size: large;
+}
+h1 {
+	margin-left: 0em; padding: 0px; text-align: center
+}
+h2 {
+	margin-left: 0em; padding: 0px; color: #580909
+}
+h3 {
+	margin-left: 1em; padding: 0px; color: #C05001;
+}
+body {
+	width: 1100px; margin-left: 30px; 
+}