Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix documentation links everywhere and local doc handling #83

Merged
merged 6 commits into from
Jan 31, 2025
Merged

Fix documentation links everywhere and local doc handling #83

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f9087de
Fix documentation links everywhere and local doc handling
mattam82 Jan 29, 2025
ee3c960
Use short names for more compact visualization
mattam82 Jan 29, 2025
ae8d9fd
Fix footer
mattam82 Jan 30, 2025
9d94187
Implement discussed fixes
mattam82 Jan 30, 2025
6383722
Fix links
mattam82 Jan 31, 2025
ae084a8
Merge branch 'main' into fix-doc
mattam82 Jan 31, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,4 +16,4 @@ _opam/
.venv/

# Copied documentation
rocq-doc/
rocq-doc
1 change: 1 addition & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ GIT_BRANCH=$(shell git branch --show-current)

export GIT_COMMIT
export GIT_BRANCH
export DOC_PATH

.PHONY: all
all:
Expand Down
10 changes: 5 additions & 5 deletions src/global/url.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,18 +56,18 @@ let minor v =
| _ -> invalid_arg (v ^ ": invalid version")

let patch v =
let pre, version =
let branch, version =
match String.split_on_char '.' v with
| x :: y :: z :: _ -> false, x ^ "." ^ y ^ "." ^ z
| x :: y :: [] ->
(match String.split_on_char '+' y with
| [] -> assert false
| [y] -> false, x ^ "." ^ y
| y :: _ -> true, x ^ "." ^ y)
| y :: z :: [] -> false, x ^ "." ^ y ^ "+" ^ z
| _ -> invalid_arg (v ^ ": invalid version"))
| ["master"] -> true, v
| _ -> invalid_arg (v ^ ": invalid version")
in
if pre then "v" ^ version
else "V" ^ version
in if branch then version else "V" ^ version

let v2 = "https://v2.ocaml.org"
let manual_with_version v = "/doc/" ^ patch v ^ "/refman/index.html"
Expand Down
6 changes: 2 additions & 4 deletions src/rocqproverorg_frontend/components/footer.eml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,9 @@ 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.learn, "Documentation");
(Url.books, "Books");
(Url.exercises, "Exercises");
(* (Url.exercises, "Exercises"); *)
(Url.papers, "Papers");
(Url.logos, "Logo");
]
Expand Down
6 changes: 3 additions & 3 deletions src/rocqproverorg_frontend/pages/learn.eml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,10 +28,10 @@ Learn_layout.single_column_layout
<%s! Hero_section.hero_button ~left_icon:(Icons.rocq "w-5 h-5") ~right_icon:(Icons.download "w-5 h-5") ~text:("Install Rocq Platform " ^ latest_platform_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:("Rocq Reference Manual") ~href:(Url.manual) "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Rocq Core Library API") ~href:(Url.corelib) "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Rocq Corelib Theories") ~href:(Url.corelib) "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Rocq OCaml 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:("Rocq Standard Library Manual") ~href:(Url.stdlib_manual) "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Rocq Standard Library API") ~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 Stdlib Manual") ~href:(Url.stdlib_manual) "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Rocq Stdlib Theories") ~href:(Url.stdlib) "" %>
</div>
</div>
</div>
Expand Down
7 changes: 7 additions & 0 deletions src/rocqproverorg_frontend/pages/release.eml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,13 @@ Layout.render
<a href="<%s! Data.Release.github_release release %>">
<%s! Icons.github "h-5 w-5 inline-block" %>Github release</a>
</div>
<div class="flex flex-row gap-4 md:gap-6 md:w-80">
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Reference Manual") ~href:(Url.manual_with_version release.version) "" %>
<%s! if release.kind = `Rocq then Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Corelib Theories") ~href:(Url.corelib_with_version release.version) "" else "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("OCaml API") ~href:(Url.api_with_version release.version) "" %>
<%s! if release.kind = `Rocq then Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Stdlib Manual") ~href:(Url.stdlib_manual_with_version release.version) "" else "" %>
<%s! Hero_section.hero_button ~left_icon:(Icons.book "w-5 h-5") ~right_icon:(Icons.link "w-5 h-5") ~text:("Stdlib Theories") ~href:(Url.stdlib_with_version release.version) "" %>
</div>
</div>
</div>
</div>
Expand Down
26 changes: 20 additions & 6 deletions src/rocqproverorg_frontend/pages/releases.eml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,12 +75,26 @@ Platform_layout.single_column_layout
<a href="<%s (base_of_kind release) ^ Url.Package.overview (Data.Release.string_of_kind release.kind) ~version:release.version %>" class="text-primary dark:text-dark-primary font-medium block">
Opam Package
</a>
<a href="<%s Url.manual_with_version release.version %>" class="text-primary dark:text-dark-primary font-medium block">
Reference Manual
</a>
<a href="<%s Url.stdlib_with_version release.version %>" class="text-primary dark:text-dark-primary font-medium block">
Standard Library
</a>
<div class="block">
<% if release.kind = `Rocq then ( %>
<a href="<%s Url.corelib_with_version release.version %>" class="text-primary dark:text-dark-primary font-medium">
Corelib |
</a>
<a href="<%s Url.manual_with_version release.version %>" class="text-primary dark:text-dark-primary font-medium">
Manual
</a>
<% ); %>
</div>
<div class="block">
<a href="<%s Url.stdlib_with_version release.version %>" class="text-primary dark:text-dark-primary font-medium">
Stdlib
</a>
<% if release.kind = `Rocq then ( %>
<a href="<%s Url.stdlib_manual_with_version release.version %>" class="text-primary dark:text-dark-primary font-medium">
| Manual
</a>
<% ); %>
</div>
</div>
</div>
</div>
Expand Down
13 changes: 11 additions & 2 deletions src/rocqproverorg_web/lib/middleware.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,13 +23,22 @@ let language_manual_version next_handler request =
let path =
match init_path with
(* When using the /doc/ path, a version is always already provided. *)
| "" :: "doc" :: version :: path ->
| "" :: "doc" :: version :: (_ :: _ as path) ->
"" :: "doc" :: version :: tweak_base path
(* We provide shorter paths that always redirect to the latest version. *)
| ""
:: (("api" | "corelib" | "refman" | "stdlib" | "refman-stdlib") :: _ as
:: (("api" | "corelib" | "refman" | "stdlib" | "refman-stdlib") as head :: tail as
path) ->
let version = patch Release.latest in
let path =
match Release.latest.kind with
| `Rocq -> path
| `Coq -> (match head with
| "refman-stdlib" -> "refman" :: tail
| "corelib" -> "stdlib" :: tail
| _ -> path)
| _ -> assert false
in
"" :: "doc" :: version :: tweak_base path
| u -> u
in
Expand Down
Loading