Plug in Rocq deployment repo (refman, stdlib and api).

Author: Zimmi48

Dockerfile

@@ -34,12 +34,12 @@ COPY --from=build /home/opam/_build/default/src/ocamlorg_web/bin/main.exe /bin/s
 
 COPY playground/asset playground/asset
 
-RUN git clone https://github.com/ocaml-web/html-compiler-manuals /manual
+RUN git clone --depth=1 https://github.com/coq/doc /doc
 
 RUN git config --global --add safe.directory /var/opam-repository
 
 ENV OCAMLORG_REPO_PATH /var/opam-repository/
-ENV OCAMLORG_MANUAL_PATH /manual
+ENV DOC_PATH /doc
 ENV OCAMLORG_PKG_STATE_PATH /var/package.state
 ENV DREAM_VERBOSITY info
 ENV OCAMLORG_HTTP_PORT 8080

doc/FOR_MAINTAINERS.md renamed to FOR_MAINTAINERS.md

@@ -3,7 +3,6 @@ let install = "/install"
 let packages = "/packages"
 let packages_search = "/packages/search"
 let packages_autocomplete_fragment = "/packages/autocomplete"
-
 let rocq_org = "https://rocq-prover.org"
 
 module Package : sig
@@ -48,12 +47,19 @@ let about = "/about"
 let minor v =
   match String.split_on_char '.' v with
   | x :: y :: _ -> x ^ "." ^ y
-  | _ -> invalid_arg (v ^ ": invalid OCaml version")
+  | _ -> invalid_arg (v ^ ": invalid  version")
+
+let patch v =
+  match String.split_on_char '.' v with
+  | x :: y :: z :: _ -> x ^ "." ^ y ^ "." ^ z
+  | _ -> invalid_arg (v ^ ": invalid  version")
 
 let v2 = "https://v2.ocaml.org"
-let manual_with_version v = "/manual/" ^ minor v ^ "/index.html"
-let manual = "/manual"
-let api_with_version v = "/manual/" ^ minor v ^ "/api/index.html"
+let manual_with_version v = "/doc/V" ^ patch v ^ "/refman/index.html"
+let manual = "/refman"
+let stdlib_with_version v = "/doc/V" ^ patch v ^ "/stdlib/index.html"
+let stdlib = "/stdlib"
+let api_with_version v = "/doc/V" ^ patch v ^ "/api/index.html"
 let api = "/api"
 let books = "/books"
 let changelog = "/changelog"

doc/personas.md

@@ -10,8 +10,8 @@ let resources = [
   (Url.install, "Install Rocq");
   (Url.getting_started, "Get Started");
   (Url.learn_platform, "Documentation");
-  (Url.manual, "Language Manual");
-  (Url.api, "Standard Library API");
+  (Url.manual, "Reference Manual");
+  (Url.stdlib, "Standard Library");
   (Url.books, "Books");
   (Url.exercises, "Exercises");
   (Url.papers, "Papers");

src/global/url.ml

@@ -41,8 +41,8 @@ let render
 =
 let search_dropdown () =
   <div id="header-search-results" aria-live="polite"></div>
-  <a class="flex py-2 px-2 mx-2 gap-4 hover:bg-primary_nav_block_hover_10 dark:hover:bg-dark-primary_nav_block_hover_10 font-normal rounded-md text-primary dark:text-dark-primary" href="<%s Url.api %>">
-    Standard Library API
+  <a class="flex py-2 px-2 mx-2 gap-4 hover:bg-primary_nav_block_hover_10 dark:hover:bg-dark-primary_nav_block_hover_10 font-normal rounded-md text-primary dark:text-dark-primary" href="<%s Url.stdlib %>">
+    Standard Library
     <%s! Icons.arrow_top_right_on_square "w-6 h-6" %>
   </a>
 in
@@ -129,7 +129,7 @@ in
       <li><%s! menu_link ~_class:"block" ~active:(active_top_nav_item=Some n) ~href:(url_of_nav_item n) ~title:(string_of_nav_item n) () %></li>
       <% ); %>
       <li>
-        <a href="<%s Url.api %>" class="flex py-3 px-1 gap-4 font-semibold text-primary dark:text-dark-primary">Standard Library API<%s! Icons.arrow_top_right_on_square "w-6 h-6" %></a>
+        <a href="<%s Url.stdlib %>" class="flex py-3 px-1 gap-4 font-semibold text-primary dark:text-dark-primary">Standard Library<%s! Icons.arrow_top_right_on_square "w-6 h-6" %></a>
       </li>
       <li class="mt-3 mb-6">
         <a href="<%s Url.getting_started %>" class="w-full rounded font-normal py-3 px-7 flex items-center justify-center bg-primary dark:bg-dark-primary text-white dark:text-dark-title">Get started</a>

src/ocamlorg_frontend/components/footer.eml

@@ -131,10 +131,10 @@ let lang_manual_banner =
       <div class="flex flex-col flex-grow my-6">
         <div class="text-white text-sm font-medium tracking-widest leading-10">GUIDE</div>
         <h2 class="text-white text-3xl font-bold leading-10">
-          Language Manual
+          Reference Manual
         </h3>
         <p class="mt-4 text-white font-normal max-w-xl text-base leading-7">
-          The Rocq prover manual is a comprehensive guide covering syntax, features, and usage. It assists developers and learners in understanding capabilities, best practices, and language features.
+          The reference manual is the authoritative source of documentation for the Rocq prover. It contains a changelog describing updates to Rocq, which we recommend you read when you upgrade.
         </p>
         <div class="w-full md:w-80 mt-6 py-2 bg-white rounded-xl text-center text-primary dark:text-dark-primary hover:underline font-bold text-lg">
           Take Me There

src/ocamlorg_frontend/components/header.eml

@@ -487,18 +487,18 @@ Layout.render
         </a>
         <a href="<%s Url.manual %>" class="card dark:dark-card p-4 text-title dark:text-dark-white">
           <%s! Icons.document "h-16 w-16 mb-8" %>
-          <p class="font-semibold text-xl mb-3">Language Manual</p>
-          <p>Read the reference manual of the language.</p>
+          <p class="font-semibold text-xl mb-3">Reference Manual</p>
+          <p>The authoritative reference for the Rocq prover (not learning oriented).</p>
         </a>
         <a href="<%s Url.books %>" class="card dark:dark-card p-4 text-title dark:text-dark-white">
           <%s! Icons.book "h-16 w-16 mb-8" %>
           <p class="font-semibold text-xl mb-3">Books</p>
           <p>Discover Rocq books from expert programmers and researchers - from beginner level to advanced topics.</p>
         </a>
-        <a href="<%s Url.api %>" class="card dark:dark-card p-4 text-title dark:text-dark-white">
+        <a href="<%s Url.stdlib %>" class="card dark:dark-card p-4 text-title dark:text-dark-white">
           <%s! Icons.command_line "h-16 w-16 mb-8" %>
           <p class="font-semibold text-xl mb-3">Standard Library</p>
-          <p>Searchable API documentation.</p>
+          <p>The documentation of the standard library.</p>
         </a>
         <a href="<%s Url.exercises %>" class="card dark:dark-card p-4 text-title dark:text-dark-white">
           <%s! Icons.hand_palm "h-16 w-16 mb-8" %>
@@ -508,7 +508,7 @@ Layout.render
         <a href="<%s Url.papers %>" class="card dark:dark-card p-4 text-title dark:text-dark-white">
           <%s! Icons.papers "h-16 w-16 mb-8" %>
           <p class="font-semibold text-xl mb-3">Papers</p>
-          <p>Explore papers that have influenced or used Rocq.</p>
+          <p>Explore papers that have influenced or used the Rocq prover.</p>
         </a>
       </div>
     </div>

src/ocamlorg_frontend/components/learn_components.eml

@@ -26,7 +26,7 @@ Learn_layout.single_column_layout
 
       <div class="flex flex-col gap-4 md:gap-6 md:w-80">
         <%s!  Hero_section.hero_button ~left_icon:(Icons.rocq "w-5 h-5") ~right_icon:(Icons.download "w-5 h-5") ~text:("Install Rocq " ^ latest_version) ~href:(Url.install) "" %>
-        <%s!  Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Standard Library API") ~href:(Url.api) "" %>
+        <%s!  Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Standard Library") ~href:(Url.stdlib) "" %>
         <%s!  Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Rocq Reference Manual") ~href:(Url.manual) "" %>
       </div>
     </div>

src/ocamlorg_frontend/pages/home.eml

@@ -9,8 +9,8 @@ Layout.render
 
 let search_dropdown () =
   <div id="packages-search-results" aria-live="polite" ></div>
-  <a class="flex py-2 px-2 mx-2 gap-4 hover:bg-primary_nav_block_hover_10 dark:hover:bg-dark-primary_nav_block_hover_10 font-normal rounded-md text-primary dark:text-[#F36528]" href="<%s Url.api %>">
-    Standard Library API
+  <a class="flex py-2 px-2 mx-2 gap-4 hover:bg-primary_nav_block_hover_10 dark:hover:bg-dark-primary_nav_block_hover_10 font-normal rounded-md text-primary dark:text-[#F36528]" href="<%s Url.stdlib %>">
+    Standard Library
     <%s! Icons.arrow_top_right_on_square "w-6 h-6"%>
   </a>
 in