Skip to content

Commit 1c200ab

Browse files
thomas-lamiauxthomas-lamiaux
authored
Improve web page (#70)
* some work on 1st page * improve web page
1 parent 7a1004a commit 1c200ab

File tree

2 files changed

+111
-31
lines changed

2 files changed

+111
-31
lines changed

‎src/index.html‎

Lines changed: 96 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,93 +1,163 @@
11
<!DOCTYPE html>
22
<html>
33
<head>
4-
<title>Coq Platform Docs - Demo</title>
4+
<title>Coq Platform Docs</title>
55
<meta charset="utf8"/>
66
<link rel="stylesheet" href="style.css"/>
77
<link rel="shortcut icon" href="images/coq-community-logo.ico" type="image/x-icon">
88
</head>
99
<body>
10-
<h1>Coq Platform Docs - Demo</h1>
10+
<h1>Coq Platform Docs</h1>
1111

12-
<div style="text-align:left">
12+
<!-- <div style="text-align:left">
1313
<img src="images/github-mark.png" height="25" style="border:0px">
1414
<a href="https://github.com/coq/platform-docs">
1515
View Coq-Platform-Doc
1616
</a>
1717
<img src="images/github-mark.png" height="25" style="border:0px">
18-
</div>
18+
</div> -->
19+
20+
<h2 id="project">About</h2>
21+
22+
<h3 id="about">Coq Platform Docs</h3>
23+
1924

20-
<h2 id="about">About</h2>
2125
<p><a href="https://coq.inria.fr"><img src="images/coq-community-logo.png" align="right" width="100"></a></p>
2226
<p>
23-
This is a demo page for the Coq Platform Docs.
24-
These tutorials are meant to become part of Rocq's next website and the
25-
github repository should be part of the Coq organization.
27+
This project aims to collaboratively create an action-oriented and interactive
28+
documentation for Coq and its Platform.
29+
Each core functionality and plugin of Coq and the Coq Platform will have one
30+
or several interactive tutorials and/or how-to guides explaining how to use
31+
them in practice.
32+
They should further be available online through an interactive interface,
33+
which this website is a demo page.
2634
</p>
2735
<p>
28-
The interactive versions can be run in a web browser, for the source code,
29-
one needs a text editor able to interact with Coq (e.g. CoqIDE, emacs with
36+
The first tutorials are already available and can be checked out below.
37+
They can either be runned interactively in a web browser thanks to JsCoq, or
38+
downloaded and runned with a text editor able to interact with Coq (e.g. CoqIDE, emacs with
3039
Proof General, vim with CoqTail, vscode with vscoq).
3140
</p>
41+
3242
<p>
33-
The documentation is working with the latesest version of <a href="https://github.com/coq/platform/blob/main/doc/README~8.19~2024.10.md">Coq Platform</a>, i.e 8.19.2.
34-
It is planned in the future to index the documentation and the Coq Platform's version and to have a dev version of it,
35-
so that users can find docmentation working for their version of the Coq and the Platform.
36-
It is not the case as of yet, so the documentation it is not guaranteed to work perfectly on other versions of Coq and the Platform,
37-
though most of the content should still be working fine.
43+
Some Ressources:
44+
<ul>
45+
<li>
46+
The <a href="https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs">zulip channel</a>
47+
we use to discuss and work on the project
48+
</li>
49+
<li>
50+
The associated <a href="https://github.com/coq/ceps/pull/91">Coq Enhacement Proposal</a>
51+
describing the project in details
52+
</li>
53+
<li>
54+
The associated <a href="https://github.com/coq/platform-docs">github repository</a>
55+
</li>
56+
</ul>
57+
</p>
58+
59+
<h3>Contributing</h3>
60+
61+
<p>
62+
We welcome contributions, and there are plenty to do depending on how much available time you have:
63+
<ul>
64+
<li>
65+
Give feedbacks on the existing tutorial and how-to guides on
66+
<a href="https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs">zulip</a>
67+
</li>
68+
<li>
69+
Answer people's questions and share folklore that should be known by all on
70+
<a href="https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs">zulip</a>
71+
</li>
72+
<li>
73+
Help to review tutorials and how-to guides, whether you are an expert or not
74+
</li>
75+
<li>
76+
Help to improve and write tutorial and how-to guides
77+
</li>
78+
<li>
79+
Help with the technical aspects of the project
80+
</li>
81+
</ul>
3882
</p>
3983

84+
<h3>Small Disclamer</h3>
85+
4086
<p>
41-
For this demo, we are relying on JsCoq1 that only supports Coq up to 8.17.
42-
Consequently, it may be failing for some content that need Coq 8.19.
43-
We hope to switch soon to JsCoq2.
87+
This is a demo, so not everything is working perfectly yet:
88+
<ul>
89+
<li>
90+
In the future, the documentation is planned to be indexed on the
91+
Coq Platform's version, but as of yet, it is only guaranteed to fully work
92+
with the latest version of the
93+
<a href="https://github.com/coq/platform/blob/main/doc/README~8.19~2024.10.md">Coq Platform</a> for Coq 8.19.2.
94+
</li>
95+
<li>
96+
The interactive interface is relying on JsCoq1 that only supports Coq up to 8.17
97+
so it may fail on some content requiring Coq 8.19.
98+
We are working towards switching to JsCoq2.
99+
</li>
100+
</ul>
44101
</p>
45102

103+
<h1 id="doc">Documentation</h1>
46104

47105
<h2 id="coq-tut">Coq Tutorials</h2>
106+
107+
<h3>Writing Proofs</h3>
48108
<ul>
49109
<li>
50-
Tutorial, Chaining Tactics to Simplify and Factorize proofs
110+
Chaining Tactics to Simplify and Factorize proofs
51111
<a href="Tutorial_Chaining_Tactics.html">interactive version</a>
52112
and
53113
<a href="Tutorial_Chaining_Tactics.v">source code</a>
54114
</li>
115+
</ul>
116+
117+
<h3>Coq's Functionalities</h3>
118+
119+
<ul>
55120
<li>
56-
Search Tutorial:
121+
Searching for Definitions and Lemma
57122
<a href="SearchTutorial.html">interactive version</a>
58123
and
59124
<a href="SearchTutorial.v">source code</a>
60125
</li>
61126
<li>
62-
Basic library files and module management:
127+
Basic Library Files and Module Management
63128
<a href="RequireImportTutorial.html">interactive version</a>
64129
and
65130
<a href="RequireImportTutorial.v">source code</a>
66131
</li>
132+
</ul>
133+
134+
<h3>Coq's Theory</h3>
135+
136+
<ul>
67137
<li>
68-
Explanation of template vs. “full” universe polymorphism:
138+
Template Polymorphism vs. Universe Polymorphism:
69139
<a href="Explanation_Template_Polymorphism.html">interactive version</a>
70140
and
71141
<a href="Explanation_Template_Polymorphism.v">source code</a>
72142
</li>
73143
</ul>
74144

75-
<h2 id=eq-tut>Equations tutorials</h2>
145+
<h2 id=eq-tut>Equations Tutorials</h2>
76146
<ul>
77147
<li>
78-
Basics:
148+
The Basics of Equations
79149
<a href="Tutorial_Equations_basics.html">interactive version</a>
80150
and
81151
<a href="Tutorial_Equations_basics.v">source code</a>
82152
</li>
83153
<li>
84-
Obligations:
154+
Equations and Obligations
85155
<a href="Tutorial_Equations_Obligations.html">interactive version</a>
86156
and
87157
<a href="Tutorial_Equations_Obligations.v">source code</a>
88158
</li>
89159
<li>
90-
Well-founded recursion:
160+
Equations and Well-founded Recursion
91161
<a href="Tutorial_Equations_wf.html">interactive version</a>
92162
and
93163
<a href="Tutorial_Equations_wf.v">source code</a>

‎src/style.css‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,17 +18,27 @@ ul.task-list {
1818
list-style: none;
1919
}
2020
body {
21-
font-family: Arial, Helvetica; margin-left: 5em; font-size: large;
21+
font-family: Arial, Helvetica; margin-left: 5em; margin-top: 1em; margin-bottom: 4em; font-size: large;
2222
}
2323
h1 {
24-
margin-left: 0em; padding: 0px; text-align: center
24+
margin-left: 0em; margin-top: 2em; text-align: center
2525
}
2626
h2 {
27-
margin-left: 0em; padding: 0px; color: #580909
27+
margin-left: 0em; padding: 0px; color: #1e6bb8
28+
/* margin-left: 0em; padding: 0px; color: #185693 */
29+
/* margin-left: 0em; padding: 0px; color: #580909 */
30+
/* margin-left: 0em; padding: 0px; color: #f15a24 */
31+
2832
}
2933
h3 {
30-
margin-left: 1em; padding: 0px; color: #C05001;
34+
/* margin-left: 1em; padding: 0px; color: #C05001; */
35+
/* margin-left: 1em; padding: 0px; color: #f7931e; */
36+
margin-left: 1em; padding: 0px; color: #f15a24
37+
/* margin-left: 1em; padding: 0px; color: #1e6bb8 */
38+
}
39+
h4 {
40+
margin-left: 2.5em; padding: 0px;
3141
}
3242
body {
33-
width: 1100px; margin-left: 30px;
43+
width: 1100px; margin-left: 30px;
3444
}

0 commit comments

Comments
 (0)