Incremental Library Search by joehendrix · Pull Request #421 · leanprover-community/batteries

joehendrix · 2023-12-06T17:40:34Z

This is a large PR that builds upon #343 to rename the Mathlib specific cache path and improve performance of library initialization when used without a cache. It does this primarily by introducing a lazy discriminator tree that defers population of tree branches from initialization to first lookup.

Testing on OSX is currently showing that initializing the tree using Mathlib takes under 2 seconds and a simply query adds an additional 2-3 seconds. It would be good to get additional information more machines (particularly Windows), but I think the timings are low enough that most users will not need caching.

digama0 · 2023-12-07T01:44:24Z

the cacheless approach has the advantage that it only selects candidates in the current environment

I'm not sure I would call that an advantage necessarily. For a search tool it is useful to be made aware of theorems from files you haven't imported.

joehendrix · 2023-12-07T03:19:08Z

the cacheless approach has the advantage that it only selects candidates in the current environment

I'm not sure I would call that an advantage necessarily. For a search tool it is useful to be made aware of theorems from files you haven't imported.

That's a good point that may impact operations other than exact? and apply?. I've made a Zulip thread since there might be more discussion on this and other changes.

Std/Tactic/LibrarySearch.lean

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Std/Tactic/LibrarySearch.lean

test/library_search/basic.lean

Std/Tactic/LibrarySearch.lean

kim-em · 2024-01-12T07:53:23Z

I think that's pretty much the last round of comments from me on this; I'm otherwise happy!

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Std/Tactic/LibrarySearch.lean

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

This brings the new implementation of `library_search` to Mathlib. It is temporarily called `std_exact?` and `std_apply?`, but if it tests okay in Mathlib we will remove the old implementation. There is some change in the ordering of results, so please report on your experiences! Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* 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: 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>

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>

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

joehendrix force-pushed the library_search branch from 89deb3d to fbe6ab5 Compare December 6, 2023 23:59

joehendrix added the depends on another PR This is stacked on top of another Batteries PR. label Dec 7, 2023

joehendrix force-pushed the library_search branch from fbe6ab5 to 5db589f Compare December 7, 2023 04:38

joehendrix mentioned this pull request Dec 7, 2023

feat: DiscrTree #394

Closed

joehendrix force-pushed the library_search branch 2 times, most recently from 5f9ef7e to fb81ec9 Compare December 7, 2023 20:04

joehendrix added the WIP work in progress label Dec 8, 2023

joehendrix force-pushed the library_search branch from 3a17f2c to e9d224f Compare December 13, 2023 21:40

ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 15, 2023

joehendrix force-pushed the library_search branch from b033e05 to b35a2f6 Compare December 21, 2023 05:52

joehendrix force-pushed the library_search branch from b35a2f6 to 38fe013 Compare January 3, 2024 02:09

ghost removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jan 3, 2024

joehendrix force-pushed the library_search branch 2 times, most recently from ad49d69 to c0dc9ff Compare January 3, 2024 02:35

ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jan 4, 2024

joehendrix force-pushed the library_search branch from c0dc9ff to 39ab9e1 Compare January 4, 2024 07:43

joehendrix removed the depends on another PR This is stacked on top of another Batteries PR. label Jan 4, 2024

kim-em and others added 11 commits January 3, 2024 23:57

feat: upstream exact? and apply?

eca65d0

import all

8f041d3

feat: Parameterize candidate finding for library search.

2d4efe9

feat: Introduce incremental candidate finder.

a7289bb

chore: Fix lint warnings

627f821

fix: Add missing import

be8124c

WIP: Towards concurrent initialization.

c13808e

feat: Add concurreny to initial import

01ee97d

chore: Migrate cache to environment.

43d6388

chore: Rename RootData to PreDiscrTree

2f9a8cd

chore: Renames in LazyDiscrTree

a6c8fcc