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.

Sign up for GitHub

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

Jump to bottom

Option to disable lia caching #10772

Closed
samuelgruetter opened this issue Sep 19, 2019 · 1 comment · Fixed by #10765
Closed

Option to disable lia caching #10772

samuelgruetter opened this issue Sep 19, 2019 · 1 comment · Fixed by #10765
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
Milestone
8.11+beta1

Comments

@samuelgruetter
Copy link
Contributor

No matter how fast or slow lia caching is, it would be good to have an option to turn off the lia cache. This would make it easier to understand benchmark results, enable us to test whether it actually improves performance at all, and simplify lia benchmarking.

/cc @fajb @thery @andres-erbsen
@pi8027 pi8027 added kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic. labels Sep 20, 2019
@llelf
Copy link
Contributor

llelf commented Sep 22, 2019

Does not #10765 (the “fast” part) address it?

fajb added a commit to fajb/coq that referenced this issue Sep 23, 2019
@fajb
Improved handling of micromega caches
9973a8f 
- Specialised hash function. Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.

fixes coq#10772, fixes coq#10743
fajb added a commit to fajb/coq that referenced this issue Sep 24, 2019
@fajb
Improved handling of micromega caches
1e473d1 
- Specialised hash function. Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.

fixes coq#10772, fixes coq#10743
@fajb fajb mentioned this issue Sep 24, 2019
Merged
fajb added a commit to fajb/coq that referenced this issue Sep 26, 2019
@fajb
Improved handling of micromega caches
e15956b 
- Specialised hash and eaulity functions.
  Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.

fixes coq#10772
@ppedrot ppedrot closed this as completed in 65b89a6 Oct 3, 2019
@Zimmi48 Zimmi48 added this to the 8.11+beta1 milestone Jul 4, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: micromega The lia, nia, lra, nra and psatz tactics. Also the legacy omega tactic.
Projects
None yet
Milestone
8.11+beta1
Development

Successfully merging a pull request may close this issue.

Improved handling of micromega caches fajb/coq
4 participants
@pi8027 @llelf @Zimmi48 @samuelgruetter