Stream: Coq devs & plugin devs

Topic: Future-proof Require from Stdlib


view this post on Zulip Karl Palmskog (Aug 10 2024 at 11:52):

For years, I've been using From Coq Require X. when requiring things from Stdlib. But apparently, it will cease to work in the near future due to PR 19310. Is the only future-proof way now to do Require X. without any prefix?

view this post on Zulip Gaëtan Gilbert (Aug 10 2024 at 12:21):

the future proof way is From Stdlib

view this post on Zulip Karl Palmskog (Aug 10 2024 at 12:23):

in some sense yes, but that breaks even with Coq 8.20, so not really viable right now

view this post on Zulip Thomas Lamiaux (Aug 10 2024 at 17:31):

isn't that working ?

For backward compatibility, "Coq" still works by being replaced on the fly with "Stdlib" and emiting a warning.

view this post on Zulip Théo Winterhalter (Aug 10 2024 at 17:33):

I think what Karl meant by future-proof is that using Coq is meant to be a temporary solution.

view this post on Zulip Karl Palmskog (Aug 10 2024 at 17:34):

right, in some of the projects we maintain I would prefer to not change simple things like Require for 1+ year

view this post on Zulip Karl Palmskog (Aug 10 2024 at 17:36):

PR 19310 explicitly does not touch the Stdlib via -R question, so one must then assume that Require Import Arith. will work for longer than From Coq Require Import Arith..

The problems we already face due to renaming are going to be considerable, so I don't think it's unreasonable if there was a recommendation on the Require idiom

view this post on Zulip Pierre Roux (Aug 10 2024 at 21:26):

Well, I'd rather do From Coq Require if you need <= 8.20 support. Then replacing From Coq by From Stdlib when droping Coq 8.20 support will just require a trivial sed script. It is indeed also possible to just do nothing and do the change directly to From Stdlib when droping 8.20 support.

view this post on Zulip Pierre Roux (Aug 10 2024 at 21:27):

Karl Palmskog said:

PR 19310 explicitly does not touch the Stdlib via -R question, so one must then assume that Require Import Arith. will work for longer than From Coq Require Import Arith..

I wouldn't assume that. We'll probably want to fix both in the same version in the future.

view this post on Zulip Karl Palmskog (Aug 10 2024 at 21:28):

this isn't really about "ease of editing", but rather about having to make releases of a bunch of packages just because of the renaming

view this post on Zulip Pierre Roux (Aug 10 2024 at 21:30):

Indeed, then doing nothing until support for 8.20 is dropped seems simpler.

view this post on Zulip Karl Palmskog (Aug 10 2024 at 21:32):

OK, would be nice if some info/plan is added to Coq roadmap, e.g., when will From Coq stop working definitively, hopefully not from Jan 2025.

view this post on Zulip Pierre Roux (Aug 10 2024 at 21:45):

We have the policy that there should always be a code working with two successive versions, so it will definitely still be supported in 8.21/9.0. It's not uncommon to keep things for a few more versions though.

view this post on Zulip Thomas Lamiaux (Aug 10 2024 at 22:23):

this isn't really about "ease of editing", but rather about having to make releases of a bunch of packages just because of the renaming

I have never done so myself but I guess it is a lot of work ? Can't this be done gradually at the same of other releases, if they are no more release because the package is stable, at occasion of the Coq Platform v 8.21 ?

view this post on Zulip Karl Palmskog (Aug 10 2024 at 22:37):

there are many packages/projects, and every maintenance action is expensive in terms of attention, time, resources. Projects can basically die off if code updates take more than a few minutes.

view this post on Zulip Karl Palmskog (Aug 10 2024 at 22:39):

for example, if I know that projects are going to die next summer due to the renaming making maintenance unfeasible, they may as well die now (time saved)

view this post on Zulip Pierre Roux (Aug 23 2024 at 15:31):

BTW @Karl Palmskog , in this case we will need to wait for dune to be adapted and such an adapted dune to be reasonably available before changing the warning to errors. I'd expect this to take a few years, hence From Coq to keep working for quite a few versions.

view this post on Zulip Karl Palmskog (Aug 23 2024 at 15:35):

so From Coq Require X is expected to last longer than Require X?

view this post on Zulip Pierre Roux (Aug 23 2024 at 15:47):

I'd say it would probably make sense to keep both for exactly as long.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:01):

Hi @Karl Palmskog , see also my comment here https://github.com/coq/coq/pull/19310#issuecomment-2237378530

view this post on Zulip Karl Palmskog (Sep 09 2024 at 15:03):

yeah, Emilio's proposal seems more painless compared to endless warnings (that are already taking a toll in many projects)

view this post on Zulip Karl Palmskog (Sep 09 2024 at 15:04):

since only a few projects are anyway depending explicitly on coq-stdlib (they instead depend on coq as a whole), shouldn't be much trouble with two alternatives that are mutually exclusive for stdlib

view this post on Zulip Pierre Roux (Sep 09 2024 at 15:19):

Note that, now that we have a nice warning system, if they are well designed, it's pretty easy to get rid of all the warnings introduced in a same version with something like -deprecated-since-8-20. Tweaking dependencies introduces something else to adapt and opens yet another pandora box.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:22):

@Pierre Roux what is the "something else to adapt" a two-package proposal would require?

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:22):

To the best of what I can see, there would be nothing to do. Newer library would become an opt-in

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:25):

Moreover having a new lib as outlined has a lot of advantages, the current proposal introduces work to almost every user for what amounts to an aesthetic detail? Maybe I'm missing something.

view this post on Zulip Pierre Roux (Sep 09 2024 at 15:28):

package dependencies

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:30):

Only as opt-in

view this post on Zulip Pierre Roux (Sep 09 2024 at 15:33):

Make sense, but on our side we need to maintain two libraries, which can be a cost.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:33):

I guess the cost would depend on what the story for Stdlib development is.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:34):

If the story for Stdlib is to follow the current model for current stdlib, then indeed, there is no point on keeping two libs.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:34):

If the story for Stdlib is somehow more disruptive (akin to the old stdlib2 proposal), then IMHO it would make sense to keep two libs.

view this post on Zulip Emilio Jesús Gallego Arias (Sep 09 2024 at 15:34):

I have quite a lot of notes and replies w.r.t. this subject, that I didn't post due to lack of time, I'll try to post them this week.

view this post on Zulip Karl Palmskog (Sep 09 2024 at 15:44):

for quite a few projects, Stdlib is a bit like an albatross around the neck, if there'd be a way to go completely Stdlib-free I'd do it [for selected projects]

view this post on Zulip Karl Palmskog (Sep 09 2024 at 15:45):

unfortunately I think there were only a few experiments in that direction


Last updated: Oct 13 2024 at 01:02 UTC