Rocq-released repository with dune package management

Learning
1

I have Rocq projects that are managed by opam+dune. The standard flow is to:

  1. Add the Rocq opam repository: opam repo add rocq-released https://rocq-prover.org/opam/released
  2. Run opam install .

This works great. But I would like to experiment with migrating to Package Management With Dune. I find it appealing that it would allow me to define my pins and repositories in a config file. Naturally, I have created the following dune-workspace file:

(lang dune 3.23)
(pkg enabled)

(lock_dir
 (repositories rocq-released :standard))

(repository
 (name rocq-released)
 (url "https://rocq-prover.org/opam/released"))

However, building fails at repo retrieval:

File "dune-workspace", line 9, characters 6-45:
9 |  (url "https://rocq-prover.org/opam/released"))
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Could not determine location of repository
https://rocq-prover.org/opam/released
Hint: Specify either a file path or git repo via SSH/HTTPS

The actual rocq repository is stored here: opam/released at master · rocq-prover/opam · GitHub . Unfortunately, it is stored in a subdirectory. And to my knowledge, specifying git subdirectories is not possible in dune.

What is the correct way to specify the rocq-released opam repository?

2

You’re right, it’s currently not possible as Dune assumes that packages are in the packages subfolder of a repository. dune is somewhat more strict when it comes to the allowed layouts of an opam-repository compared to opam.

The way I see it there’s two options:

  1. Fork the repo, move it to the top-level and publish it. It’s hacky but allows you to go ahead today and give it a spin to see what works and what doesn’t.
  2. Submit support for subdirectories in dune. We had a PR allowing pretty much arbitrary opam repo layouts but it was quite inefficient and made it slow for most. However I would assume that just extending dune to always prepend a prefix to a every repo path while retaining all the other assumptions should be fairly simple.
3

Thank you for your reply. Yes, for now I will experiment locally.

Do you know, however, why the shim URL works for opam but not for dune? In that case it is a https url and not a git one: https://rocq-prover.org/opam/released

5

The way OPAM works is that on HTTP sources it will take the URL and download an index.tar.gz thus https://rocq-prover.org/opam/released/index.tar.gz which is a tarball of the repo. OPAM then unpacks this and uses it as a repository.

Dune does not do this, as Dune tries to always keep the repo up to date, thus it prioritizes downloading just the changes (essentially git pull) when it needs an OPAM repo. In OPAM updating the OPAM repos is a separate action (opam update), in Dune it’s always implied.

(Revised my original post which was a lot of nonsense so I deleted the stuff)