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?
the future proof way is From Stdlib
in some sense yes, but that breaks even with Coq 8.20, so not really viable right now
isn't that working ?
For backward compatibility, "Coq" still works by being replaced on the fly with "Stdlib" and emiting a warning.
I think what Karl meant by future-proof is that using Coq
is meant to be a temporary solution.
right, in some of the projects we maintain I would prefer to not change simple things like Require
for 1+ year
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
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.
Karl Palmskog said:
PR 19310 explicitly does not touch the Stdlib via
-R
question, so one must then assume thatRequire Import Arith.
will work for longer thanFrom Coq Require Import Arith.
.
I wouldn't assume that. We'll probably want to fix both in the same version in the future.
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
Indeed, then doing nothing until support for 8.20 is dropped seems simpler.
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.
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.
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 ?
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.
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)
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.
so From Coq Require X
is expected to last longer than Require X
?
I'd say it would probably make sense to keep both for exactly as long.
Hi @Karl Palmskog , see also my comment here https://github.com/coq/coq/pull/19310#issuecomment-2237378530
yeah, Emilio's proposal seems more painless compared to endless warnings (that are already taking a toll in many projects)
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
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.
@Pierre Roux what is the "something else to adapt" a two-package proposal would require?
To the best of what I can see, there would be nothing to do. Newer library would become an opt-in
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.
package dependencies
Only as opt-in
Make sense, but on our side we need to maintain two libraries, which can be a cost.
I guess the cost would depend on what the story for Stdlib
development is.
If the story for Stdlib
is to follow the current model for current stdlib, then indeed, there is no point on keeping two libs.
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.
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.
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]
unfortunately I think there were only a few experiments in that direction
Last updated: Oct 13 2024 at 01:02 UTC