feat: add `Simproc`s #3124

leodemoura · 2023-12-28T23:57:20Z

Depends on #3123 and #3120

Downstream changes required:

leanprover-community-mathlib4-bot · 2023-12-29T00:12:23Z

❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-29 00:12:22)
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2023-12-30 01:06:03) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2023-12-30 01:25:37) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2023-12-31 00:42:07) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2023-12-31 19:29:18) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2023-12-31 19:43:50) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-02 02:35:17) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-02 14:35:06) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-02 22:53:05) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-02 23:33:01) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-03 13:13:57) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-06 06:14:33) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 04:59:47) View Log
🟡 Mathlib branch lean-pr-testing-3124 build against this PR was cancelled. (2024-01-07 05:12:11) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 05:18:26) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 05:31:44) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 06:17:14) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 06:49:29) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 06:54:57) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 10:15:06) View Log
❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2024-01-06' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2024-01-07 19:55:22)
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 23:27:18) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-07 23:55:58) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-08 00:31:41) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-08 00:35:30) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-08 00:48:39) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-08 00:48:49) View Log
🟡 Mathlib branch lean-pr-testing-3124 build against this PR was cancelled. (2024-01-08 01:41:44) View Log
🟡 Mathlib branch lean-pr-testing-3124 build against this PR was cancelled. (2024-01-08 02:11:17) View Log
🟡 Mathlib branch lean-pr-testing-3124 build against this PR was cancelled. (2024-01-08 02:15:57) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-08 02:18:09) View Log
🟡 Mathlib branch lean-pr-testing-3124 build against this PR was cancelled. (2024-01-08 02:18:24) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-08 02:48:19) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-08 04:25:50) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-08 05:05:53) View Log
❌ Mathlib branch lean-pr-testing-3124 built against this PR, but testing failed. (2024-01-08 05:58:57) View Log
❌ Mathlib branch lean-pr-testing-3124 built against this PR, but testing failed. (2024-01-08 06:59:11) View Log
✅ Mathlib branch lean-pr-testing-3124 has successfully built against this PR. (2024-01-08 08:43:10) View Log
🟡 Mathlib branch lean-pr-testing-3124 build this PR didn't complete normally. (2024-01-08 12:20:16) View Log
✅ Mathlib branch lean-pr-testing-3124 has successfully built against this PR. (2024-01-08 13:50:49) View Log
❌ Mathlib branch lean-pr-testing-3124 built against this PR, but testing failed. (2024-01-10 09:55:28) View Log
🟡 Mathlib branch lean-pr-testing-3124 build against this PR was cancelled. (2024-01-10 11:05:09) View Log
❌ Mathlib branch lean-pr-testing-3124 built against this PR, but linting failed. (2024-01-10 11:40:19) View Log
✅ Mathlib branch lean-pr-testing-3124 has successfully built against this PR. (2024-01-11 03:04:10) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-11 05:50:23) View Log
💥 Mathlib branch lean-pr-testing-3124 build failed against this PR. (2024-01-11 06:11:42) View Log
❌ Mathlib branch lean-pr-testing-3124 built against this PR, but testing failed. (2024-01-11 07:05:14) View Log
❌ Mathlib branch lean-pr-testing-3124 built against this PR, but testing failed. (2024-01-11 10:01:00) View Log
✅ Mathlib branch lean-pr-testing-3124 has successfully built against this PR. (2024-01-11 11:44:41) View Log

tests/lean/run/simproc1.lean

See leanprover/lean4#3124 Remark: toolchain for PR 3124 is still being built. I tested this PR with my only local lean4.

eric-wieser · 2024-01-03T10:58:36Z

src/Init/Data/Fin/Basic.lean

@@ -100,7 +100,7 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
  shiftRight := Fin.shiftRight

-instance : OfNat (Fin (no_index (n+1))) i where
+instance ofNatInst : OfNat (Fin (no_index (n+1))) i where


In mathlib, we have been using the convention of naming instances like this instOfNat as opposed to ofNatInst, which I believe is also consistent with the automatic naming rules. Is this departure from the convention an indication that the automatic naming rules are going to change soon?

Changed to instOfNat.

leodemoura · 2024-01-03T13:10:22Z

!bench

leanprover-bot · 2024-01-03T13:26:24Z

Here are the benchmark results for commit 06f577f.
There were significant changes against commit 1145976:

  Benchmark                  Metric             Change
  ===============================================================
- import Lean                branches             1.9%   (51.8 σ)
- import Lean                instructions         1.9%   (54.4 σ)
- import Lean                maxrss               1.4%   (82.1 σ)
- lake startup               instructions         1.4%   (21.8 σ)
- libleanshared.so           binary size          2.1%
- reduceMatch                maxrss               1.3%   (76.0 σ)
- stdlib                     instructions         1.6%  (516.1 σ)
- stdlib size                bytes .olean         1.4%
- stdlib size                lines C              2.4%
- tests/bench/ interpreted   maxrss               1.2%   (91.8 σ)
- tests/compiler             sum binary sizes     2.0%
- workspaceSymbols           instructions         2.2% (2525.1 σ)
- workspaceSymbols           maxrss               1.4%   (83.3 σ)

semorrison · 2024-01-06T05:21:17Z

Added full-ci label so we get a toolchain for all OSes.

See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

These are adaptations required for Leo's implementation of simprocs from leanprover/lean4#3124. This is a PR to `bump/v4.6.0`. Before it can be merged we need to merge - [x] leanprover-community/batteries#496 - [x] leanprover-community/aesop#93 and then to update the lakefile so both dependencies point at the `bump/v4.6.0` branches. I've updated a number of Mathlib tactics to adjust to the new type signatures in the simplifier, and these changes need to be reviewed carefully. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* feat: hover info for `rcases h : ...` (#486) * feat: hover info for `rcases h : ...` * fix * chore: adaptations for leanprover/lean4#3123 (#502) * chore: adaptations for leanprover/lean4#3123 * update toolchain * chore: remove unnecessary `have` (#516) After leanprover/lean4#3132 the linter will complain about this. * chore: simproc PR changes (#496) See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * chore: adaptions for nightly-2023-01-11 (#524) * advance toolchain to nightly-2024-01-12, no updates required * chore: updates to DiscrTree for changes in nightly (#536) * doc: extend docstrings for `ext` and `ext1` (#525) Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`. * docs(Data/List): typo (#529) * feat: Eq.rec lemma (#385) * chore: Add empty collection instance to BinomialHeap (#532) * Incremental Library Search (#421) This ports library_search from Mathlib to Std. It preserves the ability to do caching, but is designed to support a cacheless mode. The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * fix termination_by clauses in LazyDiscrTree fix LibrarySearch * bump toolchain --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org> * feat: adaptations for leanprover/lean4#3159 (#557) * merge origin/main * chore: fixes for `simp` refactor (#571) * move to v4.6.0-rc1 * fix proofs --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Leonardo de Moura <leonardo@microsoft.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org>

See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

) * feat: hover info for `rcases h : ...` (leanprover-community#486) * feat: hover info for `rcases h : ...` * fix * chore: adaptations for leanprover/lean4#3123 (leanprover-community#502) * chore: adaptations for leanprover/lean4#3123 * update toolchain * chore: remove unnecessary `have` (leanprover-community#516) After leanprover/lean4#3132 the linter will complain about this. * chore: simproc PR changes (leanprover-community#496) See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * chore: adaptions for nightly-2023-01-11 (leanprover-community#524) * advance toolchain to nightly-2024-01-12, no updates required * chore: updates to DiscrTree for changes in nightly (leanprover-community#536) * doc: extend docstrings for `ext` and `ext1` (leanprover-community#525) Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`. * docs(Data/List): typo (leanprover-community#529) * feat: Eq.rec lemma (leanprover-community#385) * chore: Add empty collection instance to BinomialHeap (leanprover-community#532) * Incremental Library Search (leanprover-community#421) This ports library_search from Mathlib to Std. It preserves the ability to do caching, but is designed to support a cacheless mode. The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> * fix termination_by clauses in LazyDiscrTree fix LibrarySearch * bump toolchain --------- Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org> * feat: adaptations for leanprover/lean4#3159 (leanprover-community#557) * merge origin/main * chore: fixes for `simp` refactor (leanprover-community#571) * move to v4.6.0-rc1 * fix proofs --------- Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Leonardo de Moura <leonardo@microsoft.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz> Co-authored-by: François G. Dorais <fgdorais@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org>

leodemoura requested review from semorrison and Kha as code owners December 28, 2023 23:57

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 29, 2023

nomeata reviewed Dec 29, 2023

View reviewed changes

tests/lean/run/simproc1.lean Outdated Show resolved Hide resolved

leodemoura force-pushed the simproc branch from b4e04ff to b5446cd Compare December 30, 2023 00:27

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 30, 2023

Update lean-toolchain for testing leanprover/lean4#3124

16f47e4

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 30, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 30, 2023

Trigger CI for leanprover/lean4#3124

5037cf5

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 31, 2023

Trigger CI for leanprover/lean4#3124

93d9606

leodemoura force-pushed the simproc branch from 7d72ad0 to 4d08329 Compare December 31, 2023 19:23

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 31, 2023

Trigger CI for leanprover/lean4#3124

cb7cb3b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 31, 2023

Trigger CI for leanprover/lean4#3124

d94d320

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 2, 2024

Trigger CI for leanprover/lean4#3124

f29a54b

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 2, 2024

Trigger CI for leanprover/lean4#3124

5d8d998

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 2, 2024

Trigger CI for leanprover/lean4#3124

983ed7c

leodemoura added a commit to leanprover-community/batteries that referenced this pull request Jan 2, 2024

chore: simproc PR changes

83b6a26

See leanprover/lean4#3124 Remark: toolchain for PR 3124 is still being built. I tested this PR with my only local lean4.

leodemoura mentioned this pull request Jan 2, 2024

chore: simproc PR changes leanprover-community/batteries#496

Merged

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 2, 2024

Trigger CI for leanprover/lean4#3124

bd922de

This was referenced Jan 2, 2024

refactor: simplify SimpM recursive definitions #3120

Closed

perf: simplifier performance issues on match and if-then-else terms #3118

Closed

eric-wieser reviewed Jan 3, 2024

View reviewed changes

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 3, 2024

Trigger CI for leanprover/lean4#3124

0546aed

semorrison added the full-ci label Jan 6, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 6, 2024

Trigger CI for leanprover/lean4#3124

50ffc8f

semorrison added a commit to leanprover-community/aesop that referenced this pull request Jan 7, 2024

fixes to leanprover/lean4#3124

093a93f

semorrison mentioned this pull request Jan 7, 2024

chore: adaptations for leanprover/lean4#3124 leanprover-community/aesop#93

Merged

leodemoura and others added 8 commits January 8, 2024 13:51

chore: better method names

8fbf408

chore: use mathlib naming convention

a23029a

chore: update stage0

2bab43e

chroe: fix tests

f4a213f

chore: cleanup builtin simprocs using OptionT

7c5a37b

test: test for panic in simprocs

72e5a94

fix: panic at ite and dite simprocs

e6ed385

test: timeout in Mathlib.Computability.PartrecCode

9b2b4aa

leodemoura force-pushed the simproc branch from 4b73ea8 to 9b2b4aa Compare January 8, 2024 21:54

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 8, 2024 22:18 Inactive

leodemoura mentioned this pull request Jan 9, 2024

feat: add simp configuration option Simp.Config.instances #3151

Closed

leodemoura added the will-merge-soon …unless someone speaks up label Jan 9, 2024

doc: add simproc release notes

f296779

github-actions bot temporarily deployed to lean-lang.org/lean4/doc January 9, 2024 02:10 Inactive

Kha merged commit e924ef2 into master Jan 9, 2024
19 checks passed

leodemoura mentioned this pull request Jan 9, 2024

perf: (try to) fix regression introduced by #3139 #3144

Closed

joehendrix pushed a commit to leanprover-community/batteries that referenced this pull request Jan 11, 2024

chore: simproc PR changes (#496)

5ce1202

See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

semorrison added a commit to leanprover-community/aesop that referenced this pull request Jan 11, 2024

chore: adaptations for leanprover/lean4#3124 (#93)

3ff7cbf

joehendrix pushed a commit to leanprover-community/batteries that referenced this pull request Feb 5, 2024

chore: simproc PR changes (#496)

89fe00d

See leanprover/lean4#3124 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add `Simproc`s #3124

feat: add `Simproc`s #3124

leodemoura commented Dec 28, 2023 •

edited by semorrison

leanprover-community-mathlib4-bot commented Dec 29, 2023 •

edited

eric-wieser Jan 3, 2024

leodemoura Jan 3, 2024

leodemoura commented Jan 3, 2024

leanprover-bot commented Jan 3, 2024

semorrison commented Jan 6, 2024

feat: add Simprocs #3124

feat: add Simprocs #3124

Conversation

leodemoura commented Dec 28, 2023 • edited by semorrison

leanprover-community-mathlib4-bot commented Dec 29, 2023 • edited

eric-wieser Jan 3, 2024

Choose a reason for hiding this comment

leodemoura Jan 3, 2024

Choose a reason for hiding this comment

leodemoura commented Jan 3, 2024

leanprover-bot commented Jan 3, 2024

semorrison commented Jan 6, 2024

feat: add `Simproc`s #3124

feat: add `Simproc`s #3124

leodemoura commented Dec 28, 2023 •

edited by semorrison

leanprover-community-mathlib4-bot commented Dec 29, 2023 •

edited