Ali Caglayan said:
Emilio Jesús Gallego Arias said:
Ali Caglayan said:
We have still not split the package
what do you mean, the problem Pierre-Marie sees is actually due to plugins living in
coq-core
vs thestdlib
living incoq-stdlib
At least on opam, there are a myriad of bugs to be found when you install only coq-core.
Where are these bugs?
A myriad is certainly very concerning; I was positive the current split was finished and working
2 messages were moved here from #Coq devs & plugin devs > Dune strikes back by Ali Caglayan.
Many binaries for instance don't have -noinit
or -boot
which means they cannot be run without the presense of the stdlib.
coqdoc, coq_makefile
This is due to a common Env.init path
Many plugins included in coq-core don't work without the stdlib.
coqdoc can run with an alternative stdlib, it has the --stdlib
parameter
coq_makefile doesn't support that I think
what is the plugin that requires the stdlib? We solved that long time ago
that's IMHO far from a myriad
OK maybe not a myriad
more like a feature request for coq_makefile
but still progress needs to be done before we can fully call it a split
We also have like zero coverage on the split package to see what works
I don't see what more progress is needed
Lasse is using it just fine, as well as my own stdlib2 fork
it is true coqdoc and coqchk could take better options, but that's all AFAICT
as there is no plan that I know for coq_makefile to gain understanding of libraries, tho you can likely hack something
Native compilation does some searching for coqlib which is quite fragile
But thats more a different problem I guess
It does not search if you pass -nI which is a requirement, that should be better documented but we chose to keep the option internal for now
Better documentation for sure could be used on how to use coq-core alone
because indeed you want newer dune and (stdlib no)
In fact, the best witness that it works is that opam installs them separatedly
I agree that build systems need work to make this more usable, even Dune
but that's not an issue of the split itself
Should we commit to the full split in 8.17?
i.e. package opam as coq-core and some umbrella package with coq-stdlib
Here is a bug in coqc with no stdlib: https://github.com/coq/coq/issues/16295
And in general there are a few outstanding issues: https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+noinit
I'm not saying these are difficult to solve, but we should fix them.
8.17 has already commited to the full split
that's already done in coq.dev
All the bugs you point out are not related to the split I think
Last updated: Oct 13 2024 at 01:02 UTC