Stream: Coq devs & plugin devs

Topic: ✔ coq-menhirlib


view this post on Zulip Julien Puydt (Jul 08 2022 at 10:55):

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?

view this post on Zulip Karl Palmskog (Jul 08 2022 at 11:33):

@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.

view this post on Zulip Karl Palmskog (Jul 08 2022 at 11:34):

see: https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib

view this post on Zulip Julien Puydt (Jul 08 2022 at 13:32):

I don't understand - from the gitlab, it looks like coq-menhirlib is a subdirectory of the menhir one.

view this post on Zulip Karl Palmskog (Jul 08 2022 at 13:35):

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".

view this post on Zulip Julien Puydt (Jul 08 2022 at 13:37):

Oh, dear, I found out the Debian menhir package has that directory filtered out...

view this post on Zulip Julien Puydt (Jul 08 2022 at 13:39):

It's to avoid a kind of circular dep.

view this post on Zulip Julien Puydt (Jul 08 2022 at 13:51):

@Karl Palmskog That should definitely help me package the right thing! Thanks!

view this post on Zulip Notification Bot (Jul 08 2022 at 13:51):

Julien Puydt has marked this topic as resolved.


Last updated: May 28 2023 at 13:30 UTC