Reputation: 5139

How does one install a new version of Coq when it cannot find the repositories in a new Mac M1 machine?

I got a new machine (mac book m1, not sure if it matters) and I noticed I didn't have Coq:

(base) brandomiranda~ ❯ coqc -v

zsh: command not found: coqc

So I went to the instructions to download coq (https://coq.inria.fr/opam-using.html). Some part of it seems to work:

(base) brandomiranda~ ❯ opam init
eval $(opam env)

<><> Required setup - please read <><><><><><><><><><><><><><><><><><><><><>  🐫

  In normal operation, opam only alters files within ~/.opam.

  However, to best integrate with your system, some environment variables
  should be set. If you allow it to, this initialisation step will update
  your zsh configuration by adding the following line to ~/.zshrc:

    [[ ! -r /Users/brandomiranda/.opam/opam-init/init.zsh ]] || source /Users/brandomiranda/.opam/opam-init/init.zsh  > /dev/null 2> /dev/null

  Otherwise, every time you want to access your opam installation, you will
  need to run:

    eval $(opam env)

  You can always re-run this setup with 'opam init' later.

Do you want opam to modify ~/.zshrc? [N/y/f]
(default is 'no', use 'f' to choose a different file) y
A hook can be added to opam's init scripts to ensure that the shell remains in sync with the opam environment when they are loaded. Set that up? [y/N] y

User configuration:
  Updating ~/.zshrc.

but then when I go get and pin coq opam can't find it:

(base) brandomiranda~ ❯ opam pin add coq 8.15.0
[ERROR] Package coq has no known version 8.15.0 in the repositories

anyone know what is going on? Seems puzzling.

cross: https://coq.discourse.group/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found/1562 https://github.com/coq/platform/issues/219

Getting this issue now:

(base) brandomiranda~ ❯ opam upgrade
[WARNING] Upgrade is not possible because of conflicts or packages that are no longer available:
    - Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

You may run "opam upgrade --fixup" to let opam fix the current state.
(base) brandomiranda~ ❯ opam upgrade --fixup
[ERROR] It appears that the switch invariant is no longer satisfiable. Either fix the package prerequisites or change the invariant with 'opam switch set-invariant'.
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

No solution found, exiting
(base) brandomiranda~ ❯ opam remove ocaml-base-compiler
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

No solution found, exiting

also:

(base) brandomiranda~ ❯ opam info coq

<><> coq: information on all versions <><><><><><><><><><><><><><><><><><><>  🐫
name         coq
all-versions 8.3  8.4pl1  8.4pl2  8.4pl4  8.4.5  8.4.6~camlp4  8.4.6  8.5.0~camlp4  8.5.0  8.5.1  8.5.2~camlp4  8.5.2  8.5.3  8.6  8.6.1  8.7.0  8.7.1  8.7.1+1  8.7.1+2  8.7.2
             8.8.0  8.8.1  8.8.2  8.9.0  8.9.1  8.10.0  8.10.1  8.10.2  8.11.0  8.11.1  8.11.2  8.12.0  8.12.1  8.12.2  8.13.0  8.13.1  8.13.2  8.14.0  8.14.1  8.15.0

<><> Version-specific details <><><><><><><><><><><><><><><><><><><><><><><>  🐫
version      8.15.0
repository   default
url.src      "https://github.com/coq/coq/archive/refs/tags/V8.15.0.tar.gz"
url.checksum "sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3"
homepage     "https://coq.inria.fr/"
bug-reports  "https://github.com/coq/coq/issues"
dev-repo     "git+https://github.com/coq/coq.git"
authors      "The Coq development team, INRIA, CNRS, and contributors."
maintainer   "[email protected]"
license      "LGPL-2.1-only"
depends      "ocaml" {>= "4.05.0"}
             "ocamlfind" {build}
             "dune" {>= "2.5.1"}
             "conf-findutils" {build}
             "zarith" {>= "1.10"}
depopts      "coq-native"
conflicts    "base-nnp" "ocaml-option-nnpchecker"
synopsis     Formal proof management system
description  The Coq proof assistant provides a formal language to write
             mathematical definitions, executable algorithms, and theorems, together
             with an environment for semi-interactive development of machine-checked
             proofs. Typical applications include the certification of properties of programming
             languages (e.g., the CompCert compiler certification project and the
             Bedrock verified low-level programming library), the formalization of
             mathematics (e.g., the full formalization of the Feit-Thompson theorem
             and homotopy type theory) and teaching.

(base) brandomiranda~ ❯ opam switch create NAME 4.07.0

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><>  🐫
Switch invariant: ["ocaml-base-compiler" {= "4.07.0"} | "ocaml-system" {= "4.07.0"}]
[ERROR] Could not determine which packages to install for this switch:
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0 | ocaml-system = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'
    unmet availability conditions: 'sys-ocaml-version = "4.07.0"'


Switch initialisation failed: clean up? ('n' will leave the switch partially installed) [Y/n] Y

seems there was an error:

∗ installed eprover.2.6
[ERROR] The compilation of cairo2.0.6.2 failed at "dune build -p cairo2 -j 16".
∗ installed ocamlgraph.2.0.0
∗ installed zarith.1.12
∗ installed coq-coqprime-generator.dev
∗ installed ocaml-migrate-parsetree.1.8.0
[ERROR] The compilation of z3.4.8.13 failed at "python3 scripts/mk_make.py --ml".
∗ installed menhir.dev
∗ installed ppxlib.0.15.0
∗ installed ppx_deriving.5.1
∗ installed elpi.1.14.1
⬇ retrieved coq-unimath.dev  (git+https://github.com/UniMath/UniMath.git#master)
Processing 188/279: [coq: make]

∗ installed coq.dev
∗ installed coq-dpdgraph.dev
∗ installed coq-hammer-tactics.dev
∗ installed coq-ext-lib.dev
∗ installed coq-aac-tactics.dev
∗ installed coq-libhyps.dev
∗ installed coq-hammer.dev
∗ installed coq-paramcoq.dev
∗ installed coq-menhirlib.dev
∗ installed coq-simple-io.dev
∗ installed coq-bignums.dev
∗ installed coq-unicoq.dev
∗ installed coq-mathcomp-ssreflect.dev
∗ installed coq-hott.dev
∗ installed coq-stdpp.dev
∗ installed coq-flocq.3.dev
∗ installed coq-math-classes.dev
∗ installed coq-coquelicot.dev
∗ installed coq-coqprime.dev
∗ installed coq-equations.dev
∗ installed coq-gappa.dev
∗ installed coq-mathcomp-bigenough.dev
[ERROR] The compilation of coq-interval.dev failed at "./remake -j16".
∗ installed coq-mathcomp-fingroup.dev
∗ installed coq-elpi.dev
∗ installed coq-mtac2.dev
∗ installed coq-mathcomp-finmap.dev
∗ installed coq-hierarchy-builder.dev
∗ installed coq-reglang.dev
∗ installed coq-quickchick.dev
∗ installed coq-compcert.dev
∗ installed coq-iris.dev
∗ installed coq-mathcomp-algebra.dev
∗ installed coq-mathcomp-zify.dev
∗ installed coq-mathcomp-multinomials.dev
∗ installed coq-iris-heap-lang.dev
∗ installed coq-mathcomp-solvable.dev
∗ installed coq-corn.dev
∗ installed coq-mathcomp-field.dev
∗ installed coq-mathcomp-real-closed.dev
∗ installed coq-coqeal.dev
∗ installed coq-mathcomp-character.dev
∗ installed coq-mathcomp-analysis.dev
∗ installed coq-unimath.dev
∗ installed coq-vst.dev

#=== ERROR while compiling z3.4.8.13 ==========================================#
# context              2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | file:///Users/brandomiranda/Downloads/platform-2022.01.0/opam/opam-repository
# path                 ~/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13
# command              ~/.opam/opam-init/hooks/sandbox.sh build python3 scripts/mk_make.py --ml
# exit-code            1
# env-file             ~/.opam/log/z3-96628-ab4f2a.env
# output-file          ~/.opam/log/z3-96628-ab4f2a.out
### output ###
# [...]
# Copied 'z3types.cpython-39.pyc'
# Copied 'z3core.cpython-39.pyc'
# Testing ocamlc...
# Testing ocamlopt...
# Traceback (most recent call last):
#   File "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13/scripts/mk_make.py", line 18, in <module>
#     mk_bindings(API_files)
#   File "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13/scripts/mk_util.py", line 3044, in mk_bindings
#     check_ml()
#   File "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/z3.4.8.13/scripts/mk_util.py", line 450, in check_ml
#     raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.')
# mk_exception.MKException: 'Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.'


#=== ERROR while compiling coq-interval.dev ===================================#
# context              2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | https://coq.inria.fr/opam/extra-dev#2022-02-15 19:00
# path                 ~/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/coq-interval.dev
# command              ~/.opam/opam-init/hooks/sandbox.sh build ./remake -j16
# exit-code            1
# env-file             ~/.opam/log/coq-interval-96628-942e59.env
# output-file          ~/.opam/log/coq-interval-96628-942e59.out
### output ###
# [...]
# [deprecated-syntactic-definition,deprecated]
# File "./src/Interval/Transcend.v", line 2077, characters 14-24:
# Warning: Notation plus_assoc is deprecated since 8.16.
# The Arith.Plus file is obsolete. Use Nat.add_assoc instead.
# [deprecated-syntactic-definition,deprecated]
# Finished src/Interval/Transcend.vo
# Finished src/Interval/Float_full.vo
# File "./src/Tactic.v", line 22, characters 0-42:
# Warning:
# New coercion path [real; Finite] : Rbar >-> Rbar is not definitionally an identity function.
# [ambiguous-paths,typechecker]
# Finished src/Tactic.vo


#=== ERROR while compiling cairo2.0.6.2 =======================================#
# context              2.1.2 | macos/arm64 | ocaml-base-compiler.4.10.2 | https://opam.ocaml.org#28fab8d8
# path                 ~/.opam/__coq-platform.2022.01.0~dev/.opam-switch/build/cairo2.0.6.2
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p cairo2 -j 16
# exit-code            1
# env-file             ~/.opam/log/cairo2-96628-a005f1.env
# output-file          ~/.opam/log/cairo2-96628-a005f1.out
### output ###
#   ocamlmklib src/dllcairo_stubs.so,src/libcairo_stubs.a (exit 2)
# (cd _build/default && /Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/bin/ocamlmklib.opt -g -o src/cairo_stubs src/cairo_stubs.o -L/opt/homebrew/opt/freetype/lib -lfreetype -L/opt/homebrew/Cellar/fontconfig/2.13.1/lib -L/opt/homebrew/opt/freetype/lib -lfontconfig -lfreetype -L/opt/homebrew/Cellar/cairo/1.16.0_5/lib -lcairo)
# ld: in '/usr/local/lib/libpng16.16.dylib', building for macOS-arm64 but attempting to link with file built for macOS-x86_64
# clang: error: linker command failed with exit code 1 (use -v to see invocation)



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
│ λ build cairo2       0.6.2
│ λ build coq-interval dev
│ λ build z3           4.8.13
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install camlp5                    7.14
│ ∗ install conf-adwaita-icon-theme   2
│ ∗ install conf-autoconf             0.1
│ ∗ install conf-automake             1
│ ∗ install conf-cairo                1
│ ∗ install conf-findutils            1
│ ∗ install conf-g++                  1.0
│ ∗ install conf-gcc                  1.0
│ ∗ install conf-gmp                  4
│ ∗ install conf-gtk3                 18
│ ∗ install conf-gtksourceview3       0+2
│ ∗ install conf-libtool              1
│ ∗ install conf-perl                 2
│ ∗ install conf-pkg-config           2
│ ∗ install conf-python-3             9.0.0
│ ∗ install conf-which                1
│ ∗ install coq                       dev
│ ∗ install coq-aac-tactics           dev
│ ∗ install coq-bignums               dev
│ ∗ install coq-compcert              dev
│ ∗ install coq-coqeal                dev
│ ∗ install coq-coqprime              dev
│ ∗ install coq-coqprime-generator    dev
│ ∗ install coq-coquelicot            dev
│ ∗ install coq-corn                  dev
│ ∗ install coq-dpdgraph              dev
│ ∗ install coq-elpi                  dev
│ ∗ install coq-equations             dev
│ ∗ install coq-ext-lib               dev
│ ∗ install coq-flocq                 3.dev
│ ∗ install coq-gappa                 dev
│ ∗ install coq-hammer                dev
│ ∗ install coq-hammer-tactics        dev
│ ∗ install coq-hierarchy-builder     dev
│ ∗ install coq-hott                  dev
│ ∗ install coq-iris                  dev
│ ∗ install coq-iris-heap-lang        dev
│ ∗ install coq-libhyps               dev
│ ∗ install coq-math-classes          dev
│ ∗ install coq-mathcomp-algebra      dev
│ ∗ install coq-mathcomp-analysis     dev
│ ∗ install coq-mathcomp-bigenough    dev
│ ∗ install coq-mathcomp-character    dev
│ ∗ install coq-mathcomp-field        dev
│ ∗ install coq-mathcomp-fingroup     dev
│ ∗ install coq-mathcomp-finmap       dev
│ ∗ install coq-mathcomp-multinomials dev
│ ∗ install coq-mathcomp-real-closed  dev
│ ∗ install coq-mathcomp-solvable     dev
│ ∗ install coq-mathcomp-ssreflect    dev
│ ∗ install coq-mathcomp-zify         dev
│ ∗ install coq-menhirlib             dev
│ ∗ install coq-mtac2                 dev
│ ∗ install coq-paramcoq              dev
│ ∗ install coq-quickchick            dev
│ ∗ install coq-reglang               dev
│ ∗ install coq-simple-io             dev
│ ∗ install coq-stdpp                 dev
│ ∗ install coq-unicoq                dev
│ ∗ install coq-unimath               dev
│ ∗ install coq-vst                   dev
│ ∗ install cppo                      1.6.8
│ ∗ install csexp                     1.5.1
│ ∗ install dune                      2.9.3
│ ∗ install dune-configurator         2.9.3
│ ∗ install elpi                      1.14.1
│ ∗ install eprover                   2.6
│ ∗ install gmp-ecm                   7.0.3
│ ∗ install menhir                    dev
│ ∗ install menhirLib                 dev
│ ∗ install menhirSdk                 dev
│ ∗ install num                       1.4
│ ∗ install ocaml-compiler-libs       v0.12.4
│ ∗ install ocaml-migrate-parsetree   1.8.0
│ ∗ install ocamlbuild                0.14.1
│ ∗ install ocamlfind                 1.9.3
│ ∗ install ocamlgraph                2.0.0
│ ∗ install ppx_derivers              1.2.1
│ ∗ install ppx_deriving              5.1
│ ∗ install ppxlib                    0.15.0
│ ∗ install re                        1.10.3
│ ∗ install result                    1.5
│ ∗ install seq                       base
│ ∗ install sexplib0                  v0.14.0
│ ∗ install stdlib-shims              0.3.0
│ ∗ install zarith                    1.12
└─

<><> cairo2.0.6.2 troubleshooting <><><><><><><><><><><><><><><><><><><><><>  🐫
=> Try to re-run the install command with PKG_CONFIG_PATH pointing a pkg-config path including libffi, e.g. if you use homebrew you can try
   PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig

The former state can be restored with:
    /opt/homebrew/bin/opam switch import "/Users/brandomiranda/.opam/__coq-platform.2022.01.0~dev/.opam-switch/backup/state-20220216165905.export"

when running the coq plataform script:

(base) brandomiranda~/Downloads/platform-2022.01.0 ❯ bash coq_platform_make.sh

Upvotes: 0

Answers (2)

Charlie Parker

Reputation: 5139

In case you are confsued what "install with the Coq Platform scripts" means here is a few more details:

Installing Coq

install brew: https://brew.sh/
Follow the Coq Platform scripts for installation: https://coq.inria.fr/opam-using.html or "Installation by compiling from Sources using opam" https://github.com/coq/platform/blob/main/doc/README_macOS.md.

Last time I installed this I downloaded their coq zip file with the instlal script (note check for most recent or version you want e.g. at https://github.com/coq/platform/blob/main/doc/README_macOS.md):

https://github.com/coq/platform/archive/refs/tags/2022.01.0.zip

and ran after cding to the unzipped files location of the above:

bash coq_platform_make.sh

select the version you want (likely something stable! Avoid, beta, dev. At the time of this writing option 7.

you might have to do eval $(opam env).
Check it installed correctly:

coqc -v

output something like:

The Coq Proof Assistant, version 8.16+alpha
compiled with OCaml 4.10.2

if its working

Note, for HPCs

it seems one can do this too:

# - install opam
# brew install opam
# https://stackoverflow.com/questions/72522266/how-does-one-install-opam-with-conda-for-mac-apple-os-x
conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
#eval $(opam env)

# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

Upvotes: 1

Zimm i48

Reputation: 3081

If you are not an opam / OCaml expert, then you're best bet to install Coq with opam is to rely on the scripts provided by the Coq Platform. See: https://github.com/coq/platform/releases

These interactive scripts will take care of:

creating a new opam switch
installing an appropriate version of the OCaml compiler
installing any external dependencies you need (e.g., if you want CoqIDE)
they can also propose to install a collection of additional Coq packages that can be useful for Coq projects

Finally, relying on this script creates a sound basis that you can later extend if you need more Coq packages that were not included in the Platform.

Upvotes: 4

How does one install a new version of Coq when it cannot find the repositories in a new Mac M1 machine?

Answers (2)

Installing Coq

Note, for HPCs

Related Questions