Skip to content

Commit

Permalink
Merge pull request #37 from coq/link-to-install-page
Browse files Browse the repository at this point in the history
More sensible links for beginners installing Rocq.
  • Loading branch information
tabareau authored Jan 2, 2025
2 parents bd83709 + 336190e commit 7d09cd5
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 7d09cd5

Please sign in to comment.