Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support uint constants #72

Merged
merged 5 commits into from
Nov 24, 2022
Merged

Support uint constants #72

merged 5 commits into from
Nov 24, 2022

Conversation

pi8027
Copy link
Member

@pi8027 pi8027 commented Nov 23, 2022

TODOs:

  • implement the same feature in ring and field,
  • double-check Strategy expand declarations, and
  • investigate the issue that the proof of vcgen_25 is not very fast.

cc: @proux01

@pi8027 pi8027 marked this pull request as draft November 23, 2022 21:51
@pi8027
Copy link
Member Author

pi8027 commented Nov 24, 2022

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.

@pi8027 pi8027 mentioned this pull request Nov 24, 2022
Merged
@pi8027 pi8027 changed the title [WIP] support uint constants Support uint constants Nov 24, 2022
@pi8027 pi8027 marked this pull request as ready for review November 24, 2022 16:48
@pi8027
Copy link
Member Author

pi8027 commented Nov 24, 2022

TODOs have been addressed. Let's merge.

@pi8027 pi8027 merged commit 6e29809 into master Nov 24, 2022
@pi8027 pi8027 deleted the uint branch November 24, 2022 18:13
@pi8027 pi8027 mentioned this pull request Nov 25, 2022
9 tasks
@pi8027
Copy link
Member Author

pi8027 commented Nov 25, 2022

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant