> \# 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
> \`\`\`
>
>
> cross:
> \-https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/15
> \-https://stackoverflow.com/questions/71117837/how-does-one-install-a-new-version-of-coq-when-it-cannot-find-the-repositories-i
---
### Author:  [@lthery](https://discourse.rocq-prover.org/u/lthery)
#### Post date: [February 15, 2022, 1:09am UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/2 "2022-02-15T01:09:48Z")
what does `opam info coq` tells you?
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 15, 2022, 2:33am UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/3 "2022-02-15T02:33:14Z")
```auto
(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:
```auto
(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
```
---
### Author:  [@silene](https://discourse.rocq-prover.org/u/silene)
#### Post date: [February 15, 2022, 6:46am UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/4 "2022-02-15T06:46:54Z")
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.
---
### Author:  [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)
#### Post date: [February 15, 2022, 7:34am UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/5 "2022-02-15T07:34:36Z")
> [@silene](#):
>
> while the minimal version of OCaml supported on Apple M1 is 4.12
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](https://ocaml.org/releases/4.10.2.html). This is the version currently used in the Coq Platform ([Release 2022.01.0 · coq/platform · GitHub](https://github.com/coq/platform/releases/tag/2022.01.0)) and it has been tested to work by M1 users.
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 15, 2022, 2:21pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/6 "2022-02-15T14:21:08Z")
this probably happened due to a restoring from a time machine
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 15, 2022, 6:41pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/7 "2022-02-15T18:41:07Z")
> [@silene](#):
>
> 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.
issue:
```auto
(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
```auto
(base) brandomiranda~ ❯ opam upgrade --update-invariant
```
* * *
Ok now the error is:
```auto
(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
```
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 15, 2022, 6:49pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/8 "2022-02-15T18:49:01Z")
> [@silene](#):
>
> I think your only solution is to delete your Opam switch and start again from scratch.
@silene how do I do that? I thought I had already tried that with
```auto
opam remove ocaml-base-compiler
```
* * *
This is my current state:
```auto
- 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
```
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 15, 2022, 7:06pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/9 "2022-02-15T19:06:27Z")
> [@Zimmi48](#):
>
> 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](https://ocaml.org/releases/4.10.2.html). This is the version currently used in the Coq Platform ([Release 2022.01.0 · coq/platform · GitHub](https://github.com/coq/platform/releases/tag/2022.01.0)) and it has been tested to work by M1 users.
@Zimmi48
I guess I got confused because of this page [Install Coq with opam | The Coq Proof Assistant](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).
---
### Author:  [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)
#### Post date: [February 15, 2022, 8:55pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/10 "2022-02-15T20:55:39Z")
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](https://github.com/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](https://github.com/coq/platform).
---
### Author:  [@silene](https://discourse.rocq-prover.org/u/silene)
#### Post date: [February 16, 2022, 8:13am UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/11 "2022-02-16T08:13:39Z")
> [@brando90](#):
>
> how do I do that?
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.
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 16, 2022, 4:47pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/12 "2022-02-16T16:47:45Z")
@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?
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 16, 2022, 4:58pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/13 "2022-02-16T16:58:00Z")
## Installing Coq
1. install brew: [https://brew.sh/](https://brew.sh/)
2. Follow the Coq Plataform scripts for installation: [Installing the Rocq Prover and its packages · Rocq Documentation](https://coq.inria.fr/opam-using.html) or “Installation by compiling from Sources using opam” [platform/doc/README\_macOS.md at main · rocq-prover/platform · GitHub](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 [platform/doc/README\_macOS.md at main · rocq-prover/platform · GitHub](https://github.com/coq/platform/blob/main/doc/README_macOS.md)):
```auto
https://github.com/coq/platform/archive/refs/tags/2022.01.0.zip
```
and ran after cding to the unzipped files location of the above:
```auto
bash coq_platform_make.sh
```
1. Check it installed correctly:
```auto
coqc -v
```
---
### Author:  [@silene](https://discourse.rocq-prover.org/u/silene)
#### Post date: [February 16, 2022, 5:02pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/14 "2022-02-16T17:02:06Z")
> [@brando90](#):
>
> how do I start from scratch?
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](https://coq.inria.fr/opam-using.html)
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 16, 2022, 5:42pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/15 "2022-02-16T17:42:30Z")
seems there was an error:
```auto
∗ 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
# 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:
```auto
(base) brandomiranda~/Downloads/platform-2022.01.0 ❯ bash coq_platform_make.sh
```
---
### Author:  [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)
#### Post date: [February 16, 2022, 5:48pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/16 "2022-02-16T17:48:51Z")
@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](https://github.com/coq/platform/issues/219)
@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.
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 17, 2022, 4:27pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/17 "2022-02-17T16:27:18Z")
seems this fixed it?
```auto
(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
```
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 17, 2022, 4:56pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/18 "2022-02-17T16:56:34Z")
bizzare…now my terminal is broken?
```auto
(base) brandomiranda~ ❯ eval $(opam env)$
zsh: command not found: $
```
---
### Author:  [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)
#### Post date: [February 17, 2022, 5:05pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/19 "2022-02-17T17:05:04Z")
I think it’s just the trailing `$` that shouldn’t be there.
---
### Author:  [@brando90](https://discourse.rocq-prover.org/u/brando90)
#### Post date: [February 17, 2022, 6:37pm UTC](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562/20 "2022-02-17T18:37:49Z")
I wanted to install 8.14.0 but I get this error:
```auto
(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?
[Next page](https://discourse.rocq-prover.org/t/how-to-install-coq-when-it-says-the-repository-cannot-be-found-e-g-issues-with-m1-chip-mac-apple/1562.md?page=2)