Loogle CLI

Stream: general

[Michael Stoll]

I'm trying to run loogle from the command line. I followed the instructions at the github repo and managed (with some modifications, see issue #10 there) to build it. Running lake exe loogle --help produces the expected output. But lake exe loogle 'Real.sin'just runs for a while, prints nothing and stops. Where does the output go? @Joachim Breitner

[Joachim Breitner]

You might be the first to try :-)

[Joachim Breitner]

Is this on Linux or OSX?

[Michael Stoll]

Linux SuSe Tumbleweed.

[Joachim Breitner]

Ah, it says so in the issue

[Joachim Breitner]

Maybe try to remove all the seccomp stuff from the Loogle main file (comment out the import and the one function call) to rule out issues related to that

[Michael Stoll]

The function call is Seccomp.enable on line 166, I assume?

[Joachim Breitner]

Yes!

[Michael Stoll]

OK. Commenting out the two lines and building results in me getting output on stdout. Thanks!

[Michael Stoll]

What is the purpose of the seccomp stuff?

[Michael Stoll]

(Seeing that it works well without...)

[Joachim Breitner]

It kills he process when it tries to do something unexpected; I use this on the live site as a security measure. Locally with trusted input it should not be necessary; if more people will use it locally I should build it without by default

[Joachim Breitner]

What do you plan to do with it?

[Michael Stoll]

I was trying to do some statistics on lemma names, for which it seemed to be useful to get the loogle output in a file.

[Michael Stoll]

See here.

[Joachim Breitner]

Hope it's useful! Although for statistics on names it might be easier to import Mathlib and use run_cmd to get the list of all names and do stuff with it

[Michael Stoll]

That smells of metaprogramming, which I have not yet done in Lean4, so getting the loogle CLI and using grep was the faster way for me right now.