Draft: dune build scripts

This is part of iris#471 (closed).

Instructions are needed, but with dune 3.4 this already supports dune build, dune coq top.

The CI error in https://gitlab.mpi-sws.org/Blaisorblade/stdpp/-/jobs/199312 makes no sense to me. It seems a regression in the upstream package, but https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.14.1/opam hasn't changed!

I'll investigate :-|.

What does this line do?

It's required to include subfolders of theories — like in coq_makefile's defaults. I don't think it ever makes sense to omit it. For stdpp it'd technically work, but not for iris.

Docs at https://dune.readthedocs.io/en/stable/coq.html#include-subdirs-coq.

Ah, this is coq-specific. Is it possible to move this below coq.theory, together with flags? IMO it makes more sense to first say "this is a Coq theory" and then start having coq-specific configuration.

Unfortunately it also has meaning for OCaml, and AFAIK no. I'll recheck.

changed this line in version 2 of the diff

What do these two lines do, why are there 2 names?

name is the Coq logical prefix. package says this theory is part of the coq-stdpp opam package.

name is the Coq logical prefix.

Ah, that makes sense. Can you add that as comment in the file? It might seem silly but I think it'll help us non-dune people get over the initial hurdles. ;)

changed this line in version 2 of the diff

dune is not a coq build too, it's much more general than that, right?

That is at least less confusing. I am still not entirely sure what to do with this comment, other than "here are some runes we need for dune to work".^^

Most/all of this are runes . I should probably annotate the useful parts — I could recover the comments from https://github.com/ejgallego/coq-plugin-template/blob/v8.16/theories/dune.

Actually: the runes here are needed because dune's configuration is versioned. I picked the latest documented versions.

mentioned in merge request iris!820 (closed)

In the other file we have name for the logical prefix and package for the package... here we use name for the package?

From what I understand, the way we set up stdpp_unstable is a problem for dune

FWIW, I think dune prefers/demands disjoint logical paths

so the fact that stdpp.unstable is nested inside stdpp makes dune unhappy.

This is some annoying duplication of information. We should at least make sure via CI that it remains consistent with _CoqProject.

changed this line in version 2 of the diff

I think to make progress on this we should have a dune meeting where you (@Blaisorblade and @lepigre I guess?) explain to us what this is about and why we should have in the repo and what we should be aware of.

Basically what I am concerned about is having files in the repo that neither @robbertkrebbers nor me understand at all. I am also concerned that there is no CI that checks that these files make any sense, so things I do in the repo may break dune in ways I cannot predict. Remember that Dune files are basically opaque binary blobs to us, they are not very self-explaining to people that never have and do not plan to use dune themselves. We're fine with having other people maintain this but then (a) that needs to be clear and (b) I think we need CI to at least know when we have to poke you guys about the fact that something is breaking dune.

added 108 commits

• 5b487330...c59b6199 - 107 commits from branch iris:master
• 2e7fac38 - dune build scripts

Compare with previous version

added 16 commits

• 2e7fac38...d40a9005 - 15 commits from branch iris:master
• 0c04cb06 - dune build scripts

Compare with previous version

added S-waiting-for-author label

Closing for now.

We might want to follow-up on this and iris!820 (closed), but I'm not sure keeping this MR open for now helps.

closed