install.eml

let render ~latest_platform_version =
Layout.render
~use_swiper:true
~title:"Install the Rocq Prover"
~description:"Quick setup instructions to install Rocq on your system."
~canonical:"" @@
<div class="lg:py-8 py-6">
  <div class="container-fluid" x-data='{ operating_system: persist_os_link() }'>
    <div class="prose dark:prose-invert mb-6">
      <h1 class="sr-only ">
        Install the Rocq Prover
      </h1>
      <div class="hidden lg:flex gap-2">
        <button class="btn flex gap-2" :class='operating_system == "linux"? "": "btn-ghost"' @click='operating_system = "linux"; change_anchor("linux"); '>
          Linux
        </button>
        <button class="btn flex gap-2" :class='operating_system == "mac"? "": "btn-ghost"' @click='operating_system = "mac"; change_anchor("mac"); '>
          macOS
        </button>
        <button class="btn flex gap-2" :class='operating_system == "windows"? "": "btn-ghost"' @click='operating_system = "windows"; change_anchor("windows"); '>
          Windows
        </button>
      </div>
      <div class="w-full flex md:hidden">
% let render_multi_button ~title ~active_tab ~class_ =
      <button x-on:click='operating_system = "<%s active_tab %>"' class="flex flex-auto justify-center py-4 text-sm border <%s class_ %>" :class='operating_system === "<%s active_tab %>" ? "bg-primary dark:bg-dark-primary text-white dark:text-dark-title border-primary dark:border-dark-primary" : "text-content dark:text-dark-separator_30 border-card_border dark:border-dark-separator_30"'><%s title %></button>
% in
        <% render_multi_button ~title:"Linux" ~active_tab:"linux" ~class_:"rounded-l rounded-l-lg border-r-0"; %>
        <% render_multi_button ~title:"macOS" ~active_tab:"mac" ~class_:"rounded-r rounded-r-lg"; %>
        <% render_multi_button ~title:"Windows" ~active_tab:"windows" ~class_:"rounded-r rounded-r-lg"; %>
      </div>
    </div>
    <div
      class="grid gap-6 xl:grid-cols-2 xl:gap-16"
      x-show="(operating_system == 'linux')">
      <div class="prose dark:prose-invert">
        <h2>
          Install the Rocq Prover on Linux
        </h2>
        <h3>
          Using your system's package manager
        </h3>
        <p>
          The Rocq Prover is available through many package managers, including most Linux distribution package managers.
          While this is currently the easiest way to install the Rocq Prover, it has the following limitations:
        </p>
        <ul>
          <li>
            Depending on the distribution, the available version may not be the latest version.
            See <a href="https://repology.org/project/coq/versions">Repology</a> to know which version is available in your distribution.
          </li>
          <li>
            The available packages may not include all the external packages available for the Rocq Prover.
            Installing additional packages may require manual compilation and installation.
          </li>
        </ul>
        <h3>
          Using the Rocq Platform (recommended)
        </h3>
        <p>
          The Rocq Prover has a rich ecosystem of external packages (libraries and plugins) that extend it and make it more powerful.
          The Rocq Platform provides an easy way to install Rocq and a consistent set of packages on Windows, macOS and Linux.
        </p>

        <ol>

          <li>
            Currently, there is no longer a Rocq Platform binary installer for Linux.
          </li>

          <li>
            The Rocq Platform scripts install the Rocq Prover and its packages from sources,
            while abstracting over the details of running opam.
            This provides the flexibility to install additional packages with opam later on.
            It also supports installing multiple versions of the Rocq Platform and switching between them.
          </li>

        </ol>
        <a class="btn mt-6 gap-2" href="https://github.com/coq/platform/blob/<%s latest_platform_version %>/doc/README_Linux.md#installation-by-compiling-from-sources-using-scripts--opam">Run the Rocq Platform scripts<%s! Icons.arrow_small_right "h-6 w-6" %></a>

        <h3>
          Using Opam
        </h3>
        <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.tutorial "installing-rocq" %>" >Install Rocq using Opam <%s! Icons.arrow_small_right "h-6 w-6" %></a>
        <h3>
          Using Nix
        </h3>
        <p>
          Nix support for the Rocq Prover is well-maintained and provides a way to install the Rocq Prover and its packages on any Linux distribution, or on macOS.
          See the <a href="https://nixos.org/download/">Nix installation instructions</a>
          and the <a href="https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq">Nixpkgs manual section on Rocq</a> for more information.
        </p>
        <h3>
          Using Docker
        </h3>
        <p>
          The Rocq Prover is also available as a <a href="https://hub.docker.com/r/coqorg/coq/">Docker image</a>.
        </p>
      </div>
      <div class="prose dark:prose-invert">
        <h2>
          Set Up your Editor for Rocq
        </h2>
        <p>
          After installing the Rocq Prover, you should set up your editor to write Rocq code and proofs.
        </p>
        <h3>
          VS Code / VS Codium (recommended)
        </h3>
        <ul>
          <li>
            <p>
            <a href="https://github.com/coq/vscoq">VsRocq</a> is the official Rocq extension for Visual Studio Code.
            It is available in the <a href="https://marketplace.visualstudio.com/items?itemName=maximedenes.vsrocq">Visual Studio Code Marketplace</a>
            and on <a href="https://open-vsx.org/extension/maximedenes/vsrocq">Open VSX</a>.
            To use it, you need to install the corresponding language server. Using opam, you can install it with the following command:
            </p>

            <%s! Copy_to_clipboard.small_code_snippet ~id:"install-vsrocq" "opam install vsrocq-language-server" %>

            <p>
            Starting from version 2025.01, the language server should already be installed if you installed the <a href="/platform">Rocq Platform</a>.
            </p>

            <p>
            The language server is also available as a <a href="https://search.nixos.org/packages?show=coqPackages.vscoq-language-server">Nix package</a>.
            </p>

            <p>
            For now, <a href="https://repology.org/project/vscoq-language-server/versions">vsrocq-language-server</a> is not available in all Linux distributions that have the Rocq Prover. If you have used your Linux distribution's package manager to install the Rocq Prover and it does not include the language server, you can fall back to using VsCoq Legacy (see below).
            </p>
          </li>
          <li>
            <p>
            <a href="https://github.com/ejgallego/coq-lsp">Rocq LSP</a> is an alternative language server and VS Code extension for the Rocq Prover featuring
hybrid Rocq/markdown document support.
            </p>
          </li>
          <li>
            <a href="https://github.com/coq-community/vscoq-legacy/">VsCoq Legacy</a> is a legacy Rocq extension for Visual Studio Code that only relies on the RocqIDE protocol and therefore does not require installing a language server. Linux distributions that have the Rocq Prover usually also install the RocqIDE server in their main package. You can install VsCoq Legacy from the <a href="https://marketplace.visualstudio.com/items?itemName=coq-community.vscoq1">Visual Studio Code Marketplace</a> or from <a href="https://open-vsx.org/extension/coq-community/vscoq1">Open VSX</a>.
        </ul>
        <h3>
          Emacs
        </h3>
        <p>
          Emacs users usually use <a href="https://proofgeneral.github.io/">Proof General</a> to interact with the Rocq Prover.
          It can be installed from the <a href="https://melpa.org/#/proof-general">MELPA repository</a>.
          It is often complemented with <a href="https://github.com/cpitclaudel/company-coq">Company-Coq</a> minor mode, which can also be installed from the MELPA repository.
        </p>
        <h3>
          Vim / Neovim
        </h3>
        <p>
          Vim users usually use <a href="https://github.com/whonore/Coqtail">Coqtail</a> to interact with the Rocq Prover. Various installation methods are documented in the repository's README.
        </p>
        <h3>
          Standalone IDE
        </h3>
        <p>
          The Rocq Prover also has a standalone IDE called RocqIDE. It is distributed as part of the Rocq Platform and is available in many Linux distributions (sometimes as a separate package).
        </p>
      </div>
    </div>

    <div
      class="grid gap-6 xl:grid-cols-2 xl:gap-16" 
      x-show="(operating_system == 'mac')">
      <div class="prose dark:prose-invert">
        <h2>
          Install the Rocq Prover on macOS
        </h2>
        <h3>
          Using the Rocq Platform (recommended)
        </h3>
        <p>
          The Rocq Prover has a rich ecosystem of external packages (libraries and plugins) that extend it and make it more powerful.
          The Rocq Platform provides an easy way to install Rocq and a consistent set of packages on Windows, macOS and Linux.
        </p>
        <ol>
          <li>
            Beginners and users who want to get started quickly should use the Rocq Platform binary installer for macOS.
          </li>
          <li>
            The Rocq Platform scripts install the Rocq Prover and its packages from sources,
            while abstracting over the details of running opam.
            This provides the flexibility to install additional packages with opam later on.
            It also supports installing multiple versions of the Rocq Platform and switching between them.
          </li>
        </ol>
        <a class="btn mt-6 gap-2" href="<%s Url.release latest_platform_version %>#recommended-binary-installers">Download the Rocq Platform binary installer<%s! Icons.arrow_small_right "h-6 w-6" %></a>
        <a class="btn mt-6 gap-2" href="https://github.com/coq/platform/blob/<%s latest_platform_version %>/doc/README_macOS.md#installation-by-compiling-from-sources-using-opam">Run the Rocq Platform scripts<%s! Icons.arrow_small_right "h-6 w-6" %></a>
        <h3>
          Using Homebrew
        </h3>
        <p>
          The Rocq Prover is also available through Homebrew, a package manager for macOS.
          Similar to the Linux package managers, this presents the limitations of not having all the external packages available for Rocq.
        </p>
        <%s! Copy_to_clipboard.small_code_snippet ~id:"brew" "brew install coq" %>
        <h3>
          Using Opam
        </h3>
        <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.tutorial "installing-rocq" %>" >Install Rocq using Opam <%s! Icons.arrow_small_right "h-6 w-6" %></a>
        <h3>
          Using Nix
        </h3>
        <p>
          Nix support for the Rocq Prover is well-maintained and provides a way to install the Rocq Prover and its packages on any Linux distribution, or on macOS.
          See the <a href="https://nixos.org/download/">Nix installation instructions</a>
          and the <a href="https://nixos.org/manual/nixpkgs/unstable/#sec-language-coq">Nixpkgs manual section on Rocq</a> for more information.
        </p>
        <h3>
          Using Docker
        </h3>
        <p>
          The Rocq Prover is also available as a <a href="https://hub.docker.com/r/coqorg/coq/">Docker image</a>.
        </p>
      </div>
      <div class="prose dark:prose-invert">
        <h2>
          Set Up your Editor for Rocq
        </h2>
        <p>
          After installing the Rocq Prover, you should set up your editor to write Rocq code and proofs.
        </p>
        <h3>
          VS Code / VS Codium (recommended)
        </h3>
        <ul>
          <li>
            <p>
            <a href="https://github.com/coq/vscoq">VsRocq</a> is the official Rocq extension for Visual Studio Code.
            It is available in the <a href="https://marketplace.visualstudio.com/items?itemName=maximedenes.vsrocq">Visual Studio Code Marketplace</a>
            and on <a href="https://open-vsx.org/extension/maximedenes/vsrocq">Open VSX</a>.
            To use it, you need to install the corresponding language server. Using opam, you can install it with the following command:
            </p>

            <%s! Copy_to_clipboard.small_code_snippet ~id:"install-vsrocq" "opam install vsrocq-language-server" %>

            <p>
            Starting from version 2025.01, the language server should already be installed if you installed the <a href="/platform">Rocq Platform</a>.
            </p>

            <p>
            The language server is also available as a <a href="https://search.nixos.org/packages?show=coqPackages.vscoq-language-server">Nix package</a>.
            </p>

            <p>
            If you have used Homebrew to install the Rocq Prover, there is no language server available yet. You can fall back to using VsCoq Legacy (see below).
            </p>
          </li>
          <li>
            <p>
            <a href="https://github.com/ejgallego/coq-lsp">Rocq LSP</a> is an alternative language server and VS Code extension for the Rocq Prover featuring
hybrid Rocq/markdown document support.
            </p>
          </li>
          <li>
            <a href="https://github.com/coq-community/vscoq-legacy/">VsCoq Legacy</a> is a legacy Rocq extension for Visual Studio Code that only relies on the RocqIDE protocol and therefore does not require installing a language server. You can install VsCoq Legacy from the <a href="https://marketplace.visualstudio.com/items?itemName=coq-community.vscoq1">Visual Studio Code Marketplace</a> or from <a href="https://open-vsx.org/extension/coq-community/vscoq1">Open VSX</a>.
          </li>
        </ul>
        <h3>
          Emacs
        </h3>
        <p>
          Emacs users usually use <a href="https://proofgeneral.github.io/">Proof General</a> to interact with the Rocq Prover.
          It can be installed from the <a href="https://melpa.org/#/proof-general">MELPA repository</a>.
          It is often complemented with <a href="https://github.com/cpitclaudel/company-coq">Company-Coq</a> minor mode, which can also be installed from the MELPA repository.
        </p>
        <h3>
          Vim / Neovim
        </h3>
        <p>
          Vim users usually use <a href="https://github.com/whonore/Coqtail">Coqtail</a> to interact with the Rocq Prover. Various installation methods are documented in the repository's README.
        </p>
        <h3>
          Standalone IDE
        </h3>
        <p>
          The Rocq Prover also has a standalone IDE called RocqIDE. It is distributed as part of the Rocq Platform.
        </p>
      </div>
    </div>

        <div
      class="grid gap-6 xl:grid-cols-2 xl:gap-16"
      x-show="(operating_system == 'windows')">
      <div class="prose dark:prose-invert">
        <h2>
          Install the Rocq Prover on Windows
        </h2>
        <h3>
          Using the Rocq Platform (recommended)
        </h3>
        <p>
          The Rocq Prover has a rich ecosystem of external packages (libraries and plugins) that extend it and make it more powerful.
          The Rocq Platform provides an easy way to install Rocq and a consistent set of packages on Windows, macOS and Linux.
        </p>
        <ol>
          <li>
            Beginners and users who want to get started quickly should use the Rocq Platform binary installer for Windows.
          </li>
          <li>
            The Rocq Platform scripts install the Rocq Prover and its packages from sources,
            while abstracting over the details of running opam.
            This provides the flexibility to install additional packages with opam later on.
            It also supports installing multiple versions of the Rocq Platform and switching between them.
          </li>
        </ol>
        <a class="btn mt-6 gap-2" href="<%s Url.release latest_platform_version %>#recommended-binary-installers">Download the Rocq Platform binary installer<%s! Icons.arrow_small_right "h-6 w-6" %></a>
        <a class="btn mt-6 gap-2" href="https://github.com/coq/platform/blob/<%s latest_platform_version %>/doc/README_Windows.md#installation-by-compiling-from-sources-using-scripts--opam">Run the Rocq Platform scripts<%s! Icons.arrow_small_right "h-6 w-6" %></a>
        <h3>
          Using Opam
        </h3>
        <p>
          If you want to be able to run opam commands directly, it is recommended to first install the Rocq Platform using the scripts.
          This will set up the environment variables needed to run opam commands.
        </p>
        <h3>
          Using WSL (Windows Subsystem for Linux) or a VM
        </h3>
        <p>
          All the installation methods for Linux are available on Windows Subsystem for Linux (WSL) or in a virtual machine running Linux.
        </p>
      </div>
      <div class="prose dark:prose-invert">
        <h2>
          Set Up your Editor for Rocq
        </h2>
        <p>
          After installing the Rocq Prover, you should set up your editor to write Rocq code and proofs.
        </p>
        <h3>
          VS Code / VS Codium (recommended)
        </h3>
        <ul>
          <li>
            <a href="https://github.com/coq/vscoq">VsRocq</a> is the official Rocq extension for Visual Studio Code.
            It is available in the <a href="https://marketplace.visualstudio.com/items?itemName=maximedenes.vsrocq">Visual Studio Code Marketplace</a>
            and on <a href="https://open-vsx.org/extension/maximedenes/vsrocq">Open VSX</a>.
            To use it, you need the corresponding language server, which is distributed with the Rocq Platform starting from version 2025.01.
          </li>
          <li>
            <p>
            <a href="https://github.com/ejgallego/coq-lsp">Rocq LSP</a> is an alternative language server and VS Code extension for the Rocq Prover featuring
hybrid Rocq/markdown document support.
            </p>
          </li>
          <li>
            <a href="https://github.com/coq-community/vscoq-legacy/">VsCoq Legacy</a> is a legacy Rocq extension for Visual Studio Code that only relies on the RocqIDE protocol. You can install it from the <a href="https://marketplace.visualstudio.com/items?itemName=coq-community.vscoq1">Visual Studio Code Marketplace</a> or from <a href="https://open-vsx.org/extension/coq-community/vscoq1">Open VSX</a>.
          </li>
          <li>
            If you have used WSL to install the Rocq Prover, then you can use the <a href="https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-wsl">WSL</a> VS Code extension to use a language server running in WSL. In this case, follow the instructions for Linux on how to install the language server.
          </li>
        </ul>
        <h3>
          Emacs
        </h3>
        <p>
          Emacs users usually use <a href="https://proofgeneral.github.io/">Proof General</a> to interact with the Rocq Prover.
          It can be installed from the <a href="https://melpa.org/#/proof-general">MELPA repository</a>.
          It is often complemented with <a href="https://github.com/cpitclaudel/company-coq">Company-Coq</a> minor mode, which can also be installed from the MELPA repository.
        </p>
        <h3>
          Vim / Neovim
        </h3>
        <p>
          Vim users usually use <a href="https://github.com/whonore/Coqtail">Coqtail</a> to interact with the Rocq Prover. Various installation methods are documented in the repository's README.
        </p>
        <h3>
          Standalone IDE
        </h3>
        <p>
          The Rocq Prover also has a standalone IDE called RocqIDE. It is distributed as part of the Rocq Platform.
        </p>
  </div>
</div>
<script>
function detect_os() {
  const agent = navigator.userAgent;
  if (agent.includes('Win')) {
    return "windows";
  }
  if (agent.includes('Mac')) {
    return "mac";
  }
  return "linux";
}

function change_anchor (os_str) {
  window.location.hash = os_str;
}

function anchor_os_loc() {
  if (window.location.hash) {
    return;
  }
  window.location.hash = detect_os();
}

function persist_os_link () {
  const hash_to_system = {
    "#linux": "linux",
    "#mac": "mac",
    "#windows": "windows"
  };
  if (window.location.hash) {
    return hash_to_system[window.location.hash]
  }
  return detect_os () 
}


anchor_os_loc();

</script>