math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
29 stars 1 forks source link

Support uint constants #72

Closed pi8027 closed 1 year ago

pi8027 commented 1 year ago

TODOs:

cc: @proux01

pi8027 commented 1 year ago
Lemma vcgen_25 ...
Proof.
move=> *.
Time lra. (* Finished transaction in 4.308 secs (3.801u,0.007s) (successful) *)
Restart.
Time lra. (* Finished transaction in 0.57 secs (0.552u,0.s) (successful) *)
Qed.

This is exactly the issue I pointed out in https://github.com/math-comp/algebra-tactics/pull/54#discussion_r1029139823. I will fix it in a separate PR.

pi8027 commented 1 year ago

TODOs have been addressed. Let's merge.

pi8027 commented 1 year ago
Lemma vcgen_25 ...
Proof.
move=> *.
Time lra. (* Finished transaction in 4.308 secs (3.801u,0.007s) (successful) *)
Restart.
Time lra. (* Finished transaction in 0.57 secs (0.552u,0.s) (successful) *)
Qed.

This is exactly the issue I pointed out in #54 (comment). I will fix it in a separate PR.

I implemented the proposed solution (#74), but it does not fix the issue. The significant slowdown comes from coq.typecheck. I guess that coq.typecheck can be very slow in the presence of many large hypotheses. Does it explain the issue? @gares