coq-htt as package depending on coq-htt-core

[palmskog]

For the recent release shared at coq/opam#3169 coq-htt and coq-htt-core are independent but mutually exclusive packages. This means that anyone using the core files of htt via opam needs to write that they depend on ("coq-htt" | "coq-htt-core") and test with both packages, which is complication compared to before.

A better solution in my view would be if coq-htt actually depended on coq-htt-core. Then both these packages could be installable at the same time and handle disjoint sets of files (no conflicts). Would a pull request to this effect be welcome @aleksnanevski?

[aleksnanevski]

That's a good point too. Yes, let's do it. Do you already have the pull request?

[aleksnanevski]

Actually wait. Now I'm not sure how the github repo should look like? Should there suddenly be two different repos, one for coq-htt-core, and a separate one for coq-htt? Hmm. The core part is just 2 files, it seems an overkill to have a separate repo just for them.

[palmskog]

@aleksnanevski the only difference is how dune and <package>.opam are defined, there is no difference in general repository organization. You can see here how it was done for a similar project with "core" vs. "examples":

• https://github.com/coq-community/graph-theory/blob/master/coq-graph-theory.opam
• https://github.com/coq-community/graph-theory/blob/master/coq-graph-theory-planar.opam
• https://github.com/coq-community/graph-theory/blob/master/theories/core/dune
• https://github.com/coq-community/graph-theory/blob/master/theories/planar/dune

It seems there is green light to put the pull request together, it will take up to an hour in the worst case (CI fiddling), so that's why I ask before.

[aleksnanevski]

Hmm, ok, let me give it a try. I have a feeling it will take me much longer than 1 hour, as our yaml files aren't configured for this (meta.yml in the main repo, as well as the files in templates-extra). But maybe you have a suggestion how to do this better.

[palmskog]

Unfortunately, the templates currently don't support the build approach used in the graph-theory project, so I decided manually define <package>.opam and dune (and CI through docker-action.yml). One can still use the templates to generate other files. Maybe it's best to do the same here.

You probably want to have (name htt) in both dune files, since all files should be installed into the coq-contribs/htt location. And you may want to keep the _CoqProject and Makefile in the root (but not use them at all in opam packages).

[aleksnanevski]

I'm not succeeding with doing this on my own (too green with dune). If you have a quick way to generate what's needed in a pull request, that would teach me a lot.

[palmskog]

Closed by #29