Port to use Dune as build system

[palmskog]

Using the regular coq_makefile for coq-dpdgraph is a lot of work for an essentially deprecated approach to building Coq plugins. Here is a quick port to Dune instead. The plugin and tools build fine, but two issues are not resolved yet:

1. The documentation needs to be updated to reflect that autoconf is no longer needed and give the key Dune commands.
2. The test suite needs to be ported to Dune.

The first issue is straightforward, but the second one is time-consuming without in-depth Dune knowledge that I currently lack.

@ybertot perhaps we could merge this after the documentation is done and postpone the test suite port to some later point? We may be able to get some help from the Dune experts.

[Alizter]

Since the test-suite has been ported, what is left keeping this back?

[palmskog]

@Alizter the final refactorings that I have pending locally before I mark this to be ready are:

• have the test .v files explicitly rather than as defined inside cram .t files
• split into src and theories directory

[Alizter]

@palmskog I can split those .v files.

[palmskog]

I have already done the splitting locally, but I ran into the Dune issues discussed on Zulip. I'll take care of the final changes, and you can review when I mark as ready for review.

[palmskog]

@Alizter this PR is now ready for re-review. The only other changes I might do at this point (other those than suggested during review) are to documentation, which still talks about autoconf and similar.

[Alizter]

We still have the

File "_unknown_", line 1, characters 0-0:
*** Error: in file dpdgraph.v, could not find META.coq-dpdgraph.

issue. I am unsure if there is a work around other than doing dune build twice. I'll see what I can do.

[palmskog]

@Alizter I can't replicate that locally (I don't get the error anymore). Shouldn't that error show up in CI then? I don't see it here: https://github.com/coq-community/coq-dpdgraph/runs/6453619501?check_suite_focus=true#step:4:390

[Alizter]

@palmskog Seems my cache got corrupted from before, I disabled cache now and it is working fine.

Actually no. Let me see.

---

Seems to be an issue with coqdep. I suspect its because we are relying on the META file of the coq-dpdgraph package whilst generating rules that will be installed in the coq-dpdgraph package.

[Alizter]

OK I had a discussion with Rudi about this. I think barring Coq's poor design choice to have circular deps on META, the best solution here to avoid this problem is to have two separate packages. One for the plugin and one for the theory. We can later package them up further into coq-dpdgraph at the end for opam.

[palmskog]

@Alizter I don't think this is a workable solution. The "theory" here consists of exactly one line of code:

Declare ML Module "coq-dpdgraph.plugin".

coq-dpdgraph is currently a single package using autoconf + a regular Makefile that is part of the Coq Platform. To avoid the large overhead of maintaining two packages, I think we should then instead keep this PR open until the Dune issues with coqdep are sorted.

[Alizter]

Never mind, I hadn't checked out the PR properly and was stuck on an older version where the ml and v fiels where mixed. That was causing the coq.theory stanza to break. Now that everything is in the proper folder it looks like it is working as intended.

[palmskog]

@ybertot Ali and I believe this is ready to be merged now, but we would appreciate if you could take a look at the changes, in particular in the test suite. The key command you may want to run locally is:

dune runtest

One important thing to note is that if we merge this, we must update the build scripts in Coq's CI - the old build process scripted there will not work anymore.

[ybertot]

I have to run to a few things these days, I may not have time to look at it before the end of the week. I will try to keep it on my agenda.

[palmskog]

@ybertot do you think we can rebase+merge this PR and switch to Dune for a release of dpdgraph for Coq 8.17 now that 8.17+rc1 is out? If you don't mind, I could do it.

[Alizter]

@palmskog Are we really ready to switch to Dune for this? I thought we were going to do less changes to the tests then we currently do. Also what is the rush for 8.17?

[palmskog]

There is no big rush, but if we can throw out the dependency on autoconf/autotools for good for the next Coq Platform release (in March 2023 I guess), that would be good for everyone involved. Since I believe we faithfully capture all existing tests, there is nothing in my view that stand in the way.

[ybertot]

Moving from autoconf to dune means moving from a system I don't understand fully to a system I barely understand. Right now, I have administrative duties that make that I cannot guarantee reading the documentation of Dune before end of January, but it is good of you to have sent me a reminder.

If there is no hurry, I suggest we pospone my answer another 2 or 3 weeks, to see if I can gather enough information by then.

[palmskog]

Fine by me to postpone further PR discussion until February.

[Alizter]

@ybertot I have added more details to the README.md and a basic Makefile with things like:

make
make build (same as above)
make test (runs tests)
make promote (promotes differing output tests)
make install (installs)

The CI also now runs the test-suite.

[palmskog]

@ybertot @Alizter do we have any consensus here on a plan for merging the PR? The advantage with a Dune-based build is that many people in Coq-community could potentially do releases of coq-dpdgraph when required - there is no local preparation of a release archive needed, just a Git tag and package definition.

[Alizter]

@palmskog last I spoke to @ybertot he wanted to have a look at the readme in some more detail. So we are waiting for him.

[ybertot]

Thanks for the reminder.

[SkySkimmer]

Using the regular coq_makefile for coq-dpdgraph is a lot of work for an essentially deprecated approach to building Coq plugins.

coq_makefile is not deprecated.