From 336190eb03dd2623195c6a56b2b13b6cd3497ba1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@telecom-paris.fr>
Date: Thu, 2 Jan 2025 16:55:31 +0100
Subject: [PATCH] More sensible links for beginners installing Rocq.

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.
---
 data/tutorials/getting-started/1_00_install_Rocq.md | 2 +-
 src/global/url.ml                                   | 3 +--
 src/rocqproverorg_frontend/pages/install.eml        | 4 ++--
 src/rocqproverorg_frontend/pages/learn.eml          | 3 +--
 src/rocqproverorg_frontend/pages/platform.eml       | 2 +-
 5 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/data/tutorials/getting-started/1_00_install_Rocq.md b/data/tutorials/getting-started/1_00_install_Rocq.md
index 9464de991..9cd6a701c 100644
--- a/data/tutorials/getting-started/1_00_install_Rocq.md
+++ b/data/tutorials/getting-started/1_00_install_Rocq.md
@@ -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.
 
 
diff --git a/src/global/url.ml b/src/global/url.ml
index 079ca6dd3..5679c3ab7 100644
--- a/src/global/url.ml
+++ b/src/global/url.ml
@@ -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"
 
diff --git a/src/rocqproverorg_frontend/pages/install.eml b/src/rocqproverorg_frontend/pages/install.eml
index 81b118cc1..3c7ade6cd 100644
--- a/src/rocqproverorg_frontend/pages/install.eml
+++ b/src/rocqproverorg_frontend/pages/install.eml
@@ -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>
@@ -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>
diff --git a/src/rocqproverorg_frontend/pages/learn.eml b/src/rocqproverorg_frontend/pages/learn.eml
index 99d8e177f..16934af19 100644
--- a/src/rocqproverorg_frontend/pages/learn.eml
+++ b/src/rocqproverorg_frontend/pages/learn.eml
@@ -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"}
               %>
diff --git a/src/rocqproverorg_frontend/pages/platform.eml b/src/rocqproverorg_frontend/pages/platform.eml
index c969d8548..8e5b810c8 100644
--- a/src/rocqproverorg_frontend/pages/platform.eml
+++ b/src/rocqproverorg_frontend/pages/platform.eml
@@ -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.