About
+ +Coq Platform Docs
+ -About
- 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.
- 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).
+- The documentation is working with the latesest version of Coq Platform, 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: +
-
+
- + The zulip channel + we use to discuss and work on the project + +
- + The associated Coq Enhacement Proposal + describing the project in details + +
- + The associated github repository + +
Contributing
+ ++ We welcome contributions, and there are plenty to do depending on how much available time you have: +
-
+
- + Give feedbacks on the existing tutorial and how-to guides on + zulip + +
- + Answer people's questions and share folklore that should be known by all on + zulip + +
- + Help to review tutorials and how-to guides, whether you are an expert or not + +
- + Help to improve and write tutorial and how-to guides + +
- + Help with the technical aspects of the project + +
Small Disclamer
+- 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: +
-
+
- + 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 + Coq Platform for Coq 8.19.2. + +
- + 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. + +
Documentation
Coq Tutorials
+ +Writing Proofs
- - Tutorial, Chaining Tactics to Simplify and Factorize proofs + Chaining Tactics to Simplify and Factorize proofs interactive version and source code +
Coq's Functionalities
+ +- - Search Tutorial: + Searching for Definitions and Lemma interactive version and source code
- - Basic library files and module management: + Basic Library Files and Module Management interactive version and source code +
Coq's Theory
+ +- - Explanation of template vs. “full” universe polymorphism: + Template Polymorphism vs. Universe Polymorphism: interactive version and source code
Equations tutorials
+Equations Tutorials
- - Basics: + The Basics of Equations interactive version and source code
- - Obligations: + Equations and Obligations interactive version and source code
- - Well-founded recursion: + Equations and Well-founded Recursion interactive version and source code diff --git a/src/style.css b/src/style.css index 7567172..0931a6c 100644 --- a/src/style.css +++ b/src/style.css @@ -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; }