Skip to content

Commit

Permalink
More sensible links for beginners installing Rocq.
Browse files Browse the repository at this point in the history
Link the Getting Started button to the Getting Started section in the doc.
Stop pointing beginners at the opam tutorial and use the link to the install page more often.
  • Loading branch information
Zimmi48 committed Jan 2, 2025
1 parent 4023bc4 commit 336190e
Show file tree
Hide file tree
Showing 5 changed files with 6 additions and 8 deletions.
2 changes: 1 addition & 1 deletion data/tutorials/getting-started/1_00_install_Rocq.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ On this page, you'll find installation instructions for Linux, macOS, and Window

**Note**: You'll be installing Rocq and its tools through a [command line interface (CLI), or shell](https://www.youtube.com/watch?v=0PxTAn4g20U).

Beginners are encouraged to install the [Rocq Platform](/install#rocq_platform) using one of the binary installers: we provide binary installers for Windows and macOS.
Beginners are encouraged to install the [Rocq Platform](/install) using one of the binary installers: we provide binary installers for Windows and macOS.
Installation scripts are also available for all operating systems and abstract over the installation process that is presented here.


Expand Down
3 changes: 1 addition & 2 deletions src/global/url.ml
Original file line number Diff line number Diff line change
Expand Up @@ -99,8 +99,7 @@ let platform_page name = platform ^ "/" ^ name
let consortium_page name = consortium ^ "/" ^ name
let tutorial name = "/docs/" ^ name
let tutorial_search = "/docs/search"
let installing_rocq = "/docs/installing-rocq"
let getting_started = installing_rocq
let getting_started = learn ^ "#beginner_section"
let exercises = "/exercises"
let logos = "/logo"

Expand Down
4 changes: 2 additions & 2 deletions src/rocqproverorg_frontend/pages/install.eml
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ Layout.render
<p>
If you want some finer-grained control over the installation process, you can install the Rocq Prover by running opam commands directly.
</p>
<a class="btn mt-6 gap-2" href="<%s Url.installing_rocq %>" >Install Rocq using Opam <%s! Icons.arrow_small_right "h-6 w-6" %></a>
<a class="btn mt-6 gap-2" href="<%s Url.tutorial "installing-rocq" %>" >Install Rocq using Opam <%s! Icons.arrow_small_right "h-6 w-6" %></a>
<h3>
Using Nix
</h3>
Expand Down Expand Up @@ -153,7 +153,7 @@ Layout.render
<p>
If you want some finer-grained control over the installation process, you can install the Rocq Prover by running opam commands directly.
</p>
<a class="btn mt-6 gap-2" href="<%s Url.installing_rocq %>" >Install Rocq using Opam <%s! Icons.arrow_small_right "h-6 w-6" %></a>
<a class="btn mt-6 gap-2" href="<%s Url.tutorial "installing-rocq" %>" >Install Rocq using Opam <%s! Icons.arrow_small_right "h-6 w-6" %></a>
<h3>
Using Nix
</h3>
Expand Down
3 changes: 1 addition & 2 deletions src/rocqproverorg_frontend/pages/learn.eml
Original file line number Diff line number Diff line change
Expand Up @@ -64,10 +64,9 @@ Learn_layout.single_column_layout
~icon:Learn_components.beginner_section_icon ~title:"GET STARTED" ~heading:"Introduction To Rocq"
~description:"Install Rocq and gain a high-level understanding of the language"
~tutorial_links:[
{href = Url.tutorial "installing-rocq"; title = "Installing Rocq"};
{href = Url.install; title = "Installing the Rocq Prover"};
{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"} *)
]
~see_more:{href = Url.getting_started; title = "Get Started"}
%>
Expand Down
2 changes: 1 addition & 1 deletion src/rocqproverorg_frontend/pages/platform.eml
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ Platform_layout.three_column_layout
<p>
Detailed instructions to install Rocq and the
Platform are available in <a class="text-primary"
href="<%s Url.installing_rocq %>">Installing Rocq</a>.
href="<%s Url.install %>">Installing Rocq</a>.
<h2 class="font-bold mt-8 text-title dark:text-dark-title">Packages of the Rocq Platform</h2>
<p>
Here is a list of all Platform packages sorted by their status.
Expand Down

0 comments on commit 336190e

Please sign in to comment.