How to install Coq when it says the repository cannot be found? (e.g. issues with m1 chip mac, apple)

This seems like a a weird question. I got a new mac m1 machine and I can’t install coq (maybe its unrealted to that). Opam seems fine but when I try to pin a new coq version it can’t find the repo:

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

anyone know how to fix this?

cross: How does one install a new version of Coq when it cannot find the repositories in a new mac m1 machine? - Stack Overflow

what does opam info coq tells you?

(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   "coqdev@inria.fr"
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.

Though most recent attempt:

(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

This is unrelated to Coq. For some reason, you were able to install OCaml 4.07 on your computer, while the minimal version of OCaml supported on Apple M1 is 4.12. So, Opam is utterly confused and it will refuse to install most packages.

You can try to run “opam upgrade --unlock-base”. If that does not work, I think your only solution is to delete your Opam switch and start again from scratch.

1 Like

For what is worth, the minimal OCaml version supported on Apple M1 is now lower than this. OCaml 4.10.2 was released with M1 support: OCaml 4.10.2 – OCaml. This is the version currently used in the Coq Platform (Release 2022.01.0 · coq/platform · GitHub) and it has been tested to work by M1 users.

1 Like

this probably happened due to a restoring from a time machine

issue:

(base) brandomiranda~ ❯ opam upgrade --unlock-base
opam: --unlock-base was removed in version 2.1 of the opam CLI, but version 2.1 has been requested. Use --update-invariant instead or set OPAMCLI environment variable to 2.0.

ok trying

(base) brandomiranda~ ❯ opam upgrade --update-invariant

Ok now the error is:

(base) brandomiranda~ ❯ opam pin add coq 8.15.0
coq is now pinned to version 8.15.0

[ERROR] Package conflict!
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

[NOTE] Pinning command successful, but your installed packages may be out of sync

@silene how do I do that? I thought I had already tried that with

opam remove ocaml-base-compiler

This is my current state:

- bin/ocamlc.byte
  - bin/ocaml-instr-report
  - bin/ocaml-instr-graph
  - bin/ocaml
Remove them anyway? [y/N] n
[NOTE] While removing ocaml-base-compiler.4.07.0: not removing non-empty directories:
         - lib/ocaml/vmthreads
         - lib/ocaml/threads
         - lib/ocaml/stublibs
         - lib/ocaml/ocamldoc
         - lib/ocaml/compiler-libs
         - lib/ocaml/caml

⊘ removed   ocaml-base-compiler.4.07.0
[ERROR] The installation of ocaml-base-compiler failed at "make install".

#=== ERROR while installing ocaml-base-compiler.4.13.1 ========================#
# context     2.1.2 | macos/arm64 |  | https://opam.ocaml.org#c353c5ad
# path        ~/.opam/4.07.0/.opam-switch/build/ocaml-base-compiler.4.13.1
# command     ~/.opam/opam-init/hooks/sandbox.sh install make install
# exit-code   2
# env-file    ~/.opam/log/ocaml-base-compiler-46994-ad3999.env
# output-file ~/.opam/log/ocaml-base-compiler-46994-ad3999.out
### output ###
# [...]
# /usr/bin/install -c ocamlc "/Users/brandomiranda/.opam/4.07.0/bin/ocamlc.byte"
# /Library/Developer/CommandLineTools/usr/bin/make -C stdlib install
# stale="stdlib__arg.cmi stdlib__array.cmi stdlib__arrayLabels.cmi stdlib__bigarray.cmi stdlib__buffer.cmi stdlib__bytes.cmi stdlib__bytesLabels.cmi stdlib__callback.cmi stdlib__char.cmi stdlib__complex.cmi stdlib__digest.cmi stdlib__ephemeron.cmi stdlib__lexing.cmi stdlib__list.cmi stdlib__listLabels.cmi stdlib__map.cmi stdlib__marshal.cmi stdlib__moreLabels.cmi stdlib__nativeint.cmi stdlib__o[...]
#   if test -n "$stale" ; then \
#     echo "/Users/brandomiranda/.opam/4.07.0/lib/ocaml contains stale stdlib artefacts"; \
#     echo "Please rm /Users/brandomiranda/.opam/4.07.0/lib/ocaml/stdlib__*.cm* and re-run make install"; \
#     exit 1; \
#   fi
# /Users/brandomiranda/.opam/4.07.0/lib/ocaml contains stale stdlib artefacts
# Please rm /Users/brandomiranda/.opam/4.07.0/lib/ocaml/stdlib__*.cm* and re-run make install
# make[1]: *** [install] Error 1
# make: *** [install] Error 2



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
┌─ The following actions failed
│ ∗ install ocaml-base-compiler 4.13.1
└─
┌─ The following changes have been performed (the rest was aborted)
│ ⊘ remove  base-bytes            base
│ ⊘ remove  camomile              1.0.2
│ ⊘ remove  charInfo_width        1.1.0
│ ⊘ remove  cppo                  1.6.6
│ ⊘ remove  dune                  1.11.4
│ ⊘ remove  dune-configurator     1.0.0
│ ⊘ remove  lambda-term           2.0.2
│ ⊘ remove  lwt                   4.4.0
│ ⊘ remove  lwt_log               1.1.1
│ ⊘ remove  lwt_react             1.1.3
│ ⊘ remove  mmap                  1.1.0
│ ⊘ remove  ocaml                 4.07.0
│ ⊘ remove  ocaml-base-compiler   4.07.0
│ ⊘ remove  ocaml-config          1
│ ⊘ remove  ocamlbuild            0.14.0
│ ⊘ remove  ocamlfind             1.8.1
│ ⊘ remove  ocplib-endian         1.0
│ ⊘ remove  opam-depext           1.1.3
│ ⊘ remove  react                 1.2.1
│ ⊘ remove  result                1.4
│ ⊘ remove  seq                   base
│ ⊘ remove  topkg                 1.0.1
│ ⊘ remove  utop                  2.4.2
│ ⊘ remove  zed                   2.0.3
│ ∗ install ocaml-options-vanilla 1
└─

<><> ocaml-base-compiler.4.13.1 troubleshooting <><><><><><><><><><><><><><>  🐫
=> A failure in the middle of the build may be caused by build parallelism
      (enabled by default).
      Please file a bug report at https://github.com/ocaml/opam-repository/issues
=> You can try installing again including --jobs=1
      to force a sequential build instead.

The former state can be restored with:
    /opt/homebrew/bin/opam switch import "/Users/brandomiranda/.opam/4.07.0/.opam-switch/backup/state-20220215184125.export"
Or you can retry to install your package selection with:
    /opt/homebrew/bin/opam install --restore
(base) brandomiranda~ ❯ opam pin add coq 8.15.0
coq is now pinned to version 8.15.0

[ERROR] Package conflict!
  * Missing dependency:
    - ocaml-base-compiler = 4.07.0
    unmet availability conditions: '!(os = "macos" & arch = "arm64")'

[NOTE] Pinning command successful, but your installed packages may be out of sync.
(base) brandomiranda~ ❯ opam list
# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-m4               1           Virtual package relying on m4
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled

@Zimmi48

I guess I got confused because of this page https://coq.inria.fr/opam-using.html so opam isn’t the recommended way to install Coq (especially if I want to use it outside of the coqide e.g. emacs, vscode).

I wouldn’t say that opam is not recommended given that the Platform scripts themselves are just a thin wrapper around opam. But this wrapper allows anyone without a lot of opam knowledge to easily install Coq and make sure to use some well-tested combination of versions. Note that the page you mention contains:

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.

1 Like

To remove a switch, use opam switch remove. In your case, that would be opam remove switch 4.07.0. And just, to be clear, this is more or less equivalent to rm -rf ~/.opam/4.07.0/. So, caution is advised.

@Zimmi48

ok got it. Coq installation scripts. However, given that my machine is in a weird situation – was restored from a intel time machine but the hardware is the M1. How do I unistall and removing everything and essentially start from scratch? Then I assume the script you suggest are ok to do. Right?

btw, thanks for the help!

btw, @silene what do you think of the above? how do I start from scratch?

Installing Coq

  1. install brew: https://brew.sh/

  2. Follow the Coq Plataform scripts for installation: https://coq.inria.fr/opam-using.html or “Installation by compiling from Sources using opam” platform/README_macOS.md at main · coq/platform · GitHub.

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 platform/README_macOS.md at main · coq/platform · GitHub):

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
  1. Check it installed correctly:
coqc -v

If you want to start from scratch and use Opam, then rm -rf ~/.opam and follow the instructions at https://coq.inria.fr/opam-using.html

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

@MSoegtropIMC can you have a look at this? EDIT: actually, an issue was opened at issues installing coq from plataform script · Issue #219 · coq/platform · GitHub

@brando90 Some packages failed to install, but if I am not mistaken, that should still leave you with a usable Coq installation with most Platform packages.

seems this fixed it?

(base) brandomiranda~/Downloads/platform-2022.01.0 ❯ eval $(opam env)
(base) brandomiranda~/Downloads/platform-2022.01.0 ❯ coqc -v
The Coq Proof Assistant, version 8.16+alpha
compiled with OCaml 4.10.2

bizzare…now my terminal is broken?

(base) brandomiranda~ ❯ eval $(opam env)$
zsh: command not found: $

I think it’s just the trailing $ that shouldn’t be there.

I wanted to install 8.14.0 but I get this error:

(base) brandomiranda~/coq4brando/cs598 ❯ opam pin coqide 8.14.0
coqide is now pinned to version 8.14.0

The following actions will be performed:
  ∗ install cairo2               0.6.2   [required by lablgtk3]
  ∗ install lablgtk3             3.1.2   [required by lablgtk3-sourceview3]
  ∗ install lablgtk3-sourceview3 3.1.2   [required by coqide]
  ∗ install coqide               8.14.0*
===== ∗ 4 =====
Do you want to continue? [Y/n] y

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><>  🐫
⬇ retrieved cairo2.0.6.2  (cached)
Processing  4/12:
⬇ retrieved lablgtk3-sourceview3.3.1.2  (cached)
⬇ retrieved lablgtk3.3.1.2  (cached)
⬇ retrieved coqide.8.14.0  (cached)
[ERROR] The compilation of cairo2.0.6.2 failed at "dune build -p cairo2 -j 7".

#=== ERROR while compiling cairo2.0.6.2 =======================================#
# context     2.1.2 | macos/arm64 | ocaml-base-compiler.4.12.0 | https://opam.ocaml.org#f325e639
# path        ~/.opam/4.12.0/.opam-switch/build/cairo2.0.6.2
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p cairo2 -j 7
# exit-code   1
# env-file    ~/.opam/log/cairo2-32945-6a1ec2.env
# output-file ~/.opam/log/cairo2-32945-6a1ec2.out
### output ###
#   ocamlmklib src/dllcairo_stubs.so,src/libcairo_stubs.a (exit 2)
# (cd _build/default && /Users/brandomiranda/.opam/4.12.0/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
└─
╶─ No changes have been performed

<><> 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
# Run eval $(opam env) to update the current shell environment
[NOTE] Pinning command successful, but your installed packages may be out of sync.

does this mean it’s just not installable in mac m1?