Listing all names in a namespace

Stream: new members

[Johannes C. Mayer]

Is there some way to list all names in a namespace. E.g. the String namespace. I am using lean4.

Of course you can just enter String. and see what auto-completions you get, but that does not optimal in terms of exploratory.

If you have any other suggestions of how to go about exploring what other ways exist for exploring what is available, that would also be helpful. E.g. is there some way to figure out what the ["important"/most used] functions are? String.utf8ByteSize is probably less important than String.push, but for other functions it might not be that obvious. Of course you can always look at the source. But a problem is that the definitions are often scattered around. E.g. if I have a class in java then all the function of the class are where the you define the class, whereas in lean they can I think be even spread across files.

[Henrik Böving]

You could use doc-gen4's search function for this I guess?

[Johan Commelin]

In Lean 3 you can write #print prefix String. Does something similar work in Lean 4?

[Johannes C. Mayer]

That does not seem to work, at least right now, in lean4.

[Johannes C. Mayer]

Also doc-gen4 does not want to build, i get:

error: external command /home/johannes/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with status 1
./lean_packages/lake/././Lake/CLI/Main.lean:211:2: error: failed to synthesize instance
  Decidable
    (let _discr := a✝;
    match a✝ with
    | some x => true = true
    | x => false = true)

error: external command /home/johannes/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with status 1
error: build failed

Maybe I am doing something wrong though.

[Alex J. Best]

If you are happy to use mathlib4 (at least for development) a #print prefix command is implemented there https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/PrintPrefix.lean

[Henrik Böving]

Johannes C. Mayer said:

Also doc-gen4 does not want to build, i get:

error: external command /home/johannes/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with status 1
./lean_packages/lake/././Lake/CLI/Main.lean:211:2: error: failed to synthesize instance
  Decidable
    (let _discr := a✝;
    match a✝ with
    | some x => true = true
    | x => false = true)

error: external command /home/johannes/.elan/toolchains/leanprover--lean4---stable/bin/lean exited with status 1
error: build failed

Maybe I am doing something wrong though.

It does definitely build in CI every few hours so most likely you :p

I see in the error that you are using a Lean 4 stable compiler, you should be on nightly if you want to be compatible with any of the current developments really

[Johannes C. Mayer]

Should this not work?

import Lean.Elab.Command
#print prefix String

I get the error

test.lean:3:7
expected 'axioms', identifier or string literal

[Henrik Böving]

(deleted)

[Henrik Böving]

Also you are actually not supposed to build doc-gen4 yourself, its output is hosted here https://leanprover-community.github.io/mathlib4_docs/

[Henrik Böving]

Unless of course you have your own custom package

[Johannes C. Mayer]

That make sense. BTW, the google search button is broken on https://leanprover-community.github.io/mathlib4_docs, it does String site:https://leanprover-community.github.io/mathlib_docs.

[Henrik Böving]

Yeah I never bothered to fix it because ideally we'd want our own search to work good enough at some point :tm:

[Henrik Böving]

Maybe I should just remove it all together :sweat_smile:

[Johannes C. Mayer]

The on site search seems to be broken, at lest for me, also. When I search for String I just get octopus forever :smile:

[Johannes C. Mayer]

And when I ask this:
Johannes C. Mayer said:

Should this not work?

import Lean.Elab.Command
#print prefix String

I get the error

test.lean:3:7
expected 'axioms', identifier or string literal

I actually was trying it out, after downloading mathlib4 and creating a new file in the root directory, with these contents.

[Henrik Böving]

Johannes C. Mayer said:

The on site search seems to be broken, at lest for me, also. When I search for String I just get octopus forever :smile:

That's weird...it has been working for me and everyone I've asked about it so far.., does your console show any errors?

[Alex J. Best]

You probably need import Mathlib.Tactic.PrintPrefix do you have that?

[Johannes C. Mayer]

Henrik Böving said:

Johannes C. Mayer said:

The on site search seems to be broken, at lest for me, also. When I search for String I just get octopus forever :smile:

That's weird...it has been working for me and everyone I've asked about it so far.., does your console show any errors?

2022-03-13T09-23-010100.png

[Johannes C. Mayer]

Alex J. Best said:

You probably need import Mathlib.Tactic.PrintPrefix do you have that?

Yes that actually works.

[Johannes C. Mayer]

@Henrik Böving Actually the search works in both Chromium and Firefox for me. It was only broken in Brave. This seems to be be a common pattern that Brave breaks things.

[Henrik Böving]

In that case! @Xubai Wang our resident web developer to the rescue!

[Xubai Wang]

It's surprising to know that the code fails, as Brave is also based on chromium.
I would first add some error handling to make things work (with performance regression in Brave), and then try to figure out what's going wrong when I have time.

[Xubai Wang]

@Johannes C. Mayer I have pushed a fix for better error handling, but I fail to reproduce the error in my Brave browser. Can you provide a screenshot of your browser storage? (In Developer Tools > Application > Storage > IndexedDB)

screen shot.png

[Johannes C. Mayer]

@Xubai Wang

It simply has nothing in it.
2022-03-14T09-13-330100.png

BTW, I had brave shield disabled the whole time, and don't have any additional add block lists active. Turning all extensions off also does not help (but I don't have any that would be obvious culprits anyway).

I am on Brave:
Version 1.36.111 Chromium: 99.0.4844.51 (Official Build) (64-bit)

System:
Linux Mint 19.1 Tessa
4.15.0-163-lowlatency #171-Ubuntu SMP PREEMPT Fri Nov 5 12:40:14 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux

[Xubai Wang]

@Johannes C. Mayer Let's debug from scratch. I made a minimal example to test if indexedDB can run in your brave browser (it works well on mine).

[Johannes C. Mayer]

@Xubai Wang 2022-03-14T10-58-160100.png

[Xubai Wang]

So it seems to be the problem of your brave browser, which cannot be solved by us (no related information on the web).
You can open an issue to brave developers.

Also a cache-less fallback will be available after @Henrik Böving merges this pull request, which can work for your situation.

[Johannes C. Mayer]

@Xubai Wang Ok good. I think the issue is that suspending my machine (many times) caused some corruption. Sometimes other applications behave strange after suspending. Sorry, but I actually didn't think of trying to restart Brave until now as I never do that normally because I have to resort all the windows into appropriate work-spaces and therefore only suspend my system. And I never run into an issue like this before. And restarting fixes the issue, duh.

[Henrik Böving]

merged!