Move #find command to Std?

Stream: batteries

[François G. Dorais]

There are plenty of library search tools moving to Std. This one is older and not as sophisticated as newer search tools but it's a freebie at this time: it doesn't depend on anything properly Mathlib so moving it is basically just moving one file from Mathlib to Std.

[Joachim Breitner]

For good UX, it depends on having a pre-computed index, and the whole concept of these index file works well within mathlib, but doesn't easily clearly scale to a multi-package world. The tactics that are being moved to omega either have mathlib-specific hacks (not great), or could be sped up to not need a precomputed cache (like exact?). I think this needs a solution first.

(Related thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Loogle.20is.20live!/near/417982759)

[Mario Carneiro]

Why does precomputed cache = mathlib-specific hack?

[Mario Carneiro]

just make the API to add a precomputed cache generic

[Joachim Breitner]

The std4 code no longer mentions mathlib in the file path, but at least in the coments:

/--
Once we reach Mathlib, and have `cache` available,
we may still want to load a precomputed cache for `exact?` from a `.olean` file.

This makes no sense here in Std, where there is no caching mechanism.
-/
def cachePath : IO FilePath := do
  let sp ← searchPathRef.get
  if let buildPath :: _ := sp then
    let path := buildPath / "LibrarySearch.extra"
    if ← path.pathExists then
      return path
  return ".lake" / "build" / "lib" / "LibrarySearch.extra"

[Mario Carneiro]

I think that path should not be hardcoded

[Joachim Breitner]

Even then:
Loading such a cache file only really makes sense when it was created for a root module (like Mathlib) that imports everything you care about. This exists in mathlib, but as soon as I am working in my own little project, that imports packages A, B and C, then which index could exist, and built by whom?

[Mario Carneiro]

built by you

[Mario Carneiro]

obviously we also need an interface to make it easy for people to build their own cache

[Joachim Breitner]

So no cloud-built indexes (for the packages where you have some kind of cloud cache for oleans) at all?

[Mario Carneiro]

if there is also a method to use an existing cache (which mathlib uses), then you will benefit from that

[Joachim Breitner]

It seems to not degrade wrt the mathlib experience, but scale to multiple packages, we’d need something like “for every package known to lake, look for an index, load that, efficiently merge them, and then amend the index for everything not covered”

[Mario Carneiro]

I'm not going to suggest that because it sounds like work but if you want to do it go ahead

[Mario Carneiro]

mathlib + more and built from scratch are the main use cases we need to worry about for now

[François G. Dorais]

FWIW: I would prefer moving and _then_ improving. I think that is a good policy for things that are in the wrong place. Of course, whether this is in the wrong place is debatable.

[Mario Carneiro]

and as far as a MVP, I think "cache file with path provided downstream" and "built from scratch" suffice

[Joachim Breitner]

Even “mathlib + more” doesn’t work well with the current approach: It finds the mathlib index, loads it and now you won’t find anything from the “more” set

[Mario Carneiro]

which is to say, no "more"

[Joachim Breitner]

Fair enough… do we have an idea for a mechanism to find a suitable cache file?

[Mario Carneiro]

but I think it's not too hard to implement "more", you go over the environment and for everything not in mathlib you add it to the discrimination tree

[Mario Carneiro]

initialize : Option FilePath <- pure none?

[Joachim Breitner]

So users manually set the file path?

[Joachim Breitner]

Or does every package set the filepath, and the last one wins? (not too bad actually)

[Joachim Breitner]

Since we already use the first component of the module name to more or less identify the package, another approach could be to look through

{ P.extra | P.M.M in imported module names}

and then a little bit of logic to pick the “best” one if multiple ones are found…

[François G. Dorais]

That's how $PATH works in shell, except that you have a choice to modify the path if you need to.

[Mario Carneiro]

for this MVP, there is at most one file path, i.e. either mathlib's extra file or nothing

[Mario Carneiro]

so there would be exactly one instance of setting it, in an early mathlib file

[Joachim Breitner]

That’s mathlib specific again, isn’t it? I thought we are trying to find a MVP that isn't mathlib-specific?

[Joachim Breitner]

Ah, you are looking for a mechainsm that isn’t inherently mathlib-specific, but would (initially) only used by mathlib?

[Mario Carneiro]

this isn't mathlib specific in the sense that std doesn't have to directly refer to a file in mathlib's file hierarchy

[Mario Carneiro]

and it means someone could have a not-mathlib, although I doubt that really happens in practice

[Mario Carneiro]

this is following on François G. Dorais 's point that we should get a basic version out without regressions and work to something more general later

[Joachim Breitner]

As long as we doubt that there is little point moving those tactics that don’t have good UX (i.e. are too slow) without an index, though, aren’t they?

[Joachim Breitner]

I guess that depends on whether nothing or something that’s slow is worse :-)

[Mario Carneiro]

Even without an index it's okay, users can just call #find once at the top of the file, or init_find_index or something

[Mario Carneiro]

or put that in an upstream file

[Mario Carneiro]

that's the "from scratch" workflow

[Joachim Breitner]

Yeah, or keep a separate tab open where you just use #find without having to change imports too often. Fair enough.

[Mario Carneiro]

you can just import everything when preparing the index

[Mario Carneiro]

in fact, ideally #find would be able to index files that aren't even imported

[Mario Carneiro]

but maybe that's too sci-fi

[Joachim Breitner]

BTW, are we taking about moving the #find from mathlib, or importing the #find provided by the Loogle library? (I originally wanted to replace #find in mathlib, but then never got all relevant PRs merged, and now it’s in a library.)

[Mario Carneiro]

uh... are they not the same?

[Joachim Breitner]

No, https://github.com/leanprover-community/mathlib4/pull/6363 got never merged

[Joachim Breitner]

And, in a way, any project can already import loogle as a library dependency and have (that) #find without needing mathlib; it’s not std, but still closer to that goal. (This isn’t done a lot yet and may have rough edges, but in principle should be possible.)

[Mario Carneiro]

looks like you are the one who closed the PR

[Joachim Breitner]

Right, I am not blaming anyone here!

[Joachim Breitner]

But as we all agree, this isn’t mathlib specific functionality.

[Mario Carneiro]

well it will have to be reviewed at some point, and TBH mathlib has a lot more bandwidth for that than std

[Mario Carneiro]

does #find use the same cache as library_search?

[Mario Carneiro]

or are there two caches in there

[Joachim Breitner]

#loogle (to disambiguate with the old #find that Sebastian wrote) uses it’s own cache with different data structures

[Mario Carneiro]

is mathlib generating this cache?

[Joachim Breitner]

No. (But it could, of course, should it depend on Loogle)

[Mario Carneiro]

so that means that adding #loogle to mathlib would increase the download size of mathlib significantly?

[Mario Carneiro]

how much?

[Joachim Breitner]

~230MB uncompressed
(The suffix-trie for the name matching taking most space, the constant-map was I think much smaller)

[Mario Carneiro]

hm, I'm sure we can do better but it's not important for the MVP

[Mario Carneiro]

I would encourage you to get this into mathlib first

[Joachim Breitner]

Yes, I’m not claiming exhaustive reaping of low hanging fruit there

[Mario Carneiro]

this will resolve a lot of the logistical issues

[Joachim Breitner]

By copying the code, or by require the library?

[Mario Carneiro]

copying the code I think

[Mario Carneiro]

require the library is also an option for mathlib but I'm not sure it will address the logistical issues

[Mario Carneiro]

because when it moves to std it will be closer to a "copy the code" situation

[Mario Carneiro]

how is loogle currently handling the generation of the index?

[Mario Carneiro]

doesn't mathlib need to be imported for that?

[Joachim Breitner]

Is there someone interested in co-owning that code? I would prefer to keep at least the code that runs the loogle service separate, for easier iteration, so maybe someone who actually wants to use it in mathlib can help maintain that copy?

[Mario Carneiro]

you want it to be separate from the version in std as well?

[Joachim Breitner]

echo "Replace toolchain by mathlib's"
curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
cat lean-toolchain
rm ./lake-manifest.json

echo "Updating lake"
export LOOGLE_SECCOMP=true
lake update
cat ./lake-manifest.json

echo "Fetching mathlib cache"
lake exe cache get

echo "Building loogle"
lake build loogle

echo "Building mathlib cache"
lake exec loogle --write-index ./.lake/build/lib/LoogleMathlibCache.extra

[Joachim Breitner]

It can also be built mathlib-style, using #runCmd, but since I am anyways building a CLI this is faster, as it runs in compiled code.

[Mario Carneiro]

I don't see a thing in that script that adds mathlib to the lakefile

[Joachim Breitner]

you want it to be separate from the version in std as well?

I did not think much about that yet; I guess I was waiting first for an answer to the question of ergonomic (lake-managed? reservoir-cloud-build caches) precomputed indexes; to me that seems a prerequisite

[Mario Carneiro]

I think the #find in std should be agnostic to cache distribution methods

[Joachim Breitner]

It’s already in the lakefile; although I’d probably separate that out into a “loogle-deploy” package so that the loogle lakefile itself doesn’t have to, once people want to import the loogle package

[Mario Carneiro]

right, my point being that mathlib can't require loogle if loogle requires mathlib

[Joachim Breitner]

Luckily, Loogle the library doesn't, and I can change that when and if mathlib wants to import Loogle.

[Mario Carneiro]

You will still want the loogle library of course, for the web stuff

[Mario Carneiro]

but I think the core logic of #find should move out of the loogle package and into std

[Mario Carneiro]

and I want it to go via mathlib because otherwise I don't think it will be reviewed and tested well enough

[Mario Carneiro]

mathlib is one of the primary clients of #find

[Joachim Breitner]

No objections. Does anyone here want to help with that?

[Mario Carneiro]

in the short term the fact that loogle imports mathlib already means that it won't even break or need duplication in the interim

[Mario Carneiro]

I think you are probably going to have to be the one taking point on this

[Mario Carneiro]

since you are the maintainer of the loogle library

[Mario Carneiro]

but well, if someone volunteers then that's great

[Mario Carneiro]

it doesn't seem like a major priority, so it's fine by me if this just sits until you or me or someone else has the time to take it on

[Joachim Breitner]

Agreed

[Joachim Breitner]

I’m just a bit hesitant because I personally find (heh) I don’t need it as #find, as the web interface scratches all the itches I have, and completely egoistically it’s more fun to work on code that I can just push to. So my intrinsic motivation to get it into mathlib isn’t that high, and I’d prefer to support someone who actually wants to use it.

[Eric Rodriguez]

I'm trying to get my metaprogramming up to scratch, and I think I'm one of Loogle's most prolific (ab)users - I'm happy to help out; I assume most of this would be modularising and porting to mathlib? I can fully understand wanting to keep it in a state of being able to edit easily - iteration within Mathlib is not fun.

[Joachim Breitner]

yes, this file and dependencies: https://github.com/nomeata/loogle/blob/master/Loogle/Find.lean (the main Loogle is the CLI). If you want to see that through to become Mathlib.Tactic.Find, that’d be great! I think it’s ok if they go out of sync temporarily; I can copy back improvements to keep the diff smaller.

[Mario Carneiro]

and completely egoistically it’s more fun to work on code that I can just push to

This is probably obvious and goes without saying, but this is unfortunately mutually exclusive with getting it into std

[Mario Carneiro]

if it's still changing rapidly or experimental, it should not be moved to std yet, although you can still iterate in mathlib without too much friction as long as you allow for enough lead time

[Mario Carneiro]

(the initial commit is the hardest PR, bugfixes to existing tactics are relatively easier to review)

[Joachim Breitner]

Even with a #find implementation in std or mathlib it could still be that loogle.lean-fro.org runs on a copy of the code, or a non-merged PR, so I there is probably cake to be had and eaten too.

[Mario Carneiro]

sure, if you want to do that it's fine as well