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.

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

feat: use scoped trace nodes in linarith #19855

Open
wants to merge 7 commits into
base: master
Choose a base branch
from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Dec 10, 2024

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.


Open in Gitpod

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

mergify bot commented Dec 10, 2024

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

Copy link

github-actions bot commented Dec 10, 2024

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

@github-actions github-actions bot added the t-meta Tactics, attributes or user commands label Dec 10, 2024
@leanprover-community-bot-assistant 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
@leanprover-community-bot-assistant 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
Copy link
Member Author

!bench

@leanprover-bot
Copy link
Collaborator

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

@eric-wieser eric-wieser marked this pull request as ready for review December 10, 2024 14:37
@grunweg grunweg changed the title feat: Use scoped trace nodes in linarith feat: use scoped trace nodes in linarith Dec 11, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
t-meta Tactics, attributes or user commands
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants