WIP: refactor documentation according to Diátaxis.

data/tutorials/getting-started/1_01_a_tour_of_rocq.md → data/tutorials/tutorials/1_01_a_tour_of_rocq.md

@@ -4,7 +4,7 @@ title: A Tour of Rocq
 description: >
   Hop on the Rocq sightseeing bus. This absolute beginner tutorial will drive you through the marvels and wonders of the Rocq Prover.
 category: "First Steps"
-external_html: tutorials/getting-started/1_01_a_tour_of_rocq.html
+external_html: tutorials/tutorials/1_01_a_tour_of_rocq.html
 recommended_next_tutorials:
 ---
 

data/tutorials/getting-started/1_01_a_tour_of_rocq.md.orig → data/tutorials/tutorials/1_01_a_tour_of_rocq.md.orig

@@ -8,12 +8,12 @@ Instructions to generate 1_01_a_tour_of_rocq.md from 1_01_a_tour_of_rocq.md.orig
    $ source .venv/bin/activate
    $ pip install alectryon myst_parser
 3. Run the following command:
-   $ alectryon --frontend md --backend webpage data/tutorials/getting-started/1_01_a_tour_of_rocq.md.orig -o data/tutorials/getting-started/1_01_a_tour_of_rocq.html
+   $ alectryon --frontend md --backend webpage data/tutorials/tutorials/1_01_a_tour_of_rocq.md.orig -o data/tutorials/tutorials/1_01_a_tour_of_rocq.html
 4. Remove the untracked generated files:
-   $ rm data/tutorials/getting-started/alectryon.css data/tutorials/getting-started/alectryon.js data/tutorials/getting-started/docutils_basic.css data/tutorials/getting-started/pygments.css
+   $ rm data/tutorials/tutorials/alectryon.css data/tutorials/tutorials/alectryon.js data/tutorials/tutorials/docutils_basic.css data/tutorials/tutorials/pygments.css
 5. Replace all `<h1>` tags with `<h2>` tags in the generated 1_01_a_tour_of_rocq.html file (e.g. using `sed`):
-   $ sed -i 's/<h1>/<h2>/g' data/tutorials/getting-started/1_01_a_tour_of_rocq.html
-   $ sed -i 's/<\/h1>/<\/h2>/g' data/tutorials/getting-started/1_01_a_tour_of_rocq.html
+   $ sed -i 's/<h1>/<h2>/g' data/tutorials/tutorials/1_01_a_tour_of_rocq.html
+   $ sed -i 's/<\/h1>/<\/h2>/g' data/tutorials/tutorials/1_01_a_tour_of_rocq.html
 6. Remove the `</body>`, and `</html>` closing tags at the end of the generated 1_01_a_tour_of_rocq.html file.
 7. Remove everything before the following in the generated 1_01_a_tour_of_rocq.html file (as well as the closing comment marker):
 <div class="document">

data/tutorials/platform/2_02_chaining.md → data/tutorials/tutorials/2_02_chaining.md

@@ -5,7 +5,7 @@ author: Thomas Lamiaux
 description: |
    In this tutorial, we explain how to chain tactics together to write more concise code.
 category: "Documentation of Rocq"
-external_html: tutorials/platform/2_02_chaining.html
+external_html: tutorials/tutorials/2_02_chaining.html
 external_tutorial:
     contribute_link:
         url: https://github.com/coq/platform-docs

data/tutorials/platform/2_04_require-import.md → data/tutorials/tutorials/2_04_require-import.md

@@ -4,7 +4,7 @@ title: "Basic Library Files and Module Management"
 description: |
   This tutorial explains how to use the `Require` and `Import` commands to load libraries and modules in Rocq.
 category: "Documentation of Rocq"
-external_html: tutorials/platform/2_04_require-import.html
+external_html: tutorials/tutorials/2_04_require-import.html
 external_tutorial:
     contribute_link:
         url: https://github.com/coq/platform-docs

src/global/url.ml

@@ -91,9 +91,10 @@ let papers = "/papers"
 
 let paper id = "/papers/" ^ id
 let learn = "/docs"
-let learn_docs = "/docs/docs"
-let learn_guides = "/docs/guides"
-let learn_platform = "/docs/platform-docs"
+let tutorials = "/docs/tutorials"
+let guides = "/docs/guides"
+let explanations = "/docs/explanations"
+let references = "/docs/references"
 let platform = "/platform"
 let platform_page name = platform ^ "/" ^ name
 let consortium_page name = consortium ^ "/" ^ name

src/rocqproverorg_data/data_intf.ml

@@ -657,13 +657,12 @@ end
 
 module Tutorial = struct
   module Section = struct
-    type t = GetStarted | Language | Platform | Guides [@@deriving show]
+    type t = Tutorials | Guides | Explanations [@@deriving show]
 
     let of_string = function
-      | "getting-started" -> Ok GetStarted
-      | "language" -> Ok Language
-      | "platform" -> Ok Platform
+      | "tutorials" -> Ok Tutorials
       | "guides" -> Ok Guides
+      | "explanations" -> Ok Explanations
       | s -> Error (`Msg ("Unknown section: " ^ s))
   end
 

src/rocqproverorg_frontend/components/footer.eml

@@ -10,12 +10,12 @@ let about_rocq = [
 
 let resources = [
   (Url.install, "Install Rocq");
-  (Url.getting_started, "Get Started");
-  (Url.learn_platform, "Documentation");
-  (Url.manual, "Reference Manual");
-  (Url.stdlib, "Standard Library");
-  (Url.books, "Books");
+  (Url.tutorials, "Tutorials");
+  (Url.guides, "How-to guides");
+  (Url.explanations, "Explanations");
+  (Url.references, "References");
   (Url.exercises, "Exercises");
+  (Url.books, "Books");
   (Url.papers, "Papers");
   (Url.playground, "Rocq Playground");
   (Url.logos, "Logo");

src/rocqproverorg_frontend/components/header.eml

@@ -8,7 +8,7 @@ type nav_item =
   | Playground
 
 let string_of_nav_item = function
-  | Learn -> "Learn"
+  | Learn -> "Docs"
   | Platform -> "Platform"
   | Packages -> "Packages"
   | Community -> "Community"

src/rocqproverorg_frontend/components/learn_components.eml

@@ -61,7 +61,7 @@ let block_container ~icon ~title ~heading inner_html =
     </div>
   </div>
 
-let tutorial_block ~icon ~title ~heading ~description ~(tutorial_links: link list) ~see_more  =
+let tutorial_block ~icon ~title ~heading ~description ~(tutorial_links: link list)  =
   block_container ~icon ~title ~heading @@
   <div class="mt-4 text-content dark:text-dark-content text-base font-normal h-14 text-ellipsis overflow-hidden leading-7 max-w-prose"> <%s description %> </div>
   <ul class="flex flex-col grow gap-4 mt-5 md:h-60">
@@ -75,9 +75,6 @@ let tutorial_block ~icon ~title ~heading ~description ~(tutorial_links: link lis
     </li>
     <% ); %>
   </ul>
-  <a href="<%s see_more.href %>" class="mt-4 text-primary dark:text-dark-title hover:underline dark:hover:text-dark-primary dark:underline items-center leading-10">
-    <%s see_more.title %>
-  </a>
 
 let book_cover ~free cover_src = 
   <div class="relative">

src/rocqproverorg_frontend/layouts/learn_layout.eml

@@ -1,33 +1,37 @@
 type section =
   | Overview
-  | GetStarted
-  | Language
-  | Platform
+  | Tutorials
   | Guides
+  | Explanations
+  | References
   | Exercises
   | Books
+  | Papers
 
 let tabs
 ~current =
   let url_of_section = function
     | Overview -> Url.learn
-    | GetStarted -> Url.getting_started
-    | Language -> Url.learn_docs
-    | Platform -> Url.tutorial "platform-docs"
-    | Guides -> Url.learn_guides
+    | Tutorials -> Url.tutorials
+    | Guides -> Url.guides
+    | Explanations -> Url.explanations
+    | References -> Url.references
     | Exercises -> Url.exercises
     | Books -> Url.books
+    | Papers -> Url.papers
   in
   let title_of_section = function
     | Overview -> "Overview"
-    | GetStarted -> "Get Started"
-    | Language -> "Language"
-    | Platform -> "Documentation"
-    | Guides -> "Guides"
+    | Tutorials -> "Tutorials"
+    | Guides -> "How-to Guides"
+    | Explanations -> "Explanations"
+    | References -> "References"
     | Exercises -> "Exercises"
     | Books -> "Books"
+    | Papers -> "Papers"
   in
-  Layout.subnav_tabs ~title:"Learn" ~current ~sections:[Overview; GetStarted; Platform ; Guides; Exercises; Books] ~url_of_section ~title_of_section
+  Layout.subnav_tabs ~title:"Docs" ~current ~url_of_section ~title_of_section
+    ~sections:[Overview; Tutorials; Guides; Explanations; References; Exercises; Books; Papers]
 
 let render_sidebar
   ~current_tutorial

src/rocqproverorg_frontend/pages/learn.eml

@@ -61,22 +61,21 @@ Learn_layout.single_column_layout
 
     <div class="grid gap-6 md:gap-10 mt-6 md:grid-cols-2">
       <%s! Learn_components.tutorial_block
-              ~icon:Learn_components.beginner_section_icon ~title:"GET STARTED" ~heading:"Introduction To Rocq"
+              ~icon:Learn_components.beginner_section_icon ~title:"GET STARTED" ~heading:"Introduction to the Rocq Prover"
               ~description:"Install Rocq and gain a high-level understanding of the language"
               ~tutorial_links:[
                   {href = Url.tutorial "installing-rocq"; title = "Installing Rocq"};
                   {href = Url.tutorial "set-up-editor"; title = "Configuring Your Editor"};
-                  {href = Url.tutorial "tour-of-rocq"; title = "A Tour of Rocq"}
-(*                {href = Url.tutorial "opam-switch-introduction"; title = "Introduction to opam Switches"} *)
+                  {href = Url.tutorial "tour-of-rocq"; title = "A Tour of Rocq"};
+                  {href = Url.tutorial "chaining-tactics"; title = "Chaining Tactics"}
               ]
-              ~see_more:{href = Url.getting_started; title = "Get Started"}
               %>
-      <%s! Learn_components.tutorial_block ~icon:Learn_components.beginner_section_icon ~title:"Documentation" ~heading:"The Rocq Prover" 
-              ~description:"An in-depth explanation of language features and data structures from the Standard Library" 
+      <%s! Learn_components.tutorial_block ~icon:Learn_components.beginner_section_icon ~title:"ROCQ PLATFORM" ~heading:"Introduction to the Rocq Platform" 
+              ~description:"Discover the essential packages in the Rocq Platform" 
               ~tutorial_links:[
-                  {href = Url.tutorial "platform-docs"; title = "Rocq Platform Docs"};
+                  {href = Url.tutorial "equations"; title = "Pattern-matching with Equations"};
+                  {href = Url.tutorial "ltac2"; title = "Writing tactics with Ltac2"}
               ]
-              ~see_more:{href = Url.tutorial "platform-docs"; title = "Documentation"}
               %>
     </div>
 
@@ -102,49 +101,44 @@ Learn_layout.single_column_layout
     -->
   </div>
 
+  <!--
   <div class="section-mild-contrast bg-sand dark:dark-section-strong-contrast">
     <div class="container-fluid flex flex-col py-9">
-      <%s! Learn_components.block_heading ~icon:"" ~title:"PLATFORM TOOLS" ~heading:"The Rocq Platform" %>
+      <%s! Learn_components.block_heading ~icon:"" ~title:"The Rocq Platform" ~heading:"The Rocq Platform" %>
       <div class="mt-10 flex flex-col md:flex-row gap-10">
         <%s! Learn_components.tool_card ~img_src:"img/learn/opam_logo.png"
             ~title:"opam" ~text:"OCaml's package manager for managing Rocq and libraries"
             ~url:"https://opam.ocaml.org" %>
       </div>
-      <a class="pt-6 pb-3 text-primary dark:text-dark-title hover:underline dark:underline dark:hover:text-dark-primary" href="<%s Url.learn_platform %>">Go to Platform Tools Documentation</a>
+      <a class="pt-6 pb-3 text-primary dark:text-dark-title hover:underline dark:underline dark:hover:text-dark-primary" href="<%s Url.tutorials %>">Go to Rocq Platform tutorials.</a>
     </div>
   </div>
+  -->
 
   <div class="container-fluid">
     <h2 id="intermediate_section" class="mt-16 mb-8 text-content dark:text-dark-title text-3xl font-regular leading-9 tracking-widest">
       <span class="text-gray-700 dark:text-dark-tertiary font-bold">EXPLORING</span>
       THE INTERMEDIATE LEVEL
     </h2>
-  <!--
     <div class="grid gap-6 md:gap-10 mt-6 md:grid-cols-2">
-      <%s! Learn_components.tutorial_block ~icon:Learn_components.intermediate_section_icon ~title:"GUIDES" ~heading:"Practical-Minded Tutorials and Guides" 
-              ~description:"How to solve real-world problems in OCaml" 
+      <%s! Learn_components.tutorial_block ~icon:Learn_components.intermediate_section_icon ~title:"FEATURES" ~heading:"Diving into the Rocq Prover features" 
+              ~description:"Learn all the Rocq features you need to be productive" 
               ~tutorial_links:[
-                  {href = Url.tutorial "formatting-text"; title = "Formatting and Wrapping Text"};
-                  {href = Url.tutorial "debugging"; title = "Debugging"};
-                  {href = Url.tutorial "error-handling"; title = "Error Handling"};
-                  {href = Url.tutorial "profiling"; title = "Profiling"}
+                  {href = Url.tutorial "search"; title = "Searching lemmas"};
+                  {href = Url.tutorial "require-import"; title = "Module management"};
+                  {href = Url.tutorial "template-poly"; title = "Understanding template vs. universe polymorphism"}
               ]
-              ~see_more:{href = Url.learn_guides; title = "See More Guides"}
               %>
-      <%s! Learn_components.tutorial_block ~icon:Learn_components.intermediate_section_icon ~title:"PLATFORM" ~heading:"The OCaml Platform" 
-          ~description:"Learn to leverage the tooling around OCaml and create your own projects and libraries" 
+      <%s! Learn_components.tutorial_block ~icon:Learn_components.intermediate_section_icon ~title:"ROCQ PLATFORM" ~heading:"Doing more with the Rocq Platform" 
+          ~description:"Take full advantage of the power of the Rocq ecosystem" 
           ~tutorial_links:[
-              {href = Url.tutorial "bootstrapping-a-dune-project"; title = "Bootstrapping a Project"};
-              {href = Url.tutorial "managing-dependencies"; title = "Managing Dependencies"};
-              {href = Url.tutorial "install-a-specific-ocaml-compiler-version"; title = "Install a Specific Compiler Version"};
-              {href = Url.tutorial "configuring-your-editor"; title = "Configuring Your Editor"}
+              {href = Url.tutorial "equations-obligations"; title = "Solving obligations generated by Equations"};
+              {href = Url.tutorial "equations-wf"; title = "Defining well-founded functions with Equations"}
           ]
-          ~see_more:{href = Url.learn_platform; title = "Platform Tools Documentation"}
           %>
     </div>
 
     <div class="border-t border-separator_30 dark:border-dark-separator_30 my-6"></div>
-  -->
     <div class="grid gap-6 mt-6 lg:grid-cols-2">
       <%s! Learn_components.book_recommendation
         (Data.Book.get_by_slug "mathcomp" |> Option.get)

src/rocqproverorg_frontend/pages/tutorial.eml

@@ -29,10 +29,9 @@ let left_sidebar ~tutorials ~current_tutorial ~section =
 
 let of_tutorial_section (s: Data.Tutorial.Section.t) =
   match s with
-  | GetStarted -> Learn_layout.GetStarted
-  | Language -> Learn_layout.Language
-  | Platform -> Learn_layout.Platform
+  | Tutorials -> Learn_layout.Tutorials
   | Guides -> Learn_layout.Guides
+  | Explanations -> Learn_layout.Explanations
 
 let render_related_exercises exercises =
   if List.length exercises > 0 then

src/rocqproverorg_web/lib/handler.ml

@@ -24,10 +24,10 @@ let learn _req =
   let latest_platform_version = Data.Release.latest_platform.version in
   Dream.html (Rocqproverorg_frontend.learn ~papers ~latest_platform_version)
 
-let learn_docs req =
+let learn_tutorials req =
   let tutorials =
     Data.Tutorial.all
-    |> List.filter (fun (t : Data.Tutorial.t) -> t.section = Language)
+    |> List.filter (fun (t : Data.Tutorial.t) -> t.section = Tutorials)
   in
   Dream.redirect req (Url.tutorial (List.hd tutorials).slug)
 
@@ -38,6 +38,13 @@ let learn_guides req =
   in
   Dream.redirect req (Url.tutorial (List.hd tutorials).slug)
 
+  let learn_explanations req =
+    let tutorials =
+      Data.Tutorial.all
+      |> List.filter (fun (t : Data.Tutorial.t) -> t.section = Explanations)
+    in
+    Dream.redirect req (Url.tutorial (List.hd tutorials).slug)
+
 let community _req =
   let query = Dream.query _req "e" in
   let string_to_event_type s =

src/rocqproverorg_web/lib/router.ml

@@ -26,8 +26,9 @@ let page_routes _t =
       Dream.get Url.index Handler.index;
       Dream.get Url.install Handler.install;
       Dream.get Url.learn Handler.learn;
-      Dream.get Url.learn_docs Handler.learn_docs;
-      Dream.get Url.learn_guides Handler.learn_guides;
+      Dream.get Url.tutorials Handler.learn_tutorials;
+      Dream.get Url.guides Handler.learn_guides;
+      Dream.get Url.explanations Handler.learn_explanations;
       Dream.get Url.community Handler.community;
       Dream.get Url.consortium Handler.consortium;
       Dream.get (Url.consortium_page ":id") (Handler.consortium_page Commit.hash);

src/rocqproverorg_web/lib/sitemap.ml

@@ -17,9 +17,10 @@ let urls =
     Url.consortium;
     Url.events;
     Url.exercises;
-    Url.getting_started;
+    Url.explanations;
     Url.governance;
     Url.governance_policy;
+    Url.guides;
     Url.index;
     Url.industrial_users;
     Url.industrial_businesses;
@@ -32,7 +33,9 @@ let urls =
     Url.platform;
     Url.playground;
     Url.privacy_policy;
+    Url.references;
     Url.releases;
+    Url.tutorials;
   ]
 
 let to_url u = "\n<url><loc>https://rocq-prover.org" ^ u ^ "</loc></url>"