Skip to content

Instantly share code, notes, and snippets.

@k4rtik
Created November 9, 2021 22:18
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save k4rtik/e23a87f573c7b6e16cac4ec1c89615cc to your computer and use it in GitHub Desktop.
Save k4rtik/e23a87f573c7b6e16cac4ec1c89615cc to your computer and use it in GitHub Desktop.
coq platform install log on macOS arm64
kartik@Kira platform-2021.09.0 % ./coq_platform_make.sh
====================== JUST COQ OR COMPLETE PLATFORM ? =======================
This script installs the Coq Platform version 2021.09.0, that is:
- the Coq compiler and Coq's standard library
- optionally CoqIDE, a GTK3 based graphical user interface
- optionally various widely used libraries and plugins
- optionally an extended set of libraries and plugins
The script uses opam, the OCaml package manager, to do all the work.
In case opam is not yet installed, it will install opam.
A new opam switch will be created unless a Coq Platform switch already exists.
This script is tested on Windows 10, macOS and many Linux variants.
The script compiles everything from sources, which might takes less than one
hour on a fast machine with lot's of RAM, or up to 6 hours with little RAM.
Instead of installing the full or extended Coq Platform now, you can install
just Coq (+ CoqIDE) and install additional packages via opam later as needed.
You should install CoqIDE unless you know what VSCoq or Proof General is.
====================== JUST COQ OR COMPLETE PLATFORM ? =======================
Install full (f), extended (x), Coq base (b) or Coq+CoqIDE (i)? (f/x/b/i/c=cancel) b
========================= SELECT PACKAGELIST VERSION ==========================
The Coq Platform allows to install the latest release version of Coq and
packages, but also older versions or development versions of Coq. You can
install several versions of Coq in parallel, which simplifies porting of
developments. You can use "opam switch" to switch between Coq versions.
The follwoing versions / package lists are supported:
(1): Coq 8.13.2 (released Apr 2021) with updated/extended package pick Nov 2021
(2): Coq 8.13.2 (released Apr 2021) with original package pick from Feb 2021
(3): Coq 8.12.2 (released Dec 2020)
(4): Coq 8.14.0 (released Oct 2021) with a beta package pick
(5): Coq 8.14 with Ltac debugger (unreleased preview)
(6): Coq dev (latest master of all packages)
Pleas select a version by entering the number shown at the begin of a line.
========================= SELECT PACKAGELIST VERSION ==========================
Select package list (number in 1..6, c=cancel) 1
=============================== PARALLEL BUILD ===============================
The Coq Platform opam build has two levels of parallelism:
- parallel build of (independent) opam packages
- parallel build inside the make of each opam package
Since a single coqc call can take more than 1 GB of RAM and since the two
above kinds of parallelism multiply, the total amount of memory can be large.
But it is not as bad as one might expect: test show that a full parallel
build takes less than 14GB of RAM with 15 parallel make jobs.
With 32 GB or RAM a parallel package build with 16 make jobs is recommended.
With 16 GB of RAM a parallel package build with 4 make jobs is recommended.
With 8 GB of RAM a sequential package build with 4 make jobs is recommended.
With 4 GB+1GB swap a sequential package build with 2 make jobs is recommended.
With less RAM, you might have to remove failing packages, e.g. VST.
In order to remove packages, just edit this script at "PACKAGE SELECTION".
In case these recommendations don't work for you, please report an issue at:
https://github.com/coq/platform/issues
=============================== PARALLEL BUILD ===============================
Build opam packages parallel (p) or sequential (s)? (p/s/c=cancel) p
Number of parallel make jobs (number in 1..16, c=cancel) 8
===== CHECKING VERSION OF INSTALLED OPAM =====
Found opam 2.1.0 - good!
/opt/homebrew/bin/opam
===== opam already initialized =====
===== CREATE OPAM SWITCH =====
[__coq-platform.2021.09.0.patch_ocaml] Initialised
[__coq-platform.2021.09.0.patch_coq-released] Initialised
[__coq-platform.2021.09.0.patch_coq-dev] Initialised
[coq-released] no changes from https://coq.inria.fr/opam/released
[coq-core-dev] no changes from https://coq.inria.fr/opam/core-dev
[coq-extra-dev] no changes from https://coq.inria.fr/opam/extra-dev
<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><> 🐫
Switch invariant: ["ocaml-base-compiler" {= "4.10.2"}]
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
βˆ— installed base-bigarray.base
βˆ— installed base-threads.base
βˆ— installed base-unix.base
⬇ retrieved ocaml-base-compiler.4.10.2 (https://opam.ocaml.org/cache)
βˆ— installed ocaml-base-compiler.4.10.2
βˆ— installed ocaml-config.1
βˆ— installed ocaml.4.10.2
Done.
=== OPAM REPOSITORIES ===
[NOTE] These are the repositories in use by the current switch. Use '--all' to see all configured repositories.
<><> Repository configuration for switch __coq-platform.2021.09.0~8.13 ><><> 🐫
1 __coq-platform.2021.09.0.patch_coq-released file:///Users/kartik/Downloads/platform-2021.09.0/opam/opam-coq-archive/released
2 __coq-platform.2021.09.0.patch_ocaml file:///Users/kartik/Downloads/platform-2021.09.0/opam/opam-repository
3 coq-released https://coq.inria.fr/opam/released
4 default https://opam.ocaml.org
=== OPAM PACKAGES ===
# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
ocaml 4.10.2 The OCaml compiler (virtual package)
ocaml-base-compiler 4.10.2 Official release 4.10.2
ocaml-config 1 OCaml Switch Configuration
Cleaning up switch __coq-platform.2021.09.0~8.13
===== UPDATE OPAM REPOSITORIES =====
<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><> 🐫
[__coq-platform.2021.09.0.patch_ocaml] no changes from file:///Users/kartik/Downloads/platform-2021.09.0/opam/opam-repository
[__coq-platform.2021.09.0.patch_coq-released] no changes from file:///Users/kartik/Downloads/platform-2021.09.0/opam/opam-coq-archive/released
[coq-released] no changes from https://coq.inria.fr/opam/released
[default] synchronised from https://opam.ocaml.org
Now run 'opam upgrade' to apply any package updates.
POL="$POL"'(allow network* (remote unix))'
===== INSTALL PREREQUISITES =====
[WARNING] set was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
Added 'jobs: "8"' to field variables in switch __coq-platform.2021.09.0~8.13
===== INSTALL OPAM PACKAGES (PARALLEL) =====
The following actions will be performed:
βˆ— install ocamlfind 1.9.1 [required by coq]
βˆ— install conf-gmp 3 [required by zarith]
βˆ— install conf-findutils 1 [required by coq]
βˆ— install num 1.4 [required by coq]
βˆ— install zarith 1.12 [required by coq]
βˆ— install coq 8.13.2
===== βˆ— 6 =====
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
⬇ retrieved num.1.4 (https://opam.ocaml.org/cache)
⬇ retrieved ocamlfind.1.9.1 (https://opam.ocaml.org/cache)
βˆ— installed conf-gmp.3
βˆ— installed conf-findutils.1
⬇ retrieved zarith.1.12 (https://opam.ocaml.org/cache)
⬇ retrieved coq.8.13.2 (https://opam.ocaml.org/cache)
βˆ— installed ocamlfind.1.9.1
βˆ— installed num.1.4
βˆ— installed zarith.1.12
βˆ— installed coq.8.13.2
Done.
============================== CLOSING REMARKS ===============================
The Coq Platform installation script finished successfully!
Use the following opam commands to switch to the Coq Platform opam switch:
opam switch __coq-platform.2021.09.0~8.13
eval $(opam env)
Or to just use this opam switch in the current shell (not setting the default):
eval $(opam config env --set-switch --switch __coq-platform.2021.09.0~8.13)
After switching you can list the installed packages with:
opam list
You can install additionalpackages with:
opam install <package>
There is a dedicated Zulip stream for the Coq Platform:
https://coq.zulipchat.com/#narrow/stream/250632-Coq-Platform.20devs.20.26.20users
============================== CLOSING REMARKS ===============================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment