matt-w-horn loogle: searching Lean and Mathlib
Mathlib carries on the order of 200,000 declarations with frequently
unguessable names: is it tsum_mul_left or ENNReal.tsum_mul_left? Each wrong
guess costs a rebuild.
loogle indexes a project's entire import graph, Mathlib included, and searches by name, by the shape of a statement, or by what a lemma concludes. Shape search answers "there must be a lemma like this" without knowing any of the lemma's words.
Two ways to run it
Hosted, no install
https://loogle.lean-lang.org/ runs the same query language against a recent
Mathlib. Use it when there is no local build, or for a second opinion on which
Mathlib revision carries a lemma. The hosted index tracks Mathlib's master
rather than your project, so confirm any hit against your own pin with
#check.
Locally, against your own project
A local build searches your import graph at your pin, so anything it finds will actually compile where you need it.
git clone https://github.com/nomeata/loogle.git ~/.local/share/loogle
cd ~/.local/share/loogle
cp /path/to/your-project/lean-toolchain . # match the project you will search
lake build
Run it from inside the Lean project you want to search:
cd /path/to/your-project
lake env ~/.local/share/loogle/.lake/build/bin/loogle '<query>'
lake env reads the current directory's lakefile to compute LEAN_PATH,
which is how loogle finds built .olean files. Run it outside a Lean project,
or inside one Lake has not built, and it fails with a toolchain or "no such
file" error rather than returning nothing: that error is about where you are,
not about the query.
A wrapper on PATH saves the typing:
cat > ~/.local/bin/loogle <<'EOF'
#!/bin/sh
exec lake env "$HOME/.local/share/loogle/.lake/build/bin/loogle" "$@"
EOF
chmod +x ~/.local/bin/loogle
The first query against a project takes several minutes. That is index
construction, not a hang: loogle writes a search index next to Mathlib's
.oleans (Mathlib.loogle-index) the first time it searches a module, and
every later query reuses it and returns in seconds. The message no index file at …; rebuilding is that one-time cost announcing itself.
Query syntax
One query string, up to five filter forms, comma-separated. Comma means AND.
Metavariables written ?a are independent per filter.
| Form | Example | Finds |
|---|---|---|
| By constant | Real.sin |
lemmas whose statement mentions Real.sin |
| By name substring | "differ" |
lemmas with differ in their name |
| By subexpression | _ * (_ ^ _) |
statements containing that shape anywhere |
| Non-linear subexpression | Real.sqrt ?a * Real.sqrt ?a |
the same metavariable in both positions |
| By conclusion | |- tsum _ = _ * tsum _ |
the conclusion (right of all →/∀) has this shape |
| Conclusion plus hypothesis | |- _ < _ → tsum _ < tsum _ |
that conclusion, with such a hypothesis anywhere |
| Data versus proofs | ⊢ (_ : Type _) / ⊢ (_ : Prop) |
data-producing defs versus theorems |
Combined, these narrow fast:
loogle 'Real.sin, "two", _ * _, |- _ < _ → _'
finds lemmas mentioning Real.sin, with two in the name, containing a
product, and carrying a _ < _ hypothesis, all at once.
Queries containing (, ), or |- need shell quoting:
loogle '(List.replicate (_ + _) _ = _)'
loogle '|- Monotone _ → Monotone _'
Useful flags
--module Mathlib(the default) searches all of Mathlib;--module YourLibrestricts to your project's own root library and its imports.--json/-jfor machine-readable output (hits[].name,.module,.type).--max-results n(default 200).--interactive/-ireads one query per line from stdin, avoiding thelake envstartup cost on each of several searches.--index-mode writeforces a fresh index.--helplists everything.
Writing a query that finds things
Describe the shape you want to end up with, not the concept's name.
| You want | Query |
|---|---|
Something concluding a * b ≤ c * d |
|- _ * _ ≤ _ * _ |
A lemma turning log (x*y) into a sum |
Real.log (_ * _) |
Anything about √a * √a |
Real.sqrt ?a * Real.sqrt ?a |
| A monotonicity transfer lemma | |- Monotone _ → Monotone _ |
| Cancellation for truncated subtraction | |- _ - _ + _ = _, "sub" |
Start broad, then add filters. A query returning 200 hits is more useful than one returning zero, because one more name filter narrows it and a zero result tells you nothing about where you went wrong.
Troubleshooting
Toolchain mismatch (
no default toolchain configured, or a load failure on a different project): loogle binaries are pinned to whateverlean-toolchainwas present when they were built. A project on a different toolchain needs its own build:cd ~/.local/share/loogle cp /path/to/other-project/lean-toolchain . lake buildThis overwrites the current pin, and only one can be active at a time. For projects on different toolchains, keep a second checkout rather than rebuilding back and forth: each rebuild is slow and leaves the binary's current pin unclear.
Stale results after updating Mathlib or editing your library: rerun with
--index-mode writerather than trusting the cache.Updating loogle:
cd ~/.local/share/loogle && git pull && lake build.
When loogle is the wrong tool
- The goal is in front of you and you want something that closes it now:
exact?,apply?, andrw?search the environment with your hypotheses in scope, which loogle cannot see. - You know the concept but not Lean's vocabulary for it: natural-language search (https://leansearch.net/, https://www.leanexplore.com/) bridges that gap better than shape search does.
- You want to read the surrounding theory: grep
.lake/packages/mathlib/Mathlib/directly, which is also the authoritative answer at your exact pin and needs no index.
Source and full documentation: https://github.com/nomeata/loogle.