search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Optimize tactics by locally locking ring operators (a better reimplementation of #41) #43

Closed pi8027 closed 2 years ago

pi8027 commented 2 years ago

Closes #41

pi8027 commented 2 years ago

Benchmark in Apery, with Algebra Tactics 0.2.0 and LPCIC/coq-elpi#324:

COQC theories/ops_for_b.v
Reification: 2.333564 sec.
Reflection: 80.716598 sec.
Tactic call ran for 83.249 secs (83.091u,0.175s) (success)
Reification: 0.589510 sec.
Reflection: 0.149027 sec.
Reification: 0.000801 sec.
Reflection: 0.007800 sec.
Reification: 1.444862 sec.
Reflection: 1.540885 sec.
Tactic call ran for 3.109 secs (3.1u,0.007s) (success)
Reification: 18.794122 sec.
Reflection: 18.475063 sec.
Tactic call ran for 38.268 secs (38.085u,0.172s) (success)

with this PR and LPCIC/coq-elpi#324:

COQC theories/ops_for_b.v
Reification: 2.251499 sec.
Reflection: 79.704100 sec.
Tactic call ran for 82.125 secs (81.938u,0.155s) (success)
Reification: 0.582115 sec.
Reflection: 0.117304 sec.
Reification: 0.000794 sec.
Reflection: 0.003693 sec.
Reification: 1.369246 sec.
Reflection: 0.928707 sec.
Tactic call ran for 2.409 secs (2.409u,0.s) (success)
Reification: 18.773050 sec.
Reflection: 10.341036 sec.
Tactic call ran for 30.088 secs (29.869u,0.219s) (success)