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

PatrickMassot · 2025-02-21T17:34:55Z

First make the help text clearer for people who do not know how to select stuff in the info view (in VSCode or lean4web) by mentioning Shift-click.

Then make the indentation handling more robust to various calc layouts.

Also introduces a calc? tactic to complement the calc code action. The issues with the calc code action are:

it requires a valid calc syntax so writing calc is not enough. I
typically write calc _ to get the code action. But when you write
calc and there is already something below that could vaguely be
mistaken for a calc then the code action triggers and the replacement
swallows the following syntax.
A code action is less visible than a TryThis (but this wouldn’t be
enough motivation for me without the previous point).

Also get rid of two unreachable! since experience show that those branches can be reached when handling malformed inputs, and the panic is awful for users.

First make the help text clearer for people who do not know how to select stuff in the info view (in VSCode or lean4web) by mentioning Shift-click. Then make the indentation handling more robust to various calc layouts. Also introduces a calc? tactic to complement the calc code action. The issues with the calc code action are: 1) it requires a valid calc syntax so writing calc is not enough. I typically write calc _ to get the code action. But when you write calc and there is already something below that could vaguely be mistaken for a calc then the code action triggers and the replacement swallows the following syntax. 2) A code action is less visible than a TryThis (but this wouldn’t be enough motivation for me without the previous point).

github-actions · 2025-02-21T17:35:55Z

PR summary 295dd76460

Import changes exceeding 2%

%	File
+3.23%	`Mathlib.Tactic.Widget.Calc`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Widget.Calc	31	32	+1 (+3.23%)

Import changes for all files

Files	Import difference
`Mathlib.Tactic.Widget.Calc`	1

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Tactic/Widget/Calc.lean

eric-wieser · 2025-02-22T18:34:15Z

Mathlib/Tactic/Widget/Calc.lean

+
+open Lean Meta Tactic TryThis in
+/-- Create a `calc` proof. -/
+elab stx:"calc?" : tactic => do


Can you add a test for this with guard_msgs?

eric-wieser · 2025-02-22T19:21:48Z

Mathlib/Tactic/Widget/Calc.lean

+  let s := s!"calc\n{spc}{goalFmt} := by sorry"
+  addSuggestions (← getRef) #[.suggestion s] (header := "Create calc tactic:")


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?

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)

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

I specifically want to handle spaces here.

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

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

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.

eric-wieser · 2025-02-22T19:22:50Z

Also get rid of two unreachable! since experience show that those branches can be reached when handling malformed inputs, and the panic is awful for users.

Can you add tests for those cases?

Mathlib/Tactic/Widget/Calc.lean

PatrickMassot · 2025-02-23T09:57:44Z

Also get rid of two unreachable! since experience show that those branches can be reached when handling malformed inputs, and the panic is awful for users.

Can you add tests for those cases?

I’m afraid I don’t have such case at hand. You need student superpowers to trigger such bugs.

Co-authored-by: damiano <[email protected]>

MathlibTest/CalcQuestionMark.lean

Co-authored-by: damiano <[email protected]>

adomani · 2025-02-23T18:21:40Z

I am happy with the current state of the PR. I have not used widgets much myself, but I imagine that the current PR at least fixes some issues that Patrick saw!

The only remaining issue is the indention: I prefer Eric's solution, but given that it is interlaced with a displaying bug that appears to produce the wrong indentation, maybe you can leave the code as is, but add a comment mentioning leanprover/lean4#7191 and the TSyntax approach?

This results in correct wrapping of the inserted text for multiline suggestions. Unfortunately, `#guard_msgs` renders things misleading, but there is an upstream patch that will fix that.

eric-wieser · 2025-02-23T19:10:22Z

The only remaining issue is the indention: I prefer Eric's solution

To make things easier for you, the last commit I pushed switches to my version, and shows the effect of it on some new tests I added. If you feel really strongly, then feel free to revert that commit (and add the comments @adomani requests in its place).

PatrickMassot · 2025-02-23T19:54:57Z

I don’t care about TSyntax or String, I simply need this merged.

eric-wieser · 2025-02-23T20:58:18Z

In that case

bors merge

First make the help text clearer for people who do not know how to select stuff in the info view (in VSCode or lean4web) by mentioning Shift-click. Then make the indentation handling more robust to various calc layouts. Also introduces a calc? tactic to complement the calc code action. The issues with the calc code action are: 1) it requires a valid calc syntax so writing calc is not enough. I typically write calc _ to get the code action. But when you write calc and there is already something below that could vaguely be mistaken for a calc then the code action triggers and the replacement swallows the following syntax. 2) A code action is less visible than a TryThis (but this wouldn’t be enough motivation for me without the previous point). Also get rid of two `unreachable!` since experience show that those branches can be reached when handling malformed inputs, and the panic is awful for users. Co-authored-by: Eric Wieser <[email protected]>

mathlib-bors · 2025-02-23T21:42:02Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: feat(Polynomial): polynomial sequences are bases for R[X] (#20846) feat: monoidal structure on Hopf algebras (#12011) feat(DiscreteValuationRing): addVal_eq_zero_iff (#21154) refactor(Cache): refactor getPackageDir to not use manually provided package directories (#21817) feat(CategoryTheory): categories of homological complexes have a separator (#20229) chore(Data/Complex): deprecate `Complex.abs` (#21995) feat: uncountable instances for `Ordinal` and isomorphic types (#18547) feat(Data/Set/Card): a few missing lemmas (#22186) feat: discrete topological spaces are 0-manifolds (#22105) feat(Data/Matroid/Loop): matroid loops (#22045) feat(SetTheory/Ordinal/Nimber/Field): Nimber division (#19066) feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162) feat(Data/Matroid/Circuit): matroid cocircuits (#21692) feat(Topology/Compactification/OnePoint): generalize instance (#22179) feat(Combinatorics/SimpleGraph): takeUntil properties (#21250) feat(Tactic): `pnat_to_nat` and `enat_to_nat` tactics (#21602) refactor: move `Polynomial.coeffs` and related results (#22225) chore: add AlgHom.ker_coe_equiv, resolve porting notes and erws (#22019) refactor(Order/Category): `ConcreteCategory` instance for `\omegaCPO` (#21478) feat(CategoryTheory): Grothendieck categories have a coseparator (#22224) feat: tweak calc widget (#22170) feat(CategoryTheory): the Freyd-Mitchell embedding theorem (#22222) chore(CategoryTheory): turn more `simp` into `simps!` (#22223) feat(CategoryTheory): the category of ind-objects is Grothendieck abelian (#21606) feat(AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono): epi-mono factorisation in `SimplexCategoryGenRel` (#21743) chore(CategoryTheory/DiscreteCategory): turn `simp` to `simps!` (#22217) feat(Analysis/Asymptotics): exponential growth of a sequence (#21178) feat(CategoryTheory): sigmaConst preserves monomorphisms (#21599) feat(RingTheory/Cotangent): `liftBaseChange` is injective for localizations (#21037) chore(CategoryTheory): fix incorrect name (#22210) feat(CategoryTheory): `IsPullback` version of 'pullback of iso is iso' (#22211) feat(CategoryTheory): pullbacks in functor categories (#22209) feat(CategoryTheory): detecting limit cones over connected diagrams (#22192) feat(LinearAlgebra): add theorems for injective/surjective/bijective compositions of bilinear maps (#21491)

First make the help text clearer for people who do not know how to select stuff in the info view (in VSCode or lean4web) by mentioning Shift-click. Then make the indentation handling more robust to various calc layouts. Also introduces a calc? tactic to complement the calc code action. The issues with the calc code action are: 1) it requires a valid calc syntax so writing calc is not enough. I typically write calc _ to get the code action. But when you write calc and there is already something below that could vaguely be mistaken for a calc then the code action triggers and the replacement swallows the following syntax. 2) A code action is less visible than a TryThis (but this wouldn’t be enough motivation for me without the previous point). Also get rid of two `unreachable!` since experience show that those branches can be reached when handling malformed inputs, and the panic is awful for users. Co-authored-by: Eric Wieser <[email protected]>

PatrickMassot added the t-meta Tactics, attributes or user commands label Feb 21, 2025

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Feb 21, 2025

Missing docstring

ff1784d

eric-wieser reviewed Feb 22, 2025

View reviewed changes

Mathlib/Tactic/Widget/Calc.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 22, 2025

View reviewed changes

PatrickMassot added 2 commits February 22, 2025 20:17

Add a test

3051446

Add withMainContext

cc6102e

eric-wieser reviewed Feb 22, 2025

View reviewed changes

adomani reviewed Feb 23, 2025

View reviewed changes

Mathlib/Tactic/Widget/Calc.lean Outdated Show resolved Hide resolved

Update Mathlib/Tactic/Widget/Calc.lean

873e5d1

Co-authored-by: damiano <[email protected]>

adomani reviewed Feb 23, 2025

View reviewed changes

MathlibTest/CalcQuestionMark.lean Show resolved Hide resolved

Update MathlibTest/CalcQuestionMark.lean

1b23537

Co-authored-by: damiano <[email protected]>

eric-wieser added 4 commits February 23, 2025 19:02

Add a test with an overly long line

dd2c462

indent the calc

2fcd4ea

actually test the test, oops

1255d3d

Switch to using Syntax instead of String for try this messages

295dd76

This results in correct wrapping of the inserted text for multiline suggestions. Unfortunately, `#guard_msgs` renders things misleading, but there is an upstream patch that will fix that.

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Feb 23, 2025

mathlib-bors bot changed the title ~~feat: tweak calc widget~~ [Merged by Bors] - feat: tweak calc widget Feb 23, 2025

mathlib-bors bot closed this Feb 23, 2025

mathlib-bors bot deleted the pm_calc_widget_tweaks branch February 23, 2025 21:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

PatrickMassot commented Feb 21, 2025 •

edited

Loading

github-actions bot commented Feb 21, 2025 •

edited

Loading

Import changes for modified files

eric-wieser Feb 22, 2025

PatrickMassot Feb 22, 2025

eric-wieser Feb 22, 2025

eric-wieser Feb 22, 2025 •

edited

Loading

eric-wieser Feb 22, 2025 •

edited

Loading

PatrickMassot Feb 23, 2025

eric-wieser Feb 23, 2025

adomani Feb 23, 2025

eric-wieser Feb 23, 2025 •

edited

Loading

eric-wieser commented Feb 22, 2025

PatrickMassot commented Feb 23, 2025

adomani commented Feb 23, 2025 •

edited by eric-wieser

Loading

eric-wieser commented Feb 23, 2025

PatrickMassot commented Feb 23, 2025

eric-wieser commented Feb 23, 2025

mathlib-bors bot commented Feb 23, 2025

		let s := s!"calc\n{spc}{goalFmt} := by sorry"
		addSuggestions (← getRef) #[.suggestion s] (header := "Create calc tactic:")

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

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

Conversation

PatrickMassot commented Feb 21, 2025 • edited Loading

github-actions bot commented Feb 21, 2025 • edited Loading

PR summary 295dd76460

Import changes for modified files

Declarations diff

eric-wieser Feb 22, 2025

Choose a reason for hiding this comment

PatrickMassot Feb 22, 2025

Choose a reason for hiding this comment

eric-wieser Feb 22, 2025

Choose a reason for hiding this comment

eric-wieser Feb 22, 2025 • edited Loading

Choose a reason for hiding this comment

eric-wieser Feb 22, 2025 • edited Loading

Choose a reason for hiding this comment

PatrickMassot Feb 23, 2025

Choose a reason for hiding this comment

eric-wieser Feb 23, 2025

Choose a reason for hiding this comment

adomani Feb 23, 2025

Choose a reason for hiding this comment

eric-wieser Feb 23, 2025 • edited Loading

Choose a reason for hiding this comment

eric-wieser commented Feb 22, 2025

PatrickMassot commented Feb 23, 2025

adomani commented Feb 23, 2025 • edited by eric-wieser Loading

eric-wieser commented Feb 23, 2025

PatrickMassot commented Feb 23, 2025

eric-wieser commented Feb 23, 2025

mathlib-bors bot commented Feb 23, 2025

PatrickMassot commented Feb 21, 2025 •

edited

Loading

github-actions bot commented Feb 21, 2025 •

edited

Loading

eric-wieser Feb 22, 2025 •

edited

Loading

eric-wieser Feb 22, 2025 •

edited

Loading

eric-wieser Feb 23, 2025 •

edited

Loading

adomani commented Feb 23, 2025 •

edited by eric-wieser

Loading