I'm trying to update https://github.com/coq-contribs/ipc to Coq 8.16 as a part of a hobby project to understand proof search algorithms better and I struggle to understand how building extracted code should be done properly nowadays. The most maintained example I could find of this class is https://github.com/coq-community/stalmarck/ but the make file there (as described in the readme) only builds the Coq theories and
dune build fails for me. Is there something I'm missing?
I had to change
stalmarck to make it both work in Coq's CI and using the opam packages. Right now, you can't have both a complete compositional local Dune build and two working opam packages at the same time.
To get the compositional local Dune build, you need to add
theories/dune with this content:
(coq.theory (name Stalmarck.Algorithm) (package coq-stalmarck) (synopsis "Verified implementation of Stålmarck's algorithm for proving tautologies in Coq"))
and also remove the
;(theories Stalmarck.Algorithm) in
dune build will build everything in the project.
That still gives me
Error: No rule found for theories/Algorithm/algoRun.vo
OK, it's a bit more complicated. The
dune file from above needs to be moved to
theories/Algorithm/, and the
; must be uncommented also in
but this breaks all opam files (we'd need Dune-Coq 1.0 for these things to work together)
Ok, thanks, this seems to work. But is dune generally required nowadays to have these hybrid Coq+OCaml build pipelines?
it's not required, but it's to me the only maintainable way to properly handle dependencies and incremental builds across both Coq and OCaml
in the case of Stalmarck, the classic coq_makefile way is even more complex, since the plugin (OCaml code) depends on extracted code
I see. Do you have an example of a working coq_makefile pipeline for theories+standalone ocaml tool?
Disel is one: https://github.com/DistributedComponents/disel
I can't easily Dunerize it because the extraction spits out a ton of different OCaml source files.
Thanks! Guess I'll try to make something like this and contribute back to IPC, dune seems a bit of an overkill for a "legacy" project like this.
I'm not even sure what's the legal status of this code, judging by the readme, they never got a permission out of the original author (Klaus Weich)
unfortunately, IPC is not maintained. Maybe you would consider proposing it to be moved to Coq-community and maintain it there? You can step down anytime.
Well the legal status is kind of a gray area here, no?
I'm pretty sure all contribs got permission from their authors, the only way to submit a contrib was through a web form
Dunno, the code seems to be old enough to predate any kind of procedure
but if you mean there was some other author for the algorithm, well, algorithms in themselves are not subject to copyright.
So I (Pierre Letouzey) take the liberty to place it into Coq User's Contributions, in order for it not to be definitively lost. IF YOU HAPPEN TO CONTACT KLAUS WEICH, PLEASE ASK HIM WHETHER THIS IS OK WITH HIM, OTHERWISE TELL HIM TO EMAIL ME.
this is what readme says literally
oh OK, in that case it's gray area, yes. There seems to be no license. That's unfortunate.
one of the admins of coq-contribs, like me, could merge a PR I guess.
here is a more fine-grained extraction project using coq_makefile: https://github.com/palmskog/fitch
valid concern by Pierre though, the code would very likely be lost without the contrib, in fact I suspect that a lot of current Coq artifacts that don't end up on GitHub/Lab or Zenodo are getting lost.
Sure, it's just that they get stuck in some kind of limbo where it's unclear how is one allowed to use them.
Last updated: Jun 03 2023 at 18:01 UTC