Skip to content

feat: port tactic hint#5363

Closed
Komyyy wants to merge 18 commits intomasterfrom
port/Tactic.Hint
Closed

feat: port tactic hint#5363
Komyyy wants to merge 18 commits intomasterfrom
port/Tactic.Hint

Conversation

@Komyyy
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy commented Jun 22, 2023 •
edited
Loading

This PR also change the implemention of fail_of_no_progress, because the current implemention discards some errors.

Open in Gitpod

Komyyy added 3 commits June 22, 2023 12:37
@Komyyy
feat: port Tactic.Hint
c0439d9
@Komyyy
Initial file copy from mathport
a9bc2aa
@Komyyy
automated fixes
f1346a0 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy Komyyy added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Jun 22, 2023
@Komyyy Komyyy mentioned this pull request Jun 22, 2023
Open
@Komyyy Komyyy added the t-meta Tactics, attributes or user commands label Jun 23, 2023
@Komyyy Komyyy added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Jun 23, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 23, 2023
@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 4, 2023

How do your changes to fail_if_no_progress interact with those in #3757. Do you have a MWE of situation where your changes are needed we can check out with in the #3757 branch

@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented Aug 5, 2023

@alexjbest
This change doesn't interact with #3757.

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 5, 2023

They both modify runAndFailIfNoProgress though right? I'm asking as it seems if we merge both these PRs there will be a conflict (or whichever one is merged first the other one will need to be updating). Can you give an MWE of what the difference between your modified runAndFailIfNoProgress and the original one is?

@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented Aug 5, 2023

In runAndFailIfNoProgress, Lean.Elab.Tactic.run is used to run a tactic for a metavariable. However, Lean.Elab.Tactic.run discards metavariable assignment errors and this causes issues in hint. runAndFailIfNoProgress is modified in #3757 but Lean.Elab.Tactic.run is still used so these changes are independent each other. Unfortunately, adjacent lines are changed in #3757 so there will be a conflict, so the second PR should be updated.

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 7, 2023

can you add a test to tests/fail_if_no_progress.lean demonstrating this difference? i.e something that used to fail or used to succeed before your change that doesn't any more

thorimur
thorimur reviewed Aug 10, 2023
View reviewed changes
Mathlib/Tactic/FailIfNoProgress.lean
Comment on lines +51 to +59
let l ← do
let gs ← getGoals
try
setGoals [goal]
tacs
pruneSolvedGoals
getGoals
finally
setGoals gs
Copy link
Copy Markdown
Contributor

@thorimur thorimur Aug 10, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is probably fine! It might even be better than using run. :) But I noticed that run does some fancy things with pendingMVars and the like which we don't do here. What exactly is the issue that motivated this change? I know you mentioned it involved discarding metavariable assignment errors, but do you have an example? I'd just like to diagnose what's going wrong with run.

Copy link
Copy Markdown
Contributor Author

@Komyyy Komyyy Aug 13, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Without this change, hint suggests the following tactics solve the goal: tauto even if it fails by a metavariable assignment error.

@Komyyy @thorimur
comment
7f19e65 
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
@Komyyy Komyyy added WIP Work in progress and removed awaiting-review labels Aug 11, 2023
@Komyyy Komyyy added the blocked-by-batt-PR This PR depends on a PR to Batteries label Aug 13, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 13, 2023
@Komyyy Komyyy removed the WIP Work in progress label Aug 13, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24
@kim-em kim-em changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:17
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 24, 2023
@Komyyy Komyyy added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-batt-PR This PR depends on a PR to Batteries labels Oct 24, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 24, 2023
@ghost
Copy link
Copy Markdown

ghost commented Oct 24, 2023

This PR/issue depends on:

@Komyyy Komyyy added the WIP Work in progress label Oct 25, 2023
@Komyyy Komyyy added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Oct 25, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 25, 2023
@timotree3 timotree3 mentioned this pull request Nov 13, 2023
Closed
@Komyyy
Copy link
Copy Markdown
Contributor Author

Komyyy commented Nov 14, 2023

#8363

@Komyyy Komyyy closed this Nov 14, 2023
@Komyyy Komyyy deleted the port/Tactic.Hint branch May 10, 2024 08:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@thorimur thorimur thorimur left review comments

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. t-meta Tactics, attributes or user commands

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Komyyy @alexjbest @thorimur