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

[Merged by Bors] - feat: tweak calc widget #22170

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat: tweak calc widget #22170

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
6e492e4
feat: tweak calc widget
PatrickMassot Feb 21, 2025
ff1784d
Missing docstring
PatrickMassot Feb 21, 2025
3051446
Add a test
PatrickMassot Feb 22, 2025
cc6102e
Add withMainContext
PatrickMassot Feb 22, 2025
873e5d1
Update Mathlib/Tactic/Widget/Calc.lean
PatrickMassot Feb 23, 2025
1b23537
Update MathlibTest/CalcQuestionMark.lean
PatrickMassot Feb 23, 2025
dd2c462
Add a test with an overly long line
eric-wieser Feb 23, 2025
2fcd4ea
indent the calc
eric-wieser Feb 23, 2025
1255d3d
actually test the test, oops
eric-wieser Feb 23, 2025
295dd76
Switch to using Syntax instead of String for try this messages
eric-wieser Feb 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 20 additions & 7 deletions Mathlib/Tactic/Widget/Calc.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot
-/
import Lean.Elab.Tactic.Calc
import Lean.Meta.Tactic.TryThis

import Mathlib.Data.String.Defs
import Mathlib.Tactic.Widget.SelectPanelUtils
Expand Down Expand Up @@ -76,7 +77,8 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
let mut goalType := goalType
for pos in subexprPos do
goalType ← insertMetaVar goalType pos
let some (_, newLhs, newRhs) ← Lean.Elab.Term.getCalcRelation? goalType | unreachable!
let some (_, newLhs, newRhs) ← Lean.Elab.Term.getCalcRelation? goalType |
throwError "invalid 'calc' step, relation expected{indentExpr goalType}"

let lhsStr := (toString <| ← Meta.ppExpr lhs).renameMetaVar
let newLhsStr := (toString <| ← Meta.ppExpr newLhs).renameMetaVar
Expand Down Expand Up @@ -115,7 +117,7 @@ def suggestSteps (pos : Array Lean.SubExpr.GoalsLocation) (goalType : Expr) (par
/-- Rpc function for the calc widget. -/
@[server_rpc_method]
def CalcPanel.rpc := mkSelectionPanelRPC suggestSteps
"Please select subterms."
"Please select subterms using Shift-click."
"Calc 🔍"

/-- The calc widget. -/
Expand All @@ -124,19 +126,30 @@ def CalcPanel : Component CalcParams :=
mk_rpc_widget% CalcPanel.rpc

namespace Lean.Elab.Tactic
open Meta

open Lean Meta Tactic TryThis in
/-- Create a `calc` proof. -/
elab stx:"calc?" : tactic => withMainContext do
let some calcRange := (← getFileMap).rangeOfStx? stx | throwError "calc? failed"
let indent := calcRange.start.character + 2
let spc := String.replicate indent ' '
let goalType ← whnfR (← getMainTarget)
unless (← Lean.Elab.Term.getCalcRelation? goalType).isSome do
throwError "Cannot start a calculation here: the goal{indentExpr goalType}\nis not a relation."
let goalFmt ← Meta.ppExpr (← getMainTarget)
let s := s!"calc\n{spc}{goalFmt} := by sorry"
addSuggestions (← getRef) #[.suggestion s] (header := "Create calc tactic:")
Copy link
Member

Choose a reason for hiding this comment

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

I think it would be better to construct this from a TSyntax object than from a string; was there a reason you didn't do that?

Copy link
Member

@eric-wieser eric-wieser Feb 22, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

That is

Suggested change
let s := s!"calc\n{spc}{goalFmt} := by sorry"
addSuggestions (← getRef) #[.suggestion s] (header := "Create calc tactic:")
let s ← `(tactic| calc $(← Lean.PrettyPrinter.delab (← getMainTarget)) := by sorry)
addSuggestions (← getRef) #[.suggestion s] (header := "Create calc tactic:")

(and remove all the unused code prior to this line)

Copy link
Member

@eric-wieser eric-wieser Feb 22, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

(there is a bug, leanprover/lean4#7191, in the #guard_msgs result, but the widget works correctly)

Copy link
Member Author

Choose a reason for hiding this comment

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

I specifically want to handle spaces here.

Copy link
Member

Choose a reason for hiding this comment

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

According to my test, the Syntax version already handles the spaces correctly for you in all the ways that matter (everything but guard_msgs).

Copy link
Collaborator

Choose a reason for hiding this comment

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

In case it is helpful, my local test also displays the wrong spacing, but the action really inserts the correct indentation.

Copy link
Member

@eric-wieser eric-wieser Feb 23, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

In case it is helpful, my local test also displays the wrong spacing,

I think it is worth reporting this upstream, but I don't think it is worth working around in this PR. In fact, the workaround here is actually broken if goalFmt contains a newline, but (I assume) works correctly with my suggestion.

evalTactic (← `(tactic|sorry))

/-- Elaborator for the `calc` tactic mode variant with widgets. -/
elab_rules : tactic
| `(tactic|calc%$calcstx $steps) => do
let some calcRange := (← getFileMap).rangeOfStx? calcstx | unreachable!
let indent := calcRange.start.character
let mut isFirst := true
for step in ← Lean.Elab.Term.mkCalcStepViews steps do
let some replaceRange := (← getFileMap).rangeOfStx? step.ref | unreachable!
let some replaceRange := (← getFileMap).rangeOfStx? step.ref | continue
let json := json% {"replaceRange": $(replaceRange),
"isFirst": $(isFirst),
"indent": $(indent)}
"indent": $(replaceRange.start.character)}
Widget.savePanelWidgetInfo CalcPanel.javascriptHash (pure json) step.proof
isFirst := false
evalCalc (← `(tactic|calc%$calcstx $steps))
Expand Down
24 changes: 24 additions & 0 deletions MathlibTest/CalcQuestionMark.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
import Mathlib.Tactic.Widget.Calc

/--
info: Create calc tactic:
• calc
1 = 1 := by sorry
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example : 1 = 1 := by
calc?


/--
info: Create calc tactic:
• calc
a ≤ a := by sorry
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (a : Nat) : a ≤ a := by
calc?