Packaging Coq built with Dune · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Packaging Coq built with Dune

Théo Zimmermann (Jul 04 2022 at 10:30):

Another issue that I stumbled upon is that if you forget to run make dunestrap and run dune build coq-core,coq-stdlib,coq followed by dune install..., then you do not get any build failure but the stdlib is not built / not installed. I'm betting other packagers are going to stumble on this. What about either:

reintroducing the dune files so that people using sufficiently recent version of Dune still get a stdlib even without running make dunestrap
adding a dummy dune file with a rule that always fails and that is overwritten by the make dunestrap process, so that people do not get the false success?

Gaëtan Gilbert (Jul 04 2022 at 10:38):

I guess the doc is in coq-stdlib so it's not empty

Théo Zimmermann (Jul 04 2022 at 10:43):

Well, the refman is supposed to be in its own package (coq-doc). I guess the stdlib doc is in coq-stdlib, but it needs to have built the stdlib first, no?

Gaëtan Gilbert (Jul 04 2022 at 10:46):

oh I was mistaken, I read (deps ... (package coq-stdlib)) as (deps ...) (package coq-stdlib)

Emilio Jesús Gallego Arias (Jul 04 2022 at 11:30):

Indeed I was hoping we could have gotten rid of that step by having Dune supporting just (include generated_file.sexp) in time for the PR, but it is still not working.

I'd be great if we could improve this, tho both solutions are annoying as is we put the file in git dunestrap will make the tree dirty. That's bad :S

Emilio Jesús Gallego Arias (Jul 04 2022 at 11:30):

I guess packagers should run the test suite at some point right? That should be enough

Emilio Jesús Gallego Arias (Jul 04 2022 at 11:31):

doc needs the glob files I think, but if they are missing that's not fatal

Emilio Jesús Gallego Arias (Jul 04 2022 at 11:54):

Now that I think about it a bit more, it is unfortunate @Théo Zimmermann that you can't handle the stdlib just as other packages, by adding it to COQPATH