Stream: Coq devs & plugin devs

Topic: Make hint locality warning an error


view this post on Zulip Ali Caglayan (May 09 2022 at 10:00):

What is stopping us from doing https://github.com/coq/coq/issues/13394 in 8.16?

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 10:02):

laziness

view this post on Zulip Ali Caglayan (May 09 2022 at 10:03):

If we turn the warning into an error, will it just become an overlay writing exercise?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 10:13):

yes, conceptually trivial but annoying in practice

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 10:14):

if you're brave enough to do it before the branch I'd support such an endeavour

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 10:14):

(expect quite a bit of work between writing overlays and getting them merged)

view this post on Zulip Ali Caglayan (May 09 2022 at 10:35):

We do however want to eventually introduce a default hint locality in the future right?

view this post on Zulip Ali Caglayan (May 09 2022 at 10:35):

So I won't get rid of default_hint_locality but instead throw an error on its use?

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 10:35):

make the warning AsError

view this post on Zulip Ali Caglayan (May 09 2022 at 10:43):

Let's see what happens: https://github.com/coq/coq/pull/16004

view this post on Zulip Ali Caglayan (May 09 2022 at 11:47):

Alright test-suite is the first causality, I'll work on that first.

view this post on Zulip Ali Caglayan (May 09 2022 at 12:23):

There is also a warning for Hint Rewrite should I make that an error too?

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 12:25):

check what version it was made, if it's had a version as a warning then yes

view this post on Zulip Ali Caglayan (May 09 2022 at 12:34):

That was 8.14 it seems

view this post on Zulip Ali Caglayan (May 09 2022 at 12:35):

I will do their cleanup separately however just in case

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 12:41):

The hard part is writing the overlays, fixing the bug on the Coq side is just a one-liner.

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:35):

@Ali Caglayan do you need help to write the overlays?

view this post on Zulip Ali Caglayan (May 09 2022 at 13:36):

I would welcome help on that

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:36):

(I think that if we want this to happen for 8.16 we'd need a bit more manpower.)

view this post on Zulip Ali Caglayan (May 09 2022 at 13:36):

I'm still messing around with the test-suite

view this post on Zulip Ali Caglayan (May 09 2022 at 13:36):

I'm trying to come up with a killer regexp

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:37):

there is the script that helps you tracking this

view this post on Zulip Ali Caglayan (May 09 2022 at 13:37):

So far I had

^(?<!Global)(?<!Local )(?<!#[local] )(?<!#[global] )Hint(?! Rewrite)

but this doesn't catch everything

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:37):

but then the problem is more the interaction with the build system

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 13:38):

add -w -the-warning-name to get_coq_prog_args in the makefile
the test suite shouldn't care about this warning

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 13:38):

(and add it to the _coqproject so editing works right)

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:41):

@Gaëtan Gilbert do you have a bit of spare time to write some overlays ?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:46):

I count 4 such warnings, they're all part of 8.15 right?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 13:46):

-arg "-w +deprecated-hint-rewrite-without-locality"
-arg "-w +deprecated-hint-without-locality"
-arg "-w +deprecated-typeclasses-transparency-without-locality"
-arg "-w +deprecated-instance-without-locality"

view this post on Zulip Ali Caglayan (May 09 2022 at 14:03):

The first is from 8.14

view this post on Zulip Ali Caglayan (May 09 2022 at 14:03):

I don't know about the last 2

view this post on Zulip Ali Caglayan (May 09 2022 at 14:03):

I think it is better to do one at a time for now

view this post on Zulip Ali Caglayan (May 09 2022 at 14:04):

I don't believe hint rewrite is nearly as common

view this post on Zulip Ali Caglayan (May 09 2022 at 14:07):

Doing the overlay for argosy rn

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:17):

on bignums

view this post on Zulip Ali Caglayan (May 09 2022 at 14:17):

argosy is vendoring coq-classes as a submodule so I submitted a patch there, hopefully we can bump that submodule later https://github.com/tchajed/coq-classes/pull/1

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:19):

the overlays should be performed for all these warnings at once otherwise we'll lose time for the next change

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:19):

(they will be all backwards compat)

view this post on Zulip Ali Caglayan (May 09 2022 at 14:22):

Shall I make them all errors then?

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:24):

we'll see for your PR, I think that now the important parts are the overlays

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:27):

on geocoq

view this post on Zulip Ali Caglayan (May 09 2022 at 14:30):

on mtac2

view this post on Zulip Ali Caglayan (May 09 2022 at 14:38):

deprecated-typeclasses-transparency-without-locality is 8.15

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:38):

ok

view this post on Zulip Ali Caglayan (May 09 2022 at 14:38):

deprecated-instance-without-locality is 8.14 so I will add that too

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:38):

(we don't have a ci on https://github.com/coq-community/bignums/pull/70? This looks a bit fragile given that it's a critical piece of software in the dependency graph of coq)

view this post on Zulip Ali Caglayan (May 09 2022 at 14:39):

Only on push to master it seems https://github.com/coq-community/bignums/blob/059f1738ea3409f3d3dbf805d144878de3170fc7/.github/workflows/docker-action.yml#L11

view this post on Zulip Ali Caglayan (May 09 2022 at 14:41):

@Karl Palmskog Do you remember why this is?

view this post on Zulip Gaëtan Gilbert (May 09 2022 at 14:42):

the closed PRs have CI

view this post on Zulip Karl Palmskog (May 09 2022 at 14:42):

there is no problem with the CI configuration. It's GitHub that disables CI workflows after some number of days of inactivity

view this post on Zulip Karl Palmskog (May 09 2022 at 14:42):

please do a force-push and you should get CI now

view this post on Zulip Ali Caglayan (May 09 2022 at 14:44):

Huh weird

view this post on Zulip Pierre-Marie Pédrot (May 09 2022 at 14:44):

seems to have worked (cc @Pierre Roux btw)

view this post on Zulip Ali Caglayan (May 09 2022 at 14:52):

I'm getting dynlink errors doing the overlay for mtac2 so giving up

view this post on Zulip Karl Palmskog (May 09 2022 at 14:53):

for the record @Pierre-Marie Pédrot @Gaëtan Gilbert if you notice something like this again (missing CI for a coq-community project), you can go to the "Actions" tab, and there should be a warning there for "Docker CI". If you click on the warning, there is a button to re-enable CI

view this post on Zulip Théo Zimmermann (May 09 2022 at 14:54):

IINM, this is related to a repository having scheduled workflows.

view this post on Zulip Ali Caglayan (May 09 2022 at 14:55):

on deriving

view this post on Zulip Théo Zimmermann (May 09 2022 at 14:55):

We should remove the scheduled workflow from bignums IMHO.

view this post on Zulip Théo Zimmermann (May 09 2022 at 14:56):

Ali Caglayan said:

deprecated-typeclasses-transparency-without-locality is 8.15

I don't think that make it a problem for making it a fatal warning in 8.16.

view this post on Zulip Ali Caglayan (May 09 2022 at 20:52):

on category_theory

view this post on Zulip Ali Caglayan (May 09 2022 at 21:30):

on color

view this post on Zulip Ali Caglayan (May 09 2022 at 21:30):

on menhir

view this post on Zulip Ali Caglayan (May 09 2022 at 22:06):

Can somebody add me to the INRIA gitlab?

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 06:25):

@Ali Caglayan you need an account there, right? I can invite you if this is the case.

view this post on Zulip Ali Caglayan (May 10 2022 at 07:48):

@Pierre-Marie Pédrot Yes, I need one.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:12):

Please send me you preferred email address for the account in a private message then.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:14):

(I seize the opportunity to complain about the use of the closed INRIA gitlab for CI devs.)

view this post on Zulip Ali Caglayan (May 10 2022 at 08:21):

I am struggling to port math_classes since my crude find-and-replace seems to have changed the meaning of =??

view this post on Zulip Ali Caglayan (May 10 2022 at 08:22):

I would appreciate if somebody could take a look at it with me.

view this post on Zulip Gaëtan Gilbert (May 10 2022 at 08:25):

link?

view this post on Zulip Ali Caglayan (May 10 2022 at 08:33):

I'll push in a sec

view this post on Zulip Ali Caglayan (May 10 2022 at 08:34):

For some reason github got stuck forking

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:35):

@Ali Caglayan you're not using the "official" porting script based on warning output?

view this post on Zulip Ali Caglayan (May 10 2022 at 08:35):

@Gaëtan Gilbert https://github.com/Alizter/math-classes/tree/adapt-to-16004

view this post on Zulip Ali Caglayan (May 10 2022 at 08:36):

Pierre-Marie Pédrot said:

Ali Caglayan you're not using the "official" porting script based on warning output?

No I though that was just a find and replace so I have been doing find and replace. :O

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:36):

ah, but then the problem with find and replace is that you may screw up the section hints

view this post on Zulip Paolo Giarrusso (May 10 2022 at 08:37):

That makes local instances global, indeed

view this post on Zulip Paolo Giarrusso (May 10 2022 at 08:37):

(That = I looked at the diff)

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:37):

Hopefully the overlays you already wrote are not behaviour-changing...

view this post on Zulip Ali Caglayan (May 10 2022 at 08:38):

Hmm it should only be Hint (not Rewrite) inside a section with no locality that gets affected

view this post on Zulip Ali Caglayan (May 10 2022 at 08:39):

oh dear maybe I was too zealous

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:39):

Hint inside a section can't be global IIRC, but instances can.

view this post on Zulip Ali Caglayan (May 10 2022 at 08:39):

Ah ok then its not so bad probably

view this post on Zulip Ali Caglayan (May 10 2022 at 08:39):

I didn't change Instances too eagerly

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:39):

well, it means that TC-heavy devs are probably broken

view this post on Zulip Ali Caglayan (May 10 2022 at 08:40):

I'll go and mark them as potentially broken then

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:40):

(I double-checked and indeed this only affects instances.)

view this post on Zulip Ali Caglayan (May 10 2022 at 08:40):

This probably explains why math-classes didn't work

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:41):

(Hint Rewrite is also immune to the problem because it doesn't allow global in a section either)

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:42):

I can write the mathclasses patch if you want

view this post on Zulip Ali Caglayan (May 10 2022 at 08:42):

Sure

view this post on Zulip Ali Caglayan (May 10 2022 at 08:42):

I also couldn't finish verdi_raft

view this post on Zulip Ali Caglayan (May 10 2022 at 08:42):

Probably for the same reason

view this post on Zulip Ali Caglayan (May 10 2022 at 08:42):

Though all its deps are fine

view this post on Zulip Ali Caglayan (May 10 2022 at 08:43):

verdi_raft just hangs for me, after a few changes

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:43):

TC search maybe?

view this post on Zulip Ali Caglayan (May 10 2022 at 08:45):

probably, I can't workout how to drop into coqide so I can't see it for myself

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:47):

I do spot suspicious global flags for section instances in e.g. https://github.com/uwplse/verdi/pull/132/files

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:49):

https://github.com/coq-community/math-classes/pull/111

view this post on Zulip Ali Caglayan (May 10 2022 at 08:49):

Pierre-Marie Pédrot said:

https://github.com/coq-community/math-classes/pull/111

Why did you disable the warnings?

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:50):

it's actually activating it, but it was a missing git amend from myself, I've forced-pushed

view this post on Zulip Ali Caglayan (May 10 2022 at 08:51):

Now that I think about it category_theory is also probably messed up

view this post on Zulip Ali Caglayan (May 10 2022 at 08:51):

I didn't really question the huge amount of time it took to compile before

view this post on Zulip Ali Caglayan (May 10 2022 at 08:51):

But now I think it might be tc going haywire

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:51):

meh

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:51):

in that case you should probably close your PRs that mention instances

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:52):

FTR here's the script I used to port stuff: https://gist.github.com/ppedrot/3e0c7cbabd9042474c13c25dafefa677

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:53):

you just set the warnings in the build system, redirect the stderr output to some file log and call the script on that file

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 08:56):

dafuq? math_classes has a CI that goes back to Coq 8.6

view this post on Zulip Ali Caglayan (May 10 2022 at 08:59):

https://github.com/uwplse/cheerios/pull/10 looks fine right? I don't think any of those are in sections, just modules.

view this post on Zulip Ali Caglayan (May 10 2022 at 09:00):

Ok I've closed most of the ones I suspect to be broken

view this post on Zulip Ali Caglayan (May 10 2022 at 09:03):

I can't fork menhir because "I've reached my project limit"

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 09:03):

interesting...

view this post on Zulip Ali Caglayan (May 10 2022 at 09:04):

I also think I may have botched it anyway so I probably won't bother

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 09:04):

I can port it then

view this post on Zulip Ali Caglayan (May 10 2022 at 09:05):

I'll work on perf test

view this post on Zulip Ali Caglayan (May 10 2022 at 09:11):

@Pierre-Marie Pédrot Shall I add that script to tools/ so that other users can use it?

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 09:13):

I don't think so, it has been advertised already and it's pretty specific

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 09:14):

How does menhirlib work w.r.t. versioning? We're picking a specific tag that is one year old, but there has been activity since.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 09:15):

In particular all the global warnings were fixed in master already

view this post on Zulip Ali Caglayan (May 10 2022 at 09:36):

I guess menhir is good to have in the CI since it uses a lot of coq features. Why we are not tracking the master I don't know. I guess we can fast forward to a more recent commit.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 09:51):

I've written a PR for color: https://github.com/fblanqui/color/pull/42

view this post on Zulip Ali Caglayan (May 10 2022 at 10:48):

perf tests seems to output warnings in stdout :/

view this post on Zulip Ali Caglayan (May 10 2022 at 10:48):

Will the script work when other stuff is in there?

view this post on Zulip Ali Caglayan (May 10 2022 at 11:22):

It doesn't really work for makefiles that call other makefiles

view this post on Zulip Ali Caglayan (May 10 2022 at 11:22):

I give up on perf tests then

view this post on Zulip Ali Caglayan (May 10 2022 at 11:23):

I managed to do VST that was easy, all of the work was already done

view this post on Zulip Ali Caglayan (May 10 2022 at 11:23):

I don't know how to pass flags in Unimath

view this post on Zulip Ali Caglayan (May 10 2022 at 11:24):

I haven't touched any of the fiat stuff except for rewriter

view this post on Zulip Ali Caglayan (May 10 2022 at 11:25):

AFAICT they want to keep their backwards compatibility as much as possible, so I guess we will disable warnings instead

view this post on Zulip Ali Caglayan (May 10 2022 at 11:37):

see https://github.com/mit-plv/rewriter/pull/42

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 11:38):

I think that disabling warnings is just putting the dust under the rug.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 11:38):

It will bite us when we want to switch anyways.

view this post on Zulip Ali Caglayan (May 10 2022 at 11:41):

I'm working on category_theory again trying to do it properly this time

view this post on Zulip Théo Zimmermann (May 10 2022 at 11:44):

Pierre-Marie Pédrot said:

I don't think so, it has been advertised already and it's pretty specific

IMHO it should be advertised again if we make these warnings fatal in 8.16. Especially now that it has been battle-tested.

view this post on Zulip Théo Zimmermann (May 10 2022 at 11:44):

Ali Caglayan said:

I guess menhir is good to have in the CI since it uses a lot of coq features. Why we are not tracking the master I don't know. I guess we can fast forward to a more recent commit.

This probably is because it used to be a non-Coq dependency for menhirlib. But now I think the two are in the same repo.

view this post on Zulip Théo Zimmermann (May 10 2022 at 11:45):

Pierre-Marie Pédrot said:

It will bite us when we want to switch anyways.

Especially true if we switch right after branching.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 11:49):

I'm not super fond of doing this change in 8.16 given the current state of affairs.

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 11:50):

I'd rather try to fix the CI as much as possible so that the amount of work is limited when we really perform the warning > error switch.

view this post on Zulip Ali Caglayan (May 10 2022 at 11:53):

I guess there is no rush to do it now, but at some point it had to be done.

view this post on Zulip Ali Caglayan (May 10 2022 at 12:06):

Pierre-Marie Pédrot said:

I'm not super fond of doing this change in 8.16 given the current state of affairs.

What exactly do you mean by current state of affairs?

view this post on Zulip Ali Caglayan (May 10 2022 at 12:06):

If it is about the CI then surely we can fix it?

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 12:08):

The fact that there are some devs that make strong commitment on supporting pretty old Coq versions. This is reasonable (to some extent).

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 12:09):

While striving to support 8.6 is probably not reasonable, 8.13 or so is not utterly crazy.

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

Also there are some devs which are probably nasty like fcl.

view this post on Zulip Ali Caglayan (May 10 2022 at 12:15):

fcl?

view this post on Zulip Ali Caglayan (May 10 2022 at 12:15):

Did you mean tcl?

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 12:15):

fiat-crypto-legacy

view this post on Zulip Ali Caglayan (May 10 2022 at 12:16):

OK so you want to give them more time to have a longer string of compatible versions?

view this post on Zulip Pierre-Marie Pédrot (May 10 2022 at 12:17):

Let's see what they say first, but I don't mind postponing the change to one more version.

view this post on Zulip Ali Caglayan (May 10 2022 at 12:19):

How bad do you think bedrock2 will be?

view this post on Zulip Ali Caglayan (May 10 2022 at 12:20):

I might start it...

view this post on Zulip Ali Caglayan (May 10 2022 at 12:33):

It's looking messy :(

view this post on Zulip Pierre-Marie Pédrot (May 11 2022 at 09:53):

FWIW I'm on unimath

view this post on Zulip Pierre-Marie Pédrot (May 11 2022 at 10:02):

it was surprisingly easy, they basically declare no hints except in their prelude

view this post on Zulip Ali Caglayan (May 11 2022 at 15:19):

category theory done

view this post on Zulip Ali Caglayan (May 11 2022 at 15:21):

@Jason Gross You say for rewriter that you would rather have your hint localities silently export and fix it when this happens, what is wrong with dropping support for older versions and fixing it properly now?

view this post on Zulip Jason Gross (May 11 2022 at 15:22):

@Ali Caglayan I don't plan to drop support for older versions when the default behavior changes, I plan to fix it in a way that is backwards compatible.

view this post on Zulip Ali Caglayan (May 11 2022 at 15:24):

Will you wait until we switch the locality and everything breaks to fix it or fix it before?

view this post on Zulip Ali Caglayan (May 11 2022 at 15:24):

In that case, your fixes will be doing the job of our overlays.

view this post on Zulip Ali Caglayan (May 11 2022 at 15:25):

It looks like this won't make it to 8.16 anyway, so there is around 6 months to fix everything give or take

view this post on Zulip Ali Caglayan (May 11 2022 at 15:25):

Is this the same for fiat_crypto etc. too?

view this post on Zulip Jason Gross (May 11 2022 at 15:27):

I'm inclined to wait until there is at least an option to change the default locality, so that there's no chance of regression (because the option will be a no-op on older versions of Coq and CI will test newer versions of Coq). (Speaking of which, how do you / the devs feel about adding a deprecated option to change default locality?) Once this option exists, I can make the change (for rewriter, bbv, f-c-l, fiat-crypto, and to some extent coqutil; for bedrock2 and rupicola we drop version support much more quickly).

view this post on Zulip Gaëtan Gilbert (May 11 2022 at 15:31):

there's no option plan is there?

view this post on Zulip Pierre-Marie Pédrot (May 11 2022 at 15:32):

The option plan is literally already there.

view this post on Zulip Ali Caglayan (May 11 2022 at 17:14):

@Pierre-Marie Pédrot You mean that there is currently an option to do this in Coq? What is it called, I cannot find it.

view this post on Zulip Paolo Giarrusso (May 11 2022 at 19:36):

@Jason Gross when you say “the option will be a no-op on older versions of Coq”, you must mean “we will not pass the option to older Coq versions” I suppose (say, you’ll autogenerate _CoqProject through conditional compilation)? Otherwise I’m not sure adding the option is technically possible.

view this post on Zulip Paolo Giarrusso (May 11 2022 at 19:42):

Whether devs are willing to provide it is another matter. Could you enlighten us why you still support Coq 8.6? Is that because the cryptography code from fiat-crypto has active non-Coq users on older distributions?

view this post on Zulip Paolo Giarrusso (May 11 2022 at 19:44):

In that case, I wonder if the code generation should be done upstream and the pre-generated C should be distributed for older distros, but there might be complexities there too.

view this post on Zulip Ali Caglayan (May 11 2022 at 20:28):

Paolo Giarrusso said:

Jason Gross when you say “the option will be a no-op on older versions of Coq”, you must mean “we will not pass the option to older Coq versions” I suppose (say, you’ll autogenerate _CoqProject through conditional compilation)? Otherwise I’m not sure adding the option is technically possible.

If I do

Set Option "foo".

it just throws a warning.

view this post on Zulip Jason Gross (May 11 2022 at 22:22):

Let me lay out my plan all in one place:
Fiat Crypto supports the latest Ubuntu LTS and Debian Stable. I think these versions don't support Global Hint Rewrite, but if they do I'm happy to explicitly annotate. (I would like to eventually switch to #[export], once the Ubuntu LTS / Debian Stable versions of Coq support it.). Part of the sales pitch of fiat-crypto is that users can generate code for new primes, so I'd prefer to maintain out-of-the-box compatibly with these distributions.

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.

My plan, for Fiat Crypto Legacy, bbv, and for Fiat Crypto and the rewriter if necessary, is:

  1. Disable the to-be-fatal-by-default warning. (This is possible, right?)
  2. Once the default behavior changes, I can take responsibility for making the code bases compatible with both hint localities. The sledgehammer approach is to give literally every file an Exports module that re-exports the Exports modules of all files that it requires, and stick the necessary hints in these modules. However, as I'd like to eventually move to #[export] behavior, I will aim to be less sledgehammery about following the export discipline. Since no file will rely on default-export hints not being available via Require, and all files will work with default-export behavior, this should be backwards compatible.
  3. If Coq provides a flag to make hints export-by-default earlier, I will aim to fix the developments to be compatible with this default behavior before the switch to export-by-default is made. I will globally set this flag (which will be a no-op on older versions of Coq because Set Foo is a no-op for unrecognized Foo) to enforce that the CI checks compatibility with the upcoming default behavior

view this post on Zulip Paolo Giarrusso (May 12 2022 at 06:37):

https://packages.ubuntu.com/jammy/coq is 8.15.0, but https://packages.debian.org/bullseye/coq uses 8.12.0 and https://wiki.debian.org/DebianReleases implies the next release is expected around (late) next year, so after Coq 8.18.

view this post on Zulip Paolo Giarrusso (May 12 2022 at 06:48):

I now suspect the option might be Set Loose Hint Behavior "Strict", which was available in 8.12! But it seems to affect only Hint Resolve and Instance: https://coq.inria.fr/distrib/V8.12.2/refman/proof-engine/tactics.html#coq:opt.loose-hint-behavior.

view this post on Zulip Paolo Giarrusso (May 12 2022 at 06:53):

but as defined, that seems to affect even hints that are explicitly marked #[global], instead of just unannotated hints?

view this post on Zulip Théo Zimmermann (May 12 2022 at 08:10):

FTR @Jason Gross, your strategy of using an option because unknown options just trigger a warning would also work with attributes as long as you are willing to make Coq 8.11 a hard requirement for all your projects (which seems reasonable given the versions available in Ubuntu LTS and Debian reported by Paolo just above): https://github.com/coq/coq/pull/10997

view this post on Zulip Théo Zimmermann (May 12 2022 at 08:11):

This warning is fatal by default, but you can locally disable it since it's a warning.

view this post on Zulip Théo Zimmermann (May 12 2022 at 08:12):

See also: https://coq.inria.fr/refman/language/core/basic.html#coq:warn.This-command-does-not-support-this-attribute

view this post on Zulip Pierre-Marie Pédrot (May 12 2022 at 08:24):

My point was exactly what Théo said, i.e. unset unknown attribute fatality.

view this post on Zulip Ali Caglayan (May 19 2022 at 10:38):

on bedrock2

view this post on Zulip Ali Caglayan (May 19 2022 at 13:34):

I've updated the list and it has grown

view this post on Zulip Maxime Dénès (May 20 2022 at 11:57):

Incidentally, it seems the implementation of this warning makes elaboration of attributes depend on the logical environment, doesn't it?

view this post on Zulip Maxime Dénès (May 20 2022 at 11:57):

I hit it in my parsing / execution separation branch

view this post on Zulip Maxime Dénès (May 20 2022 at 11:59):

(it is because the only way to know if a section is open currently seems to be by asking the kernel, but this warning wants to do it more or less at parsing time, if you consider attribute elaboration being part of parsing)

view this post on Zulip Ali Caglayan (May 20 2022 at 12:43):

Can we not simply lex the file and check if a section is open? I don't know about Undo tho.

view this post on Zulip Maxime Dénès (May 20 2022 at 13:07):

Undo is only about tactics IIRC

view this post on Zulip Maxime Dénès (May 20 2022 at 13:08):

I believe Lib used to have the right information about sections, but it was moved to the kernel

view this post on Zulip Ali Caglayan (Jul 30 2022 at 14:54):

@Pierre-Marie Pédrot I see that there has been a lot of progress recently. What are we waiting for with fiat parsers and engine bench?

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

I've just written an overlay for fiat-parsers today, but it's breaking backwards compat so it'll need some tweak. Same problem for engine-bench, @Jason Gross wants it to be backwards compatible with quite old versions.


Last updated: Apr 18 2024 at 23:01 UTC