Skip to content

[Merged by Bors] - chore: bump dependencies#3475

Closed
kim-em wants to merge 1 commit intomasterfrom
bump-dependencies-20230417
Closed

[Merged by Bors] - chore: bump dependencies#3475
kim-em wants to merge 1 commit intomasterfrom
bump-dependencies-20230417

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Apr 17, 2023


Open in Gitpod

@kim-em kim-em added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 17, 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 Apr 17, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 17, 2023

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Here are the benchmark results for commit f329ca8.
There were significant changes against commit b000aad:

  Benchmark                        Metric           Change
  ========================================================
+ build                            interpretation    -6.6%
+ ~Aesop.Frontend.Command          instructions     -19.7%
+ ~Aesop.Main                      instructions     -22.8%
+ ~Aesop.Options                   instructions     -80.6%
- ~Aesop.Rule.Name                 instructions      12.5%
+ ~Aesop.RuleTac.Basic             instructions     -15.8%
+ ~Aesop.RuleTac.Tactic            instructions      -8.0%
+ ~Aesop.Search.ExpandSafePrefix   instructions      -8.9%
+ ~Aesop.Search.Expansion          instructions     -54.2%
+ ~Aesop.Search.Main               instructions      -7.9%
+ ~Aesop.Search.Queue              instructions     -16.7%
+ ~Aesop.Search.RuleSelection      instructions     -42.6%
- ~Aesop.Tracing                   instructions     102.0%
- ~Aesop.Tree.ExtractScript        instructions      19.6%
+ ~Aesop.Util.Basic                instructions     -17.0%

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Apr 17, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 17, 2023
bors bot pushed a commit that referenced this pull request Apr 17, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore: bump dependencies [Merged by Bors] - chore: bump dependencies Apr 17, 2023
@bors bors bot closed this Apr 17, 2023
@bors bors bot deleted the bump-dependencies-20230417 branch April 17, 2023 23:25
kim-em added a commit that referenced this pull request May 10, 2023
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants