Stream: Coq devs & plugin devs

Topic: Script for automatically addressing Coq warnings


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

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

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

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

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

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

view this post on Zulip Théo Zimmermann (Jan 31 2022 at 18:53):

Hugo Herbelin said:

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.

I think this would be awesome.

view this post on Zulip Paolo Giarrusso (Feb 01 2022 at 00:18):

Iris changelogs carry sed scripts for similar goals, but Hugo’s proposal could respect lexical binding :-)

view this post on Zulip Jason Gross (Feb 01 2022 at 20:13):

Hugo Herbelin said:

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?

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.

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

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

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

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

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