search

mit-plv / bbv

Bedrock Bit Vector Library
MIT License
27 stars 23 forks source link

Adapt w.r.t. coq/coq#16004. #40

Closed ppedrot closed 2 years ago

ppedrot commented 2 years ago

Should be backwards compatible.

JasonGross commented 2 years ago

This is not backwards compatible because Hint Rewrite did not support Global in 8.8, which Fiat Crypto legacy still supports. Is there a fix that is backwards compatible all the way to 8.7?

ppedrot commented 2 years ago

I am afraid not...

JasonGross commented 2 years ago

Why can't this error be turned back into a warning or suppressed by command-line flags?

JasonGross commented 2 years ago

Can we just disable the warning instead? And fix the imports when we need to in the future

ppedrot commented 2 years ago

I basically disagree with the disabling of warning. This is just hiding the problem, and it will explode at our face as soon as we switch the semantics of the default locality attribute of hints. I'd rather postpone the switch and / or apply political pressure on the devs that both want to be in the CI while retaining a broad backwards compatibility spectrum.

JasonGross commented 2 years ago

it will explode at our face as soon as we switch the semantics of the default locality attribute of hints. I'd rather [...] apply political pressure on the devs that both want to be in the CI while retaining a broad backwards compatibility spectrum.

Would you be satisfied with a PR that had all of our developments that disable the warning also pass -set 'Loose Hint Behavior "Strict"' on the command line (or otherwise set it in the relevant places)? If I understand correctly, this will make the developments compatible with switching the default behavior from Global to Export, right?

ppedrot commented 2 years ago

@JasonGross that's better than nothing, but it will require a lot of work while still being quite brittle. But I guess I'd be fine with this first step.

ppedrot commented 2 years ago

Same solution as the other devs, by deactivating the unsupported attributes we can go as far as 8.11. Would you be fine with that @JasonGross ?