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.

[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-fiat_crypto_legacy, ci-http

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

[JasonGross]

@JasonGross fcl will need a bbv bump it seems.

dependabot + CI takes care of this automatically, cf mit-plv/fiat-crypto#2168. Or is there a bbv bump beyond this?

[ppedrot]

OK, then it should be fine.

[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.