Stream: Coq devs & plugin devs

Topic: Bugs with lonely coq-core


view this post on Zulip 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-core vs the stdlib living in coq-stdlib

At least on opam, there are a myriad of bugs to be found when you install only coq-core.

Where are these bugs?

view this post on Zulip 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

view this post on Zulip Notification Bot (Oct 19 2022 at 21:28):

2 messages were moved here from #Coq devs & plugin devs > Dune strikes back by Ali Caglayan.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:29):

coqdoc, coq_makefile

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:30):

This is due to a common Env.init path

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:31):

Many plugins included in coq-core don't work without the stdlib.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:31):

coqdoc can run with an alternative stdlib, it has the --stdlib parameter

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:32):

coq_makefile doesn't support that I think

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:32):

that's IMHO far from a myriad

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:32):

OK maybe not a myriad

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:33):

more like a feature request for coq_makefile

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:33):

but still progress needs to be done before we can fully call it a split

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:33):

We also have like zero coverage on the split package to see what works

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:33):

I don't see what more progress is needed

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:34):

Lasse is using it just fine, as well as my own stdlib2 fork

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:35):

Native compilation does some searching for coqlib which is quite fragile

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:35):

But thats more a different problem I guess

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:37):

because indeed you want newer dune and (stdlib no)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:38):

but that's not an issue of the split itself

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:38):

Should we commit to the full split in 8.17?

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:39):

i.e. package opam as coq-core and some umbrella package with coq-stdlib

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:40):

Here is a bug in coqc with no stdlib: https://github.com/coq/coq/issues/16295

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Oct 19 2022 at 21:40):

I'm not saying these are difficult to solve, but we should fix them.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:41):

8.17 has already commited to the full split

view this post on Zulip Emilio Jesús Gallego Arias (Oct 19 2022 at 21:41):

that's already done in coq.dev

view this post on Zulip 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: Feb 01 2023 at 16:03 UTC