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?
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.
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 Release Notes. 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.
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
I guess I got confused because of this page Install Coq with opam | The Coq Proof Assistant 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.
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.
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?
install brew: https://brew.sh/
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
coqc -v
If you want to start from scratch and use Opam, then rm -rf ~/.opam and follow the instructions at Install Coq with opam | The Coq Proof Assistant
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?