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:
dune
files so that people using sufficiently recent version of Dune still get a stdlib even without running make dunestrap
dune
file with a rule that always fails and that is overwritten by the make dunestrap
process, so that people do not get the false success?I guess the doc is in coq-stdlib so it's not empty
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?
oh I was mistaken, I read (deps ... (package coq-stdlib))
as (deps ...) (package coq-stdlib)
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
I guess packagers should run the test suite at some point right? That should be enough
doc needs the glob files I think, but if they are missing that's not fatal
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
we should really move forward with https://github.com/coq/coq/issues/16091
Yes, this would also solve the issue I was raising in the other thread (#Coq devs & plugin devs > Running coqtop without stdlib).
For now indeed you want to set COQLIB I guess
that's the Nixy way
it seems to me
In the other thread there is a real bug, we actually noticed just a few days ago when we ported the test suite
how do other packages in Nix extend the search path, for example python?
For OCaml, there is OCAMLPATH for instance.
For Python, I'm not sure.
But probably based on something similar.
PYTHONHOME
and PYTHONPATH
. I believe Nix is using the latter.
Last updated: May 28 2023 at 16:30 UTC