Repository navigation
fix(clone): no quadratic check of proved lemmas in theory overrides - #1208
Merged
Merged
Conversation
A theory override leaves alone the items that already have an override. For each lemma of the overridden theory, it scanned the whole list of the proofs given so far, which includes those implied by the previous theory overrides of the clone: a clone threading several large theories with theory overrides spent most of its time comparing qualified names. The names of the lemmas already proved are now collected in a hash table, once per theory override.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A theory override leaves alone the items that already have an
override. For each lemma of the overridden theory, it scanned the
whole list of the proofs given so far, which includes those implied by
the previous theory overrides of the clone: a clone threading several
large theories with theory overrides spent most of its time comparing
qualified names. The names of the lemmas already proved are now
collected in a hash table, once per theory override.