From d6106074a81b38299d6195a47dd53ea419e45d42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= Date: Thu, 16 Jan 2025 17:43:39 +0100 Subject: [PATCH] WIP: import existing guides. --- data/tutorials/guides/1_00_install_Rocq.md | 175 ------------------ data/tutorials/guides/1_00_opam_using.md | 142 ++++++++++++++ .../guides/1_01_managing_versions.md | 66 +++++++ 3 files changed, 208 insertions(+), 175 deletions(-) delete mode 100644 data/tutorials/guides/1_00_install_Rocq.md create mode 100644 data/tutorials/guides/1_00_opam_using.md create mode 100644 data/tutorials/guides/1_01_managing_versions.md diff --git a/data/tutorials/guides/1_00_install_Rocq.md b/data/tutorials/guides/1_00_install_Rocq.md deleted file mode 100644 index cad1099a..00000000 --- a/data/tutorials/guides/1_00_install_Rocq.md +++ /dev/null @@ -1,175 +0,0 @@ ---- -id: installing-rocq -title: Installing the Rocq Prover -description: | - This page will help you install Rocq and the Rocq Platform Tools. | - These instructions work on Windows, and Unix systems like Linux, and macOS. -category: "First Steps" ---- - -This guide will walk you through a minimal installation of Rocq. That includes installing a package manager and the Rocq Prover itself. We'll also install some support for your editor. - -On this page, you'll find installation instructions for Linux, macOS, and Windows. - -**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) 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. - - -## Install opam - -[opam](https://opam.ocaml.org/), the official package manager of OCaml and the Rocq Prover, allows users to download and install Rocq tools and libraries. Opam also makes it practical to deal with different projects which require different versions of the Rocq Prover. - -Opam can be used to install the OCaml compiler and the Rocq Prover. - -To install opam, you can [use your system package manager](https://opam.ocaml.org/doc/Install.html#Using-your-distribution-39-s-package-system) or download the [binary distribution](https://opam.ocaml.org/doc/Install.html#Binary-distribution). The details are available in these links, but for convenience, we use package distributions: - -**For macOS** - -If you're installing with [Homebrew](https://brew.sh/): - -```shell -$ brew install opam -``` - -Or if you're using [MacPorts](https://www.macports.org/): - -```shell -$ port install opam -``` - -**For Linux** - -It's preferable to install opam with your system's package manager on Linux, as superuser. On the opam site, find [details of all installation methods](https://opam.ocaml.org/doc/Install.html). A version of opam above 2.0 is packaged in all supported Linux distributions. If you are using an unsupported Linux distribution, please either download a precompiled binary or build opam from sources. - -If you are installing in Debian or Ubuntu: -```shell -$ sudo apt-get install opam -``` - -If you are installing in Arch Linux: -```shell -$ sudo pacman -S opam -``` - -**Note**: The Debian package for opam, which is also used in Ubuntu, has the OCaml compiler as a recommended dependency. By default, such dependencies are installed. If you want to only install opam without OCaml, you need to run something like this: -```shell -sudo apt-get install --no-install-recommends opam -``` - -**For Windows** - -It's easiest to install opam with [WinGet](https://github.com/microsoft/winget-cli): - -```shell -PS C:\> winget install Git.Git OCaml.opam -``` - -**Binary Distribution** - -If you want the latest release of opam, install it through the binary distribution. On Unix and macOS, you'll need to install the following system packages first: `gcc`, `build-essential`, `curl`, `bubblewrap`, and `unzip`. Note that they might have different names depending on your operating system or distribution. Also, note this script internally calls `sudo`. - -The following command will install the latest version of opam that applies to your system: -```shell -$ bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)" -``` - -On Windows, the winget package is maintained by opam's developers and uses the binaries released [on GitHub](https://github.com/ocaml/opam/releases), however you can also install using an equivalent PowerShell script: - -```powershell -Invoke-Expression "& { $(Invoke-RestMethod https://opam.ocaml.org/install.ps1) }" -``` - -## Initialise opam - -After you install opam, you'll need to initialise it. To do so, run the following command, as a normal user. This might take a few minutes to complete. - -```shell -$ opam init -y -``` - -**Note**: In case you are running `opam init` inside a Docker container, you will need to disable sandboxing, which is done by running `opam init --disable-sandboxing -y`. This is necessary, unless you run a privileged Docker container. - -Make sure you follow the instructions provided at the end of the output of `opam init` to complete the initialisation. Typically, this is: -``` -$ eval $(opam env) -``` - -on Unix, and from the Windows Command Prompt: - -``` -for /f \"tokens=*\" %i in ('opam env') do @%i -``` - -or from PowerShell: - -```powershell -(& opam env) -split '\r?\n' | ForEach-Object { Invoke-Expression $_ } -``` - -Opam initialisation may take several minutes. While waiting for its installation and configuration to complete, start reading [A Tour of Rocq](tour-of-rocq). - -**Note**: opam can manage something called _switches_. This is key when switching between several OCaml projects. However, in this “getting started” series of tutorials, switches are not needed. If interested, you can read an introduction to [opam switches here](/docs/opam-switch-introduction). - -**Any problems installing?** Be sure to read the [latest release notes](https://opam.ocaml.org/blog/opam-2-2-0/). You can file an issue at https://github.com/ocaml/opam/issues or https://github.com/ocaml-windows/papercuts/issues. - -## Install the Rocq Prover - - -To install Rocq, simply run the following command. It will pin the Rocq package to version 9.0.0 and install it. -Note that installing Rocq using opam will build it from sources, -which will take several minutes to complete: - - ```shell -$ opam pin add rocq 9.0.0 -``` - -Pinning prevents opam from upgrading Rocq automatically, to avoid causing inadvertent breakage in your Rocq projects. -You can upgrade Rocq explicitly to `$NEW_VERSION` with essentially the same command: - - ```shell -$ opam pin add rocq $NEW_VERSION -``` - -To ensure that installation was successful, check that `rocq -v` prints the expected version of Rocq. - -## Install Platform Tools - -VsRocq is an extension for [Visual Studio Code]("https://code.visualstudio.com/) (VS Code) and -[VSCodium](https://vscodium.com/) which provides support for the Rocq Prover. - -It is built around a language server which natively speaks the -[LSP protocol](https://learn.microsoft.com/en-us/visualstudio/extensibility/language-server-protocol?view=vs-2022). - -To install it in your current opam switch, run this command: - - ```shell -$ opam install vsrocq-language-server -``` -You can alternatively install [rocq-lsp](https://github.com/ejgallego/coq-lsp). - -Now you are ready to write some Rocq code and proofs! - -## Check Installation - -To check that everything is working properly, you can start the Rocq toplevel: -```shell -$ rocq repl -Welcome to Rocq 9.0.O - -Rocq < -``` - -You're now in an Rocq toplevel, and you can start typing Rocq expressions. For instance, try typing `Eval compute in 2*10.` at the `>` prompt, then hit `Enter`. You'll see the following: -```coq -Rocq > Eval compute in 2*10. - = 20 - : nat -``` - -**Congratulations**! You've installed Rocq! 🎉 - -## Join the Community - -Make sure you [join the Rocq community](/community). You'll find many community members on [Discuss](https://discuss.rocq.org/) or [Discord](https://discord.com/invite/cCYQbqN). These are great places to ask for help if you have any issues. diff --git a/data/tutorials/guides/1_00_opam_using.md b/data/tutorials/guides/1_00_opam_using.md new file mode 100644 index 00000000..889c37a0 --- /dev/null +++ b/data/tutorials/guides/1_00_opam_using.md @@ -0,0 +1,142 @@ +--- +id: using-opam +title: Installing the Rocq Prover and its packages +description: | + This page will help you get started using opam to install the Rocq Prover and its packages. +category: Opam +--- + +## What is opam? + +

Opam is the package manager for the OCaml programming language, the language +in which Coq is implemented. +Opam 2.1 is the recommended version, and is assumed below. +Instructions on +how to install opam +itself are available on the opam website. +The following command displays the version of opam you have installed:

+ +
# Make sure opam version is 2.1.0 or above.
+opam --version
+
+ +

Follow the instructions below to install the last stable version of +Coq and additional packages. The instructions target an opam +newcomer.

+ +

Note that these instructions will also work for Opam 2.0 but this +may require you to manually install any external dependencies. In this +case you will have to use opam-depext to see which +external dependencies are missing.

+ +

For some operating systems, opam +and opam-depext might still be unable to detect external +dependencies, which will mean you have to check and install them +yourself. To see more detailed information on external dependencies +please consult +the INSTALL.md +documentation in the GitHub repository.

+ +## The Coq Platform scripts + +

The Coq Platform +provides interactive scripts that allow installing Coq and a standard +set of packages through opam without having to learn anything about +opam.

+ +

If a standard setup works for you, then we recommend that you use +these scripts. +If you do, you can skip directly to Using opam to +install Coq packages to learn how to add additional packages to +the initial package set provided by the Platform.

+ +

Note that the Platform scripts are compatible with existing opam +installations. They will create a +fresh switch.

+ +

If you prefer to do a fully manual installation, you can proceed to +the next section.

+ +## Initializing opam + +

Once opam is installed, it must be initialized before first +usage:

+ +
opam init
+eval $(opam env)
+
+ +

opam init will prompt you to allow opam to set up +initialization scripts, which is generally fine to accept. Otherwise, +every time a new shell is opened you have to type in the +eval $(opam env) command above to update environment variables.

+ +

By default, opam will use the global installation of OCaml. You can +initialize opam with an explicit compiler version, for example +<#OCAMLV>, with the option +--compiler=ocaml-base-compiler.<#OCAMLV>. +See also the section "Managing different versions of OCaml and Coq" below, +about switches and roots. +

+ +## Installing Coq + +

To install Coq, simply run the following command. Note that +installing Coq using opam will build it from sources, which will take +several minutes to complete:

+ +
# Pin the coq package to version <#CURRENTVERSION> and install it.
+opam pin add coq <#CURRENTVERSION>
+
+ +

Pinning prevents opam from upgrading Coq automatically, to avoid +causing inadvertent breakage in your Coq projects. You can upgrade Coq +explicitly to +$NEW_VERSION with essentially the same command:

+ +
opam pin add coq $NEW_VERSION
+
+ +

To ensure that installation was successful, check that coqc +-v prints the expected version of Coq.

+ +### Installing CoqIDE + +

You may also want to install CoqIDE. Note that this requires GTK+ +development files (gtksourceview3) to be available on the +system. Opam (>=2.1) will ensure that these packages are installed (on +most operating systems). To install CoqIDE, simply run:

+ +
opam install coqide
+
+ +

There exist many alternative user +interfaces / editor extensions for Coq. See their respective +websites for instructions on how to install them.

+ +## Installing Coq packages + +

Coq packages live in a repository separate from the standard OCaml +opam repository. The following command adds that repository to the +current opam switch (you can skip this step if +you used the Platform scripts):

+ +
opam repo add coq-released https://coq.inria.fr/opam/released
+
+ +

The following command lists the names of all Coq packages along +with short descriptions:

+ +
opam search coq
+
+ +

You can access a more detailed description of a package, +say coq-sudoku, using the command:

+ +
opam show coq-sudoku
+
+ +

You can then install the package using the command:

+ +
opam install coq-sudoku
+
diff --git a/data/tutorials/guides/1_01_managing_versions.md b/data/tutorials/guides/1_01_managing_versions.md new file mode 100644 index 00000000..0bfaefa5 --- /dev/null +++ b/data/tutorials/guides/1_01_managing_versions.md @@ -0,0 +1,66 @@ +--- +id: managing-versions +title: Managing different versions of OCaml and Coq +description: | + This page explains how to manage different versions of OCaml and Coq using opam. +category: Opam +--- + +

By default, opam will use the global OCaml installation. Opam can +handle different versions of OCaml and other packages (including Coq) +via +switches or roots.

+ +## Switches + +

Switches provide separate environments, with their own versions of +OCaml and installed packages. More information about opam +switches can +be found here.

+ +

The following command creates a switch named with-coq +with OCaml <#OCAMLV>:

+ +
# Run one of the following depending on your version of opam
+opam switch create with-coq <#OCAMLV>
+
+ +

Change to an existing switch named other-switch with +this command:

+ +
opam switch other-switch
+eval $(opam env)
+
+ +## Roots + +

Opam stores all its configuration (including switches) in a +directory called root (by default, ~/.opam). The +path to the root can be set using the $OPAMROOT +environment variable, providing an alternative way of creating fresh +opam environments. +

+ +

The main benefit of roots is that they can be used simultaneously, +but they require some external bookkeeping. In comparison. switches +are entirely managed by opam, and they can share the global +configuration of a single root. +

+ +
# Set a new root location export
+OPAMROOT=~/.opam-coq.<#CURRENTVERSION>
+
+# Initialize the root with an explicit OCaml version.
+opam init -n --compiler=ocaml-base-compiler.<#OCAMLV>
+
+# Install Coq in this new root (same commands as above)
+opam pin add coq <#CURRENTVERSION>
+
+ +

Every time a new shell is opened, or you want to use a different +root, type in the following lines: +

+ +
export OPAMROOT=~/.opam-coq.<#CURRENTVERSION>
+eval $(opam env)
+