docgen4 not working?

Stream: lean4

[Joseph O]

I tried using docgen4 on my project with \my\path\to\docgen-4 / Itertools. But this is what i get when I run the server:
image.png image.png
I tried again by specifying the directory (Itertools) where all my documentated functions are: \my\path\to\docgen-4 /Itertools Itertools, but i get the same thing

[Joseph O]

By the way, here was my build output:

PS C:\Users\[REDACTED]\Desktop\programming\Itertools> C:\clones\doc-gen4\build\bin\doc-gen4.exe /Itertools.lean Itertools
Loading modules from: [c:\users\vatis\desktop\programming\itertools\build\lib]
Processing modules
WARNING: Failed to calculate equational lemmata for Lean.expandExplicitBindersAux.loop: tactic 'simp' failed, nested error:
(deterministic) timeout at 'simp', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Outputting HTML
uncaught exception: invalid argument (error code: 22, invalid argument)
  file: ./build/doc/\find\Lean.SourceInfo.getPos?

[Xubai Wang]

Does \path\to\docgen-4 /Itertools/ Itertoolswork? (notice the trailing slash)

[Xubai Wang]

Are there html pages in your build/doc directory?

[Joseph O]

Xubai Wang said:

Are there html pages in your build/doc directory?

yes

[Joseph O]

Xubai Wang said:

Does \path\to\docgen-4 /Itertools/ Itertoolswork? (notice the trailing slash)

its the same thing

[Henrik Böving]

Is your project somewhere so we can try this ourselves?

[Joseph O]

Henrik Böving said:

Is your project somewhere so we can try this ourselves?

https://github.com/crabbo-rave/lean4-Itertools

[Henrik Böving]

Building with doc-gen4 / Itertools then cd-ing into build/doc and running a python test server with python -m http.server works for me. are you sure you are building and hosting this in the right way?

[Joseph O]

I did git pull
Im going to try again

[Xubai Wang]

May be a clearer approach:
Run doc-gen4 /build/doc/ Itertools and python3 -m http.server, just in your project root without changing directory. and then visit http://localhost:8000/build/doc/ in your browser.

[Joseph O]

Thanks I will try it out

[Joseph O]

I get an error

PS C:\Users\rrrrr\Desktop\programming\Itertools> C:\clones\doc-gen4\build\bin\doc-gen4.exe  /build/doc/ Itertool
Loading modules from: [c:\users\vatis\desktop\programming\itertools\build\lib]
uncaught exception: unknown package 'Itertool'

[Henrik Böving]

well yes your package is called Itertools

[Joseph O]

Yes

[Henrik Böving]

So you should give doc-gen that name and not the singular form

[Joseph O]

Sorry if im being a bit annoying, but isnt that what I did?

[Henrik Böving]

You wrote Itertool not Itertools.

[Joseph O]

ah i see lol

[Joseph O]

image.png

[Xubai Wang]

Can you provide a screen capture (or ls) of your build/doc dir?

[Joseph O]

Xubai Wang said:

Can you provide a screen capture (or ls) of your build/doc dir?

(much longer)
image.png

[Xubai Wang]

Emmm, so the problem is here: there are only find folder in your build/doc, but a normal one should be like this:

screenshot

Which commit of doc-gen4 do you use?

[Joseph O]

I just cloned the one from github, and recently did git pull

[Xubai Wang]

Then try lake clean and doc-gen it again?

[Joseph O]

i have done that a thousand times already. everytime i build the doc

[Xubai Wang]

Joseph O said:

By the way, here was my build output:

PS C:\Users\[REDACTED]\Desktop\programming\Itertools> C:\clones\doc-gen4\build\bin\doc-gen4.exe /Itertools.lean Itertools
Loading modules from: [c:\users\vatis\desktop\programming\itertools\build\lib]
Processing modules
WARNING: Failed to calculate equational lemmata for Lean.expandExplicitBindersAux.loop: tactic 'simp' failed, nested error:
(deterministic) timeout at 'simp', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
Outputting HTML
uncaught exception: invalid argument (error code: 22, invalid argument)
  file: ./build/doc/\find\Lean.SourceInfo.getPos?

At first there is an uncaught exception. Probably it stops doc-gen from generating other parts of the doc. Does this error appears again and again? (Just ignore the heartbeat warning, that's problem from Lean itself)

[Joseph O]

yes

[Henrik Böving]

That's either an issue with the harcoded build/doc base path or with the fact that windows file system might not like a ? in its file names, can you create a directory with a ? in its name under Windows?

[Mauricio Collares]

Also, does your user name contain spaces?

[Henrik Böving]

It doesnt, we can see it in the doc-gen log which he forgot to redact.

[Mauricio Collares]

Looks like you're right, Windows does not support question marks in file names

[Xubai Wang]

https://docs.microsoft.com/en-us/windows/win32/fileio/naming-a-file
Yes, that would unfortunately be a problem for find.

[Xubai Wang]

How much do we rely on a file based find?

[Henrik Böving]

docs4#Nat is completely based on it.

[Henrik Böving]

(referring to the linking Zulip feature here).

[Xubai Wang]

Maybe we can link to a single /find.html page and rely on JavaScript to figure out the right place?

[Henrik Böving]

I was about to write that yes^^

[Henrik Böving]

Although I'm completely unfamiliar with frontend development so someone else would have to do that

[Henrik Böving]

Oh and there is also an open issue for the src# variant here https://github.com/leanprover/doc-gen4/issues/30 which would have to be addressed the same way then.

[Xubai Wang]

@Joseph O For temporal workaround, you can remove these lines in DocGen4/Output.lean and rebuild doc-gen to disable the find feature and that will work for your platform.

DocGen4/Output.lean

EDITED: also remove the "searchable_data.bmp" line.

[Henrik Böving]

That's not gonna compile the next line uses the json variable still.

[Henrik Böving]

But if you comment that one out too it will

[Joseph O]

let me try rebuilding docgen4

[Joseph O]

first. That could fix it

[Joseph O]

Xubai Wang said:

Joseph O For temporal workaround, you can remove these lines in DocGen4/Output.lean and rebuild doc-gen to disable the find feature and that will work for your platform.

DocGen4/Output.lean

EDITED: also remove the "searchable_data.bmp" line.

When i do that it wont build

[Joseph O]

I recloned it from github and that version is not building. Should I report this as an issue?

[Henrik Böving]

The version very much is building according to both my machine and the CLI, what's your error with a new cloned one?

[Joseph O]

Well it worked right now. Let me try generating documentation

[Joseph O]

What does this mean?

uncaught exception: invalid argument (error code: 22, invalid argument)
  file: .\build\doc\find\Lean.SourceInfo.getPos?

i always get it

[Joseph O]

Why is it working on you machine and not mine? Are you using windows?

[Henrik Böving]

No, I'm on Fedora, Xubai is on MacOS (at least his screenshots look like that) and all the CLI and automation runs some Linux flavour as well. I neither have a Windows machine nor has someone with a Windows machine yet tried to run doc-gen4 so this is why it wasnt discovered before.

[Joseph O]

No one has tried docgen4 on windows yet? This could be the problem

[Joseph O]

Any ideas why it doesnt work on Windows?

[Henrik Böving]

Why it doesn't work was already elaborated in detail above.

[Henrik Böving]

However it should work if you comment out the lines in the screenshot above as well as the next one that uses the json variable because then these directories are not created anymore.

[Joseph O]

Henrik Böving said:

That's either an issue with the harcoded build/doc base path or with the fact that windows file system might not like a ? in its file names, can you create a directory with a ? in its name under Windows?

I can try

[Henrik Böving]

Read the discussion fully we know that a ? is illegal already by now.

[Joseph O]

yeah Windows doesn't allow it

[Joseph O]

I can try what this message says again

[Joseph O]

It worked! :+1:

[Joseph O]

Are the docstrings supposed to show up somewhere?

[Henrik Böving]

Not yet

[Xubai Wang]

@Henrik Böving docstring now works perfectly on mathlib4 when i test it locally but when I merge it into main, there are PANIC at Std.HashMap.find! Std.Data.HashMap:177:14: key is not in the map errors.

[Henrik Böving]

Aha....it's a little bit annoying panics don't have a backtrace, you could try to git bisect the issue.

[Henrik Böving]

I can't reproduce it with the current doc-gen main so it's probably some interaction between a change on main and a change of yours.

[Joseph O]

Im aware that right now the lean 4 devs are worried about other things at the moment, but will there be a centralized website for lake packages like crates.io, or is it still not known yet?

[Henrik Böving]

Not known.

[Xubai Wang]

I can help write a simple unofficial one based on the GitHub search https://github.com/search?q=lakefile.lean+in%3Apath&type=Code, much like that of lib.rs.

[Joseph O]

Xubai Wang said:

I can help write a simple unofficial one based on the GitHub search https://github.com/search?q=lakefile.lean+in%3Apath&type=Code.

Wow 625k

[Henrik Böving]

Lots of those are false positives by the relatively liberal github search

[Joseph O]

If you do end up writing one I would love to help

[Henrik Böving]

I would estimate the amount of Lean 4 projects out there is at most in the 100s at the moment.

[Joseph O]

Yeah towards the end it is not counting lakefile.lean anymore: image.png