ssr: skip impargs in pattern FO unif #20707
Conversation
|
@coqbot run full ci |
|
Great!!! There will be legitimate breakage! Maybe we need a flag ? |
|
🔴 CI failures at commit de05d31 without any failure in the test-suite ✔️ Corresponding jobs for the base commit cfa8967 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
FWIW, a quick look at mathcomp show 85 proofs requiring an update. |
016614c to
5559aa7
Compare
|
I'm still tweaking it, I have an overlay for mathcomp that should work. But there is one ugly thing that stays, eg |
|
On the positive side, most of the broken proof were bad ones, i.e. relying in some way on the FO pass to select "the wrong one". The only cases where now things are reversed are because of the behavior above, IIRC 2 occurrences in MC. |
|
@coqbot run full ci |
|
🔴 CI failures at commit 5559aa7 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 5e040b6 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
5559aa7 to
6a10c2d
Compare
|
@coqbot run full ci |
|
🔴 CI failures at commit 6a10c2d without any failure in the test-suite ✔️ Corresponding jobs for the base commit 4df59ab succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
This is an attempt to make changes in the algebraic hierarchy of mathcomp less painful.
When a structure s with op1 and op2 is broken into s1 with op1 and s2 with op2 it may be the case that lemmas involving both operations have a type like
forall i:sj, op1 i x (op2 i y) z = ..where an instance of the structure sj (join of s1 and s2) occurs non linearly. A concrete goal may have after the split the shapeop1 canon_s1_on_T x (op2 (sj_to_s2 canon_sj_on_T) y) zor something like that, while before both ops would have the same canonical instance on T (the type of x, y, z).Because of the 2 syntactically different instances the FO pass makes a different choice than before.
This PR tries to avoid breakage by making the FO pass ignore implicit arguments of constants, e.g. structure instances.
CC @CalosciMatteo @CohenCyril @Tragicus
make doc_gram_rsts.