Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve web page #70

Merged
merged 3 commits into from
Nov 7, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 96 additions & 26 deletions src/index.html
Original file line number Diff line number Diff line change
@@ -1,93 +1,163 @@
<!DOCTYPE html>
<html>
<head>
<title>Coq Platform Docs - Demo</title>
<title>Coq Platform Docs</title>
<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>
<h1>Coq Platform Docs</h1>

<div style="text-align:left">
<!-- <div style="text-align:left">
<img src="images/github-mark.png" height="25" style="border:0px">
<a href="https://github.com/coq/platform-docs">
View Coq-Platform-Doc
</a>
<img src="images/github-mark.png" height="25" style="border:0px">
</div>
</div> -->

<h2 id="project">About</h2>

<h3 id="about">Coq Platform Docs</h3>


<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.
These tutorials are meant to become part of Rocq's next website and the
github repository should be part of the Coq organization.
This project aims to collaboratively create an action-oriented and interactive
documentation for Coq and its Platform.
Each core functionality and plugin of Coq and the Coq Platform will have one
or several interactive tutorials and/or how-to guides explaining how to use
them in practice.
They should further be available online through an interactive interface,
which this website is a demo page.
</p>
<p>
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
The first tutorials are already available and can be checked out below.
They can either be runned interactively in a web browser thanks to JsCoq, or
downloaded and runned with a text editor able to interact with Coq (e.g. CoqIDE, emacs with
Proof General, vim with CoqTail, vscode with vscoq).
</p>

<p>
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.
It is planned in the future to index the documentation and the Coq Platform's version and to have a dev version of it,
so that users can find docmentation working for their version of the Coq and the Platform.
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,
though most of the content should still be working fine.
Some Ressources:
<ul>
<li>
The <a href="https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs">zulip channel</a>
we use to discuss and work on the project
</li>
<li>
The associated <a href="https://github.com/coq/ceps/pull/91">Coq Enhacement Proposal</a>
describing the project in details
</li>
<li>
The associated <a href="https://github.com/coq/platform-docs">github repository</a>
</li>
</ul>
</p>

<h3>Contributing</h3>

<p>
We welcome contributions, and there are plenty to do depending on how much available time you have:
<ul>
<li>
Give feedbacks on the existing tutorial and how-to guides on
<a href="https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs">zulip</a>
</li>
<li>
Answer people's questions and share folklore that should be known by all on
<a href="https://coq.zulipchat.com/#narrow/stream/437203-Platform-docs">zulip</a>
</li>
<li>
Help to review tutorials and how-to guides, whether you are an expert or not
</li>
<li>
Help to improve and write tutorial and how-to guides
</li>
<li>
Help with the technical aspects of the project
</li>
</ul>
</p>

<h3>Small Disclamer</h3>

<p>
For this demo, we are relying on JsCoq1 that only supports Coq up to 8.17.
Consequently, it may be failing for some content that need Coq 8.19.
We hope to switch soon to JsCoq2.
This is a demo, so not everything is working perfectly yet:
<ul>
<li>
In the future, the documentation is planned to be indexed on the
Coq Platform's version, but as of yet, it is only guaranteed to fully work
with the latest version of the
<a href="https://github.com/coq/platform/blob/main/doc/README~8.19~2024.10.md">Coq Platform</a> for Coq 8.19.2.
</li>
<li>
The interactive interface is relying on JsCoq1 that only supports Coq up to 8.17
so it may fail on some content requiring Coq 8.19.
We are working towards switching to JsCoq2.
</li>
</ul>
</p>

<h1 id="doc">Documentation</h1>

<h2 id="coq-tut">Coq Tutorials</h2>

<h3>Writing Proofs</h3>
<ul>
<li>
Tutorial, Chaining Tactics to Simplify and Factorize proofs
Chaining Tactics to Simplify and Factorize proofs
<a href="Tutorial_Chaining_Tactics.html">interactive version</a>
and
<a href="Tutorial_Chaining_Tactics.v">source code</a>
</li>
</ul>

<h3>Coq's Functionalities</h3>

<ul>
<li>
Search Tutorial:
Searching for Definitions and Lemma
<a href="SearchTutorial.html">interactive version</a>
and
<a href="SearchTutorial.v">source code</a>
</li>
<li>
Basic library files and module management:
Basic Library Files and Module Management
<a href="RequireImportTutorial.html">interactive version</a>
and
<a href="RequireImportTutorial.v">source code</a>
</li>
</ul>

<h3>Coq's Theory</h3>

<ul>
<li>
Explanation of template vs. “full” universe polymorphism:
Template Polymorphism vs. Universe Polymorphism:
<a href="Explanation_Template_Polymorphism.html">interactive version</a>
and
<a href="Explanation_Template_Polymorphism.v">source code</a>
</li>
</ul>

<h2 id=eq-tut>Equations tutorials</h2>
<h2 id=eq-tut>Equations Tutorials</h2>
<ul>
<li>
Basics:
The Basics of Equations
<a href="Tutorial_Equations_basics.html">interactive version</a>
and
<a href="Tutorial_Equations_basics.v">source code</a>
</li>
<li>
Obligations:
Equations and 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:
Equations and Well-founded Recursion
<a href="Tutorial_Equations_wf.html">interactive version</a>
and
<a href="Tutorial_Equations_wf.v">source code</a>
Expand Down
20 changes: 15 additions & 5 deletions src/style.css
Original file line number Diff line number Diff line change
Expand Up @@ -18,17 +18,27 @@ ul.task-list {
list-style: none;
}
body {
font-family: Arial, Helvetica; margin-left: 5em; font-size: large;
font-family: Arial, Helvetica; margin-left: 5em; margin-top: 1em; margin-bottom: 4em; font-size: large;
}
h1 {
margin-left: 0em; padding: 0px; text-align: center
margin-left: 0em; margin-top: 2em; text-align: center
}
h2 {
margin-left: 0em; padding: 0px; color: #580909
margin-left: 0em; padding: 0px; color: #1e6bb8
/* margin-left: 0em; padding: 0px; color: #185693 */
/* margin-left: 0em; padding: 0px; color: #580909 */
/* margin-left: 0em; padding: 0px; color: #f15a24 */

}
h3 {
margin-left: 1em; padding: 0px; color: #C05001;
/* margin-left: 1em; padding: 0px; color: #C05001; */
/* margin-left: 1em; padding: 0px; color: #f7931e; */
margin-left: 1em; padding: 0px; color: #f15a24
/* margin-left: 1em; padding: 0px; color: #1e6bb8 */
}
h4 {
margin-left: 2.5em; padding: 0px;
}
body {
width: 1100px; margin-left: 30px;
width: 1100px; margin-left: 30px;
}
Loading