Recently migrated from older MacBook Pro intel-based processor to MacBook Pro M3 Max and have tried everything I can think of to get Coq (8.17.1) installed, following the instructions and trying both the platform installation script and the more independent manual opam approach. I hope to continue use VSCode and its vscoq for working with coq. The good news is that the result is quite consistent; the bad news is that the installation process always ends up hanging at approximately the same stage of the processing. I’ve tried the various options offered in the platform installation script to see if anything helps move it along (variously trying the combinations of full/extended/base/ide with parallel vs sequential with various numbers of jobs, etc), and trying to simply re-run the installation script multiple times (keeping the same switch) to see if it will continue building on previous results). But absolutely no joy.
Further below, I’ve posted an excerpt from a typical output from the attempted installation process (one in which I’ve chosen to re-create the associated switch using the extended version with parallel and 12 make jobs not including compcert and excluding large packages) to help illustrate how far the installation process gets (apologies for the long post) and to illustrate how most of the process seems to be going fine with no obvious errors.
The process hangs with that “final” message “Processing 249/384: [coq-core: ./configure no],” and I have tried letting that continue to “run” for up to 15 hrs or so, just in case, but it continues to hang. All the various installation attempts have produced similar results.
When I ctl-C out of the hanging process, I get the output I’ve included even further below the example terminal output — again, apologies for the long post but trying to supply as much info as I can to anyone that might be able to offer guidance or suggestions. Any help or suggestions greatly appreciated.
EXAMPLE TERMINAL OUTPUT
===== CHECKING VERSION OF INSTALLED OPAM =====
Found opam 2.1.5 - good!
/usr/local/bin/opam
===== opam already initialized =====
===== CREATE OPAM SWITCH =====
[CP.2023.03.0.patch_ocaml] Initialised
[CP.2023.03.0.patch_coq-released] Initialised
[CP.2023.03.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-variants” {= “4.14.1+options”} “ocaml-option-flambda”]
Constructing initial basis…
<><> Processing actions <><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-option-flambda.1
retrieved ocaml-variants.4.14.1+options (cached)
∗ installed ocaml-variants.4.14.1+options
∗ installed ocaml-config.2
∗ installed ocaml.4.14.1
Done.
=== OPAM SWITCHES ===
switch compiler description
→ CP.2023.03.0~8.17~2023.08 ocaml-option-flambda.1,ocaml-variants.4.14.1+options Coq 8.17.1 (released Jun
2023) with the first package
pick from Aug 2023
coq.8.18.1 ocaml-base-compiler.4.14.1 coq.8.18.1
[NOTE] Current switch is set locally through the OPAMSWITCH variable.
The current global system switch is unset.
=== OPAM REPOSITORIES ===
[NOTE] These are the repositories in use by the current switch. Use ‘–all’ to see all configured repositories.
<><> Repository configuration for switch CP.2023.03.0~8.17~2023.08 ><><><><>
1 CP.2023.03.0.patch_coq-released file:///Users/warrencraft/Downloads/platform-2023.03.0/opam/opam-coq-archive/released
2 CP.2023.03.0.patch_ocaml file:///Users/warrencraft/Downloads/platform-2023.03.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.14.1 The OCaml compiler (virtual package)
ocaml-config 2 OCaml Switch Configuration
ocaml-option-flambda 1 Set OCaml to be compiled with flambda activated
ocaml-variants 4.14.1+options Official release of OCaml 4.14.1
Cleaning up switch CP.2023.03.0~8.17~2023.08
===== UPDATE OPAM REPOSITORIES =====
<><> Updating package repositories ><><><><><><><><><><><><><><><><><><><><>
[CP.2023.03.0.patch_ocaml] no changes from file:///Users/warrencraft/Downloads/platform-2023.03.0/opam/opam-repository
[CP.2023.03.0.patch_coq-released] no changes from file:///Users/warrencraft/Downloads/platform-2023.03.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.
===== FINAL OPAM SANITY CHECKS =====
[NOTE] These are the repositories in use by the current switch. Use ‘–all’ to see all configured repositories.
[NOTE] These are the repositories in use by the current switch. Use ‘–all’ to see all configured repositories.
[NOTE] These are the repositories in use by the current switch. Use ‘–all’ to see all configured repositories.
[NOTE] These are the repositories in use by the current switch. Use ‘–all’ to see all configured repositories.
POL=“$POL”‘(allow network* (remote unix))’
===== INSTALL PREREQUISITES (PARALLEL) =====
Constructing initial basis…
Number of 0-1 knapsack inequalities = 491
Constructing conflict graph…
Conflict graph has 158 + 70 = 228 vertices
[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: “12”’ to field variables in switch CP.2023.03.0~8.17~2023.08
===== INSTALL OPAM PACKAGES (PARALLEL) =====
Constructing initial basis…
Number of 0-1 knapsack inequalities = 491
Constructing conflict graph…
Conflict graph has 158 + 70 = 228 vertices
The following actions will be performed:
∗ install conf-g++ 1.0 [required by gappa, coq-hammer, coq-flocq, etc.]
∗ install num 1.5 [required by coq-coqprime-generator]
… [VARIOUS THINGS OMITTED HERE FOR BREVITY] …
∗ install coq-metacoq-erasure-plugin 1.2+8.17 [required by coq-metacoq]
∗ install coq-metacoq 1.2+8.17
===== ∗ 128 =====
<><> Processing actions <><><><><><><><><><>
retrieved atd.2.15.0 (cached)
retrieved atdgen-runtime.2.15.0 (cached)
retrieved atdgen.2.15.0 (cached)
retrieved base.v0.15.1 (cached)
retrieved biniou.1.2.2 (cached)
retrieved camlp-streams.5.0.1 (cached)
∗ installed conf-boost.1
∗ installed conf-g++.1.0
∗ installed conf-gcc.1.0
retrieved coq.8.17.1 (cached)
∗ installed conf-flex.2
retrieved coq-aac-tactics.8.17.0 (cached)
retrieved cmdliner.1.2.0 (cached)
retrieved coq-coqeal.1.1.3 (cached)
retrieved coq-bignums.9.0.0+coq8.17 (cached)
∗ installed conf-bison.2
∗ installed conf-c++.1.0
∗ installed conf-gmp.4
∗ installed conf-libtool.1
∗ installed conf-pkg-config.3
∗ installed conf-python-3.9.0.0
∗ installed conf-which.1
retrieved coq-coqprime.1.3.0 (cached)
∗ installed conf-autoconf.0.1
∗ installed conf-mpfr.3
retrieved coq-coqprime-generator.1.1.1 (cached)
retrieved coq-coquelicot.3.4.0 (cached)
retrieved atdts.2.15.0 (cached)
retrieved coq-corn.8.16.0 (cached)
retrieved coq-deriving.0.1.1 (cached)
retrieved coq-dpdgraph.1.0+8.17 (cached)
∗ installed conf-automake.1
retrieved coq-elpi.1.17.1 (cached)
retrieved coq-equations.1.3+8.17 (cached)
retrieved coq-ext-lib.0.11.8 (cached)
retrieved coq-extructures.0.3.1 (cached)
retrieved coq-flocq.4.1.1 (cached)
retrieved coq-gappa.1.5.3 (cached)
retrieved coq-hammer.1.3.2+8.17 (cached)
retrieved coq-hammer-tactics.1.3.2+8.17 (cached)
retrieved coq-hierarchy-builder.1.4.0 (cached)
retrieved coq-core.8.17.1 (cached)
retrieved coq-interval.4.8.0 (cached)
retrieved coq-iris.4.0.0 (cached)
retrieved coq-iris-heap-lang.4.0.0 (cached)
retrieved coq-itauto.8.17.0 (cached)
retrieved coq-libhyps.2.0.6 (cached)
retrieved coq-math-classes.8.17.0 (cached)
retrieved coq-mathcomp-algebra.1.17.0 (cached)
retrieved coq-mathcomp-algebra-tactics.1.1.1 (cached)
retrieved coq-mathcomp-analysis.0.6.3 (cached)
retrieved coq-mathcomp-bigenough.1.0.1 (cached)
retrieved coq-hott.8.17 (cached)
retrieved coq-mathcomp-classical.0.6.3 (cached)
retrieved coq-mathcomp-field.1.17.0 (cached)
retrieved coq-mathcomp-fingroup.1.17.0 (cached)
retrieved coq-mathcomp-finmap.1.5.2 (cached)
retrieved coq-mathcomp-multinomials.1.6.0 (cached)
retrieved coq-mathcomp-real-closed.1.1.4 (cached)
retrieved coq-mathcomp-character.1.17.0 (cached)
retrieved coq-mathcomp-ssreflect.1.17.0 (cached)
retrieved coq-mathcomp-word.2.1 (cached)
retrieved coq-mathcomp-zify.1.3.0+1.12+8.13 (cached)
retrieved coq-mathcomp-solvable.1.17.0 (cached)
retrieved coq-menhirlib.20220210 (cached)
retrieved coq-metacoq-common.1.2+8.17 (cached)
retrieved coq-metacoq-erasure.1.2+8.17 (cached)
retrieved coq-metacoq-erasure-plugin.1.2+8.17 (cached)
retrieved coq-metacoq-pcuic.1.2+8.17 (cached)
retrieved coq-metacoq-quotation.1.2+8.17 (cached)
retrieved coq-metacoq-safechecker.1.2+8.17 (cached)
retrieved coq-metacoq-safechecker-plugin.1.2+8.17 (cached)
retrieved coq-metacoq-template.1.2+8.17 (cached)
retrieved coq-metacoq-template-pcuic.1.2+8.17 (cached)
retrieved coq-metacoq-translations.1.2+8.17 (cached)
retrieved coq-metacoq-utils.1.2+8.17 (cached)
retrieved coq-mtac2.1.4+8.17 (cached)
retrieved coq-metacoq.1.2+8.17 (cached)
retrieved coq-paramcoq.1.1.3+coq8.17 (cached)
retrieved coq-ott.0.33 (cached)
retrieved coq-record-update.0.3.2 (cached)
retrieved coq-reduction-effects.0.1.4 (cached)
retrieved coq-reglang.1.1.3 (cached)
retrieved coq-relation-algebra.1.7.9 (cached)
retrieved coq-quickchick.1.6.5 (cached)
retrieved coq-simple-io.1.8.0 (cached)
retrieved coq-serapi.8.17.0+0.17.0 (cached)
retrieved coq-stdpp.1.8.0 (cached)
retrieved coq-unicoq.1.6+8.17 (cached)
retrieved cppo.1.6.9 (cached)
retrieved csexp.1.5.2 (cached)
∗ installed cmdliner.1.2.0
retrieved coq-stdlib.8.17.1 (cached)
retrieved dune.3.7.0 (cached)
retrieved easy-format.1.3.4 (cached)
retrieved dune-configurator.3.7.0 (cached)
retrieved elpi.1.16.9 (cached)
retrieved coqide-server.8.17.1 (cached)
retrieved gappa.1.4.1 (cached)
retrieved gmp-ecm.7.0.3 (cached)
retrieved menhirLib.20220210 (cached)
retrieved menhir.20220210 (cached)
retrieved menhirSdk.20220210 (cached)
retrieved num.1.5 (cached)
retrieved ocaml-compiler-libs.v0.12.4 (cached)
retrieved ocamlbuild.0.14.3 (cached)
retrieved ocamlfind.1.9.5~relocatable (cached)
retrieved ocamlgraph.2.1.0 (cached)
retrieved ott.0.33 (cached)
retrieved parsexp.v0.15.0 (cached)
retrieved ppx_compare.v0.15.0 (cached)
retrieved ppx_derivers.1.2.1 (cached)
retrieved eprover.2.6 (cached)
retrieved ppx_hash.v0.15.0 (cached)
retrieved ppx_deriving_yojson.3.7.0 (cached)
retrieved ppx_import.1.10.0 (cached)
retrieved ppx_sexp_conv.v0.15.1 (cached)
retrieved ppx_deriving.5.2.1 (cached)
retrieved re.1.11.0 (cached)
∗ installed seq.base
retrieved result.1.5 (cached)
retrieved ppxlib.0.31.0 (cached)
retrieved sexplib0.v0.15.1 (cached)
retrieved stdlib-shims.0.3.0 (cached)
retrieved sexplib.v0.15.1 (cached)
retrieved yojson.2.1.2 (cached)
∗ installed num.1.5
retrieved zarith.1.13 (cached)
retrieved z3.4.11.2 (cached)
retrieved z3_tptp.4.11.2 (cached)
∗ installed ocamlfind.1.9.5~relocatable
∗ installed ocamlbuild.0.14.3
∗ installed zarith.1.13
∗ installed gappa.1.4.1
∗ installed dune.3.7.0
∗ installed camlp-streams.5.0.1
∗ installed easy-format.1.3.4
∗ installed csexp.1.5.2
∗ installed ppx_derivers.1.2.1
∗ installed biniou.1.2.2
∗ installed sexplib0.v0.15.1
∗ installed gmp-ecm.7.0.3
∗ installed cppo.1.6.9
∗ installed menhirLib.20220210
∗ installed menhirSdk.20220210
∗ installed ocaml-compiler-libs.v0.12.4
∗ installed re.1.11.0
∗ installed result.1.5
∗ installed stdlib-shims.0.3.0
∗ installed dune-configurator.3.7.0
∗ installed yojson.2.1.2
∗ installed atdgen-runtime.2.15.0
∗ installed ocamlgraph.2.1.0
∗ installed base.v0.15.1
∗ installed parsexp.v0.15.0
∗ installed eprover.2.6
∗ installed sexplib.v0.15.1
∗ installed ott.0.33
∗ installed ppxlib.0.31.0
∗ installed ppx_compare.v0.15.0
∗ installed ppx_import.1.10.0
∗ installed ppx_deriving.5.2.1
∗ installed ppx_sexp_conv.v0.15.1
∗ installed menhir.20220210
∗ installed ppx_hash.v0.15.0
∗ installed ppx_deriving_yojson.3.7.0
∗ installed atd.2.15.0
∗ installed atdts.2.15.0
∗ installed coq-coqprime-generator.1.1.1
∗ installed atdgen.2.15.0
∗ installed elpi.1.16.9
∗ installed z3.4.11.2
∗ installed z3_tptp.4.11.2
Processing 249/384: [coq-core: ./configure no]
EXAMPLE OUTPUT WHEN CTL-C OUT OF HUNG PROCESS
[ERROR] User interruption
<><> Error report <><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-core 8.17.1
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install atd 2.15.0
│ ∗ install atdgen 2.15.0
│ … [VARIOUS THINGS OMITTED HERE FOR BREVITY] …
│ ∗ install z3 4.11.2
│ ∗ install z3_tptp 4.11.2
│ ∗ install zarith 1.13
└─
The former state can be restored with:
/usr/local/bin/opam switch import
“/Users/warrencraft/.opam/CP.2023.03.0~8.17~2023.08/.opam-switch/backup/state-20240112173542.export”