Skip to content

Commit 489a5ad

Browse files
committed
Add a line for an optional latest prerelease (is_latest + is_prerelease must be true in the .md file). Try to debug handling of + in version names
1 parent 1087e54 commit 489a5ad

File tree

8 files changed

+22
-6
lines changed

8 files changed

+22
-6
lines changed

data/releases/9.0-rc1.md renamed to data/releases/9.0+rc1.md

+2
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,14 @@ kind: rocq
33
version: 9.0+rc1
44
date: 2025-01-24
55
is_latest: true
6+
is_prerelease: true
67
is_lts: false
78
intro: |
89
This page describes Rocq version **9.0+rc1**, released on
910
Jan 24, 2025. Go [here](/releases) for a list of all releases.
1011
1112
This is the first release candidate of Rocq 9.
13+
This is a pre-release, mainly useful to library develpers and package managers.
1214
highlights: |
1315
- A single command line tool: `rocq`
1416
- Compatibility Coq binaries and packages

src/rocqproverorg_data/data.mli

+1
Original file line numberDiff line numberDiff line change
@@ -133,6 +133,7 @@ module Release : sig
133133
val all : t list
134134
val get_by_version : string -> t option
135135
val latest : t
136+
val latest_prerelease : t option
136137
val latest_platform : t
137138
val lts : t
138139
end

src/rocqproverorg_data/data_intf.ml

+1
Original file line numberDiff line numberDiff line change
@@ -527,6 +527,7 @@ module Release = struct
527527
version : string;
528528
date : string;
529529
is_latest : bool;
530+
is_prerelease : bool;
530531
is_lts : bool;
531532
intro_md : string;
532533
intro_html : string;

src/rocqproverorg_frontend/pages/home.eml

+4
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ let package_card ~href ~img_path ~name description =
1313

1414
let render
1515
~(latest_release: Data.Release.t)
16+
~(latest_prerelease: Data.Release.t option)
1617
~(latest_platform_release : Data.Release.t)
1718
~(lts_release: Data.Release.t)
1819
~(releases : Data.Release.t list)
@@ -48,6 +49,9 @@ Layout.render
4849
<div class="mt-8">
4950
<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>
5051
</div>
52+
<% begin match latest_prerelease with | Some latest_prerelease -> %><div class="mt-2">
53+
<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>
54+
</div><% | None -> () end; %>
5155
<div class="mt-2">
5256
<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>
5357
</div>

src/rocqproverorg_frontend/pages/release.eml

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

src/rocqproverorg_web/lib/handler.ml

+4-1
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,10 @@ let ( let</>? ) opt = http_or_404 opt
1010
let index _req =
1111
Dream.html
1212
(Rocqproverorg_frontend.home ~latest_release:Data.Release.latest
13+
~latest_prerelease:Data.Release.latest_prerelease
1314
~latest_platform_release:Data.Release.latest_platform
1415
~lts_release:Data.Release.lts
15-
~releases:(List.take 2 Data.Release.all)
16+
~releases:(List.take 3 Data.Release.all)
1617
~changelogs:(List.take 3 Data.Changelog.all))
1718

1819
let install _req =
@@ -508,6 +509,8 @@ let releases req =
508509

509510
let release req =
510511
let version = Dream.param req "id" in
512+
Logs.info (fun f -> f "version string: %s" version);
513+
Logs.info (fun f -> f "decoded version string: %s" (Dream.from_percent_encoded version));
511514
let</>? version = Data.Release.get_by_version version in
512515
Dream.html (Rocqproverorg_frontend.release version)
513516

src/rocqproverorg_web/lib/rocqproverorg_web.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ module Graphql = Graphql
66
(* Set up basic logging for logs that would happen before Dream is set up. *)
77
let () =
88
Logs.set_reporter (Logs.format_reporter ());
9-
Logs.set_level (Some Info)
9+
Logs.set_level ~all:true (Some Debug)
1010

1111
let run () =
1212
Mirage_crypto_rng_lwt.initialize (module Mirage_crypto_rng.Fortuna);

tool/ood-gen/lib/release.ml

+8-3
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,15 @@ type metadata = {
55
version : string;
66
date : string;
77
is_latest : bool option;
8+
is_prerelease : bool option;
89
is_lts : bool option;
910
intro : string;
1011
highlights : string;
1112
}
1213
[@@deriving
1314
of_yaml,
1415
stable_record ~version:t ~remove:[ intro; highlights ]
15-
~modify:[ is_latest; is_lts ]
16+
~modify:[ is_latest; is_prerelease; is_lts ]
1617
~add:
1718
[
1819
intro_md;
@@ -32,6 +33,7 @@ let of_metadata m =
3233
(m.highlights |> Markdown.Content.of_string
3334
|> Markdown.Content.render ~syntax_highlighting:true)
3435
~modify_is_latest:(Option.value ~default:false)
36+
~modify_is_prerelease:(Option.value ~default:false)
3537
~modify_is_lts:(Option.value ~default:false)
3638

3739
let sort_by_decreasing_version (x : t) (y : t) =
@@ -54,17 +56,19 @@ let all () =
5456

5557
let is_coq_or_rocq (r : t) = r.kind == `Coq || r.kind == `Rocq
5658
let is_coq_or_rocq_platform (r : t) = r.kind == `CoqPlatform || r.kind == `RocqPlatform
59+
let is_rocq (r : t) = r.kind == `Rocq
5760

5861
let template () =
5962
let all = all () in
6063
let latest =
61-
try List.find (fun (r : t) -> is_coq_or_rocq r && r.is_latest) all
64+
try List.find (fun (r : t) -> is_coq_or_rocq r && r.is_latest && not r.is_prerelease) all
6265
with Not_found ->
6366
raise
6467
(Invalid_argument
6568
"none of the Coq/Rocq releases in data/releases is marked with is_latest: \
6669
true")
6770
in
71+
let latest_prerelease = List.find_opt (fun (r : t) -> is_rocq r && r.is_prerelease && r.is_latest) all in
6872
let latest_platform =
6973
try List.find (fun (r : t) -> is_coq_or_rocq_platform r && r.is_latest) all
7074
with Not_found ->
@@ -85,8 +89,9 @@ let template () =
8589
include Data_intf.Release
8690
let all = %a
8791
let latest = %a
92+
let latest_prerelease = %a
8893
let latest_platform = %a
8994
let lts = %a
9095
|}
9196
(Fmt.brackets (Fmt.list pp ~sep:Fmt.semi))
92-
all pp latest pp latest_platform pp lts
97+
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

0 commit comments

Comments
 (0)