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
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: Dec 01 2023 at 06:01 UTC