Stream: Coq devs & plugin devs

Topic: Packaging Coq built with Dune


view this post on Zulip Théo Zimmermann (Jul 04 2022 at 10:30):

Another issue that I stumbled upon is that if you forget to run make dunestrap and run dune build coq-core,coq-stdlib,coq followed by dune install..., then you do not get any build failure but the stdlib is not built / not installed. I'm betting other packagers are going to stumble on this. What about either:

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 10:38):

I guess the doc is in coq-stdlib so it's not empty

view this post on Zulip Théo Zimmermann (Jul 04 2022 at 10:43):

Well, the refman is supposed to be in its own package (coq-doc). I guess the stdlib doc is in coq-stdlib, but it needs to have built the stdlib first, no?

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 10:46):

oh I was mistaken, I read (deps ... (package coq-stdlib)) as (deps ...) (package coq-stdlib)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:30):

Indeed I was hoping we could have gotten rid of that step by having Dune supporting just (include generated_file.sexp) in time for the PR, but it is still not working.

I'd be great if we could improve this, tho both solutions are annoying as is we put the file in git dunestrap will make the tree dirty. That's bad :S

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:30):

I guess packagers should run the test suite at some point right? That should be enough

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:31):

doc needs the glob files I think, but if they are missing that's not fatal

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:54):

Now that I think about it a bit more, it is unfortunate @Théo Zimmermann that you can't handle the stdlib just as other packages, by adding it to COQPATH

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:54):

we should really move forward with https://github.com/coq/coq/issues/16091

view this post on Zulip Théo Zimmermann (Jul 04 2022 at 11:55):

Yes, this would also solve the issue I was raising in the other thread (#Coq devs & plugin devs > Running coqtop without stdlib).

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:55):

For now indeed you want to set COQLIB I guess

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:55):

that's the Nixy way

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:55):

it seems to me

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:56):

In the other thread there is a real bug, we actually noticed just a few days ago when we ported the test suite

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2022 at 11:56):

how do other packages in Nix extend the search path, for example python?

view this post on Zulip Théo Zimmermann (Jul 04 2022 at 13:30):

For OCaml, there is OCAMLPATH for instance.

view this post on Zulip Théo Zimmermann (Jul 04 2022 at 13:30):

For Python, I'm not sure.

view this post on Zulip Théo Zimmermann (Jul 04 2022 at 13:30):

But probably based on something similar.

view this post on Zulip Guillaume Melquiond (Jul 04 2022 at 13:34):

PYTHONHOME and PYTHONPATH. I believe Nix is using the latter.


Last updated: Nov 29 2023 at 19:01 UTC