I'm trying to package coq-menhirlib for Debian, but I'm a bit at loss what it consists of.
It builds many things that are already provided by menhir itself (a binary, menhirLib, menhirSdk)... the only coq-related things I have seen is coq-menhirlib/dune-package.
Can someone shed a light on this?
@Julien Puydt to my knowledge, coq-menhirlib
is a pure Coq library, but lives in the Menhir repository along with OCaml code. The workflow is that menhir
with certain options generates Coq .v
files, and those files use functions/lemmas in coq-menhirlib
, so that Coq library must be installed/available for the generated files to be accepted by Coq. Compare to the Ott tool and its pure-Coq coq-ott
library.
see: https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib
I don't understand - from the gitlab, it looks like coq-menhirlib is a subdirectory of the menhir one.
yes, so the menhir GitLab repo has several packages of both OCaml and Coq code. In this case of coq-menhirlib, it can be built from scratch without using any of the other code. The dependency between coq-menhirlib and code generated by menhir
then occurs at "runtime".
Oh, dear, I found out the Debian menhir package has that directory filtered out...
It's to avoid a kind of circular dep.
@Karl Palmskog That should definitely help me package the right thing! Thanks!
Julien Puydt has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC