This repository was archived by the owner on Jul 24, 2024. It is now read-only.
fix(tactic/core): remove all_goals option from apply_any#2275
Merged
mergify[bot] merged 3 commits intomasterfrom Mar 29, 2020
Merged
fix(tactic/core): remove all_goals option from apply_any#2275mergify[bot] merged 3 commits intomasterfrom
mergify[bot] merged 3 commits intomasterfrom
Conversation
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
Fixes the -T50000 regression just noticed by Kevin.
#2245 introduced a regression, essentially breaking
set_theory/pgame.lean. This wasn't caught by CI because it's a performance regression, which madesolve_by_elimenormously slower on some tasks.The problem was that I added an
all_goalsoption toapply_any, which told it to try to apply one of its lemmas to any of the goals.apply_any lemmas {all_goals := tt}is equivalent toany_goal {apply_any lemmas}.all_goalsto true. In some situations, this now causessolve_by_elimto try solving unsolvable subgoals in all possible orders, causing a combinatorial slowdown.This PR simply removes the
all_goalsoption fromapply_any. (See point 1!) Note thatsolve_by_elim*, which tries to solve all goals at once, still works exactly as before, and as expected --- as long as you expect that its behaviour is to first solve the first goal, then try to solve the second goal, backtracking to a different solution of the first goal if that fails, and so on.The file
src/set_theory/pgame.leannow compiles again all the way down to-T6000.(I also took the opportunity to remove some unnecessary imports from this file, and I promise this is orthogonal to the slowdown issue!)