Stream: coq-community devs & users

Topic: extracted code & IPC

Alexander Gryzlov (Feb 09 2023 at 15:08):

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?

Karl Palmskog (Feb 09 2023 at 15:17):

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 ; in ;(theories Stalmarck.Algorithm) in src/dune.

Then, dune build will build everything in the project.

Alexander Gryzlov (Feb 09 2023 at 15:24):

That still gives me
Error: No rule found for theories/Algorithm/algoRun.vo

Karl Palmskog (Feb 09 2023 at 15:30):

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 theories/Tactic/dune.

Karl Palmskog (Feb 09 2023 at 15:32):

but this breaks all opam files (we'd need Dune-Coq 1.0 for these things to work together)

Alexander Gryzlov (Feb 09 2023 at 15:34):

Ok, thanks, this seems to work. But is dune generally required nowadays to have these hybrid Coq+OCaml build pipelines?

Karl Palmskog (Feb 09 2023 at 15:35):

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

Karl Palmskog (Feb 09 2023 at 15:36):

in the case of Stalmarck, the classic coq_makefile way is even more complex, since the plugin (OCaml code) depends on extracted code

Alexander Gryzlov (Feb 09 2023 at 15:36):

I see. Do you have an example of a working coq_makefile pipeline for theories+standalone ocaml tool?

Karl Palmskog (Feb 09 2023 at 15:37):

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.

Alexander Gryzlov (Feb 09 2023 at 15:38):

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.

Alexander Gryzlov (Feb 09 2023 at 15:39):

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)

Karl Palmskog (Feb 09 2023 at 15:39):

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.

Alexander Gryzlov (Feb 09 2023 at 15:40):

Well the legal status is kind of a gray area here, no?

Karl Palmskog (Feb 09 2023 at 15:40):

I'm pretty sure all contribs got permission from their authors, the only way to submit a contrib was through a web form

Alexander Gryzlov (Feb 09 2023 at 15:41):

Dunno, the code seems to be old enough to predate any kind of procedure

Karl Palmskog (Feb 09 2023 at 15:41):

but if you mean there was some other author for the algorithm, well, algorithms in themselves are not subject to copyright.

Alexander Gryzlov (Feb 09 2023 at 15:41):

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.

Alexander Gryzlov (Feb 09 2023 at 15:41):

this is what readme says literally

Karl Palmskog (Feb 09 2023 at 15:42):

oh OK, in that case it's gray area, yes. There seems to be no license. That's unfortunate.

Karl Palmskog (Feb 09 2023 at 15:43):

one of the admins of coq-contribs, like me, could merge a PR I guess.

Karl Palmskog (Feb 09 2023 at 15:45):

here is a more fine-grained extraction project using coq_makefile: https://github.com/palmskog/fitch

Karl Palmskog (Feb 09 2023 at 15:57):

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.

Alexander Gryzlov (Feb 09 2023 at 16:07):

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