Replace `lia_tactics` and `field_tactics` with mczify and Algebra Tactics #4

pi8027 · 2021-10-18T09:29:38Z

This PR is based on #3, #9, and #11. The plan is to use apery as a benchmark of mczify and Algebra Tactics (in terms of LoC, performance, and some other specific details). Therefore, changes independent from those libraries should be done in #3 (or in another separate PR).

Major changes:

binomialz now returns int instead of rat.
rat_of_positive has been replaced with rat_of_Z. CoqEAL refinements in rho_computations.v have also been adapted.

Some observations:

rat_of_Z has been redefined using int_of_Z and declared as a ring morphism (ring instances of Z is declared in ssrZ.v of mczify). Algebra Tactics can handle rat_of_Z without any special treatment since they support ring morphisms. Also, declaring rat_of_Z as a ring morphism drastically simplifies hanson.v.
~~Two invocations of the field tactic in ops_for_b.v are still too slow. Investigation needed.~~ They are now faster than before.

theories/hanson.v

theories/ops_for_b.v

pi8027 · 2021-12-15T19:52:08Z

GitHub Actions kill coqc since compiling ops_for_b.v now consumes too much memory (more than 8GB).

pi8027 · 2021-12-16T15:50:39Z

GitHub Actions kill coqc since compiling ops_for_b.v now consumes too much memory (more than 8GB).

FTR, I managed to obtain a memory trace using the Memtrace utilities. coqc ops_for_b.v consumes approximately 9GB RAM in the end. I looked into the objects living in the last one second and found that Coq_elpi_HOAS.lp2constr (the read-back function from Elpi to Coq, I guess) allocated a significant amount of memory, although this may not be the only bottleneck. cc: @gares

pi8027 · 2021-12-16T15:56:42Z

I think I'm going to optimize the size of reified terms (by inserting let-ins for structure instances) for the moment. I can also share the memory trace I obtained if it is useful.

pi8027 · 2021-12-22T13:28:57Z

In the last invocation of the field tactic in ops_for_b.v, I have 23 items in the proof context. Every time I call coq.unify-eq those items have to be read back to Coq. I guess this is one of the main sources of this performance issue. Discarding useless items from the context or caching the result of conversion would improve the performance.

gares · 2021-12-23T08:06:20Z

Hi, thanks for running memory profiler. You are right context readback is naive and could be cached.

It would be nice to have an issue on coq elpi with all the dzta so that I can reproduce and test any optimization

pi8027 · 2021-12-23T15:22:59Z

I also attempted to replace the use of rat_of_positive with rat_of_Z, but then failed to adapt CoqEAL style refinements in rho_computations.v. I think that the source of the issue is that CoqEAL defines its own computable integer type and does not provide support for the standard Z type.

pi8027 · 2021-12-23T15:47:07Z

@CohenCyril I guess I need your suggestion on the above point before further investigation. My understanding is that, in theory, we should use CoqEAL's computable (parameterized) Z instead. But, in the presence of other tools (e.g., mczify, and the heavy use of the opaque rat_of_Z in apery, which is also a ring morphism now!), we may consider refining ssrint to the standard Z, which has better interoperability. Is there any issue with having more than two computation-oriented types on one proof-oriented type in CoqEAL?

pi8027 · 2021-12-28T06:03:08Z

I also attempted to replace the use of rat_of_positive with rat_of_Z, but then failed to adapt CoqEAL style refinements in rho_computations.v. I think that the source of the issue is that CoqEAL defines its own computable integer type and does not provide support for the standard Z type.

Done. (But I still have to release mczify 1.2.0 to fix CI.)

amahboubi · 2022-01-06T15:04:55Z

This is really cool! If I read the CI correctly, this PR remains ~23% slower than the original code (16s vs 13s with coq 8.14 + mathcomp 1.12). I have seen that the two largest instances of polynomials are now normalized (both in ops_for_b.v) in a comparable time in the original code and with algebra-tactics respectively. Do you know where the additional time is spent?

pi8027 · 2022-01-06T15:14:57Z

@amahboubi I think that execution time in CI is not reliable for benchmarking purposes. I will do that on a more reliable machine and report. BTW, I recently observed that several performance issues related to rat have been disappeared in MathComp 1.13.0. (So I prefer to eventually drop the support for MathComp 1.12.0 and do benchmark only with MathComp 1.13.0.)

pi8027 · 2022-01-07T12:08:06Z

Here is the benchmark result with Coq 8.14.0 and MathComp 1.13.0, comparing this PR (after) with the current master branch (before).

   After |   Peak Mem | File Name               |   Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
--------------------------------------------------------------------------------------------------------------------------------
9m04.02s | 6247696 ko | Total Time / Peak Mem   | 9m46.53s | 3562224 ko || -0m42.50s ||   2685472 ko |   -7.24% |        +75.38%
--------------------------------------------------------------------------------------------------------------------------------
1m14.85s | 1646212 ko | hanson.vo               | 2m50.72s | 1863036 ko || -1m35.87s ||   -216824 ko |  -56.15% |        -11.63%
5m25.07s | 6247696 ko | ops_for_b.vo            | 4m45.88s | 3562224 ko || +0m39.18s ||   2685472 ko |  +13.70% |        +75.38%
0m20.07s |  723740 ko | a_props.vo              | 0m10.56s |  647148 ko || +0m09.50s ||     76592 ko |  +90.05% |        +11.83%
0m12.55s |  810924 ko | ops_for_s.vo            | 0m08.79s |  629180 ko || +0m03.76s ||    181744 ko |  +42.77% |        +28.88%
0m03.99s |  620052 ko | b_props.vo              | 0m02.63s |  613920 ko || +0m01.36s ||      6132 ko |  +51.71% |         +0.99%
  N/A    |     N/A    | field_tactics.vo        | 0m01.94s |  547760 ko || -0m01.94s ||   -547760 ko | -100.00% |       -100.00%
  N/A    |     N/A    | lia_tactics.vo          | 0m01.67s |  565740 ko || -0m01.67s ||   -565740 ko | -100.00% |       -100.00%
  N/A    |     N/A    | test_field_tactics.vo   | 0m01.44s |  545984 ko || -0m01.43s ||   -545984 ko | -100.00% |       -100.00%
0m25.05s |  811708 ko | z3irrational.vo         | 0m25.23s |  813452 ko || -0m00.17s ||     -1744 ko |   -0.71% |         -0.21%
0m11.33s |  721256 ko | reduce_order.vo         | 0m12.00s |  731920 ko || -0m00.67s ||    -10664 ko |   -5.58% |         -1.45%
0m04.36s |  611524 ko | algo_closures.vo        | 0m03.88s |  603468 ko || +0m00.48s ||      8056 ko |  +12.37% |         +1.33%
0m04.32s |  625632 ko | ops_for_v.vo            | 0m03.58s |  597812 ko || +0m00.74s ||     27820 ko |  +20.67% |         +4.65%
0m04.21s |  648556 ko | ops_for_a.vo            | 0m03.22s |  594696 ko || +0m00.98s ||     53860 ko |  +30.74% |         +9.05%
0m03.60s |  598884 ko | hanson_elem_analysis.vo | 0m03.78s |  596408 ko || -0m00.17s ||      2476 ko |   -4.76% |         +0.41%
0m03.10s |  579252 ko | binomialz.vo            | 0m03.13s |  570460 ko || -0m00.02s ||      8792 ko |   -0.95% |         +1.54%
0m03.01s |  559204 ko | extra_mathcomp.vo       | 0m02.96s |  558676 ko || +0m00.04s ||       528 ko |   +1.68% |         +0.09%
0m02.99s |  617984 ko | ops_for_u.vo            | 0m02.25s |  592152 ko || +0m00.74s ||     25832 ko |  +32.88% |         +4.36%
0m02.68s |  601324 ko | initial_conds.vo        | 0m02.47s |  597048 ko || +0m00.20s ||      4276 ko |   +8.50% |         +0.71%
0m02.49s |  601116 ko | hanson_elem_arith.vo    | 0m02.37s |  596216 ko || +0m00.12s ||      4900 ko |   +5.06% |         +0.82%
0m02.43s |  560164 ko | bigopz.vo               | 0m02.45s |  563476 ko || -0m00.02s ||     -3312 ko |   -0.81% |         -0.58%
0m02.42s |  626964 ko | b_over_a_props.vo       | 0m02.05s |  612124 ko || +0m00.37s ||     14840 ko |  +18.04% |         +2.42%
0m02.34s |  591628 ko | punk.vo                 | 0m02.25s |  560780 ko || +0m00.08s ||     30848 ko |   +3.99% |         +5.50%
0m02.25s |  595440 ko | harmonic_numbers.vo     | 0m01.86s |  570196 ko || +0m00.38s ||     25244 ko |  +20.96% |         +4.42%
0m02.21s |  536952 ko | extra_cauchyreals.vo    | 0m02.25s |  534616 ko || -0m00.04s ||      2336 ko |   -1.77% |         +0.43%
0m02.08s |  599348 ko | z3seq_props.vo          | 0m01.84s |  592672 ko || +0m00.24s ||      6676 ko |  +13.04% |         +1.12%
0m02.01s |  558064 ko | multinomial.vo          | 0m02.05s |  559660 ko || -0m00.04s ||     -1596 ko |   -1.95% |         -0.28%
0m01.99s |  588084 ko | c_props.vo              | 0m01.60s |  590700 ko || +0m00.38s ||     -2616 ko |  +24.37% |         -0.44%
0m01.93s |  593748 ko | annotated_recs_v.vo     | 0m01.91s |  595604 ko || +0m00.02s ||     -1856 ko |   +1.04% |         -0.31%
0m01.91s |  583156 ko | rho_computations.vo     | 0m01.62s |  565584 ko || +0m00.28s ||     17572 ko |  +17.90% |         +3.10%
0m01.82s |  583360 ko | s_props.vo              | 0m01.91s |  587900 ko || -0m00.08s ||     -4540 ko |   -4.71% |         -0.77%
0m01.73s |  552416 ko | posnum.vo               | 0m01.76s |  552880 ko || -0m00.03s ||      -464 ko |   -1.70% |         -0.08%
0m01.66s |  564080 ko | rat_of_Z.vo             | 0m01.37s |  547308 ko || +0m00.28s ||     16772 ko |  +21.16% |         +3.06%
0m01.62s |  532272 ko | arithmetics.vo          | 0m01.61s |  532556 ko || +0m00.01s ||      -284 ko |   +0.62% |         -0.05%
0m01.46s |  585360 ko | annotated_recs_d.vo     | 0m01.45s |  585680 ko || +0m00.01s ||      -320 ko |   +0.68% |         -0.05%
0m01.46s |  585080 ko | annotated_recs_s.vo     | 0m01.40s |  585648 ko || +0m00.06s ||      -568 ko |   +4.28% |         -0.09%
0m01.41s |  530256 ko | floor.vo                | 0m01.40s |  529460 ko || +0m00.01s ||       796 ko |   +0.71% |         +0.15%
0m01.40s |  583968 ko | annotated_recs_c.vo     | 0m01.36s |  581208 ko || +0m00.03s ||      2760 ko |   +2.94% |         +0.47%
0m01.40s |  582436 ko | annotated_recs_z.vo     | 0m01.34s |  581232 ko || +0m00.05s ||      1204 ko |   +4.47% |         +0.20%
0m01.39s |  584000 ko | annotated_recs_b.vo     | 0m01.36s |  586364 ko || +0m00.02s ||     -2364 ko |   +2.20% |         -0.40%
0m01.37s |  561824 ko | shift.vo                | 0m01.17s |  527944 ko || +0m00.20s ||     33880 ko |  +17.09% |         +6.41%
0m01.29s |  580864 ko | seq_defs.vo             | 0m01.34s |  585912 ko || -0m00.05s ||     -5048 ko |   -3.73% |         -0.86%
0m00.78s |  537192 ko | tactics.vo              |   N/A    |    N/A     || +0m00.78s ||    537192 ko |        ∞ |              ∞
  N/A    |     N/A    | conj.vo                 | 0m00.39s |  433896 ko || -0m00.39s ||   -433896 ko | -100.00% |       -100.00%
  N/A    |     N/A    | test_conj.vo            | 0m00.30s |  347852 ko || -0m00.30s ||   -347852 ko | -100.00% |       -100.00%

Overall this PR is faster because of hanson.v, but many files become slower, e.g., a_props.v, ops_for_s.v, and b_props.v. Probably the source of the issue is my ring_lia tactic.

pi8027 · 2022-01-07T13:01:48Z

And here is the same comparison except that it uses MathComp 1.12.0.

    After |   Peak Mem | File Name               |    Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------
12m09.03s | 6309928 ko | Total Time / Peak Mem   | 10m37.53s | 3602780 ko || +1m31.50s ||   2707148 ko |  +14.35% |        +75.14%
----------------------------------------------------------------------------------------------------------------------------------
 7m25.83s | 6309928 ko | ops_for_b.vo            |  4m54.27s | 3602780 ko || +2m31.56s ||   2707148 ko |  +51.50% |        +75.14%
 1m18.43s | 1471056 ko | hanson.vo               |  2m54.84s | 1656092 ko || -1m36.40s ||   -185036 ko |  -55.14% |        -11.17%
 0m23.40s |  816648 ko | ops_for_s.vo            |  0m09.68s |  635416 ko || +0m13.71s ||    181232 ko | +141.73% |        +28.52%
 0m30.74s |  828240 ko | z3irrational.vo         |  0m41.59s |  804876 ko || -0m10.85s ||     23364 ko |  -26.08% |         +2.90%
 0m33.20s |  729496 ko | a_props.vo              |  0m23.84s |  652260 ko || +0m09.36s ||     77236 ko |  +39.26% |        +11.84%
 0m11.85s |  593568 ko | hanson_elem_analysis.vo |  0m04.82s |  600956 ko || +0m07.02s ||     -7388 ko | +145.85% |         -1.22%
 0m10.57s |  653376 ko | ops_for_a.vo            |  0m03.26s |  593376 ko || +0m07.31s ||     60000 ko | +224.23% |        +10.11%
 0m07.79s |  615808 ko | algo_closures.vo        |  0m03.89s |  601024 ko || +0m03.89s ||     14784 ko | +100.25% |         +2.45%
 0m06.89s |  632744 ko | ops_for_v.vo            |  0m03.62s |  595000 ko || +0m03.26s ||     37744 ko |  +90.33% |         +6.34%
   N/A    |     N/A    | field_tactics.vo        |  0m03.64s |  546972 ko || -0m03.64s ||   -546972 ko | -100.00% |       -100.00%
 0m14.62s |  731488 ko | reduce_order.vo         |  0m12.29s |  737732 ko || +0m02.33s ||     -6244 ko |  +18.95% |         -0.84%
 0m04.27s |  613564 ko | ops_for_u.vo            |  0m02.23s |  588100 ko || +0m02.03s ||     25464 ko |  +91.47% |         +4.32%
 0m03.99s |  623588 ko | b_props.vo              |  0m02.63s |  613840 ko || +0m01.36s ||      9748 ko |  +51.71% |         +1.58%
 0m03.65s |  593128 ko | hanson_elem_arith.vo    |  0m02.58s |  592388 ko || +0m01.06s ||       740 ko |  +41.47% |         +0.12%
   N/A    |     N/A    | lia_tactics.vo          |  0m01.66s |  564904 ko || -0m01.65s ||   -564904 ko | -100.00% |       -100.00%
   N/A    |     N/A    | test_field_tactics.vo   |  0m01.40s |  545432 ko || -0m01.39s ||   -545432 ko | -100.00% |       -100.00%
 0m04.01s |  556632 ko | extra_mathcomp.vo       |  0m03.92s |  556500 ko || +0m00.08s ||       132 ko |   +2.29% |         +0.02%
 0m03.61s |  586740 ko | harmonic_numbers.vo     |  0m03.12s |  566596 ko || +0m00.48s ||     20144 ko |  +15.70% |         +3.55%
 0m03.26s |  595500 ko | z3seq_props.vo          |  0m03.04s |  588620 ko || +0m00.21s ||      6880 ko |   +7.23% |         +1.16%
 0m03.10s |  573296 ko | binomialz.vo            |  0m03.92s |  567852 ko || -0m00.81s ||      5444 ko |  -20.91% |         +0.95%
 0m02.91s |  583536 ko | s_props.vo              |  0m02.90s |  585808 ko || +0m00.01s ||     -2272 ko |   +0.34% |         -0.38%
 0m02.59s |  606236 ko | initial_conds.vo        |  0m02.49s |  593540 ko || +0m00.09s ||     12696 ko |   +4.01% |         +2.13%
 0m02.53s |  623700 ko | b_over_a_props.vo       |  0m02.10s |  607908 ko || +0m00.42s ||     15792 ko |  +20.47% |         +2.59%
 0m02.42s |  556796 ko | bigopz.vo               |  0m02.38s |  556504 ko || +0m00.04s ||       292 ko |   +1.68% |         +0.05%
 0m02.33s |  590120 ko | punk.vo                 |  0m02.19s |  558756 ko || +0m00.14s ||     31364 ko |   +6.39% |         +5.61%
 0m02.23s |  532512 ko | extra_cauchyreals.vo    |  0m02.23s |  532668 ko || +0m00.00s ||      -156 ko |   +0.00% |         -0.02%
 0m02.04s |  586364 ko | c_props.vo              |  0m01.60s |  586148 ko || +0m00.43s ||       216 ko |  +27.49% |         +0.03%
 0m02.01s |  557020 ko | multinomial.vo          |  0m02.02s |  556508 ko || -0m00.01s ||       512 ko |   -0.49% |         +0.09%
 0m01.97s |  590532 ko | annotated_recs_v.vo     |  0m01.91s |  589208 ko || +0m00.06s ||      1324 ko |   +3.14% |         +0.22%
 0m01.90s |  586652 ko | rho_computations.vo     |  0m01.59s |  563820 ko || +0m00.30s ||     22832 ko |  +19.49% |         +4.04%
 0m01.72s |  554320 ko | posnum.vo               |  0m01.70s |  554712 ko || +0m00.02s ||      -392 ko |   +1.17% |         -0.07%
 0m01.61s |  561292 ko | rat_of_Z.vo             |  0m01.35s |  544716 ko || +0m00.26s ||     16576 ko |  +19.25% |         +3.04%
 0m01.59s |  528072 ko | arithmetics.vo          |  0m01.55s |  530260 ko || +0m00.04s ||     -2188 ko |   +2.58% |         -0.41%
 0m01.44s |  584744 ko | annotated_recs_d.vo     |  0m01.42s |  581236 ko || +0m00.02s ||      3508 ko |   +1.40% |         +0.60%
 0m01.43s |  582056 ko | annotated_recs_s.vo     |  0m01.36s |  580208 ko || +0m00.06s ||      1848 ko |   +5.14% |         +0.31%
 0m01.43s |  527752 ko | floor.vo                |  0m01.39s |  527316 ko || +0m00.04s ||       436 ko |   +2.87% |         +0.08%
 0m01.40s |  581340 ko | annotated_recs_z.vo     |  0m01.36s |  579060 ko || +0m00.03s ||      2280 ko |   +2.94% |         +0.39%
 0m01.40s |  562120 ko | shift.vo                |  0m01.16s |  527072 ko || +0m00.24s ||     35048 ko |  +20.68% |         +6.64%
 0m01.39s |  584464 ko | annotated_recs_b.vo     |  0m01.33s |  580796 ko || +0m00.05s ||      3668 ko |   +4.51% |         +0.63%
 0m01.39s |  583280 ko | annotated_recs_c.vo     |  0m01.30s |  582784 ko || +0m00.08s ||       496 ko |   +6.92% |         +0.08%
 0m01.31s |  578296 ko | seq_defs.vo             |  0m01.28s |  582328 ko || +0m00.03s ||     -4032 ko |   +2.34% |         -0.69%
 0m00.79s |  536020 ko | tactics.vo              |    N/A    |    N/A     || +0m00.79s ||    536020 ko |        ∞ |              ∞
   N/A    |     N/A    | conj.vo                 |  0m00.37s |  428064 ko || -0m00.37s ||   -428064 ko | -100.00% |       -100.00%
   N/A    |     N/A    | test_conj.vo            |  0m00.32s |  344520 ko || -0m00.32s ||   -344520 ko | -100.00% |       -100.00%

pi8027 · 2022-01-07T16:09:35Z

Note that fixing LPCIC/coq-elpi#320 seems to unblock possibilities for further performance improvements, e.g., locally introducing locked versions of field operators to optimize the second step of conversion (I have a patch to do this but it rather deoptimizes reification because of the issue of Coq-Elpi), that may make Algebra Tactics faster than the rat_field tactic, but I don't think it is mandatory for publishing a paper.

amahboubi · 2022-01-07T16:21:19Z

When trying to compile this branch on my machine (coq 8.14, mathcomp 1.13.0, algebra-tactics 0.1.0), I get an error in file binomialz.v at line l.187 (Cannot find witness). This line is a call to ring_lia. Any idea why?

pi8027 · 2022-01-07T16:24:48Z

@amahboubi You need Algebra Tactics 0.2.0 and Mczify 1.2.0 to compile this branch.

amahboubi · 2022-01-07T16:25:37Z

OK thanks.

theories/ops_for_s.v

theories/tactics.v

pi8027 · 2022-01-10T06:14:50Z

The last commit fixes some performance issues. So here is the new result of performance comparison using Coq 8.14.0 and MathComp 1.13.0:

   After |   Peak Mem | File Name               |   Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
--------------------------------------------------------------------------------------------------------------------------------
8m59.33s | 6131040 ko | Total Time / Peak Mem   | 9m50.52s | 3560136 ko || -0m51.19s ||   2570904 ko |   -8.66% |        +72.21%
--------------------------------------------------------------------------------------------------------------------------------
1m18.87s | 1699768 ko | hanson.vo               | 2m50.82s | 1885828 ko || -1m31.94s ||   -186060 ko |  -53.82% |         -9.86%
5m24.15s | 6131040 ko | ops_for_b.vo            | 4m45.78s | 3560136 ko || +0m38.37s ||   2570904 ko |  +13.42% |        +72.21%
0m12.30s |  805528 ko | ops_for_s.vo            | 0m09.10s |  631180 ko || +0m03.20s ||    174348 ko |  +35.16% |        +27.62%
  N/A    |     N/A    | field_tactics.vo        | 0m02.06s |  547732 ko || -0m02.06s ||   -547732 ko | -100.00% |       -100.00%
0m25.80s |  805636 ko | z3irrational.vo         | 0m26.82s |  814900 ko || -0m01.01s ||     -9264 ko |   -3.80% |         -1.13%
0m04.17s |  619672 ko | b_props.vo              | 0m02.75s |  618104 ko || +0m01.41s ||      1568 ko |  +51.63% |         +0.25%
  N/A    |     N/A    | lia_tactics.vo          | 0m01.67s |  566292 ko || -0m01.67s ||   -566292 ko | -100.00% |       -100.00%
  N/A    |     N/A    | test_field_tactics.vo   | 0m01.45s |  546172 ko || -0m01.44s ||   -546172 ko | -100.00% |       -100.00%
0m11.54s |  724044 ko | reduce_order.vo         | 0m11.92s |  731624 ko || -0m00.38s ||     -7580 ko |   -3.18% |         -1.03%
0m10.69s |  682080 ko | a_props.vo              | 0m10.61s |  644868 ko || +0m00.08s ||     37212 ko |   +0.75% |         +5.77%
0m04.29s |  626172 ko | ops_for_v.vo            | 0m03.84s |  600272 ko || +0m00.45s ||     25900 ko |  +11.71% |         +4.31%
0m04.22s |  652944 ko | ops_for_a.vo            | 0m03.45s |  596860 ko || +0m00.76s ||     56084 ko |  +22.31% |         +9.39%
0m04.19s |  612012 ko | algo_closures.vo        | 0m03.85s |  603680 ko || +0m00.34s ||      8332 ko |   +8.83% |         +1.38%
0m03.56s |  595684 ko | hanson_elem_analysis.vo | 0m03.99s |  597028 ko || -0m00.43s ||     -1344 ko |  -10.77% |         -0.22%
0m03.08s |  574880 ko | binomialz.vo            | 0m03.33s |  570740 ko || -0m00.25s ||      4140 ko |   -7.50% |         +0.72%
0m03.00s |  558980 ko | extra_mathcomp.vo       | 0m03.00s |  559160 ko || +0m00.00s ||      -180 ko |   +0.00% |         -0.03%
0m02.79s |  619400 ko | ops_for_u.vo            | 0m02.26s |  594316 ko || +0m00.53s ||     25084 ko |  +23.45% |         +4.22%
0m02.69s |  602796 ko | initial_conds.vo        | 0m02.51s |  595884 ko || +0m00.18s ||      6912 ko |   +7.17% |         +1.15%
0m02.55s |  560220 ko | bigopz.vo               | 0m02.48s |  563636 ko || +0m00.06s ||     -3416 ko |   +2.82% |         -0.60%
0m02.50s |  596908 ko | hanson_elem_arith.vo    | 0m02.53s |  595828 ko || -0m00.02s ||      1080 ko |   -1.18% |         +0.18%
0m02.49s |  624356 ko | b_over_a_props.vo       | 0m02.05s |  611828 ko || +0m00.44s ||     12528 ko |  +21.46% |         +2.04%
0m02.42s |  595548 ko | harmonic_numbers.vo     | 0m01.97s |  569904 ko || +0m00.44s ||     25644 ko |  +22.84% |         +4.49%
0m02.36s |  591428 ko | punk.vo                 | 0m02.25s |  560440 ko || +0m00.10s ||     30988 ko |   +4.88% |         +5.52%
0m02.27s |  535004 ko | extra_cauchyreals.vo    | 0m02.24s |  536036 ko || +0m00.02s ||     -1032 ko |   +1.33% |         -0.19%
0m02.11s |  587612 ko | c_props.vo              | 0m01.71s |  588168 ko || +0m00.39s ||      -556 ko |  +23.39% |         -0.09%
0m02.10s |  602248 ko | z3seq_props.vo          | 0m01.81s |  593036 ko || +0m00.29s ||      9212 ko |  +16.02% |         +1.55%
0m02.08s |  592612 ko | annotated_recs_v.vo     | 0m01.96s |  592720 ko || +0m00.12s ||      -108 ko |   +6.12% |         -0.01%
0m02.08s |  584728 ko | rho_computations.vo     | 0m01.67s |  565148 ko || +0m00.41s ||     19580 ko |  +24.55% |         +3.46%
0m02.00s |  557612 ko | multinomial.vo          | 0m02.01s |  561156 ko || -0m00.00s ||     -3544 ko |   -0.49% |         -0.63%
0m01.81s |  583644 ko | s_props.vo              | 0m01.98s |  588848 ko || -0m00.16s ||     -5204 ko |   -8.58% |         -0.88%
0m01.72s |  554092 ko | posnum.vo               | 0m01.70s |  552708 ko || +0m00.02s ||      1384 ko |   +1.17% |         +0.25%
0m01.69s |  531960 ko | arithmetics.vo          | 0m01.60s |  532736 ko || +0m00.08s ||      -776 ko |   +5.62% |         -0.14%
0m01.62s |  564544 ko | rat_of_Z.vo             | 0m01.37s |  548644 ko || +0m00.25s ||     15900 ko |  +18.24% |         +2.89%
0m01.53s |  583584 ko | annotated_recs_c.vo     | 0m01.49s |  581940 ko || +0m00.04s ||      1644 ko |   +2.68% |         +0.28%
0m01.52s |  585716 ko | annotated_recs_d.vo     | 0m01.52s |  585608 ko || +0m00.00s ||       108 ko |   +0.00% |         +0.01%
0m01.44s |  585316 ko | annotated_recs_z.vo     | 0m01.35s |  581972 ko || +0m00.08s ||      3344 ko |   +6.66% |         +0.57%
0m01.43s |  530312 ko | floor.vo                | 0m01.44s |  530196 ko || -0m00.01s ||       116 ko |   -0.69% |         +0.02%
0m01.42s |  585336 ko | annotated_recs_s.vo     | 0m01.43s |  586044 ko || -0m00.01s ||      -708 ko |   -0.69% |         -0.12%
0m01.39s |  584984 ko | annotated_recs_b.vo     | 0m01.41s |  585416 ko || -0m00.02s ||      -432 ko |   -1.41% |         -0.07%
0m01.36s |  563956 ko | shift.vo                | 0m01.20s |  527124 ko || +0m00.16s ||     36832 ko |  +13.33% |         +6.98%
0m01.31s |  580472 ko | seq_defs.vo             | 0m01.43s |  585972 ko || -0m00.11s ||     -5500 ko |   -8.39% |         -0.93%
0m00.80s |  536748 ko | tactics.vo              |   N/A    |    N/A     || +0m00.80s ||    536748 ko |        ∞ |              ∞
  N/A    |     N/A    | conj.vo                 | 0m00.41s |  435140 ko || -0m00.41s ||   -435140 ko | -100.00% |       -100.00%
  N/A    |     N/A    | test_conj.vo            | 0m00.31s |  347284 ko || -0m00.31s ||   -347284 ko | -100.00% |       -100.00%

and that using Coq 8.14.0 and MathComp 1.12.0:

    After |   Peak Mem | File Name               |    Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
----------------------------------------------------------------------------------------------------------------------------------
11m53.94s | 6262340 ko | Total Time / Peak Mem   | 10m50.40s | 3583380 ko || +1m03.53s ||   2678960 ko |   +9.76% |        +74.76%
----------------------------------------------------------------------------------------------------------------------------------
 7m21.56s | 6262340 ko | ops_for_b.vo            |  5m01.56s | 3583380 ko || +2m20.00s ||   2678960 ko |  +46.42% |        +74.76%
 1m17.65s | 1380956 ko | hanson.vo               |  2m57.93s | 1656176 ko || -1m40.28s ||   -275220 ko |  -56.35% |        -16.61%
 0m23.09s |  819044 ko | ops_for_s.vo            |  0m10.23s |  632292 ko || +0m12.85s ||    186752 ko | +125.70% |        +29.53%
 0m30.55s |  825204 ko | z3irrational.vo         |  0m41.25s |  803476 ko || -0m10.69s ||     21728 ko |  -25.93% |         +2.70%
 0m10.53s |  652984 ko | ops_for_a.vo            |  0m03.45s |  593180 ko || +0m07.07s ||     59804 ko | +205.21% |        +10.08%
 0m11.74s |  594072 ko | hanson_elem_analysis.vo |  0m04.88s |  598968 ko || +0m06.86s ||     -4896 ko | +140.57% |         -0.81%
 0m07.64s |  616420 ko | algo_closures.vo        |  0m04.18s |  600308 ko || +0m03.46s ||     16112 ko |  +82.77% |         +2.68%
 0m06.84s |  629132 ko | ops_for_v.vo            |  0m03.63s |  594656 ko || +0m03.20s ||     34476 ko |  +88.42% |         +5.79%
   N/A    |     N/A    | field_tactics.vo        |  0m03.64s |  546612 ko || -0m03.64s ||   -546612 ko | -100.00% |       -100.00%
 0m14.58s |  732992 ko | reduce_order.vo         |  0m13.10s |  739220 ko || +0m01.48s ||     -6228 ko |  +11.29% |         -0.84%
 0m04.17s |  611776 ko | ops_for_u.vo            |  0m02.40s |  588568 ko || +0m01.77s ||     23208 ko |  +73.75% |         +3.94%
 0m03.97s |  623680 ko | b_props.vo              |  0m02.64s |  612724 ko || +0m01.33s ||     10956 ko |  +50.37% |         +1.78%
 0m03.65s |  590780 ko | hanson_elem_arith.vo    |  0m02.61s |  592996 ko || +0m01.04s ||     -2216 ko |  +39.84% |         -0.37%
   N/A    |     N/A    | lia_tactics.vo          |  0m01.67s |  563840 ko || -0m01.67s ||   -563840 ko | -100.00% |       -100.00%
   N/A    |     N/A    | test_field_tactics.vo   |  0m01.44s |  544048 ko || -0m01.43s ||   -544048 ko | -100.00% |       -100.00%
 0m24.28s |  697460 ko | a_props.vo              |  0m23.67s |  655220 ko || +0m00.60s ||     42240 ko |   +2.57% |         +6.44%
 0m04.02s |  557784 ko | extra_mathcomp.vo       |  0m04.01s |  557124 ko || +0m00.00s ||       660 ko |   +0.24% |         +0.11%
 0m03.59s |  586292 ko | harmonic_numbers.vo     |  0m03.10s |  565768 ko || +0m00.48s ||     20524 ko |  +15.80% |         +3.62%
 0m03.30s |  594520 ko | z3seq_props.vo          |  0m03.01s |  590656 ko || +0m00.29s ||      3864 ko |   +9.63% |         +0.65%
 0m03.05s |  572188 ko | binomialz.vo            |  0m03.90s |  566080 ko || -0m00.85s ||      6108 ko |  -21.79% |         +1.07%
 0m02.85s |  583048 ko | s_props.vo              |  0m02.92s |  585348 ko || -0m00.06s ||     -2300 ko |   -2.39% |         -0.39%
 0m02.66s |  606020 ko | initial_conds.vo        |  0m02.49s |  594924 ko || +0m00.16s ||     11096 ko |   +6.82% |         +1.86%
 0m02.55s |  622632 ko | b_over_a_props.vo       |  0m02.21s |  609184 ko || +0m00.33s ||     13448 ko |  +15.38% |         +2.20%
 0m02.39s |  557432 ko | bigopz.vo               |  0m02.40s |  558480 ko || -0m00.00s ||     -1048 ko |   -0.41% |         -0.18%
 0m02.37s |  589428 ko | punk.vo                 |  0m02.19s |  559512 ko || +0m00.18s ||     29916 ko |   +8.21% |         +5.34%
 0m02.24s |  535512 ko | extra_cauchyreals.vo    |  0m02.24s |  532820 ko || +0m00.00s ||      2692 ko |   +0.00% |         +0.50%
 0m02.01s |  586768 ko | c_props.vo              |  0m01.71s |  586524 ko || +0m00.29s ||       244 ko |  +17.54% |         +0.04%
 0m01.98s |  556412 ko | multinomial.vo          |  0m02.01s |  555876 ko || -0m00.02s ||       536 ko |   -1.49% |         +0.09%
 0m01.97s |  592392 ko | annotated_recs_v.vo     |  0m01.98s |  591512 ko || -0m00.01s ||       880 ko |   -0.50% |         +0.14%
 0m01.89s |  580844 ko | rho_computations.vo     |  0m01.73s |  562728 ko || +0m00.15s ||     18116 ko |   +9.24% |         +3.21%
 0m01.71s |  552588 ko | posnum.vo               |  0m01.73s |  553132 ko || -0m00.02s ||      -544 ko |   -1.15% |         -0.09%
 0m01.58s |  530296 ko | arithmetics.vo          |  0m01.57s |  530280 ko || +0m00.01s ||        16 ko |   +0.63% |         +0.00%
 0m01.58s |  562220 ko | rat_of_Z.vo             |  0m01.44s |  547008 ko || +0m00.14s ||     15212 ko |   +9.72% |         +2.78%
 0m01.47s |  582796 ko | annotated_recs_d.vo     |  0m01.41s |  584876 ko || +0m00.06s ||     -2080 ko |   +4.25% |         -0.35%
 0m01.43s |  583260 ko | annotated_recs_s.vo     |  0m01.36s |  580704 ko || +0m00.06s ||      2556 ko |   +5.14% |         +0.44%
 0m01.41s |  527320 ko | floor.vo                |  0m01.39s |  528928 ko || +0m00.02s ||     -1608 ko |   +1.43% |         -0.30%
 0m01.40s |  583064 ko | annotated_recs_c.vo     |  0m01.36s |  581072 ko || +0m00.03s ||      1992 ko |   +2.94% |         +0.34%
 0m01.39s |  583860 ko | annotated_recs_b.vo     |  0m01.33s |  581720 ko || +0m00.05s ||      2140 ko |   +4.51% |         +0.36%
 0m01.38s |  582856 ko | annotated_recs_z.vo     |  0m01.44s |  580260 ko || -0m00.06s ||      2596 ko |   -4.16% |         +0.44%
 0m01.35s |  560552 ko | shift.vo                |  0m01.16s |  526724 ko || +0m00.19s ||     33828 ko |  +16.37% |         +6.42%
 0m01.31s |  579760 ko | seq_defs.vo             |  0m01.32s |  587464 ko || -0m00.01s ||     -7704 ko |   -0.75% |         -1.31%
 0m00.81s |  540340 ko | tactics.vo              |    N/A    |    N/A     || +0m00.81s ||    540340 ko |        ∞ |              ∞
   N/A    |     N/A    | conj.vo                 |  0m00.40s |  431612 ko || -0m00.40s ||   -431612 ko | -100.00% |       -100.00%
   N/A    |     N/A    | test_conj.vo            |  0m00.31s |  344256 ko || -0m00.31s ||   -344256 ko | -100.00% |       -100.00%

pi8027 · 2022-01-10T06:26:02Z

theories/a_props.v

-         by vm_compute. 
+    have squared (rat2 := rat_of_Z 2) :
+        (rho 2 * rat2 - alpha rat2) ^+ 2 <= delta rat2.
+      by rewrite /delta rho2_eq /alpha [_ <= _]refines_eq; vm_compute.


I found this rewrite [_ <= _]refines_eq fragile performance-wise. In the case of MathComp 1.12.0, if I do not unfold alpha before that, it becomes too slow. Is this because typeclass search performs wasteful computations?

pi8027 · 2022-02-02T17:29:42Z

Here is a new result of performance comparison using Coq 8.15.0, MathComp 1.14.0, LPCIC/coq-elpi#324, and the master branch of Algebra Tactics.

   After |   Peak Mem | File Name               |   Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
--------------------------------------------------------------------------------------------------------------------------------
7m18.91s | 3065132 ko | Total Time / Peak Mem   | 9m25.04s | 3533036 ko || -2m06.12s ||   -467904 ko |  -22.32% |        -13.24%
--------------------------------------------------------------------------------------------------------------------------------
1m12.04s | 1737720 ko | hanson.vo               | 2m54.96s | 1939128 ko || -1m42.92s ||   -201408 ko |  -58.82% |        -10.38%
4m24.57s | 3065132 ko | ops_for_b.vo            | 4m46.41s | 3533036 ko || -0m21.83s ||   -467904 ko |   -7.62% |        -13.24%
0m10.19s |  673116 ko | reduce_order.vo         | 0m11.32s |  723620 ko || -0m01.13s ||    -50504 ko |   -9.98% |         -6.97%
0m03.62s |  612472 ko | b_props.vo              | 0m02.26s |  607928 ko || +0m01.36s ||      4544 ko |  +60.17% |         +0.74%
  N/A    |     N/A    | field_tactics.vo        | 0m01.43s |  543488 ko || -0m01.42s ||   -543488 ko | -100.00% |       -100.00%
  N/A    |     N/A    | lia_tactics.vo          | 0m01.25s |  561420 ko || -0m01.25s ||   -561420 ko | -100.00% |       -100.00%
  N/A    |     N/A    | test_field_tactics.vo   | 0m01.12s |  542532 ko || -0m01.12s ||   -542532 ko | -100.00% |       -100.00%
0m13.64s |  784364 ko | z3irrational.vo         | 0m14.05s |  767756 ko || -0m00.41s ||     16608 ko |   -2.91% |         +2.16%
0m09.51s |  638484 ko | a_props.vo              | 0m10.10s |  642804 ko || -0m00.58s ||     -4320 ko |   -5.84% |         -0.67%
0m09.10s |  654320 ko | ops_for_s.vo            | 0m08.48s |  626024 ko || +0m00.61s ||     28296 ko |   +7.31% |         +4.51%
0m03.83s |  604180 ko | algo_closures.vo        | 0m03.51s |  595348 ko || +0m00.32s ||      8832 ko |   +9.11% |         +1.48%
0m03.32s |  598400 ko | ops_for_v.vo            | 0m03.34s |  590032 ko || -0m00.02s ||      8368 ko |   -0.59% |         +1.41%
0m03.12s |  603444 ko | ops_for_a.vo            | 0m02.77s |  586112 ko || +0m00.35s ||     17332 ko |  +12.63% |         +2.95%
0m02.83s |  585780 ko | hanson_elem_analysis.vo | 0m03.08s |  587744 ko || -0m00.25s ||     -1964 ko |   -8.11% |         -0.33%
0m02.50s |  572128 ko | binomialz.vo            | 0m02.85s |  564872 ko || -0m00.35s ||      7256 ko |  -12.28% |         +1.28%
0m02.25s |  550448 ko | extra_mathcomp.vo       | 0m02.33s |  549428 ko || -0m00.08s ||      1020 ko |   -3.43% |         +0.18%
0m02.20s |  595356 ko | initial_conds.vo        | 0m02.19s |  586796 ko || +0m00.01s ||      8560 ko |   +0.45% |         +1.45%
0m02.11s |  554040 ko | bigopz.vo               | 0m02.18s |  552448 ko || -0m00.07s ||      1592 ko |   -3.21% |         +0.28%
0m02.10s |  590856 ko | hanson_elem_arith.vo    | 0m01.99s |  589748 ko || +0m00.11s ||      1108 ko |   +5.52% |         +0.18%
0m02.09s |  582804 ko | punk.vo                 | 0m01.82s |  553996 ko || +0m00.26s ||     28808 ko |  +14.83% |         +5.20%
0m02.02s |  592964 ko | ops_for_u.vo            | 0m01.91s |  584628 ko || +0m00.11s ||      8336 ko |   +5.75% |         +1.42%
0m01.99s |  608484 ko | b_over_a_props.vo       | 0m01.71s |  602084 ko || +0m00.28s ||      6400 ko |  +16.37% |         +1.06%
0m01.83s |  586184 ko | harmonic_numbers.vo     | 0m01.50s |  564168 ko || +0m00.33s ||     22016 ko |  +22.00% |         +3.90%
0m01.76s |  530620 ko | extra_cauchyreals.vo    | 0m01.77s |  530776 ko || -0m00.01s ||      -156 ko |   -0.56% |         -0.02%
0m01.72s |  551172 ko | multinomial.vo          | 0m01.77s |  551880 ko || -0m00.05s ||      -708 ko |   -2.82% |         -0.12%
0m01.64s |  585732 ko | z3seq_props.vo          | 0m01.45s |  581516 ko || +0m00.18s ||      4216 ko |  +13.10% |         +0.72%
0m01.60s |  581372 ko | c_props.vo              | 0m01.15s |  579308 ko || +0m00.45s ||      2064 ko |  +39.13% |         +0.35%
0m01.59s |  578320 ko | rho_computations.vo     | 0m01.16s |  558532 ko || +0m00.43s ||     19788 ko |  +37.06% |         +3.54%
0m01.53s |  584688 ko | annotated_recs_v.vo     | 0m01.51s |  585140 ko || +0m00.02s ||      -452 ko |   +1.32% |         -0.07%
0m01.52s |  581376 ko | s_props.vo              | 0m01.42s |  582388 ko || +0m00.10s ||     -1012 ko |   +7.04% |         -0.17%
0m01.26s |  525564 ko | arithmetics.vo          | 0m01.24s |  525628 ko || +0m00.02s ||       -64 ko |   +1.61% |         -0.01%
0m01.15s |  577864 ko | annotated_recs_z.vo     | 0m00.99s |  575536 ko || +0m00.15s ||      2328 ko |  +16.16% |         +0.40%
0m01.13s |  578656 ko | annotated_recs_b.vo     | 0m01.11s |  577736 ko || +0m00.01s ||       920 ko |   +1.80% |         +0.15%
0m01.13s |  562632 ko | rat_of_Z.vo             | 0m01.02s |  542420 ko || +0m00.10s ||     20212 ko |  +10.78% |         +3.72%
0m01.12s |  577964 ko | annotated_recs_d.vo     | 0m01.18s |  576252 ko || -0m00.05s ||      1712 ko |   -5.08% |         +0.29%
0m01.08s |  578092 ko | annotated_recs_c.vo     | 0m01.02s |  576012 ko || +0m00.06s ||      2080 ko |   +5.88% |         +0.36%
0m01.08s |  579252 ko | annotated_recs_s.vo     | 0m01.10s |  577392 ko || -0m00.02s ||      1860 ko |   -1.81% |         +0.32%
0m01.02s |  523992 ko | floor.vo                | 0m01.03s |  525264 ko || -0m00.01s ||     -1272 ko |   -0.97% |         -0.24%
0m01.01s |  575768 ko | seq_defs.vo             | 0m00.98s |  578440 ko || +0m00.03s ||     -2672 ko |   +3.06% |         -0.46%
0m00.99s |  543756 ko | posnum.vo               | 0m01.01s |  543112 ko || -0m00.02s ||       644 ko |   -1.98% |         +0.11%
0m00.99s |  559376 ko | shift.vo                | 0m00.82s |  520612 ko || +0m00.17s ||     38764 ko |  +20.73% |         +7.44%
0m00.74s |  538172 ko | tactics.vo              |   N/A    |    N/A     || +0m00.74s ||    538172 ko |        ∞ |              ∞
  N/A    |     N/A    | conj.vo                 | 0m00.45s |  428188 ko || -0m00.45s ||   -428188 ko | -100.00% |       -100.00%
  N/A    |     N/A    | test_conj.vo            | 0m00.31s |  343464 ko || -0m00.31s ||   -343464 ko | -100.00% |       -100.00%

pi8027 · 2022-03-30T15:16:08Z

FYI, the Algebra Tactics paper has been accepted to ITP'22. I will try to finish this PR before submitting the final version (deadline: Apr. 27).

gares · 2022-04-01T15:31:54Z

Ci failure should solve itself automagically soon when the docker images will get opam 2.1

erikmd · 2022-04-14T16:38:26Z

Just FYI @pi8027 I restarted the last GHA run, and the recompilation-slowdown issue you reported seems to be fixed:

Details / beforehand → 41 minutes

Details / henceforth → 21 minutes

→ no spurious switch recompilation anymore (see e.g. these ⋅ three ⋅ jobs)

pi8027 · 2022-04-22T08:41:52Z

Thanks @erikmd. That's really helpful.

gares · 2022-04-22T10:13:11Z

Is this PR ready then?

pi8027 · 2022-04-22T10:21:40Z

@gares I'd like to merge #11 first and then rebase again, but could not get any response from Assia until now.

gares · 2022-04-22T12:08:03Z

well, lets tag @amahboubi

pi8027 · 2022-04-25T12:04:07Z

I will do the benchmark again. Then this PR should be ready to merge.

pi8027 · 2022-04-25T14:19:10Z

With Coq Platform 2022.04.0, Algebra Tactics a2edba0, and Apery 4f6f581...7335782, I obtained the following result:

   After |   Peak Mem | File Name               |   Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
--------------------------------------------------------------------------------------------------------------------------------
6m52.12s | 2563904 ko | Total Time / Peak Mem   | 9m23.25s | 3639592 ko || -2m31.13s ||  -1075688 ko |  -26.83% |        -29.55%
--------------------------------------------------------------------------------------------------------------------------------
0m54.94s | 1352004 ko | hanson.vo               | 2m51.03s | 1646412 ko || -1m56.09s ||   -294408 ko |  -67.87% |        -17.88%
4m15.97s | 2563904 ko | ops_for_b.vo            | 4m48.03s | 3639592 ko || -0m32.05s ||  -1075688 ko |  -11.13% |        -29.55%
0m13.50s |  774940 ko | z3irrational.vo         | 0m14.77s |  778320 ko || -0m01.26s ||     -3380 ko |   -8.59% |         -0.43%
0m10.09s |  665816 ko | reduce_order.vo         | 0m11.91s |  718232 ko || -0m01.82s ||    -52416 ko |  -15.28% |         -7.29%
0m03.53s |  612436 ko | b_props.vo              | 0m02.25s |  608064 ko || +0m01.27s ||      4372 ko |  +56.88% |         +0.71%
  N/A    |     N/A    | field_tactics.vo        | 0m01.45s |  545316 ko || -0m01.44s ||   -545316 ko | -100.00% |       -100.00%
  N/A    |     N/A    | lia_tactics.vo          | 0m01.29s |  563080 ko || -0m01.29s ||   -563080 ko | -100.00% |       -100.00%
0m09.91s |  635132 ko | a_props.vo              | 0m10.62s |  633328 ko || -0m00.70s ||      1804 ko |   -6.68% |         +0.28%
0m09.18s |  640628 ko | ops_for_s.vo            | 0m08.48s |  625784 ko || +0m00.69s ||     14844 ko |   +8.25% |         +2.37%
0m03.60s |  603812 ko | algo_closures.vo        | 0m03.55s |  599884 ko || +0m00.05s ||      3928 ko |   +1.40% |         +0.65%
0m03.30s |  602776 ko | ops_for_v.vo            | 0m03.37s |  596696 ko || -0m00.07s ||      6080 ko |   -2.07% |         +1.01%
0m02.76s |  599272 ko | ops_for_a.vo            | 0m03.00s |  599852 ko || -0m00.24s ||      -580 ko |   -8.00% |         -0.09%
0m02.62s |  573368 ko | binomialz.vo            | 0m02.83s |  572448 ko || -0m00.20s ||       920 ko |   -7.42% |         +0.16%
0m02.62s |  589324 ko | hanson_elem_analysis.vo | 0m02.64s |  589540 ko || -0m00.02s ||      -216 ko |   -0.75% |         -0.03%
0m02.25s |  551112 ko | extra_mathcomp.vo       | 0m02.41s |  552128 ko || -0m00.16s ||     -1016 ko |   -6.63% |         -0.18%
0m02.17s |  589936 ko | hanson_elem_arith.vo    | 0m02.09s |  592156 ko || +0m00.08s ||     -2220 ko |   +3.82% |         -0.37%
0m02.10s |  600032 ko | initial_conds.vo        | 0m02.16s |  596140 ko || -0m00.06s ||      3892 ko |   -2.77% |         +0.65%
0m02.09s |  553876 ko | bigopz.vo               | 0m02.08s |  559804 ko || +0m00.00s ||     -5928 ko |   +0.48% |         -1.05%
0m02.00s |  598240 ko | ops_for_u.vo            | 0m01.97s |  589956 ko || +0m00.03s ||      8284 ko |   +1.52% |         +1.40%
0m02.00s |  583488 ko | punk.vo                 | 0m01.87s |  560440 ko || +0m00.12s ||     23048 ko |   +6.95% |         +4.11%
0m01.93s |  530572 ko | extra_cauchyreals.vo    | 0m01.86s |  537416 ko || +0m00.06s ||     -6844 ko |   +3.76% |         -1.27%
0m01.82s |  607664 ko | b_over_a_props.vo       | 0m01.68s |  606664 ko || +0m00.14s ||      1000 ko |   +8.33% |         +0.16%
0m01.70s |  585536 ko | harmonic_numbers.vo     | 0m01.49s |  572376 ko || +0m00.20s ||     13160 ko |  +14.09% |         +2.29%
0m01.63s |  578860 ko | rho_computations.vo     | 0m01.17s |  561716 ko || +0m00.46s ||     17144 ko |  +39.31% |         +3.05%
0m01.60s |  584932 ko | z3seq_props.vo          | 0m01.32s |  587340 ko || +0m00.28s ||     -2408 ko |  +21.21% |         -0.40%
0m01.58s |  592540 ko | annotated_recs_v.vo     | 0m01.63s |  590528 ko || -0m00.04s ||      2012 ko |   -3.06% |         +0.34%
0m01.58s |  582932 ko | c_props.vo              | 0m01.18s |  585436 ko || +0m00.40s ||     -2504 ko |  +33.89% |         -0.42%
0m01.53s |  552584 ko | multinomial.vo          | 0m01.52s |  557220 ko || +0m00.01s ||     -4636 ko |   +0.65% |         -0.83%
0m01.49s |  581360 ko | s_props.vo              | 0m01.55s |  583396 ko || -0m00.06s ||     -2036 ko |   -3.87% |         -0.34%
0m01.21s |  529124 ko | arithmetics.vo          | 0m01.28s |  536876 ko || -0m00.07s ||     -7752 ko |   -5.46% |         -1.44%
0m01.15s |  561512 ko | rat_of_Z.vo             | 0m01.13s |  548008 ko || +0m00.02s ||     13504 ko |   +1.76% |         +2.46%
0m01.14s |  586688 ko | annotated_recs_d.vo     | 0m01.12s |  585108 ko || +0m00.01s ||      1580 ko |   +1.78% |         +0.27%
0m01.09s |  586796 ko | annotated_recs_c.vo     | 0m01.14s |  584292 ko || -0m00.04s ||      2504 ko |   -4.38% |         +0.42%
0m01.09s |  589640 ko | annotated_recs_z.vo     | 0m01.02s |  584640 ko || +0m00.07s ||      5000 ko |   +6.86% |         +0.85%
0m01.08s |  592156 ko | annotated_recs_s.vo     | 0m01.01s |  585320 ko || +0m00.07s ||      6836 ko |   +6.93% |         +1.16%
0m01.07s |  568296 ko | shift.vo                | 0m00.88s |  530136 ko || +0m00.19s ||     38160 ko |  +21.59% |         +7.19%
0m01.02s |  525544 ko | floor.vo                | 0m01.04s |  534924 ko || -0m00.02s ||     -9380 ko |   -1.92% |         -1.75%
0m01.01s |  588528 ko | annotated_recs_b.vo     | 0m00.99s |  584988 ko || +0m00.02s ||      3540 ko |   +2.02% |         +0.60%
0m01.01s |  545952 ko | posnum.vo               | 0m01.04s |  545780 ko || -0m00.03s ||       172 ko |   -2.88% |         +0.03%
0m00.99s |  578420 ko | seq_defs.vo             | 0m00.97s |  581636 ko || +0m00.02s ||     -3216 ko |   +2.06% |         -0.55%
0m00.77s |  539688 ko | tactics.vo              |   N/A    |    N/A     || +0m00.77s ||    539688 ko |        ∞ |              ∞
  N/A    |     N/A    | conj.vo                 | 0m00.44s |  430944 ko || -0m00.44s ||   -430944 ko | -100.00% |       -100.00%

pi8027 · 2022-04-25T14:28:17Z

@amahboubi This PR is also ready to merge. When you merge this PR, please "create a merge commit" rather than "squash and merge" if you are ok with that. I intentionally split this work into 6 commits, which might be useful for further performance investigation.

pi8027 commented Oct 18, 2021

View reviewed changes

theories/hanson.v Outdated Show resolved Hide resolved

pi8027 changed the title ~~Replace lia_tactics and field_tactics with mczify and Algebra Tactics~~ [DO NOT MERGE] Replace lia_tactics and field_tactics with mczify and Algebra Tactics Oct 18, 2021

pi8027 commented Oct 20, 2021

View reviewed changes

theories/ops_for_b.v Show resolved Hide resolved

theories/ops_for_b.v Show resolved Hide resolved

This was referenced Oct 20, 2021

Fix some performance issues in reification math-comp/algebra-tactics#26

Merged

Fine grained addition in rat math-comp/math-comp#808

Merged

Bump MathComp version to >= 1.12.0 #3

Merged

pi8027 mentioned this pull request Dec 23, 2021

Context readback can be a performance bottleneck LPCIC/coq-elpi#320

Closed

pi8027 commented Jan 8, 2022

View reviewed changes

theories/ops_for_s.v Show resolved Hide resolved

pi8027 commented Jan 8, 2022

View reviewed changes

theories/tactics.v Outdated Show resolved Hide resolved

pi8027 commented Jan 10, 2022

View reviewed changes

pi8027 mentioned this pull request Feb 3, 2022

Clean up proofs #9

Merged

pi8027 mentioned this pull request Mar 31, 2022

Clean up deprecation warnings and Require Imports #11

Merged

pi8027 changed the title ~~[DO NOT MERGE] Replace lia_tactics and field_tactics with mczify and Algebra Tactics~~ Replace lia_tactics and field_tactics with mczify and Algebra Tactics Apr 25, 2022

pi8027 added 6 commits April 25, 2022 21:01

Remove test files for tactics

4f6f581

Replace lia_tactics and field_tactics with mczify and Algebra Tactics

dde1a72

Modify binomialz to return int rather than rat

8449081

Replace rat_of_positive with rat_of_Z

84b5e9d

Ad-hoc fix for a performance issue

85b750d

Compatibility with math-comp/math-comp#841

7335782

pi8027 marked this pull request as ready for review April 25, 2022 14:19

amahboubi merged commit aa7d914 into coq-community:master May 3, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Replace `lia_tactics` and `field_tactics` with mczify and Algebra Tactics #4

Replace `lia_tactics` and `field_tactics` with mczify and Algebra Tactics #4

pi8027 commented Oct 18, 2021 •

edited

Loading

pi8027 commented Dec 15, 2021 •

edited

Loading

pi8027 commented Dec 16, 2021 •

edited

Loading

pi8027 commented Dec 16, 2021 •

edited

Loading

pi8027 commented Dec 22, 2021

gares commented Dec 23, 2021

pi8027 commented Dec 23, 2021

pi8027 commented Dec 23, 2021 •

edited

Loading

pi8027 commented Dec 28, 2021 •

edited

Loading

amahboubi commented Jan 6, 2022 •

edited

Loading

pi8027 commented Jan 6, 2022 •

edited

Loading

pi8027 commented Jan 7, 2022 •

edited

Loading

pi8027 commented Jan 7, 2022

pi8027 commented Jan 7, 2022 •

edited

Loading

amahboubi commented Jan 7, 2022 •

edited

Loading

pi8027 commented Jan 7, 2022

amahboubi commented Jan 7, 2022

pi8027 commented Jan 10, 2022

pi8027 Jan 10, 2022 •

edited

Loading

pi8027 commented Feb 2, 2022

pi8027 commented Mar 30, 2022

gares commented Apr 1, 2022

erikmd commented Apr 14, 2022

pi8027 commented Apr 22, 2022

gares commented Apr 22, 2022

pi8027 commented Apr 22, 2022

gares commented Apr 22, 2022

pi8027 commented Apr 25, 2022

pi8027 commented Apr 25, 2022 •

edited

Loading

pi8027 commented Apr 25, 2022 •

edited

Loading

Replace lia_tactics and field_tactics with mczify and Algebra Tactics #4

Replace lia_tactics and field_tactics with mczify and Algebra Tactics #4

Conversation

pi8027 commented Oct 18, 2021 • edited Loading

pi8027 commented Dec 15, 2021 • edited Loading

pi8027 commented Dec 16, 2021 • edited Loading

pi8027 commented Dec 16, 2021 • edited Loading

pi8027 commented Dec 22, 2021

gares commented Dec 23, 2021

pi8027 commented Dec 23, 2021

pi8027 commented Dec 23, 2021 • edited Loading

pi8027 commented Dec 28, 2021 • edited Loading

amahboubi commented Jan 6, 2022 • edited Loading

pi8027 commented Jan 6, 2022 • edited Loading

pi8027 commented Jan 7, 2022 • edited Loading

pi8027 commented Jan 7, 2022

pi8027 commented Jan 7, 2022 • edited Loading

amahboubi commented Jan 7, 2022 • edited Loading

pi8027 commented Jan 7, 2022

amahboubi commented Jan 7, 2022

pi8027 commented Jan 10, 2022

pi8027 Jan 10, 2022 • edited Loading

Choose a reason for hiding this comment

pi8027 commented Feb 2, 2022

pi8027 commented Mar 30, 2022

gares commented Apr 1, 2022

erikmd commented Apr 14, 2022

pi8027 commented Apr 22, 2022

gares commented Apr 22, 2022

pi8027 commented Apr 22, 2022

gares commented Apr 22, 2022

pi8027 commented Apr 25, 2022

pi8027 commented Apr 25, 2022 • edited Loading

pi8027 commented Apr 25, 2022 • edited Loading

Replace `lia_tactics` and `field_tactics` with mczify and Algebra Tactics #4

Replace `lia_tactics` and `field_tactics` with mczify and Algebra Tactics #4

pi8027 commented Oct 18, 2021 •

edited

Loading

pi8027 commented Dec 15, 2021 •

edited

Loading

pi8027 commented Dec 16, 2021 •

edited

Loading

pi8027 commented Dec 16, 2021 •

edited

Loading

pi8027 commented Dec 23, 2021 •

edited

Loading

pi8027 commented Dec 28, 2021 •

edited

Loading

amahboubi commented Jan 6, 2022 •

edited

Loading

pi8027 commented Jan 6, 2022 •

edited

Loading

pi8027 commented Jan 7, 2022 •

edited

Loading

pi8027 commented Jan 7, 2022 •

edited

Loading

amahboubi commented Jan 7, 2022 •

edited

Loading

pi8027 Jan 10, 2022 •

edited

Loading

pi8027 commented Apr 25, 2022 •

edited

Loading

pi8027 commented Apr 25, 2022 •

edited

Loading