Make rapply handle all numbers of underscores by JasonGross · Pull Request #10760 · rocq-prover/rocq

JasonGross · 2019-09-17T00:09:50Z

Kind: enhancement.

Also add a tactic notation so that it takes in uconstrs by default.

Also add some basic tests for rapply.

I made this PR because I hit a case where I needed 16 underscores (the existing rapply only gives me 15).

Added / updated test-suite
Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

JasonGross · 2019-09-17T03:46:54Z

I shall investigate the mathclasses failure (it is a genuine bug with this PR, though I'm not sure what the bug is yet).

Can someone from @coq/doc-maintainers tell me the suggested fix for

doc/unreleased.rst:73:coq:tacn reference target not found: rapply

? Is tacn only for built-in tactics and not for ones defined in the standard library?

cpitclaudel · 2019-09-17T04:13:27Z

tacn is a link to documentation. Is rapply documented?

Zimmi48 · 2019-09-17T07:25:29Z

Is tacn only for built-in tactics and not for ones defined in the standard library?

We don't make any difference between built-in and in standard library, but all the tactics should be documented within the reference manual, and that's the only way we can reference them later on. For instance now is documented despite being defined in the standard library (and there are many more examples).

Zimmi48

Changelog entry looks good. Would be really great if you could take advantage of this PR to add documentation of rapply to the Tactics chapter.

JasonGross · 2019-09-17T20:45:51Z

Would be really great if you could take advantage of this PR to add documentation of rapply to the Tactics chapter.

Documentation for rapply added to the tactics chapter.

JasonGross · 2019-09-17T20:58:42Z

The incompatibility with math-classes is a real one. The issue is that they frequently rely on the fact that rapply would do typeclass resolution before attempting to refine with the lemma applied to underscores, whereas in the new version, first Coq will attempt to unify the term with the goal, and only after that will it perform typeclass resolution. I see a couple of solutions to this:

Submit an overlay to math-classes (and any other development that breaks) blindly replacing all failing rapply with Tactics.rapply. This invokes the underlying Ltac rather than the tactic notation, and also is backwards compatible.
Make rapply continue to mean the constr version, and add, say, erapply for a version taking an open_constr and urapply for a version taking a uconstr

Thoughts?

cc @spitters

This backwards compatible change makes math-classes work with rocq-prover/rocq#10760 by replacing all instances of `rapply` which were relying on typeclass resolution happening *before* `refine` (instead of simultaneously with it) to instead invoke `Tactics.rapply` (which is the same tactic in Coq <= 8.10, and which will be the tactic rather than the `uconstr`-taking tactic notation in Coq >= 8.11). See also rocq-prover/rocq#10760 (comment)

JasonGross · 2019-09-17T21:11:02Z

Overlay added for math-classes (rocq-community/math-classes#78). For reference, I needed to change 9 of the 34 uses of rapply. Discussion on alternatives still welcome.

gares · 2019-09-18T06:49:14Z

Your patch and the motivation seem not the same. I was expecting one more line with more _ but your change is more ambitious and indeed you get a good deal of breakage. Would it make sense to try the more conservative approach?

Zimmi48 · 2019-09-18T07:14:22Z

I didn't know what rapply did before reading the documentation you added. Given the broad scope of the goal, I wonder why rapply is not defined in ML to be as close as possible to eapply except the underlying unification engine. @mattam82 may have produced such a tactic during his work on unifall...

JasonGross · 2019-09-18T15:27:58Z

@gares if I remove the Tactic Notation part, I expect there will be no breakage. This is in fact demonstrated by the fact that the fix is merely to reference the underlying tactic. The breakage comes from interpreting the argument as a uconstr, not from the ambitious goal of handling any number of underscores. But it is a bit subtle, saying that for rapply all holes in the lemma you pass must be fully resolvable, but holes that the tactic adds need not be; it occupies a sort-of half-way place between apply and eapply while also using the new proof engine. I would be willing to backtrack on the tactic notation, if there is no consensus on what the spec of rapply should be beyond what it is already doing.

@Zimmi48 indeed, if someone wants to redefine rapply in OCaml I would not object. I suspect this would break backwards compatibility even more, though, because math-classes relies on the fact that rapply currently does typeclass resolution before application, which is not true of eapply (nor of my new tactic notation).

JasonGross · 2019-09-19T20:33:35Z

I've removed the tactic notation, the overlay, and updated the doc about the more complicated spec of rapply. Hopefully, this is more acceptable?

JasonGross · 2019-09-19T23:39:20Z

Build failure is unrelated to this PR, as it also occurs in master.

SkySkimmer · 2019-10-28T14:23:41Z

Lots of commits, maybe could use a squash.

JasonGross · 2019-10-28T18:51:12Z

Squashed to three commits (I want to leave the uconstr version of rapply in version history, in case anyone wants to come back to it).

Zimmi48 · 2019-11-25T14:44:49Z

Any assignee for this PR? @mattam82 or @gares?

gares · 2019-11-25T16:15:47Z

It's not my territory and I'm not very competent on that (last time I've tried to use uconstr I failed miserably proving I don't get much of ltac1 :-/)

ejgallego · 2019-11-25T17:08:05Z

Should this get a bench?

Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual

This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.

JasonGross · 2019-11-26T19:19:22Z

I've rebased, and started a bench at https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/810/consoleText

JasonGross · 2019-11-29T21:24:42Z

Partial bench:

┌────────────────────────┬─────────────────────────┬───────────────────────────────────────────┬───────────────────────────────────────────┬───────────────────────────────┬───────────────────┐
│                        │      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-coqutil │   58.95   59.14 -0.32 % │     164578719784     164901613955 -0.20 % │     210334130238     210332239113 +0.00 % │     544056     544336 -0.05 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│            coq-bignums │   63.77   63.96 -0.30 % │     176979438014     177218124635 -0.13 % │     248805553150     248764672402 +0.02 % │     494868     495012 -0.03 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│               coq-hott │  362.71  363.70 -0.27 % │     989723887622     989489187981 +0.02 % │    1592242256876    1592139330539 +0.01 % │     608496     608436 +0.01 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│              coq-color │ 2848.86 2855.58 -0.24 % │    7949644759747    7964297596891 -0.18 % │    9617901878901    9618162115505 -0.00 % │    1554060    1553912 +0.01 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│ coq-mathcomp-odd-order │ 1373.83 1375.95 -0.15 % │    3829933097826    3834798947908 -0.13 % │    6803706179785    6803708603963 -0.00 % │    1296048    1296316 -0.02 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│     coq-mathcomp-field │  214.04  214.33 -0.14 % │     596296697309     596727980301 -0.07 % │     895411985286     895446832283 -0.00 % │     757492     757512 -0.00 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│              coq-flocq │  244.74  245.07 -0.13 % │     679986835305     680893423705 -0.13 % │     913506623704     913556078347 -0.01 % │    1017664    1017520 +0.01 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│       coq-math-classes │  552.71  553.05 -0.06 % │    1541058082506    1543024964749 -0.13 % │    2145066080099    2146604414844 -0.07 % │     636856     637312 -0.07 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│  coq-mathcomp-solvable │  178.73  178.78 -0.03 % │     497967942233     498075901812 -0.02 % │     705476404789     705555238025 -0.01 % │     788992     788428 +0.07 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│               coq-corn │ 1485.51 1485.67 -0.01 % │    4140517353262    4141980839974 -0.04 % │    6359658431229    6359487972570 +0.00 % │     855588     855608 -0.00 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│   coq-mathcomp-algebra │  154.01  154.00 +0.01 % │     427901076072     428082589750 -0.04 % │     557369732982     557381483669 -0.00 % │     613724     613908 -0.03 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│             coq-geocoq │ 1530.17 1529.29 +0.06 % │    4268559938505    4265884500706 +0.06 % │    6541159976758    6539208388093 +0.03 % │    1362444    1362708 -0.02 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│ coq-mathcomp-character │  166.79  166.64 +0.09 % │     464042728812     464035786783 +0.00 % │     647312621553     647310071813 +0.00 % │     803280     821512 -2.22 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│           coq-bedrock2 │  486.29  485.75 +0.11 % │    1353558754164    1352039281153 +0.11 % │    2367607311471    2367834786877 -0.01 % │    3168116    3168084 +0.00 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│           coq-compcert │  728.90  727.93 +0.13 % │    2032071779870    2030616591478 +0.07 % │    2914531971452    2914374774697 +0.01 % │    1068192    1067608 +0.05 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│           coq-coqprime │  181.22  180.79 +0.24 % │     501310433144     500691700470 +0.12 % │     916232712554     916235385801 -0.00 % │     810808     810936 -0.02 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│  coq-mathcomp-fingroup │   48.80   48.65 +0.31 % │     135086509062     134972113934 +0.08 % │     186578396881     186567111598 +0.01 % │     559900     560208 -0.05 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│  coq-performance-tests │   11.49   11.45 +0.35 % │      31523232851      31548771983 -0.08 % │      54429897175      54421814170 +0.01 % │     424020     424132 -0.03 % │    0    0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼───────────────────┤
│ coq-mathcomp-ssreflect │   40.10   39.58 +1.31 % │     108569504191     108456251602 +0.10 % │     140715246909     140731268495 -0.01 % │     522820     522776 +0.01 % │    0    0  +nan % │
└────────────────────────┴─────────────────────────┴───────────────────────────────────────────┴───────────────────────────────────────────┴───────────────────────────────┴───────────────────┘

Since this one was interrupted, I've spun up a new one at https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/813/consoleText . But so far it looks to be mostly noise.

JasonGross · 2019-12-07T02:13:44Z

Another partial bench result:


┌────────────────────────┬─────────────────────────┬───────────────────────────────────────────┬───────────────────────────────────────────┬───────────────────────────────┬─────────────────────┐
│                        │      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-hott │  361.92  363.86 -0.53 % │     989384804073     991412603305 -0.20 % │    1592205165912    1592237358960 -0.00 % │     608496     608324 +0.03 % │     8     7 +14.29 % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│  coq-performance-tests │   11.50   11.53 -0.26 % │      31520147102      31697493098 -0.56 % │      54373619448      54404663515 -0.06 % │     424292     424336 -0.01 % │    15     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│  coq-mathcomp-solvable │  178.76  179.22 -0.26 % │     498152805640     498755578452 -0.12 % │     705116333787     705121053403 -0.00 % │     788596     788668 -0.01 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│     coq-mathcomp-field │  214.67  215.22 -0.26 % │     598513337461     598712153987 -0.03 % │     896452606960     896511773393 -0.01 % │     753192     753296 -0.01 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│       coq-math-classes │  553.61  554.91 -0.23 % │    1544476551134    1549406943350 -0.32 % │    2145061361633    2146600528683 -0.07 % │     636856     637240 -0.06 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│ coq-mathcomp-character │  167.00  167.34 -0.20 % │     464730024490     465193054134 -0.10 % │     647370005341     647334141719 +0.01 % │     854644     854396 +0.03 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│               coq-corn │ 1485.62 1487.91 -0.15 % │    4144907464728    4148783172813 -0.09 % │    6359687137536    6359657843595 +0.00 % │     855672     855548 +0.01 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│   coq-mathcomp-algebra │  154.18  154.37 -0.12 % │     429312644941     428829561609 +0.11 % │     557415239874     557422725324 -0.00 % │     614176     609924 +0.70 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│              coq-color │ 2859.90 2862.21 -0.08 % │    7973435002136    7981711174726 -0.10 % │    9614801740341    9615495663829 -0.01 % │    1553896    1554024 -0.01 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│  coq-mathcomp-fingroup │   48.87   48.90 -0.06 % │     135213618948     135183643870 +0.02 % │     186654141450     186572964699 +0.04 % │     560028     560076 -0.01 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│           coq-bedrock2 │  488.63  488.91 -0.06 % │    1359558733706    1360016351824 -0.03 % │    2370796692406    2370575817782 +0.01 % │    3168112    3168144 -0.00 % │     4     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│            coq-coqutil │   59.24   59.27 -0.05 % │     164685445220     164625424558 +0.04 % │     209623598492     209581246041 +0.02 % │     545536     545856 -0.06 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│           coq-compcert │  730.93  730.85 +0.01 % │    2036600861548    2035210266974 +0.07 % │    2914452546091    2914372144311 +0.00 % │    1068284    1067736 +0.05 % │     1     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│ coq-mathcomp-odd-order │ 1375.82 1374.70 +0.08 % │    3835614001695    3833218102459 +0.06 % │    6806282113618    6806251572331 +0.00 % │    1285624    1285644 -0.00 % │     2    15 -86.67 % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│              coq-flocq │  244.78  244.50 +0.11 % │     681626984789     679921678556 +0.25 % │     913497086703     913528385583 -0.00 % │    1017616    1017752 -0.01 % │    27     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│           coq-coqprime │  181.12  180.82 +0.17 % │     501538627489     501645162975 -0.02 % │     916069360947     916060831792 +0.00 % │     807948     808372 -0.05 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│            coq-bignums │   64.04   63.85 +0.30 % │     177369874704     177205490551 +0.09 % │     248818985630     248755086514 +0.03 % │     494968     494908 +0.01 % │    24     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│           coq-rewriter │  582.46  578.20 +0.74 % │    1617676389490    1607127324201 +0.66 % │    2475187614357    2474301473763 +0.04 % │     991000    1008336 -1.72 % │     0     0  +nan % │
├────────────────────────┼─────────────────────────┼───────────────────────────────────────────┼───────────────────────────────────────────┼───────────────────────────────┼─────────────────────┤
│ coq-mathcomp-ssreflect │   40.78   40.40 +0.94 % │     110695586389     110431508668 +0.24 % │     142744974801     142779471929 -0.02 % │     524504     524724 -0.04 % │     2     0  +nan % │
└────────────────────────┴─────────────────────────┴───────────────────────────────────────────┴───────────────────────────────────────────┴───────────────────────────────┴─────────────────────┘

Trying once more for everything at https://ci.inria.fr/coq/view/opam/job/benchmark-part-of-the-branch/816/consoleText

JasonGross · 2019-12-16T20:09:14Z

Everything except for coq-rewriter-perf:

┌────────────────────────┬─────────────────────────┬─────────────────────────────────────────────┬─────────────────────────────────────────────┬───────────────────────────────┬────────────────────┐
│                        │      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-mathcomp-fingroup │   48.28   48.95 -1.37 % │      134843515999      135348715758 -0.37 % │      186982527056      187019679318 -0.02 % │     560000     560036 -0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│           coq-rewriter │  576.29  581.21 -0.85 % │     1600351069536     1613583600958 -0.82 % │     2478445466283     2477592768716 +0.03 % │     994732    1012040 -1.71 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│         coq-coquelicot │   73.06   73.52 -0.63 % │      200210353445      200876136187 -0.33 % │      261452786995      261446472131 +0.00 % │     679268     679128 +0.02 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│          coq-fiat-core │  106.74  107.18 -0.41 % │      302603780340      302596274918 +0.00 % │      400278378489      400269647601 +0.00 % │     466340     466384 -0.01 % │    16    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│               coq-hott │  373.44  374.89 -0.39 % │     1018588353072     1019411360672 -0.08 % │     1649829556198     1649786237419 +0.00 % │     608384     608400 -0.00 % │     2    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│   coq-mathcomp-algebra │  153.76  154.25 -0.32 % │      428023108198      428438483489 -0.10 % │      557865144252      557831386438 +0.01 % │     609752     614196 -0.72 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│       coq-fiat-parsers │  667.77  669.63 -0.28 % │     1869963431098     1873925200282 -0.21 % │     2892728384916     2894021815592 -0.04 % │    3107324    3105684 +0.05 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│               coq-corn │ 1482.12 1486.10 -0.27 % │     4136649685749     4140899896978 -0.10 % │     6360179052946     6360002900140 +0.00 % │     855680     855548 +0.02 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│  coq-performance-tests │   11.52   11.55 -0.26 % │       31719966426       31683621700 +0.11 % │       54820090687       54910723308 -0.17 % │     424292     424100 +0.05 % │     1    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│        coq-lambda-rust │ 1569.89 1573.68 -0.24 % │     4374904371083     4384181177885 -0.21 % │     6324871600274     6325517820730 -0.01 % │    1137936    1138140 -0.02 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│       coq-math-classes │  552.96  554.14 -0.21 % │     1541798792335     1546685643684 -0.32 % │     2145489014549     2147115638422 -0.08 % │     636760     636956 -0.03 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│ coq-mathcomp-ssreflect │   40.27   40.35 -0.20 % │      110409362953      110382312840 +0.02 % │      143117630318      143145844773 -0.02 % │     524712     524696 +0.00 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│  coq-mathcomp-solvable │  179.32  179.57 -0.14 % │      498205921637      498599573013 -0.08 % │      705563067085      705626189280 -0.01 % │     789088     789048 +0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│ coq-mathcomp-character │  166.48  166.68 -0.12 % │      463754214992      464109371171 -0.08 % │      647813945624      647746510400 +0.01 % │     853812     829584 +2.92 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│           coq-compcert │  726.96  727.75 -0.11 % │     2028268760306     2028172498545 +0.00 % │     2914910289790     2915031893194 -0.00 % │    1068168    1068220 -0.00 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│            coq-unimath │ 4009.08 4013.23 -0.10 % │    11161392608938    11179826777524 -0.16 % │    21336925308891    21334924794698 +0.01 % │    1068124    1068032 +0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│          coq-fourcolor │ 2079.34 2080.38 -0.05 % │     5801118523427     5806259658109 -0.09 % │    11373865216300    11373674757700 +0.00 % │     949828     949956 -0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│           coq-bedrock2 │  510.26  510.40 -0.03 % │     1419579127381     1420028842310 -0.03 % │     2476668211166     2476739642509 -0.00 % │    3168024    3167948 +0.00 % │     1    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│              coq-flocq │  244.26  244.31 -0.02 % │      678641618574      680408981757 -0.26 % │      913927122503      913915371515 +0.00 % │    1017648    1017616 +0.00 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│        coq-fiat-crypto │ 4209.26 4208.60 +0.02 % │    11686343366147    11689872586549 -0.03 % │    19115989699883    19115418580704 +0.00 % │    2385828    2395264 -0.39 % │     1    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│         coq-verdi-raft │ 1272.97 1272.76 +0.02 % │     3547131851037     3545910687166 +0.03 % │     5030280879930     5030792307134 -0.01 % │    1823388    1823524 -0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│     coq-mathcomp-field │  214.51  214.43 +0.04 % │      596498394919      596732658464 -0.04 % │      896887880663      896884516518 +0.00 % │     753124     753148 -0.00 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│ coq-mathcomp-odd-order │ 1373.21 1372.68 +0.04 % │     3828231362153     3826973836888 +0.03 % │     6806753666609     6806696491995 +0.00 % │    1288956    1285576 +0.26 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│             coq-geocoq │ 1534.94 1534.29 +0.04 % │     4279164813277     4279975052284 -0.02 % │     6541777308435     6539061878790 +0.04 % │    1362304    1362240 +0.00 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│ coq-fiat-crypto-legacy │ 6440.82 6436.14 +0.07 % │    17932788129818    17923127196351 +0.05 % │    30121146363570    30121166301429 -0.00 % │    2389472    2389444 +0.00 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│              coq-color │ 2867.54 2863.26 +0.15 % │     7992990142661     7986006808120 +0.09 % │     9618386159165     9618567061112 -0.00 % │    1553960    1553852 +0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│              coq-verdi │  116.44  116.23 +0.18 % │      321903657073      321852142222 +0.02 % │      423288261722      423279422981 +0.00 % │     555912     556008 -0.02 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│            coq-bignums │   64.07   63.94 +0.20 % │      177638957559      177443888717 +0.11 % │      249167437568      249168051794 -0.00 % │     494856     495120 -0.05 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│           coq-coqprime │  181.32  180.84 +0.27 % │      501803348032      500929542145 +0.17 % │      916598594148      916661722936 -0.01 % │     810652     810568 +0.01 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│            coq-coqutil │   60.54   60.29 +0.41 % │      168419903050      168101725164 +0.19 % │      213975133627      213991262554 -0.01 % │     544088     544308 -0.04 % │     0    0  +nan % │
├────────────────────────┼─────────────────────────┼─────────────────────────────────────────────┼─────────────────────────────────────────────┼───────────────────────────────┼────────────────────┤
│             coq-sf-plf │   44.69   44.46 +0.52 % │      124390775100      124451243368 -0.05 % │      169751843596      169845698008 -0.06 % │     487536     494280 -1.36 % │     0    0  +nan % │
└────────────────────────┴─────────────────────────┴─────────────────────────────────────────────┴─────────────────────────────────────────────┴───────────────────────────────┴────────────────────┘

I think this is within noise, and hence ready to be merged.

JasonGross · 2019-12-17T20:31:38Z

@mattam82 @ppedrot Is one of you willing to be assignee here?

ppedrot · 2019-12-23T10:54:15Z

Let's merge, this has waited for too long already.

Ack-by: Zimmi48 Reviewed-by: ppedrot

JasonGross added zARCHIVED: standard library Previously standard library (do not use anymore, now its own repo). part: tactics kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Sep 17, 2019

JasonGross added this to the 8.11+beta1 milestone Sep 17, 2019

JasonGross requested review from a team and mattam82 as code owners September 17, 2019 00:09

Zimmi48 reviewed Sep 17, 2019

View reviewed changes

JasonGross mentioned this pull request Sep 17, 2019

Fix for a new rapply tactic rocq-community/math-classes#78

Merged

JasonGross force-pushed the more-rapply branch from ba77093 to 2d53e80 Compare September 19, 2019 20:32

JasonGross force-pushed the more-rapply branch from 2d53e80 to f993d15 Compare September 19, 2019 20:35

JasonGross force-pushed the more-rapply branch from f993d15 to 5635b3c Compare October 17, 2019 19:37

JasonGross mentioned this pull request Oct 25, 2019

new and improved issig HoTT/Coq-HoTT#1106

Merged

JasonGross force-pushed the more-rapply branch from 5635b3c to 5a28203 Compare October 28, 2019 18:50

ppedrot modified the milestones: 8.11+beta1, 8.12+beta1 Nov 1, 2019

JasonGross force-pushed the more-rapply branch from 5a28203 to 7b1dc94 Compare November 25, 2019 04:42

JasonGross added 3 commits November 26, 2019 14:14

Remove some trailing whitespace in theories/Program/Tactics.v

49d21a2

Make rapply handle all numbers of underscores

b09444f

Also add a tactic notation so that it takes in uconstrs by default. Also add some basic tests for `rapply`. Also document rapply in the manual

Remove rapply tactic notation in favor of just the tactic

8d9afb9

This increases backwards compatibility. If desired, we can add a tactic notation to simplify the spec of `rapply` in the future if we want.

JasonGross force-pushed the more-rapply branch from 7b1dc94 to 8d9afb9 Compare November 26, 2019 19:14

ppedrot self-assigned this Dec 17, 2019

ppedrot approved these changes Dec 18, 2019

View reviewed changes

ppedrot added a commit that referenced this pull request Dec 23, 2019

Merge PR #10760: Make rapply handle all numbers of underscores

95fc326

Ack-by: Zimmi48 Reviewed-by: ppedrot

ppedrot merged commit 8d9afb9 into rocq-prover:master Dec 23, 2019

JasonGross deleted the more-rapply branch June 2, 2021 11:56

Conversation

JasonGross commented Sep 17, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JasonGross commented Sep 17, 2019

Uh oh!

cpitclaudel commented Sep 17, 2019

Uh oh!

Zimmi48 commented Sep 17, 2019

Uh oh!

Zimmi48 left a comment

Choose a reason for hiding this comment

Uh oh!

JasonGross commented Sep 17, 2019

Uh oh!

JasonGross commented Sep 17, 2019

Uh oh!

JasonGross commented Sep 17, 2019

Uh oh!

gares commented Sep 18, 2019

Uh oh!

Zimmi48 commented Sep 18, 2019

Uh oh!

JasonGross commented Sep 18, 2019

Uh oh!

JasonGross commented Sep 19, 2019

Uh oh!

JasonGross commented Sep 19, 2019

Uh oh!

SkySkimmer commented Oct 28, 2019

Uh oh!

JasonGross commented Oct 28, 2019

Uh oh!

Zimmi48 commented Nov 25, 2019

Uh oh!

gares commented Nov 25, 2019

Uh oh!

ejgallego commented Nov 25, 2019

Uh oh!

JasonGross commented Nov 26, 2019

Uh oh!

JasonGross commented Nov 29, 2019

Uh oh!

JasonGross commented Dec 7, 2019

Uh oh!

JasonGross commented Dec 16, 2019

Uh oh!

JasonGross commented Dec 17, 2019

Uh oh!

ppedrot commented Dec 23, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

JasonGross commented Sep 17, 2019 •

edited

Loading