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
```

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

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

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.

Definitively you need to do `opam pin add coq-core https://github.com/coq/coq`

until at least coq-core is released in opam

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

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
```

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

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

@Théo Zimmermann I am not sure.

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

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

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

in the makefile files that are just going to be removed

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

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

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

the rest would be needed for coq-stdlib

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

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

@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

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: Jun 18 2024 at 21:01 UTC