Pierre-Marie Pédrot (Jun 30 2022 at 12:29): Pierre-Marie Pédrot (Jun 30 2022 at 12:29):I'd like to make progress on https://github.com/coq/coq/pull/16004 which is, I believe, critical for 8.17. It's even part of the elusive roadmap, can't be more serious stuff!
Pierre-Marie Pédrot (Jun 30 2022 at 12:30):Most of the devs have been ported, but now we have a massive block of interdependencies where some people want backwards compatibility with very old versions of Coq (8.6 IIUC).
Pierre-Marie Pédrot (Jun 30 2022 at 12:30):Best I can offer is compatibility up to 8.11, unfortunately.
Pierre-Marie Pédrot (Jun 30 2022 at 12:30):Indeed, this is the version that introduced the unsupported-attribute warning.
Pierre-Marie Pédrot (Jun 30 2022 at 12:31):I've heard @Jason Gross asking for deactivating the warnings totally and wait until the switch of behaviour is performed.
Pierre-Marie Pédrot (Jun 30 2022 at 12:32):Hopefully by then the miracle will have occurred and legacy code will work the same both in global and export mode.
Pierre-Marie Pédrot (Jun 30 2022 at 12:33):To be clear, I think this is a terrible way of action because it puts the burden on the Coq developers. Basically, that means that the switch will never be performed because it will break the CI for all devs depending on the old behaviour. Let us not be gullible, the miracle of bicompatibility will never happen before the heat death of the universe.
Pierre-Marie Pédrot (Jun 30 2022 at 12:34):Rather, I advocate that we should drop support for pre-8.11 versions, set all attributes explicitly and unset the unknown attribute warning for the few devs that want to support Coq up to 8.11.
Pierre-Marie Pédrot (Jun 30 2022 at 12:34):This is much better because for the poor Coq dev who will write the behaviour switching PR, this will be transparent.
Pierre-Marie Pédrot (Jun 30 2022 at 12:35):No waiting for a CI that will never arrive!
Pierre-Marie Pédrot (Jun 30 2022 at 12:36):So, this thread is essentially call for bullying^W political pressure on the CI devs that would like to be compatible with pre-8.11 Coq.
Pierre-Marie Pédrot (Jun 30 2022 at 12:38):@Jason Gross would you be fine with a compat up to 8.11 for the devs of which you're the maintainer?
Enrico Tassi (Jun 30 2022 at 12:38):FTR, Today's release of math-comp dropped 8.11 and 8.12... so that entire ecosystem is fine w.r.t. dropping old version
Pierre-Marie Pédrot (Jun 30 2022 at 12:39):The mathcomp ecosystem is already compatible with #16004 AFAIC, so you people are not on the critical path.
Pierre-Marie Pédrot (Jun 30 2022 at 12:40):From what I see from the PR overlays, the major concern is every dev part of the mit-plv organization.
Pierre-Marie Pédrot (Jun 30 2022 at 12:42):Not sure about compcert also.
Gaëtan Gilbert (Jun 30 2022 at 12:44):we always have the option of removing them from CI until they get fixed
CI is to make things easier for everyone, not a tool to let 3rd party developments dictate coq changes or lack of changes
Pierre-Marie Pédrot (Jun 30 2022 at 12:44):We're talking about a good chunk of the CI though, which is useful for regression testing
Pierre-Marie Pédrot (Jun 30 2022 at 12:45):(As usual, there is also the one CI development whose name must not be uttered which starts with fiat-crypto and ends with legacy).
Enrico Tassi (Jun 30 2022 at 12:49):My opinion is that this transition to mandatory hint locality has been long enough, I'd remove the jobs, and add them back once they are fixed (in the sense of dropping compat with ancient versions or adding even more makefile magic assuming it is possible).
Pierre-Marie Pédrot (Jun 30 2022 at 12:50):The problem is there are two fixes, a good one and a bad one.
Pierre-Marie Pédrot (Jun 30 2022 at 12:51):The good one is adding the attributes now and drop < 8.11 support.
Enrico Tassi (Jun 30 2022 at 12:51):Well, I think their devs must choose.
Pierre-Marie Pédrot (Jun 30 2022 at 12:51):But it's a choice that affects Coq devs, that's the point.
Enrico Tassi (Jun 30 2022 at 12:51):It also affects them, if they want to be in CI
Pierre-Marie Pédrot (Jun 30 2022 at 12:51):The bad one is that they just deactivate the warning and wait for the apocalypse when Coq switches behaviour in 8.18.
Enrico Tassi (Jun 30 2022 at 12:52):Hence I agree in putting more pressure
Enrico Tassi (Jun 30 2022 at 12:52):This was not one of my options
Pierre-Marie Pédrot (Jun 30 2022 at 12:52):I see.
Enrico Tassi (Jun 30 2022 at 12:52):adding the attributes is a must
Enrico Tassi (Jun 30 2022 at 12:53):then you can drop older version, or sed the attributes away (on old version)
Jason Gross (Jun 30 2022 at 12:53):I was just working on bicompatibility. I don't think it's as unattainable as you claim. I have a PR prepared for bbv at https://github.com/mit-plv/bbv/pull/41 that is bicompatible via Set Loose Hint Behavior "Strict"., I will prepare one for fiat-crypto-legacy and coqprime now as well. (fiat-crypto non-legacy already demands >= 8.11, so rewriter and fiat-crypto are fine with the 8.11 solution)
Pierre-Marie Pédrot (Jun 30 2022 at 12:54):Bicompatibility will still break in the transitory phase, though.
Jason Gross (Jun 30 2022 at 12:54):Why?
Pierre-Marie Pédrot (Jun 30 2022 at 12:54):So you'll still have one version of Coq where it doesn't work.
Jason Gross (Jun 30 2022 at 12:55):I'm passing -w -deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality
Pierre-Marie Pédrot (Jun 30 2022 at 12:55):Hmm, maybe you're right, if we go directly from the phase where the warning is an error to the behaviour change it should be fine.
Pierre-Marie Pédrot (Jun 30 2022 at 12:56):(Though I'd still expect fallout because there will probably be some weird cornercases. The Loose Hint option is only an approximation.)
Jason Gross (Jun 30 2022 at 12:56):Indeed, but I think it's an overapproximation rather than an underapproximation
Pierre-Marie Pédrot (Jun 30 2022 at 12:56):Doesn't matter, hints are not monotone.
Gaëtan Gilbert (Jun 30 2022 at 12:57):how is it an approximation?
Pierre-Marie Pédrot (Jun 30 2022 at 12:57):@Gaëtan Gilbert you don't really know if a hint is really needed if you only look at the dynamic trace.
Jason Gross (Jun 30 2022 at 12:57):Ah, sure. But these are developments that are hardly changed these days, if it works with Loose Hint Behavior Warn and Strict, I think it'll be fine when the default switches to Export, in almost all cases
Pierre-Marie Pédrot (Jun 30 2022 at 12:58):@Jason Gross if I were you I'd double-check. I can produce a branch with the switch so that you can test.
Jason Gross (Jun 30 2022 at 12:58):@Pierre-Marie Pédrot @Gaëtan Gilbert It's not just that, it's also that Loose Hint Behavior Strict applies also to explicitly-declared Global Instances. This is much more annoying.
Gaëtan Gilbert (Jun 30 2022 at 12:59):Pierre-Marie Pédrot said:
Gaëtan Gilbert you don't really know if a hint is really needed if you only look at the dynamic trace.
that's about Warn mode not Strict mode no?
Jason Gross (Jun 30 2022 at 12:59):I still think it'd be much nicer to have an option like Set Default Hint Declaration Behavior Export (something without quotes so old Coq will ignore it) so that I can make the behavior change early, rather than having to go through Set Loose Hint Behavior "Strict", so I don't have to do things like Local Existing Instances N.le_preorder Nat.add_wd Nat.div_wd Nat.divide_reflexive Nat.le_preorder Nat.le_wd Nat.lt_wd Nat.mod_wd Nat.mul_wd Nat.sub_wd Z.le_wd Z.le_preorder Z.lt_strorder. (can't just Import Nat Z. because that shadows eq_refl and Coq 8.7 doesn't revert the shadowing even if I do Import Prelude)
Gaëtan Gilbert (Jun 30 2022 at 13:00):something without quotes so old Coq will ignore it
??? old coq will ignore unknown string valued options
Pierre-Marie Pédrot (Jun 30 2022 at 13:01):@Jason Gross also the problem with bicompatibility is that it only works for leaf developments, because it's not transitive.
Pierre-Marie Pédrot (Jun 30 2022 at 13:01):You never know whether there isn't a dev downstream that depends on the precise semantics.
Pierre-Marie Pédrot (Jun 30 2022 at 13:02):I really, really think that it's looking for trouble and we should instead go through the mandatory attribute route for safety.
Jason Gross (Jun 30 2022 at 13:03):something without quotes so old Coq will ignore it
??? old coq will ignore unknown string valued options
Ah, I guess some of my mental model is still running on Coq 8.4. It looks like this was changed between 8.5beta2 and 8.5beta3.
Théo Zimmermann (Jun 30 2022 at 14:39):I'm still missing the point for keeping compatibility with such old Coq versions...
Paolo Giarrusso (Jun 30 2022 at 17:17):@Théo Zimmermann Jason answered last time — IIRC, fiat-crypto-legacy is just a paper artifact that should be a Docker/VM image, while fiat-crypto has constraints of having to build on the latest Debian/Ubuntu LTS
Paolo Giarrusso (Jun 30 2022 at 17:21):Fiat Crypto Legacy supports back to 8.7. There is no pressing reason to keep this support in place, as indeed there are no users of f-c-l other than Coq's CI and anyone that is trying to do archeology on the code from our 2019 paper. However, I'd like to keep this support in place as long as it doesn't incur too much burden.
Paolo Giarrusso (Jun 30 2022 at 17:22):the emphasis is mine (and the message said more), but clearly @Pierre-Marie Pédrot thinks fiat-crypto-legacy _is_ too much burden
Théo Zimmermann (Jun 30 2022 at 17:33):Thanks for digging this message, but indeed, I think at this point we are way past the reasonable here. There are no actual users, and people would still be able to play with the code using old Coq versions by using past versions (maybe doing a tagged release would be a good idea). In particular, I don't think it is reasonable to ask for a new option to be introduced if there is not any actual use case in mind. As for Debian, it contains Coq 8.12 (and Ubuntu LTS contains 8.15, and even the previous LTS contains 8.11).
Jason Gross (Jul 01 2022 at 02:45):I'm willing to do a tagged release and drop compat for the older versions. However, I've gotten most of the way towards having a bicompatible version, though.
I'm having comparatively more trouble with updating Fiat Crypto non-legacy (which is only supporting back through 8.11).
Does anyone have a script that will take output of the warnings and insert the right attributes? (Is it always #[global]?)
Ali Caglayan (Jul 01 2022 at 06:51):@Jason Gross We use this script of PMP that I keep losing: https://gist.github.com/ppedrot/3e0c7cbabd9042474c13c25dafefa677
Ali Caglayan (Jul 01 2022 at 06:54):you run this on the output of a build containing only the hint locality warnings
Ali Caglayan (Jul 01 2022 at 06:54):so you might have to disable all other warnings and pipe stderr or something
Ali Caglayan (Jul 01 2022 at 06:55):ofc @Pierre-Marie Pédrot can say more
Pierre-Marie Pédrot (Jul 01 2022 at 09:35):Basically I set COQFLAGS to remove all warnings except the locality ones and then I make 2> log or something and call the script on the result.
Pierre-Marie Pédrot (Jul 01 2022 at 09:35):You might need to tweak the script or the process a bit if your dev is using fancy features like submodules.
Last updated: Jun 08 2023 at 04:01 UTC