Loogle!

Stream: general

[Joachim Breitner]

loogle.gif
So far running only locally, but a publicly accessible mathlib search engine exposing the functionality of the (improved, not yet merged) #find command seems within reach.

[Joachim Breitner]

And/or a Zulip bot, for use in “Is there code for X?”

[Joachim Breitner]

The process needs about 3GB according to top here. Seems reasonable given that it loads all of mathlib and keeps an index.
Just saying in case someone says “shut up and take my server to run it on” :-)

[Henrik Böving]

That's more RAM than I have to spare :P

[Henrik Böving]

If you can get it down to 1.5G I'll do it until we find a more permanent thing^^

[Joachim Breitner]

Code at https://github.com/nomeata/loogle if someone wants to play around with it. No Readme yet, but

nix develop
lake exe cache get
lake build
./server.py

could potentially work.

[Joachim Breitner]

It seems that 3G of the 3.5G are memory-mapped oleans, and only about 500MB is actually anonymous memory (according to pmap). But before worrying about this there is plenty of other things to do to get this beyond then bragging-on-zulip proof-of-concept stage :-)