Add a line for an optional latest prerelease (is_latest + is_prerelea…

…se must be true in the .md file). Try to debug handling of + in version names

data/releases/9.0-rc1.md → data/releases/9.0+rc1.md

@@ -3,12 +3,14 @@ kind: rocq
 version: 9.0+rc1
 date: 2025-01-24
 is_latest: true
+is_prerelease: true
 is_lts: false
 intro: |
   This page describes Rocq version **9.0+rc1**, released on
   Jan 24, 2025. Go [here](/releases) for a list of all releases.
 
   This is the first release candidate of Rocq 9.
+  This is a pre-release, mainly useful to library develpers and package managers. 
 highlights: |
   - A single command line tool: `rocq`
   - Compatibility Coq binaries and packages

src/rocqproverorg_data/data.mli

@@ -133,6 +133,7 @@ module Release : sig
   val all : t list
   val get_by_version : string -> t option
   val latest : t
+  val latest_prerelease : t option
   val latest_platform : t
   val lts : t
 end

src/rocqproverorg_data/data_intf.ml

@@ -527,6 +527,7 @@ module Release = struct
     version : string;
     date : string;
     is_latest : bool;
+    is_prerelease : bool;
     is_lts : bool;
     intro_md : string;
     intro_html : string;

src/rocqproverorg_frontend/pages/home.eml

@@ -13,6 +13,7 @@ let package_card ~href ~img_path ~name description =
 
 let render
   ~(latest_release: Data.Release.t)
+  ~(latest_prerelease: Data.Release.t option)
   ~(latest_platform_release : Data.Release.t)
   ~(lts_release: Data.Release.t)
   ~(releases : Data.Release.t list)
@@ -48,6 +49,9 @@ Layout.render
         <div class="mt-8">
           <a class="text-1xl text-primary dark:text-dark-primary font-semibold" href="<%s Url.release latest_release.version %>">Latest Rocq Prover release: <%s latest_release.version %></a>
         </div>
+        <% begin match latest_prerelease with | Some latest_prerelease -> %><div class="mt-2">
+          <a class="text-1xl text-primary dark:text-dark-primary font-semibold" href="<%s Url.release (Dream.to_percent_encoded latest_prerelease.version) %>">Latest Rocq Prover release candidate: <%s latest_prerelease.version %></a>
+        </div><% | None -> () end; %>
         <div class="mt-2">
           <a class="text-1xl text-primary dark:text-dark-primary font-semibold" href="<%s Url.release latest_platform_release.version %>">Latest Rocq Platform release: <%s latest_platform_release.version %></a>
         </div>

src/rocqproverorg_frontend/pages/release.eml

@@ -3,7 +3,7 @@ let render (release : Data.Release.t) =
 Layout.render
 ~title:(Printf.sprintf "%s %s Release Notes" name release.version)
 ~description:(Printf.sprintf "%s %s was released on %s. Learn more about this in the release notes." name release.version release.date)
-~canonical:(Url.release release.version) @@
+~canonical:(Url.release (Dream.to_percent_encoded release.version)) @@
 <div class="lg:-mt-32 lg:pt-44 intro-section-simple dark:dark-intro-section-simple">
     <div class="container-fluid">
         <div class="flex md:flex-row lg:px-6 items-center md:space-x-36 flex-col-reverse">

src/rocqproverorg_web/lib/handler.ml

@@ -10,9 +10,10 @@ let ( let</>? ) opt = http_or_404 opt
 let index _req =
   Dream.html
     (Rocqproverorg_frontend.home ~latest_release:Data.Release.latest
+       ~latest_prerelease:Data.Release.latest_prerelease
        ~latest_platform_release:Data.Release.latest_platform
        ~lts_release:Data.Release.lts
-       ~releases:(List.take 2 Data.Release.all)
+       ~releases:(List.take 3 Data.Release.all)
        ~changelogs:(List.take 3 Data.Changelog.all))
 
 let install _req =
@@ -508,6 +509,8 @@ let releases req =
 
 let release req =
   let version = Dream.param req "id" in
+  Logs.info (fun f -> f "version string: %s" version);
+  Logs.info (fun f -> f "decoded version string: %s" (Dream.from_percent_encoded version));
   let</>? version = Data.Release.get_by_version version in
   Dream.html (Rocqproverorg_frontend.release version)
 

src/rocqproverorg_web/lib/rocqproverorg_web.ml

@@ -6,7 +6,7 @@ module Graphql = Graphql
 (* Set up basic logging for logs that would happen before Dream is set up. *)
 let () =
   Logs.set_reporter (Logs.format_reporter ());
-  Logs.set_level (Some Info)
+  Logs.set_level ~all:true (Some Debug)
 
 let run () =
   Mirage_crypto_rng_lwt.initialize (module Mirage_crypto_rng.Fortuna);

tool/ood-gen/lib/release.ml

@@ -5,14 +5,15 @@ type metadata = {
   version : string;
   date : string;
   is_latest : bool option;
+  is_prerelease : bool option;
   is_lts : bool option;
   intro : string;
   highlights : string;
 }
 [@@deriving
   of_yaml,
     stable_record ~version:t ~remove:[ intro; highlights ]
-      ~modify:[ is_latest; is_lts ]
+      ~modify:[ is_latest; is_prerelease; is_lts ]
       ~add:
         [
           intro_md;
@@ -32,6 +33,7 @@ let of_metadata m =
       (m.highlights |> Markdown.Content.of_string
       |> Markdown.Content.render ~syntax_highlighting:true)
     ~modify_is_latest:(Option.value ~default:false)
+    ~modify_is_prerelease:(Option.value ~default:false)
     ~modify_is_lts:(Option.value ~default:false)
 
 let sort_by_decreasing_version (x : t) (y : t) =
@@ -54,17 +56,19 @@ let all () =
 
 let is_coq_or_rocq (r : t) = r.kind == `Coq || r.kind == `Rocq
 let is_coq_or_rocq_platform (r : t) = r.kind == `CoqPlatform || r.kind == `RocqPlatform
+let is_rocq (r : t) = r.kind == `Rocq
 
 let template () =
   let all = all () in
   let latest =
-    try List.find (fun (r : t) -> is_coq_or_rocq r && r.is_latest) all
+    try List.find (fun (r : t) -> is_coq_or_rocq r && r.is_latest && not r.is_prerelease) all
     with Not_found ->
       raise
         (Invalid_argument
            "none of the Coq/Rocq releases in data/releases is marked with is_latest: \
             true")
   in
+  let latest_prerelease = List.find_opt (fun (r : t) -> is_rocq r && r.is_prerelease && r.is_latest) all in
   let latest_platform =
     try List.find (fun (r : t) -> is_coq_or_rocq_platform r && r.is_latest) all
     with Not_found ->
@@ -85,8 +89,9 @@ let template () =
 include Data_intf.Release
 let all = %a
 let latest = %a
+let latest_prerelease = %a
 let latest_platform = %a
 let lts = %a
 |}
     (Fmt.brackets (Fmt.list pp ~sep:Fmt.semi))
-    all pp latest pp latest_platform pp lts
+    all pp latest (Fmt.option ~none:(Fmt.const Fmt.string "None") (Fmt.append (Fmt.const Fmt.string "Some ") (Fmt.parens pp))) latest_prerelease pp latest_platform pp lts