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