[Merged by Bors] - feat: use scoped trace nodes in linarith by eric-wieser · Pull Request #19855 · leanprover-community/mathlib4

eric-wieser · 2024-12-10T04:18:54Z

Inspired by hacking done with @robertylewis and @hrmacbeth which resulted in #19771.

The effect is that the traces messages are now hierarchical; though it's easy not to notice in VSCode without a better version of leanprover/lean4#6345.

See https://profiler.firefox.com/public/smkc5ffh9318w177gps2x9e5b6wy117s6f18e6g/flame-graph/?globalTrackOrder=0&thread=0&transforms=ff-2659&v=10 for an example output produced with

lake lean MathlibTest/linarith.lean -- \
  -Dtrace.profiler=true \
  -Dtrace.profiler.threshold=1 \
  -Dtrace.profiler.output.pp=true \
  -Dtrace.profiler.output=linarith-profile.json

Some inconclusive discussion about best practices for withTraceNode is on Zulip here.

This makes it a little easier to trace the two halves separately, which is desirable since the second half has quadratic complexity.

mergify · 2024-12-10T04:19:32Z

⚠️ The sha of the head commit of this PR conflicts with #19841. Mergify cannot evaluate rules on this PR. ⚠️

github-actions · 2024-12-10T04:19:45Z

PR summary e56ce516a1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ PreprocessorBase
+ linarithGetProofsMessage

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).

…h-trace

eric-wieser · 2024-12-10T13:52:10Z

!bench

leanprover-bot · 2024-12-10T14:20:47Z

Here are the benchmark results for commit e56ce51.
There were no significant changes against commit c90bcde.

kim-em · 2025-01-11T10:05:32Z

bors merge

@robertylewis

Inspired by hacking done with @robertylewis and @hrmacbeth which resulted in #19771. The effect is that the traces messages are now hierarchical; though it's easy not to notice in VSCode without a better version of leanprover/lean4#6345. See https://profiler.firefox.com/public/smkc5ffh9318w177gps2x9e5b6wy117s6f18e6g/flame-graph/?globalTrackOrder=0&thread=0&transforms=ff-2659&v=10 for an example output produced with ```bash lake lean MathlibTest/linarith.lean -- \ -Dtrace.profiler=true \ -Dtrace.profiler.threshold=1 \ -Dtrace.profiler.output.pp=true \ -Dtrace.profiler.output=linarith-profile.json ``` Some inconclusive discussion about best practices for `withTraceNode` is [on Zulip here](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Using.20withTraceNode/near/489198580). Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-01-11T10:36:51Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...

eric-wieser added 3 commits December 9, 2024 08:49

chore: split the nlinarith preprocessor for clarity

48f8752

This makes it a little easier to trace the two halves separately, which is desirable since the second half has quadratic complexity.

feat: Use scoped trace nodes in linarith

7fd4f6e

more tracing for linarith

97adcaa

github-actions bot added the t-meta Tactics, attributes or user commands label Dec 10, 2024

a few more traces

24b5d07

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 10, 2024

eric-wieser and others added 3 commits December 9, 2024 20:26

Merge branch 'master' into eric-wieser/linarith-trace

e0d0411

Merge remote-tracking branch 'origin/master' into eric-wieser/linarit…

c26b469

…h-trace

fix

e56ce51

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 10, 2024

eric-wieser marked this pull request as ready for review December 10, 2024 14:37

grunweg changed the title ~~feat: Use scoped trace nodes in linarith~~ feat: use scoped trace nodes in linarith Dec 11, 2024

eric-wieser requested a review from robertylewis December 18, 2024 19:13

ghost added the ready-to-merge This PR has been sent to bors. label Jan 11, 2025

mathlib-bors bot changed the title ~~feat: use scoped trace nodes in linarith~~ [Merged by Bors] - feat: use scoped trace nodes in linarith Jan 11, 2025

mathlib-bors bot closed this Jan 11, 2025

mathlib-bors bot deleted the eric-wieser/linarith-trace branch January 11, 2025 10:36

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: use scoped trace nodes in linarith#19855

[Merged by Bors] - feat: use scoped trace nodes in linarith#19855
eric-wieser wants to merge 7 commits intomasterfrom
eric-wieser/linarith-trace

eric-wieser commented Dec 10, 2024 •

edited

Loading

Uh oh!

mergify bot commented Dec 10, 2024

Uh oh!

github-actions bot commented Dec 10, 2024 •

edited

Loading

Uh oh!

eric-wieser commented Dec 10, 2024

Uh oh!

leanprover-bot commented Dec 10, 2024

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

eric-wieser commented Dec 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mergify bot commented Dec 10, 2024

Uh oh!

github-actions bot commented Dec 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e56ce516a1

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser commented Dec 10, 2024

Uh oh!

leanprover-bot commented Dec 10, 2024

Uh oh!

kim-em commented Jan 11, 2025

Uh oh!

mathlib-bors bot commented Jan 11, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

eric-wieser commented Dec 10, 2024 •

edited

Loading

github-actions bot commented Dec 10, 2024 •

edited

Loading