Open zoickx opened 3 years ago
An example of a failed invocation looks like this (no user input)
$ coq-config
<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.12.0"} | "ocaml-system" {= "4.12.0"}]
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
-> installed base-bigarray.base
-> installed base-threads.base
-> installed base-unix.base
-> installed ocaml-options-vanilla.1
-> retrieved ocaml-base-compiler.4.12.0 (https://opam.ocaml.org/cache)
-> installed ocaml-base-compiler.4.12.0
-> installed ocaml-config.2
-> installed ocaml.4.12.0
Done.
# Run eval $(opam env --switch=asn1-vst28) to update the current shell environment
[coq-released] Initialised
coq-vst-32 is now pinned to version 2.8
Package coq-struct-tact does not exist, create as a NEW package? [Y/n] y
[coq-struct-tact.~dev] synchronised (git+https://github.com/uwplse/StructTact.git)
coq-struct-tact is now pinned to git+https://github.com/uwplse/StructTact.git (version dev)
<><> Synchronising pinned packages ><><><><><><><><><><><><><><><><><><><><><><>
[coq-struct-tact.dev] synchronised (no changes)
The following actions will be performed:
- install ocamlfind 1.9.1 [required by coq]
- install conf-g++ 1.0 [required by coq-flocq]
- install conf-gmp 3 [required by zarith]
- install conf-findutils 1 [required by coq]
- install dune 2.9.0 [required by coq-struct-tact]
- install num 1.4 [required by coq]
- install zarith 1.12 [required by coq]
- install menhirSdk 20210419 [required by menhir]
- install menhirLib 20210419 [required by menhir]
- install coq 8.13.2 [required by coq-struct-tact, coq-ext-lib, coq-vst-32]
- install menhir 20210419 [required by coq-compcert-32]
- install coq-struct-tact dev*
- install coq-menhirlib 20210419 [required by coq-compcert-32]
- install coq-flocq 3.4.2 [required by coq-vst-32]
- install coq-ext-lib 0.11.3
- install coq-compcert-32 3.9 [required by coq-vst-32]
- install coq-vst-32 2.8*
===== 17 to install =====
The following system packages will first need to be installed:
libgmp-dev
<><> Handling external dependencies <><><><><><><><><><><><><><><><><><><><><><>
Let opam run your package manager to install the required system packages?
(answer 'n' for other options) [Y/n] n
This command should get the requirements installed:
apt-get install libgmp-dev
[NOTE] Use 'opam option depext-run-installs=false' if you don't want to be prompted again.
You can retry with '--assume-depexts' to skip this check, or run 'opam option depext=false' to permanently disable handling of system packages altogether.
Error installing pakages
Some opam packages have system non-OCaml dependencies, managed by the system's package manager. As of now,
coq-config
will fail to install such dependencies, despite them being supported by default withopam depext
since 2.1.0. See more in opam FAQ, GitHub repo.