在新的Mac M1机器中找不到存储库时，如何安装新版本的Coq？
在新的Mac M1机器中找不到存储库时，如何安装新版本的Coq？
提问于 2022-02-14 20:20:02
我买了一台新机器(mac book m1，不确定这是否重要)，我注意到我没有Coq：
(base) brandomiranda~ ❯ coqc -v
zsh: command not found: coqc因此，我按照说明下载coq (https://coq.inria.fr/opam-using.html)。它的某些部分似乎起作用了：
(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.但是当我去找和钉coq opam时找不到它：
(base) brandomiranda~ ❯ opam pin add coq 8.15.0
[ERROR] Package coq has no known version 8.15.0 in the repositories有人知道怎么回事吗？似乎令人费解。
十字：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
现在解决这个问题：
(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此外：
(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.(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似乎有一个错误：
∗ 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"运行coq平台脚本时：
(base) brandomiranda~/Downloads/platform-2022.01.0 ❯ bash coq_platform_make.shStack Overflow用户
发布于 2022-02-15 07:27:56
如果您不是opam / OCaml专家，那么最好使用opam安装Coq是依赖Coq平台提供的脚本。请参阅：https://github.com/coq/platform/releases
这些交互脚本将负责：
创建一个新的opam switch
- installing --您需要的任何外部依赖项(例如，如果需要compiler
- installing )的适当版本的
- --
- ，他们还可以建议安装一个额外的Coq包集合，这些包对于Coq项目
非常有用。
最后，依赖此脚本创建了一个良好的基础，如果需要更多未包含在平台中的Coq包，则可以对其进行扩展。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/71117837
复制相关文章
相似问题
腾讯云开发者
