Stream: Coq users

Topic: Installing development Coq with OPAM

Alexander Gryzlov (Mar 08 2021 at 16:10):

Is there some additional OPAM repository I need to add for the installation to work? Currently I'm getting

The following dependencies couldn't be met:
  - coq → coq-core
      unknown package

Pierre-Marie Pédrot (Mar 08 2021 at 16:12):

Looks like a fallout of https://github.com/coq/coq/pull/12567

Pierre-Marie Pédrot (Mar 08 2021 at 16:14):

ping @Gaëtan Gilbert who might have fixed the bench issue in the meantime

Emilio Jesús Gallego Arias (Mar 08 2021 at 16:23):

Likely some option to pin is missing, or you may need to do pin coq-core too with the right --kind argument; I never understood the mess that is opam pin in terms of what is being used and how.

Emilio Jesús Gallego Arias (Mar 08 2021 at 16:37):

Definitively you need to do opam pin add coq-core https://github.com/coq/coq until at least coq-core is released in opam

Alexander Gryzlov (Mar 08 2021 at 17:51):

Hmm, I guess I'll just temporarily roll back to 8.13.1 until coq-core is released, but thanks

Alexander Gryzlov (Mar 08 2021 at 18:23):

Ok, doing the following did actually help in installing the dev version, maybe this would be useful to someone else:

opam pin add --no-action coq-core https://github.com/coq/coq.git --yes
opam pin add --no-action coq-stdlib https://github.com/coq/coq.git --yes

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:27):

Indeed, that seems like the right thing to do , we should update the instructions

Théo Zimmermann (Mar 08 2021 at 18:48):

But if you install from the core-dev repo instead of pinning from the git repository, you don't need any of this, right?

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:49):

@Théo Zimmermann I am not sure.

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:50):

I hope that for 8.14 tho we can finally have a single set of opam files

Guillaume Melquiond (Mar 08 2021 at 18:50):

In theory yes. Except that no one ever submitted the packages, so no.

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:50):

I was planning to submit the packages once I get coq-core build exclusively with dune, otherwise there are some issues that would require a lot of work

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:50):

in the makefile files that are just going to be removed

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:51):

if I am not wrong, once the dune pr is done, we would need to refactor loadpath to coq-core.boot , then finish the coqnative pr

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:52):

then at that point the auto-generated opam files can be used without any problem

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:53):

I mean after https://github.com/coq/coq/pull/13617 , we can already use the auto-generated file for coq-core

Emilio Jesús Gallego Arias (Mar 08 2021 at 18:53):

the rest would be needed for coq-stdlib

Théo Zimmermann (Mar 08 2021 at 18:56):

Guillaume Melquiond said:

In theory yes. Except that no one ever submitted the packages, so no.

I was talking about this: https://github.com/coq/opam-coq-archive/blob/master/core-dev/packages/coq/coq.dev/opam

Guillaume Melquiond (Mar 08 2021 at 19:05):

Yes, but I was under the impression that this file was no longer correct since the stdlib split.

Emilio Jesús Gallego Arias (Mar 08 2021 at 19:10):

@Guillaume Melquiond that file should still work, the problem is that opam pin chooses a the file in the repos but can't see the new coq-core.opam file unless explictly told so

Guillaume Melquiond (Mar 09 2021 at 07:30):

But that is only because the files are missing from the Opam repository, right? Otherwise, you would just need to add the following to coq.opam in Coq's repository and pinning would work out of the box:

pin-depends: [
  [ "coq-core" "." ]
  [ "coq-stdlib" "." ]
]

Last updated: Oct 05 2023 at 02:01 UTC