Stream: Coq users

Topic: metacoq install issue: coq-equations not found


view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 09 2023 at 23:24):

@Mario Carneiro , you are missing the Coq opam repos

view this post on Zulip Emilio Jesús Gallego Arias (Dec 09 2023 at 23:24):

https://github.com/coq/opam

view this post on Zulip Mario Carneiro (Dec 09 2023 at 23:25):

tell me more?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 09 2023 at 23:26):

Does that help?

view this post on Zulip Mario Carneiro (Dec 09 2023 at 23:26):

seems to be doing more this time...

view this post on Zulip Mario Carneiro (Dec 09 2023 at 23:27):

I think it's working

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Dec 09 2023 at 23:28):

in the documentation, it is very distributed

view this post on Zulip 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

view this post on Zulip 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: Jun 23 2024 at 04:03 UTC