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