Check guardedness of fixpoints also in erasable subterms by herbelin · Pull Request #15434 · rocq-prover/rocq

herbelin · 2022-01-04T20:09:20Z

Kind: Enhancement

We do that by splitting guard errors into two categories:

fatal recursive calls to non guarded arguments
recursive calls on descendants of variables bound in subterms of a redex and thus liable to be instantiated by reduction of the redex + not applied enough recursive calls which also may become enough applied after reduction.

We also maintain a stack of redexes so that when a variable is bound in the subterm of a redex, we directly know which redex needs to be reduced to trigger the instantiation of the variable.

In situations of the form C(if c then x else y) where x is a recursion variable, y needs the unfolding of a redex C[], we use a rich notion of subterm which remembers both that we need to reduce the redex to check a possible recursive call on y, but that we need to check that we don't also make a recursive call on x even w/o reducing the redex. So, the union of specifications of subterms of a match/if is now a set.

We are also more tolerant in subterms with recursive calls on internal uninstantiatable variables and on not applied enough recursive calls which cannot be applied more (e.g. Fixpoint foo (n : nat) := forall x : foo = foo, True).

For the beta and zeta-redex cases, we choose to check the argument for possibly fatal non guarded calls and reduce anyway. Another strategy could have been to reduce only when a subterm of the redex needs a reduction (but the stack call is then a bit complicated to manage).

Fixes #6487
Fixes #7061
Incidentally also fixes #5702 (reporting about a non-guarded fixpoint is exponential in the number of unfoldable constants encapsulating the illegal recursive call).

See examples in file test-suite/success/FixStronglyWf.v.

Added / updated test-suite.
Added changelog.

coqbot-app · 2022-01-04T20:55:37Z

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

coqbot-app · 2022-01-04T22:19:28Z

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

✔️ Corresponding jobs for the base commit 4d78b1f 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-compcert, ci-elpi, ci-equations, ci-fiat_crypto, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-hott, ci-iris, ci-itauto, ci-mtac2, ci-perennial, ci-verdi_raft, ci-vst

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

coqbot-app · 2022-01-04T22:19:38Z

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

✔️ Corresponding jobs for the base commit 4d78b1f 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-compcert, ci-elpi, ci-equations, ci-fiat_crypto, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-hott, ci-iris, ci-itauto, ci-mtac2, ci-perennial, ci-verdi_raft, ci-vst

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

coqbot-app · 2022-01-05T14:51:29Z

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

✔️ Corresponding jobs for the base commit 9dbb613 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-color, ci-compcert, ci-equations, ci-math_classes, ci-perennial, ci-rewriter, ci-sf

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

Alizter · 2022-01-05T16:36:57Z

    Fixpoint F (n : nat) (A : Type) {struct n} : nat
    with G (n : nat) (A:Type@{_})  {struct n} : nat.
    Proof.
-      1: pose (G n A).


Why is this no longer accepted?

I've noticed you've expanded a lot of these kinds of terms, that seems a bit strange. Were we doing something wrong before?

Yes, these examples were doing something "wrong" before: they were building fixpoints which were not strongly guarded! Their point was only to test #14057, not to be non-looping. I replaced them with strongly guarded tests (as was suggested in #14057 already).

coqbot-app · 2022-01-08T21:26:16Z

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

✔️ Corresponding jobs for the base commit 1b1206e 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-fiat_crypto, ci-itauto

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

coqbot-app · 2022-01-08T23:48:30Z

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

✔️ Corresponding job for the base commit 1b1206e succeeded

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

🏃 @coqbot ci minimize will minimize the following target: ci-fiat_crypto

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

herbelin · 2022-01-09T12:32:47Z

The failure in fiat-crypto is of the form:

Fixpoint f n :=
  match n with
  | 0 => 0
  | S n =>
      (fix aux n :=
       match n with
       | 0 => f n
       | S n => aux n
       end) (S n)
  end.

which indeed is not strongly normalizing (unless we decide that unfolding a fix automatically iota-reduce at the same time the match destructing the main argument of the fix).

coqbot-app · 2022-01-09T16:03:37Z

🔴 CI failure at commit 6e3757f without any failure in the test-suite

✔️ Corresponding job for the base commit bd6cead succeeded

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

🏃 @coqbot ci minimize will minimize the following target: ci-fiat_crypto

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

coqbot-app · 2022-01-09T16:13:40Z

🔴 CI failure at commit 6e3757f without any failure in the test-suite

✔️ Corresponding job for the base commit bd6cead succeeded

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

🏃 @coqbot ci minimize will minimize the following target: ci-fiat_crypto

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

mattam82 · 2022-01-10T10:26:02Z

@herbelin can you get around defining f this way in fiat_crypto?
It looks like a counterexample to normalization we didn't know of before: it's not about K redexes only in this case.
Or we should "generalize" the notion of K redex to match.

The example currently guard checks because it reduces the definition to:

Fixpoint f n :=
  match n with
  | 0 => 0
  | S n =>
     let aux :=
      (fix aux n :=
       match n with
       | 0 => f n
       | S n => aux n
       end)
   in aux n
  end.

Right?

herbelin · 2022-01-10T11:52:41Z

@herbelin can you get around defining f this way in fiat_crypto?

I did not try yet, but yes, one could certainly unroll the loop one step further (as you did in your redefinition of f) to avoid the non strongly normalizing subterm.

It looks like a counterexample to normalization we didn't know of before: it's not about K redexes only in this case. Or we should "generalize" the notion of K redex to match.

I think so, yes, the notion of K-redex / erasable-subterm should be generalized to match.

herbelin · 2022-01-13T11:58:16Z

@ppedrot: you mentioned a slow guard checking at Qed time in a file called Wf.v. I suspect you referred to wf_eval_decision_tree' in file Rewriter/Wf.v from mit-plv/rewriter. Then, it goes down from 26s to 10s.

herbelin · 2022-01-13T12:07:23Z

Bench did not go the end. Before failing on installing the fiat-crypto overlay it gave:

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┬─────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]   │   mem faults    │
│                             │                         │                                       │                                       │                          │                 │
│                package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD   PDIFF │ NEW  OLD  PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼──────────────────────────┼─────────────────┤
│                coq-rewriter │  358.62   371.29  -3.41 │  1636427056509   1691600912742  -3.26 │  2669968690793   2770468196822  -3.63 │  983832  1066328   -7.74 │   0    0    nan │
│ coq-rewriter-perf-SuperFast │  903.28   913.80  -1.15 │  4126710222592   4170523022917  -1.05 │  7091674435212   7191461785419  -1.39 │ 1113948  1113568    0.03 │   0    0    nan │
│                  coq-stdlib │  402.10   404.10  -0.49 │  1659638143436   1668249743563  -0.52 │  1444968115091   1445186017153  -0.02 │  591772   590620    0.20 │   0    0    nan │
│               coq-fourcolor │ 1463.58  1469.32  -0.39 │  6681549713754   6704198874745  -0.34 │ 12083100093250  12082757172741   0.00 │  724636   725992   -0.19 │   0    0    nan │
│                  coq-geocoq │  714.14   716.90  -0.38 │  3256202120910   3269995293586  -0.42 │  5156947754508   5156847865187   0.00 │  978424   979164   -0.08 │   0    0    nan │
│              coq-verdi-raft │  576.11   576.80  -0.12 │  2630890515953   2633900124235  -0.11 │  4042478953249   4042624706833  -0.00 │ 1216612  1218664   -0.17 │   0    0    nan │
│       coq-mathcomp-solvable │   87.29    87.29   0.00 │   399573723441    399324043862   0.06 │   612138597498    612160527068  -0.00 │  668676   671828   -0.47 │   0    0    nan │
│                 coq-unimath │ 3638.88  3638.47   0.01 │ 16644757778776  16642359019802   0.01 │ 33136938043120  33137749079196  -0.00 │ 3903996  3903380    0.02 │   0    0    nan │
│                 coq-coqutil │   34.51    34.49   0.06 │   155935955672    155527169958   0.26 │   208193119534    208137937175   0.03 │  601220   599408    0.30 │   0    0    nan │
│                    coq-corn │  794.46   793.96   0.06 │  3623699628119   3619421623328   0.12 │  5586844250879   5586237534657   0.01 │  875616   876560   -0.11 │   0    0    nan │
│           coq-iris-examples │  460.56   460.06   0.11 │  2099685088869   2096266543701   0.16 │  3137498459404   3137635843448  -0.00 │ 1181004  1184796   -0.32 │   0    0    nan │
│                    coq-core │   95.53    95.42   0.12 │   389801313546    386233717391   0.92 │   433214398021    433038564565   0.04 │  250160   248844    0.53 │   0    0    nan │
│            coq-fiat-parsers │  328.22   327.53   0.21 │  1479749036166   1475418536829   0.29 │  2422503699594   2421671700977   0.03 │ 2789584  2791128   -0.06 │   0    0    nan │
│               coq-perennial │ 4097.63  4085.96   0.29 │ 18717140514572  18658942438968   0.31 │ 30710701029107  30682024022009   0.09 │ 2596384  2598516   -0.08 │   0    0    nan │
│       coq-mathcomp-fingroup │   23.30    23.21   0.39 │   106241084743    106030661581   0.20 │   155230839126    155223010422   0.01 │  483612   477908    1.19 │   0    0    nan │
│                   coq-verdi │   47.97    47.76   0.44 │   217435455005    217257113721   0.08 │   323004290402    323096280292  -0.03 │  825008   826124   -0.14 │   0    0    nan │
│                coq-bedrock2 │  188.11   187.25   0.46 │   858345427153    854486938150   0.45 │  1573282085730   1573908289584  -0.04 │ 2053824  2053828   -0.00 │   1    0    nan │
│      coq-mathcomp-odd-order │  560.38   557.67   0.49 │  2567640194903   2555651121658   0.47 │  4309449635755   4309338779910   0.00 │  933536   931264    0.24 │   0    0    nan │
│                    coq-hott │  153.16   152.34   0.54 │   693571891537    688638131567   0.72 │  1077417393118   1075371537786   0.19 │  656044   659820   -0.57 │   0    0    nan │
│                 coq-bignums │   28.33    28.17   0.57 │   129308460314    128576245873   0.57 │   175959350605    175945171332   0.01 │  468868   468836    0.01 │   0    0    nan │
│              coq-coquelicot │   34.41    34.18   0.67 │   154983483573    153587106818   0.91 │   201346897233    201316591023   0.02 │  749316   753172   -0.51 │   4    0    nan │
│      coq-mathcomp-character │   76.54    76.00   0.71 │   350032678789    347643591252   0.69 │   527756076551    527784539443  -0.01 │  729812   729260    0.08 │   0    0    nan │
│                  coq-flocq3 │   76.07    75.39   0.90 │   345787286608    343826000420   0.57 │   455001209538    454978563067   0.00 │  988876   991880   -0.30 │   9    0    nan │
│        coq-mathcomp-algebra │   63.59    63.02   0.90 │   290276989679    288545651646   0.60 │   399104446331    399066054039   0.01 │  559064   563348   -0.76 │   0    0    nan │
│                   coq-color │  265.41   262.96   0.93 │  1205073435436   1192688116453   1.04 │  1608613910368   1598793261047   0.61 │ 1147064  1144948    0.18 │   0    0    nan │
│                     coq-vst │ 1155.24  1144.09   0.97 │  5270877370553   5221537247836   0.94 │  8514335134655   8408159229300   1.26 │ 1895500  1893680    0.10 │   0    0    nan │
│          coq-mathcomp-field │  113.95   112.85   0.97 │   521794006578    517178356772   0.89 │   851258690362    851295619716  -0.00 │  661780   661512    0.04 │   0    0    nan │
│                coq-compcert │  291.30   288.37   1.02 │  1322293426195   1309716455168   0.96 │  1955517710881   1943920648914   0.60 │ 1097780  1097180    0.05 │   0    0    nan │
│      coq-mathcomp-ssreflect │   25.94    25.64   1.17 │   118082193935    116348851371   1.49 │   147509736678    147491630213   0.01 │  531384   533628   -0.42 │   0    0    nan │
│  coq-performance-tests-lite │  782.24   772.69   1.24 │  3550968903345   3508062891532   1.22 │  5957180866065   5959968572598  -0.05 │ 1630556  1826268  -10.72 │   3    0    nan │
│            coq-math-classes │   94.06    92.87   1.28 │   427271298110    421509297941   1.37 │   591638507418    591606722532   0.01 │  495976   495784    0.04 │   0    0    nan │
│       coq-engine-bench-lite │  177.85   175.56   1.30 │   771586793088    759270754985   1.62 │  1488681974622   1485309727285   0.23 │ 1175656  1173992    0.14 │   0    0    nan │
│               coq-fiat-core │   54.20    53.12   2.03 │   236012566537    232480730914   1.52 │   323947407951    323969797432  -0.01 │  473824   473760    0.01 │   0    0    nan │
│                coq-coqprime │  181.74   176.37   3.04 │   831126858102    806950465188   3.00 │  1559806241915   1559766138767   0.00 │  855940   856356   -0.05 │   0    0    nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴─────────────────┘

Should we investigate more what happens in e.g. fiat-core or coq-performance-tests-lite? (And if yes, what are the best tools to investigate?)

SkySkimmer · 2022-01-13T12:10:02Z

Before failing on installing the fiat-crypto overlay

The bench doesn't use overlays, you have to upstream it to bench it.

…subterms, Checking guard in previously ignored erasable or inert subterms of fixpoints. We do that by splitting guard errors into categories: - fatal recursive calls to non guarded arguments - recursive calls on descendants of variables bound in subterms of a redex and thus liable to be instantiated by reduction of the redex + not applied enough recursive calls which also may become enough applied after reduction. We also maintain a stack of redexes so that when a variable is bound in the subterm of a redex, we directky know which redex needs to be reduced to trigger the instantiation of the variable. In situations of the form "C(if c then x else y)" where x is a recursion variable, y needs the unfolding of a redex C[], we use a rich notion of subterm which remembers both that we need to reduce the redex to check a possible recursive call on y, but that we need to check that we don't also make a recursive call on x even w/o reducing the redex. So, the union of specifications of subterms of a match/if is now a set. For the beta and zeta-redex cases, we choose to check the argument for possibly fatal non guarded calls and reduce anyway. Another strategy could have been to reduce only when a subterm of the redex needs a reduction (but the stack call is then a bit complicated to manage). Note: We could have been more tolerant in subterms with recursive calls on internal uninstantiatable variables and on not applied enough recursive calls which cannot be applied more (e.g. "Fixpoint foo (n : nat) := forall x : foo = foo, True"). To accept these calls, "check_erasable_inert_subterm_rec_call" should be renamed into "check_inert_subterm_rec_call" to emphasize that it becomes more general and checks in types (Ind, Prod, types in Fix/Cofix/Lambda/Array) should call it in place of "check_rec_call".

Indeed, if the "match" needs to be reduced but its argument is not a constructor, it can eventually be reduced by any arbitrary term and there is no hope to be guarded at all, even by reducing outer redexes.

ppedrot · 2022-04-09T11:16:39Z

@herbelin I took the liberty to rebase the PR myself.

ppedrot · 2022-04-09T11:17:18Z

@coqbot bench

coqbot-app · 2022-04-10T01:44:41Z

🏁 Bench results:

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬───────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │    mem faults     │
│                             │                         │                                       │                                       │                         │                   │
│        package_name         │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │ NEW  OLD   PDIFF  │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼───────────────────┤
│                coq-rewriter │  365.49   397.08  -7.96 │  1596265247769   1732791369230  -7.88 │  2575410421604   2760320615955  -6.70 │  983668  1060384  -7.23 │   7    5    40.00 │
│ coq-rewriter-perf-SuperFast │  964.52   996.87  -3.25 │  4219641378025   4359711504008  -3.21 │  7067455556278   7251212113272  -2.53 │ 1136908  1144724  -0.68 │   0    0      nan │
│                  coq-stdlib │  451.25   457.36  -1.34 │  1568318651660   1582407967760  -0.89 │  1416189564732   1426467024014  -0.72 │  632688   625880   1.09 │   0    0      nan │
│           coq-iris-examples │  432.41   435.85  -0.79 │  1888853435616   1903991110783  -0.80 │  2834316225045   2834802122849  -0.02 │ 1183764  1183416   0.03 │   0    0      nan │
│     coq-metacoq-safechecker │  167.46   168.70  -0.74 │   730015442213    735329412142  -0.72 │   953842496395    957140110299  -0.34 │ 1206820  1204108   0.23 │   1    7   -85.71 │
│         coq-metacoq-erasure │   62.23    62.63  -0.64 │   266677561277    268525983320  -0.69 │   393082150919    393176854971  -0.02 │ 1099932  1085400   1.34 │   0    0      nan │
│                coq-compcert │  291.80   293.62  -0.62 │  1268707573606   1275986843362  -0.57 │  1872093106608   1870429949267   0.09 │ 1106888  1106056   0.08 │   0   13  -100.00 │
│              coq-verdi-raft │  583.31   586.48  -0.54 │  2547739122842   2561164345399  -0.52 │  3900854120570   3902127966092  -0.03 │ 1228092  1226768   0.11 │   0    0      nan │
│               coq-perennial │ 4191.37  4211.93  -0.49 │ 18336481941730  18421099584543  -0.46 │ 29868973633305  29868011787534   0.00 │ 2609428  2609248   0.01 │   0    0      nan │
│                coq-bedrock2 │  395.57   397.50  -0.49 │  1731270397020   1739777343430  -0.49 │  3259976711272   3260694792220  -0.02 │ 2051952  2052036  -0.00 │   6    1   500.00 │
│           coq-metacoq-pcuic │  558.38   560.32  -0.35 │  2440158256037   2447244928959  -0.29 │  3377089028297   3378263639274  -0.03 │ 1490516  1490656  -0.01 │  10   21   -52.38 │
│          coq-mathcomp-field │  104.20   104.54  -0.33 │   456140871153    457620938388  -0.32 │   738515748958    738556605942  -0.01 │  708404   708476  -0.01 │   0    0      nan │
│        coq-metacoq-template │   80.63    80.87  -0.30 │   344591425250    345715079087  -0.33 │   506284564502    506242499979   0.01 │  911600   911720  -0.01 │  12    3   300.00 │
│      coq-mathcomp-character │   70.91    71.12  -0.30 │   310383375652    311430353660  -0.34 │   464337426263    464399875973  -0.01 │  829688   831684  -0.24 │   0    0      nan │
│               coq-fourcolor │ 1551.30  1554.80  -0.23 │  6797487344376   6813389831834  -0.23 │ 12067879208066  12068354130278  -0.00 │  790064   790068  -0.00 │   0    0      nan │
│  coq-performance-tests-lite │  828.25   830.05  -0.22 │  3606986427019   3615412143592  -0.23 │  5993442250858   5992881113290   0.01 │ 1824440  1824544  -0.01 │   0    0      nan │
│       coq-mathcomp-solvable │   84.39    84.56  -0.20 │   369406665176    370142719282  -0.20 │   554989029756    555225450713  -0.04 │  667968   665172   0.42 │   0    0      nan │
│                  coq-flocq3 │   80.59    80.71  -0.15 │   350739372619    351121676109  -0.11 │   456399154189    456506597932  -0.02 │  993220   991476   0.18 │   0    0      nan │
│                     coq-vst │ 1242.32  1242.64  -0.03 │  5430517370818   5434181855309  -0.07 │  8528351745129   8515041500113   0.16 │ 2027976  2027280   0.03 │   1    0      nan │
│    coq-metacoq-translations │   21.23    21.23   0.00 │    92352098276     92219961227   0.14 │   154791909085    155117097884  -0.21 │  920252   920176   0.01 │   0    0      nan │
│                 coq-bignums │   29.39    29.38   0.03 │   128131689266    128183077902  -0.04 │   172304511296    172296644245   0.00 │  469172   468088   0.23 │   0    0      nan │
│      coq-mathcomp-ssreflect │   26.18    26.17   0.04 │   114067276539    113606165251   0.41 │   139670575932    139603419915   0.05 │  538760   537252   0.28 │   0    0      nan │
│                   coq-verdi │   48.85    48.83   0.04 │   211970594904    212538139735  -0.27 │   311819382260    311843627755  -0.01 │  836884   838404  -0.18 │   0    0      nan │
│                    coq-corn │  801.81   801.41   0.05 │  3500490935735   3499936309528   0.02 │  5295384281093   5295376548067   0.00 │  880528   880240   0.03 │   0    0      nan │
│            coq-fiat-parsers │  352.78   352.60   0.05 │  1525066741557   1523879501275   0.08 │  2435829969591   2436224972524  -0.02 │ 3042600  3042660  -0.00 │   0    2  -100.00 │
│               coq-fiat-core │   58.07    58.04   0.05 │   240363320186    239643637311   0.30 │   330889877494    330852983990   0.01 │  480260   481480  -0.25 │   5    0      nan │
│                  coq-geocoq │  737.96   737.55   0.06 │  3221061244666   3220415913556   0.02 │  4989483335359   4989709049199  -0.00 │ 1075012  1075316  -0.03 │   3   16   -81.25 │
│        coq-mathcomp-algebra │   61.41    61.37   0.07 │   268885971817    268432334227   0.17 │   359275651380    359185301054   0.03 │  594240   595428  -0.20 │   0    0      nan │
│                coq-coqprime │   45.27    45.24   0.07 │   196512089892    196328908161   0.09 │   284625455644    284656872020  -0.01 │  763728   761816   0.25 │   0    0      nan │
│            coq-math-classes │   96.10    95.95   0.16 │   417135553761    417022540728   0.03 │   575207240445    575249639760  -0.01 │  502076   501996   0.02 │   0    0      nan │
│                   coq-color │  226.35   225.98   0.16 │   982021268120    982032308126  -0.00 │  1364297596245   1362349975216   0.14 │ 1232548  1232548   0.00 │   4    4     0.00 │
│                 coq-unimath │ 4938.57  4928.77   0.20 │ 21627181194063  21586105227216   0.19 │ 42088098633195  42088397314789  -0.00 │ 3259116  3259092   0.00 │   1    0      nan │
│                    coq-hott │  171.95   171.55   0.23 │   745974238538    745097306164   0.12 │  1160827639098   1160558112121   0.02 │  623432   623316   0.02 │   0    0      nan │
│              coq-coquelicot │   34.99    34.90   0.26 │   150760516112    150878012711  -0.08 │   194663255471    194665490201  -0.00 │  754452   754392   0.01 │  22    0      nan │
│      coq-mathcomp-odd-order │  557.76   556.27   0.27 │  2444255880755   2438184480229   0.25 │  4079400681443   4079517908311  -0.00 │ 1210280  1210284  -0.00 │   0    0      nan │
│                    coq-core │  116.86   116.45   0.35 │   407354653640    407109983150   0.06 │   441768406630    441855812886  -0.02 │  280756   280608   0.05 │   0    0      nan │
│       coq-engine-bench-lite │  186.89   186.23   0.35 │   790590987090    788067854378   0.32 │  1481161320033   1478927370515   0.15 │ 1198176  1197996   0.02 │   0    0      nan │
│       coq-mathcomp-fingroup │   22.76    22.67   0.40 │    98909270969     98936911969  -0.03 │   140226046588    140230205801  -0.00 │  486884   487992  -0.23 │   0    0      nan │
│                 coq-coqutil │   37.21    36.99   0.59 │   160369821450    159385583404   0.62 │   211596488304    211615895981  -0.01 │  604620   604388   0.04 │   4    4     0.00 │
│         coq-category-theory │ 1750.74  1736.17   0.84 │  7668146857184   7603983830481   0.84 │ 15696916279230  15696949154965  -0.00 │ 1499596  1499560   0.00 │   0    0      nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴───────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                        │
│   OLD      NEW     DIFF    %DIFF     Ln                    FILE                                                                        │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 49.4500  51.1120  1.6620     3.36%    57  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                         │
│  3.2090   4.0800  0.8710    27.14%   152  coq-vst/veric/binop_lemmas2.v.html                                                           │
│  2.8130   3.4250  0.6120    21.76%  1017  coq-vst/veric/expr_lemmas.v.html                                                             │
│  0.3930   0.8150  0.4220   107.38%   281  coq-vst/veric/Clight_mem_lessdef.v.html                                                      │
│ 16.1670  16.5560  0.3890     2.41%   320  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 18.7830  19.1560  0.3730     1.99%   271  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 13.8280  14.1810  0.3530     2.55%    65  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                         │
│ 45.1970  45.5080  0.3110     0.69%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                   │
│  0.0150   0.3080  0.2930  1953.33%  1005  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html                    │
│ 19.4270  19.6880  0.2610     1.34%   237  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 16.5460  16.7980  0.2520     1.52%   251  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 20.3660  20.6180  0.2520     1.24%   773  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 15.9440  16.1800  0.2360     1.48%   132  coq-category-theory/Functor/Strong/Product.v.html                                            │
│ 10.7250  10.9600  0.2350     2.19%   289  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 29.7670  30.0020  0.2350     0.79%  1938  coq-unimath/UniMath/Bicategories/MonoidalCategories/ActionBasedStrongFunctorsMonoidal.v.html │
│ 67.5640  67.7960  0.2320     0.34%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                 │
│ 39.3500  39.5810  0.2310     0.59%   445  coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html                                   │
│ 12.4070  12.6240  0.2170     1.75%   717  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│  2.6100   2.8230  0.2130     8.16%   851  coq-category-theory/Functor/Construction/Product/Monoidal.v.html                             │
│ 63.0330  63.2450  0.2120     0.34%   641  coq-unimath/UniMath/SubstitutionSystems/LiftingInitial_alt.v.html                            │
│ 25.0140  25.2240  0.2100     0.84%   287  coq-unimath/UniMath/Bicategories/MonoidalCategories/Actions.v.html                           │
│  9.4080   9.6170  0.2090     2.22%   297  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│ 18.0680  18.2640  0.1960     1.08%   526  coq-unimath/UniMath/SubstitutionSystems/MonadsFromSubstitutionSystems.v.html                 │
│ 10.1970  10.3870  0.1900     1.86%   226  coq-category-theory/Construction/Comma/Adjunction.v.html                                     │
│  8.7190   8.9090  0.1900     2.18%    70  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                         │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│   OLD       NEW       DIFF     %DIFF    Ln                    FILE                                                                     │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  31.3730    1.3450  -30.0280  -95.71%   510  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                               │
│  31.1390    1.3060  -29.8330  -95.81%   510  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                              │
│  99.5340   98.3820   -1.1520   -1.16%   803  coq-vst/veric/binop_lemmas4.v.html                                                        │
│  45.8460   44.7230   -1.1230   -2.45%   235  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│  41.0340   40.2650   -0.7690   -1.87%   520  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html                      │
│ 139.0620  138.3440   -0.7180   -0.52%   706  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                               │
│   2.1320    1.4980   -0.6340  -29.74%   321  coq-rewriter/src/Rewriter/Rewriter/InterpProofs.v.html                                    │
│   2.1290    1.5250   -0.6040  -28.37%   321  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/InterpProofs.v.html                     │
│  24.1320   23.6570   -0.4750   -1.97%   828  coq-vst/veric/binop_lemmas2.v.html                                                        │
│  48.9620   48.5530   -0.4090   -0.84%   578  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                           │
│ 127.0520  126.7030   -0.3490   -0.27%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│  27.9950   27.6660   -0.3290   -1.18%    10  coq-fourcolor/theories/job486to489.v.html                                                 │
│  33.2520   32.9490   -0.3030   -0.91%    10  coq-fourcolor/theories/job563to588.v.html                                                 │
│   0.3520    0.0540   -0.2980  -84.66%  1005  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html                 │
│  29.0120   28.7150   -0.2970   -1.02%    10  coq-fourcolor/theories/job291to294.v.html                                                 │
│  30.8110   30.5180   -0.2930   -0.95%    10  coq-fourcolor/theories/job531to534.v.html                                                 │
│  43.9650   43.6890   -0.2760   -0.63%   222  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html            │
│  30.6190   30.3520   -0.2670   -0.87%    10  coq-fourcolor/theories/job611to617.v.html                                                 │
│   0.3020    0.0430   -0.2590  -85.76%   165  coq-metacoq-safechecker/safechecker/theories/PCUICErrors.v.html                           │
│  34.2050   33.9500   -0.2550   -0.75%    10  coq-fourcolor/theories/job589to610.v.html                                                 │
│  34.8500   34.6000   -0.2500   -0.72%    10  coq-fourcolor/theories/job323to383.v.html                                                 │
│ 127.0640  126.8390   -0.2250   -0.18%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│  36.1910   35.9750   -0.2160   -0.60%    10  coq-fourcolor/theories/job254to270.v.html                                                 │
│  13.2000   12.9870   -0.2130   -1.61%  1715  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                       │
│  56.9760   56.7740   -0.2020   -0.35%   857  coq-unimath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v.html        │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

coqbot-app · 2022-04-10T01:44:45Z

🔴 CI failure at commit 17ade41 without any failure in the test-suite

✔️ Corresponding job for the base commit be7781b succeeded

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

🏃 @coqbot ci minimize will minimize the following target: ci-fiat_crypto

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

Alizter · 2022-04-10T08:28:48Z

@coqbot ci minimize ci-fiat_crypto

coqbot-app · 2022-04-10T08:28:55Z

I am now running minimization at commit 17ade41 on requested target ci-fiat_crypto. I'll come back to you with the results once it's done.

coqbot-app · 2022-04-10T08:51:15Z

Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src/Util/ListUtil.v (from ci-fiat_crypto) (full log on GitHub Actions)

We are collecting data on the user experience of the Coq Bug Minimizer.
If you haven't already filled the survey for this PR, please fill out our short survey!

Minimized Coq File (consider adding this file to the test-suite)

(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive" "-w" "-notation-overridden,-undeclared-scope,-deprecated-hint-rewrite-without-locality,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths" "-w" "-deprecated-native-compiler-option" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src" "Crypto" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src/Rupicola" "Rupicola" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2" "bedrock2" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples" "bedrock2Examples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler" "compiler" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compilerExamples" "compilerExamples" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv" "riscv" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Bignums" "Bignums" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Coqprime" "Coqprime" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Rewriter" "Rewriter" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src" "-top" "ListUtil" "-native-compiler" "ondemand") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 3112 lines to 25 lines, then from 30 lines to 26 lines *)
(* coqc version 8.16+alpha compiled with OCaml 4.13.0
   coqtop version runner-nthfetyx-project-6138686-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at 19a6ae0) (19a6ae06ebc93ba02c6183df9ce9cecb197c655c)
   Expected coqc runtime on this file: 0.191 sec *)
Require Coq.Lists.List.

Import Coq.Lists.List.
Import ListNotations.

Definition span_cps' {A} (f : A -> bool) {T} (k : list A * list A -> T)
  := fix span_cps' (ls : list A) (prefix : list A) : T
    := match ls with
       | nil => k (List.rev prefix, nil)
       | x :: xs => if f x then span_cps' xs (x :: prefix) else k (List.rev prefix, ls)
       end.

Definition groupBy' {A} (f : A -> A -> bool)
  := fix groupBy' (ls : list A) (prefix : list A) : list (list A)
    := match ls with
       | [] => []
       | x :: xs => span_cps'
                      (f x) (fun '(xs, ys)
                             => (x :: xs) :: match ys with
                                             | [] => []
                                             | _ => groupBy' ys []
                                             end)
                      xs prefix
       end.

Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)

Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 6.7MiB file on GitHub Actions Artifacts under build.log)

uilds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src
MINIMIZER_DEBUG: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola
MINIMIZER_DEBUG: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig --print-version 
COQC src/Util/ListUtil.v
MINIMIZER_DEBUG: /github/workspace/builds/coq/coq-failing/_install_ci/bin//coqc
MINIMIZER_DEBUG: coqpath: COQPATH=/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src:/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src
MINIMIZER_DEBUG: pwd: PWD=/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto
MINIMIZER_DEBUG: exec: /github/workspace/builds/coq/coq-failing/_install_ci/bin/coqc.orig -q -w +implicit-core-hint-db\,+implicits-in-term\,+non-reversible-notation\,+deprecated-intros-until-0\,+deprecated-focus\,+unused-intro-pattern\,+variable-collision\,+omega-is-deprecated\,+deprecated-instantiate-syntax\,+non-recursive -w -notation-overridden\,-undeclared-scope\,-deprecated-hint-rewrite-without-locality\,-deprecated-hint-constr\,-fragile-hint-constr\,-native-compiler-disabled\,-ambiguous-paths -w -deprecated-native-compiler-option -native-compiler ondemand -R /github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto/src Crypto src/Util/ListUtil.v 
File "./src/Util/ListUtil.v", line 199, characters 27-39:
Warning: Notation lt_irrefl is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 199, characters 43-57:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 199, characters 27-39:
Warning: Notation lt_irrefl is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.lt_irrefl instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 199, characters 43-57:
Warning: Notation le_lt_trans is deprecated since 8.16.
The Arith.Lt file is obsolete. Use Nat.le_lt_trans instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 202, characters 32-46:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 202, characters 32-46:
Warning: Notation le_lt_or_eq is deprecated since 8.16.
The Arith.Lt file is obsolete. Use the bidirectional version Nat.lt_eq_cases instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 253, characters 38-47:
Warning: Notation le_n_0_eq is deprecated since 8.16.
The Arith.Le file is obsolete. Use the bidirectional version Nat.le_0_r (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 253, characters 38-47:
Warning: Notation le_n_0_eq is deprecated since 8.16.
The Arith.Le file is obsolete. Use the bidirectional version Nat.le_0_r (with symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 265, characters 76-85:
Warning: Notation minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 265, characters 76-85:
Warning: Notation minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 265, characters 76-85:
Warning: Notation minus_n_O is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_0_r (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 274, characters 44-62:
Warning: Notation minus_diag_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 274, characters 44-62:
Warning: Notation minus_diag_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 274, characters 44-62:
Warning: Notation minus_diag_reverse is deprecated since 8.16.
The Arith.Minus file is obsolete. Use Nat.sub_diag (and symmetry of equality) instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 358, characters 0-30:
Warning: The default value for hint locality is currently "local" in a
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding hints outside of sections without
specifying an explicit locality attribute is therefore deprecated. It is
recommended to use "export" whenever possible. Use the attributes #[local],
#[global] and #[export] depending on your choice. For example: "#[export]
Hint Unfold foo : bar." [deprecated-hint-without-locality,deprecated]
File "./src/Util/ListUtil.v", line 1369, characters 48-59:
Warning: Tactic instantiate is deprecated since 8.16.
[deprecated-tactic,deprecated]
File "./src/Util/ListUtil.v", line 1509, characters 8-27:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 1509, characters 8-27:
Warning: Notation Min.min_case_strong is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_case_strong instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 2002, characters 14-23:
Warning: Notation Min.min_l is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 2002, characters 14-23:
Warning: Notation Min.min_l is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 2002, characters 14-23:
Warning: Notation Min.min_l is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 2002, characters 14-23:
Warning: Notation Min.min_l is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 2002, characters 14-23:
Warning: Notation Min.min_l is deprecated since 8.16.
The Arith.Min file is obsolete. Use Nat.min_l instead.
[deprecated-syntactic-definition,deprecated]
File "./src/Util/ListUtil.v", line 2902, characters 5-452:
Error: Cannot guess decreasing argument of fix.

Command exited with non-zero status 1
src/Util/ListUtil.vo (real: 4.35, user: 4.21, sys: 0.13, mem: 491544 ko)
Makefile.coq:790: recipe for target 'src/Util/ListUtil.vo' failed
make[1]: *** [src/Util/ListUtil.vo] Error 1
make[1]: Leaving directory '/github/workspace/builds/coq/coq-failing/_build_ci/fiat_crypto'
Makefile.ci:128: recipe for target 'ci-fiat_crypto' failed
make: *** [ci-fiat_crypto] Error 2
/github/workspace/builds/coq /github/workspace
::endgroup::

Minimization Log (truncated to last 8.0KiB; full 61KiB file on GitHub Actions Artifacts under bug.log)

rkspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src -R /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/src Crypto -Q /github/workspace/cwd Top -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src/coqutil coqutil -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/src/Rupicola Rupicola -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2 bedrock2 -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src/bedrock2Examples bedrock2Examples -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compiler compiler -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src/compilerExamples compilerExamples -Q /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv riscv -Q /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Bignums Bignums -Q /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Coqprime Coqprime -Q /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Ltac2 Ltac2 -Q /github/workspace/builds/coq/coq-passing/_install_ci/lib/coq/user-contrib/Rewriter Rewriter -I /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/coqutil/src -I /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/src -I /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/bedrock2/src -I /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/compiler/src -I /github/workspace/builds/coq/coq-passing/_build_ci/fiat_crypto/rupicola/bedrock2/deps/riscv-coq/src -arg -q -arg -w -arg +implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive -arg -w -arg -notation-overridden,-undeclared-scope,-deprecated-hint-rewrite-without-locality,-deprecated-hint-constr,-fragile-hint-constr,-native-compiler-disabled,-ambiguous-paths -arg -w -arg -deprecated-native-compiler-option -arg -native-compiler -arg ondemand bug_01.v
getting Makefilexoyza3b1.coq (/github/workspace/cwd/Makefilexoyza3b1.coq)
make -k -f Makefilexoyza3b1.coq bug_01.glob
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
getting bug_01.glob (/github/workspace/cwd/bug_01.glob)
�[92m
Succeeded in normalizing Requires.�[0m

Now, I will attempt to split up [Require] statements...
getting /github/workspace/cwd/bug_01.v
NOTE: The file /github/workspace/cwd/bug_01.v is very new (1649580670, 0 seconds old), delaying until it's a bit older
getting /github/workspace/cwd/bug_01.glob
getting /github/workspace/cwd/bug_01.glob

No Requires to split.

In order to efficiently manipulate the file, I have to break it into statements.  I will attempt to do this by matching on periods.
�[92m
Splitting successful.�[0m

I will now attempt to remove any lines after the line which generates the error.

No lines to trim.

In order to efficiently manipulate the file, I have to break it into definitions.  I will now attempt to do this.
Sending statements to coqtop...
Done.  Splitting to definitions...
�[92m
Splitting to definitions successful.�[0m

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Qed Obligation with Admit Obligations
�[92m
Admitting Qed Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qed Obligations unsuccessful.
No successful changes.

I will now attempt to replace Qeds with Admitteds
�[92m
Admitting Qeds successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to replace Qeds with admit. Defined.
�[92m
Admitting Qeds successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Qeds unsuccessful.
No successful changes.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to admit [abstract ...]s
�[92m
Admitting [abstract ...] successful.�[0m
�[92m
Admitting [abstract ...] successful.�[0m
Admitting [abstract ...] unsuccessful.
Admitting [abstract ...] unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to replace Obligation with Admit Obligations
�[92m
Admitting Obligations successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting Obligations unsuccessful.
No successful changes.

I will now attempt to admit lemmas with Admitted
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with Admitted
�[92m
Admitting definitions successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to admit lemmas with admit. Defined
�[92m
Admitting lemmas successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting lemmas unsuccessful.
No successful changes.

I will now attempt to admit definitions with admit. Defined
�[92m
Admitting definitions successful.�[0m
Failed to do everything at once; trying one at a time.
Admitting definitions unsuccessful.
No successful changes.

I will now attempt to export modules
Module exportation unsuccessful.

I will now attempt to split imports and exports
Import/Export splitting unsuccessful.

I will now attempt to split := definitions
One-line definition splitting unsuccessful.

I will now attempt to remove all lines, one at a time
Line removal unsuccessful.

I will now attempt to remove goals ending in [Abort.]
�[92m
Aborted removal successful.�[0m

I will now attempt to remove unused Ltacs
�[92m
Ltac removal successful.�[0m

I will now attempt to remove unused definitions
�[92m
Definition removal successful.�[0m

I will now attempt to remove unused non-instance, non-canonical structure definitions
�[92m
Non-instance definition removal successful.�[0m

I will now attempt to remove unused variables
�[92m
Variable removal successful.�[0m

I will now attempt to remove unused contexts
�[92m
Context removal successful.�[0m

I will now attempt to remove empty sections

No empty sections to remove.

Now, I will attempt to strip repeated newlines and trailing spaces from this file...

No strippable newlines or spaces.

If you have any comments on your experience of the minimizer, please share them in a reply (possibly tagging @JasonGross).
If you believe there's a bug in the bug minimizer, please report it on the bug minimizer issue tracker.

ppedrot · 2022-04-10T10:18:18Z

The error message on the minimized example is weird. It says

Recursive call to groupBy' has principal argument equal to 
"[]" instead of one of the following variables: 
"xs" "ls0".

but I don't see where this empty list is coming from in the syntax. Maybe there is an off-by-one error somewhere.

ppedrot · 2022-04-10T10:30:45Z

Here is a simplified example.

Definition span_cps' {A} (f : A -> bool) {T} (k : list A -> T) :=
  fix span_cps' (ls : list A) {struct ls} : T := match ls with
  | nil => k nil
  | cons x xs => if f x then span_cps' xs else k ls
  end.

Definition groupBy' {A} (f : A -> A -> bool) :=
  fix groupBy' (ls : list A) {struct ls} : unit := match ls with
  | nil => tt
  | cons x xs =>
    span_cps' (f x) (fun ys => match ys with nil => tt | _ => groupBy' ys end) xs
  end.

Interestingly, the match in the continuation is necessary in master to make this pass the guard checking, but I don't understand why. The ys variable should be a subterm regardless.

EDIT: this will teach me to turn seven times my fingers over my keyboard before writing a post, but it's obvious: the problem is that in the nil branch of span_cps' we do k nil instead of k ls. The latter will be a guarded subcall, but the former won't be. I don't understand enough of the guard condition to grasp why the example was working on master but there is an easy fix for fiat-crypto.

SkySkimmer · 2022-04-10T10:38:47Z

On master it probably reduces the match nil with nil => tt that is produced by k nil

ppedrot · 2022-04-12T19:09:22Z

@mattam82 AFAICT this PR is ready and waiting for your approval / merge.

mattam82

This looks good to me, as far as I could understand the code. I'm very happy with the test-suite file which matches exactly my intuitions, thanks @herbelin.

mattam82 · 2022-04-20T10:21:01Z

@ppedrot do we need to worry about the bench failures?

ppedrot · 2022-04-20T10:28:16Z

@mattam82 no, it was a transient failure at the time. This should be ready to merge.

mattam82 · 2022-04-20T12:01:27Z

@coqbot merge now

herbelin added part: kernel kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: inductives Inductive types, fixpoints, etc. labels Jan 4, 2022

herbelin added this to the 8.16+rc1 milestone Jan 4, 2022

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from 75e78c7 to e765aba Compare January 5, 2022 12:45

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from e765aba to d05cbf4 Compare January 5, 2022 16:33

Alizter reviewed Jan 5, 2022

View reviewed changes

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from d05cbf4 to e28d141 Compare January 8, 2022 19:09

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from e28d141 to a731603 Compare January 8, 2022 21:28

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from a731603 to 7746fec Compare January 9, 2022 13:49

herbelin mentioned this pull request Jan 9, 2022

Incompletenesses of guard condition in the presence of cofix redexes or not enough immediately applied primitive projection #15451

Closed

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from 7746fec to 6e3757f Compare January 9, 2022 13:54

herbelin mentioned this pull request Jan 9, 2022

Computation of the guardedness of a subterm assumes too strong invariants on the internal form of fixpoints #15453

Merged

herbelin force-pushed the master+check-guard-also-erasable-subterms branch from 6e3757f to 8f0863f Compare January 11, 2022 12:10

mattam82 self-assigned this Jan 12, 2022

herbelin mentioned this pull request Jan 12, 2022

Adapt to Coq PR #15434: even erasable subterms of fixpoints must be guarded mit-plv/fiat-crypto#1094

Merged

herbelin added 6 commits April 9, 2022 12:09

Splitting guard errors into Fix and CoFix guard errors.

245572d

Guard refinement: we remember a unreduced "match" to optimize failure.

8e9e810

Indeed, if the "match" needs to be reduced but its argument is not a constructor, it can eventually be reduced by any arbitrary term and there is no hope to be guarded at all, even by reducing outer redexes.

Adding change log for rocq-prover#15434

abe6524

Removing debugging export from inductive.ml, not needed in general.

4b70a30

New algorithm which avoids repeating checking argument stack.

17ade41

ppedrot force-pushed the master+check-guard-also-erasable-subterms branch from 169ac11 to 17ade41 Compare April 9, 2022 11:16

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Apr 9, 2022

ppedrot added a commit to ppedrot/fiat-crypto that referenced this pull request Apr 10, 2022

Adapt w.r.t. rocq-prover/rocq#15434.

499487e

JasonGross pushed a commit to mit-plv/fiat-crypto that referenced this pull request Apr 12, 2022

Adapt w.r.t. rocq-prover/rocq#15434. (#1185)

78b499b

mattam82 approved these changes Apr 20, 2022

View reviewed changes

ppedrot added this to the 8.16+rc1 milestone Apr 20, 2022

coqbot-app Bot merged commit 8086c9f into rocq-prover:master Apr 20, 2022

ana-borges pushed a commit to ana-borges/coq that referenced this pull request Nov 15, 2022

Adding change log for rocq-prover#15434

f8cd1a5

herbelin mentioned this pull request Jan 14, 2023

Fix #17073: guard checking in the presence of "match" with inaccessible branches #17116

Merged

2 tasks

yannl35133 mentioned this pull request Apr 3, 2025

Proof of False because of guard checker issue #20455

Closed

Conversation

herbelin commented Jan 4, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

coqbot-app Bot commented Jan 4, 2022

Uh oh!

coqbot-app Bot commented Jan 4, 2022

Uh oh!

coqbot-app Bot commented Jan 4, 2022

Uh oh!

coqbot-app Bot commented Jan 5, 2022

Uh oh!

Alizter Jan 5, 2022

Choose a reason for hiding this comment

Uh oh!

Alizter Jan 5, 2022

Choose a reason for hiding this comment

Uh oh!

herbelin Jan 5, 2022

Choose a reason for hiding this comment

Uh oh!

coqbot-app Bot commented Jan 8, 2022

Uh oh!

coqbot-app Bot commented Jan 8, 2022

Uh oh!

herbelin commented Jan 9, 2022

Uh oh!

coqbot-app Bot commented Jan 9, 2022

Uh oh!

coqbot-app Bot commented Jan 9, 2022

Uh oh!

mattam82 commented Jan 10, 2022

Uh oh!

herbelin commented Jan 10, 2022

Uh oh!

herbelin commented Jan 13, 2022

Uh oh!

herbelin commented Jan 13, 2022

Uh oh!

SkySkimmer commented Jan 13, 2022

Uh oh!

ppedrot commented Apr 9, 2022

Uh oh!

ppedrot commented Apr 9, 2022

Uh oh!

coqbot-app Bot commented Apr 10, 2022

Uh oh!

coqbot-app Bot commented Apr 10, 2022

Uh oh!

Alizter commented Apr 10, 2022

Uh oh!

coqbot-app Bot commented Apr 10, 2022

Uh oh!

coqbot-app Bot commented Apr 10, 2022

Uh oh!

ppedrot commented Apr 10, 2022

Uh oh!

ppedrot commented Apr 10, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer commented Apr 10, 2022

Uh oh!

ppedrot commented Apr 12, 2022

Uh oh!

mattam82 left a comment

Choose a reason for hiding this comment

Uh oh!

mattam82 commented Apr 20, 2022

Uh oh!

ppedrot commented Apr 20, 2022

Uh oh!

mattam82 commented Apr 20, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

herbelin commented Jan 4, 2022 •

edited

Loading

ppedrot commented Apr 10, 2022 •

edited

Loading