Hugo Herbelin (Jan 31 2022 at 11:40): Hugo Herbelin (Jan 31 2022 at 11:40):Hi, let's assume I'd like to write a script that automatically address Coq warnings, such as Warning: The default value for instance locality is currently "local" in a section and "global" otherwise, but is scheduled to change in a future release. or Warning: Notation mult_comm is deprecated since 8.16. The Arith.Mult file is obsolete. Use Nat.mul_comm instead.
IIRC, there was a script at some time from Jason parsing make logs and modifying files in place. Should we extend this script so that it supports arbitrary warnings? Should we let Coq ouputs a file with specific "optimized" data indicating modifications to do to the files (say of the form: Replace chars YYY-ZZZ with STRING)?
Any idea?
Théo Zimmermann (Jan 31 2022 at 11:47):I think that there indeed exist scripts for the two particular examples that you gave. But indeed, making a generic framework for automatic fixing of warnings could be nice, but would probably require starting from scratch again.
Théo Zimmermann (Jan 31 2022 at 11:49):See https://github.com/coq/coq/issues/15030 / https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140 for references on the scripts for the first warning.
Théo Zimmermann (Jan 31 2022 at 11:50):See https://gist.github.com/JasonGross/9770653967de3679d131c59d42de6d17#file-replace-notations-py for the second warning (although it hasn't been tested for a while, I think).
Hugo Herbelin (Jan 31 2022 at 17:21):The Hint script does not rely on the Coq warning while it could. Relying on Coq warnings would prevent it wrongly adds #[global] for hints in section. Jason's script is nice but struggles a bit to find the warnings in the log. Any new warning dispatched over several lines may similarly requires special care.
My question was about the opportunity to output a file say foo.upgrade for all automatically addressable warnings/errors issued when compiling foo.v. The format of the file would be easy to parse.
Théo Zimmermann (Jan 31 2022 at 18:52):The Hint script does not rely on the Coq warning while it could.
There are several scripts AFAIR and at least one of them is relying on the warning (to produce better results).
Théo Zimmermann (Jan 31 2022 at 18:53):Hugo Herbelin said:
My question was about the opportunity to output a file say
foo.upgradefor all automatically addressable warnings/errors issued when compilingfoo.v. The format of the file would be easy to parse.
I think this would be awesome.
Paolo Giarrusso (Feb 01 2022 at 00:18):Iris changelogs carry sed scripts for similar goals, but Hugo’s proposal could respect lexical binding :-)
Jason Gross (Feb 01 2022 at 20:13):Hugo Herbelin said:
IIRC, there was a script at some time from Jason parsing
makelogs and modifying files in place. Should we extend this script so that it supports arbitrary warnings?
There's also https://github.com/JasonGross/coq-tools/blob/master/proof-using-helper.py worked on an old form of the proof using guidelines. The changelog points at fix.py which fixes numeral notations imports.
Jason Gross (Feb 01 2022 at 20:20):Jason's script is nice but struggles a bit to find the warnings in the log. Any new warning dispatched over several lines may similarly requires special care.
This is another problem that would be solved by https://github.com/coq/coq/issues/11953 / https://github.com/coq/coq/issues/14120 / https://github.com/coq/coq/pull/14724
Hugo Herbelin (Feb 02 2022 at 12:47):Probably too late to schedule this for the call today, but we may schedule it for next week? My primary (local) interest is to be able to easily adapt the CI to #14637 and if one of your scripts can do it easily, that'll be wonderful.
Jason Gross (Feb 02 2022 at 14:35):@Hugo Herbelin probably the scripts can be adapted to do that, though it might be nice to add a --replacement-format or something which emits messages such as "replace bytes n--m on line X with ..." which can then be uniformly handled by a script
Jason Gross (Feb 02 2022 at 14:38):However, I'm a bit concerned with that PR; IIRC, name was introduced after 8.11 (is that right?), which means Fiat Crypto can't use it without losing compatibility with Ubuntu LTS. I guess there we could start versioning the reserved Notation file if we have to, though.
Hugo Herbelin (Feb 02 2022 at 15:52):Jason Gross said:
However, I'm a bit concerned with that PR; IIRC, name was introduced after 8.11 (is that right?), which means Fiat Crypto can't use it without losing compatibility with Ubuntu LTS. I guess there we could start versioning the reserved Notation file if we have to, though.
This is another question I guess. That is, does the current policy for deprecation span over a long enough time?
Last updated: Jun 04 2023 at 19:30 UTC