Stop using auto with * in intuition solver.

[ppedrot]

This started to spit a warning from 8.17 onwards, it is probably time to get rid of this dubious behaviour.

Fixes #4949: [intuition] should not use [auto with *] by default.

Backwards compatible overlays:

• Adapt to rocq-prover/rocq#21129. mit-plv/bbv#54
• Adapt to rocq-prover/rocq#21129. rocq-community/coq-ext-lib#156
• Adapt to rocq-prover/rocq#21129. jwiegley/category-theory#165
• Adapt to rocq-prover/rocq#21129. smtcoq/smtcoq#156
• Adapt to rocq-prover/rocq#21129. rocq-community/math-classes#140
• Adapt to rocq-prover/rocq#21129. MetaRocq/metarocq#1206
• Adapt to rocq-prover/rocq#21129. mit-plv/fiat#125
• Adapt to rocq-prover/rocq#21129. rocq-community/corn#220
• Adapt to rocq-prover/rocq#21129. liyishuai/coq-http#7
• Adapt w.r.t. rocq-prover/rocq#21129. adampetcher/fcf#50
• Adapt to rocq-prover/rocq#21129. mit-plv/cross-crypto#41

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-bbv, ci-category_theory, ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-math_classes, ci-metarocq, ci-smtcoq

• You can also pass me a specific list of targets to minimize as arguments.

[ppedrot]

Non trivial amount of broken code, which was not totally unexpected. I guess someone will have to write overlays...

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-math_classes, ci-metarocq, ci-smtcoq

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-math_classes, ci-smtcoq

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-corn, ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-smtcoq

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-corn, ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy, ci-fiat_parsers

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-category_theory, ci-corn, ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy

• You can also pass me a specific list of targets to minimize as arguments.

[coqbot-app]

🔴 CI failures at commit c6cd7d6 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 17eccdd succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-cross_crypto, ci-ext_lib, ci-fiat_crypto_legacy

• You can also pass me a specific list of targets to minimize as arguments.

[ppedrot]

@JasonGross fcl will need a bbv bump it seems.

[ppedrot]

Fixing cross-crypto is a bit annoying. It depends on FCF which calls intuition auto with * a lot, and fixing the code takes some time. I've done a little bit already but if anybody wants to take the baton I wouldn't complain.

[SkySkimmer]

How annoying the fix is to make really depends on how precise you want it to be. In principle you could add at the beginning of every file

(* TODO stop using "with *" *)
Local Ltac intuition_solver ::= solve [auto with *].

and it should work.

[ppedrot]

Meh. Out of procrastination I started writing a script to parse the warning messages and autofix the issues.

[ppedrot]

Here is the fcf PR: adampetcher/fcf#50. It needs to be merged and then the corresponding submodule must be bumped in cross-crypto.

[ppedrot]

Modulo CI, this should be ready now.

[SkySkimmer]

@coqbot merge now

[Zimmi48]

Meh. Out of procrastination I started writing a script to parse the warning messages and autofix the issues.

Is your script reusable? Because in this case, you could put it in a gist, and advertise it in the changelog.

[ppedrot]

It's a bit too ad-hoc, I'm afraid.

[ppedrot]

For the record I did publish it as a gist, although I'm not sure it'll be of any use to somebody: https://gist.github.com/ppedrot/bd4af9aeb6855085527b21d99cd141d2

[Zimmi48]

This looks usable and useful. What about adding a direct link from the changelog entry to the gist?