Mario Carneiro (Dec 09 2023 at 23:22): Mario Carneiro (Dec 09 2023 at 23:22):I'm trying to build metacoq following the installation instructions. I don't use opam very often and somehow things never seem to go as planned. The steps that follow come after rm -rf ~/.opam and sudo apt remove opam to remove any previous configuration and (hopefully) revert to a fresh build:
$ sudo apt install opam
[...]
Setting up opam (2.1.2-1) ...
$ opam init
No configuration file found, using built-in defaults.
Checking for available remotes: rsync and local, git, mercurial, darcs. Perfect!
[...]
<><> Creating initial switch 'default' (invariant ["ocaml" {>= "4.05.0"}] - initially with ocaml-system)
<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml" {>= "4.05.0"}]
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-system.4.13.1
∗ installed ocaml-config.2
∗ installed ocaml.4.13.1
Done.
# Run eval (opam env --switch=default) to update the current shell environment
$ opam switch create coq.8.16 --packages=ocaml-variant
s.4.13.1+options,ocaml-option-flambda
<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-variants" {= "4.13.1+options"} "ocaml-option-flambda"]
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
∗ installed base-bigarray.base
∗ installed base-threads.base
∗ installed base-unix.base
∗ installed ocaml-option-flambda.1
⬇ retrieved ocaml-variants.4.13.1+options (https://opam.ocaml.org/cache)
∗ installed ocaml-variants.4.13.1+options
∗ installed ocaml-config.2
∗ installed ocaml.4.13.1
Done.
$ eval (opam env)
$ coqc -v
The Coq Proof Assistant, version 8.15.0
compiled with OCaml 4.13.1
$ opam install . --deps-only
[ERROR] Package conflict!
* Missing dependency:
- coq-equations
unknown package
No solution found, exiting
$ opam install coq-equations
[ERROR] No package named coq-equations found.
@Mario Carneiro , you are missing the Coq opam repos
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:24): Mario Carneiro (Dec 09 2023 at 23:25):tell me more?
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:25):For your current setup, just run opam repo add coq-released https://coq.inria.fr/opam/released
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:25):then you can install the coq-equations package, and a few other 100s of coq-* packages that live in this repos
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:26):Does that help?
Mario Carneiro (Dec 09 2023 at 23:26):seems to be doing more this time...
Mario Carneiro (Dec 09 2023 at 23:27):I think it's working
Mario Carneiro (Dec 09 2023 at 23:28):Is this something that should have been mentioned on the readme, or something that is mentioned on a centralized readme for installing opam+coq?
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:28):If my memory serves me correctly, this is mentioned in the main Coq install page, however I wouldn't be surprised to find many inconsistencies
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:28):in the documentation, it is very distributed
Emilio Jesús Gallego Arias (Dec 09 2023 at 23:29):Yeah it is mentioned here but IMHO it could be a bit more visible
Mario Carneiro (Dec 09 2023 at 23:29):(My first attempt failed for a different reason, but it's a lot harder to explain that one what with all the configuration that could potentially have come over from a previous install of an older coq switch)
Last updated: Oct 13 2024 at 01:02 UTC