Stream: Coq devs & plugin devs

Topic: Annotation of hint commands with locality attributes


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

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

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:30):

Best I can offer is compatibility up to 8.11, unfortunately.

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:30):

Indeed, this is the version that introduced the unsupported-attribute warning.

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

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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:35):

No waiting for a CI that will never arrive!

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

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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:42):

Not sure about compcert also.

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

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

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

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

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:50):

The problem is there are two fixes, a good one and a bad one.

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:51):

The good one is adding the attributes now and drop < 8.11 support.

view this post on Zulip Enrico Tassi (Jun 30 2022 at 12:51):

Well, I think their devs must choose.

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:51):

But it's a choice that affects Coq devs, that's the point.

view this post on Zulip Enrico Tassi (Jun 30 2022 at 12:51):

It also affects them, if they want to be in CI

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

view this post on Zulip Enrico Tassi (Jun 30 2022 at 12:52):

Hence I agree in putting more pressure

view this post on Zulip Enrico Tassi (Jun 30 2022 at 12:52):

This was not one of my options

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:52):

I see.

view this post on Zulip Enrico Tassi (Jun 30 2022 at 12:52):

adding the attributes is a must

view this post on Zulip Enrico Tassi (Jun 30 2022 at 12:53):

then you can drop older version, or sed the attributes away (on old version)

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

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:54):

Bicompatibility will still break in the transitory phase, though.

view this post on Zulip Jason Gross (Jun 30 2022 at 12:54):

Why?

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:54):

So you'll still have one version of Coq where it doesn't work.

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

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

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

view this post on Zulip Jason Gross (Jun 30 2022 at 12:56):

Indeed, but I think it's an overapproximation rather than an underapproximation

view this post on Zulip Pierre-Marie Pédrot (Jun 30 2022 at 12:56):

Doesn't matter, hints are not monotone.

view this post on Zulip Gaëtan Gilbert (Jun 30 2022 at 12:57):

how is it an approximation?

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Jun 30 2022 at 14:39):

I'm still missing the point for keeping compatibility with such old Coq versions...

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

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 17:21):

Found the MSG: https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Make.20hint.20locality.20warning.20an.20error/near/282035834

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.

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

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

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

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

view this post on Zulip Ali Caglayan (Jul 01 2022 at 06:54):

you run this on the output of a build containing only the hint locality warnings

view this post on Zulip Ali Caglayan (Jul 01 2022 at 06:54):

so you might have to disable all other warnings and pipe stderr or something

view this post on Zulip Ali Caglayan (Jul 01 2022 at 06:55):

ofc @Pierre-Marie Pédrot can say more

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

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