local documentation?

Stream: std4

[Adrien Champion]

I would like to contribute to the documentation effort, and I'm wondering what the idiomatic way to generate local documentation for std4 is.

Should I hack into the lakefile.lean as discussed on docgen 4, or is there a clean way to do this?

[Mario Carneiro]

cc: @Henrik Böving , I don't know the answer to this question as I've never used doc-gen locally

[Adrien Champion]

I'm only asking this because std4 does not have the magic lakefile.lean bit for docgen. @Mario Carneiro wouldn't it make sense to have it there?

[Mario Carneiro]

Possibly, if you can make it work I'll take a PR for that

[Adrien Champion]

Well following https://github.com/leanprover/doc-gen4#usage does work, but the documentation generated is all broken. Seems like missing images and broken CSS or something

[Adrien Champion]

It makes it hard to write doc if I can't make sure it looks nice and lean, I'll wait for @Henrik Böving to get back to us in case he's got a solution

[Henrik Böving]

What is in the mathlib4 lakefile works locally without issues. For me. Once upon a time there was an idea to ship doc-gen with lean which would allow lake to provide this facet natively but that was postponed at least for now.

If something is broken with the local documentation I'd say that's either a bug or a mistake you made. I can try generating it locally myself when I'm home.

[Mario Carneiro]

the question is about std4 not mathlib4 though. Do the links still work if you run the same code in std4?

[Henrik Böving]

Yes they should work arbitrarily there is nothing specific to mathlib in doc-gen that I can think of

[Henrik Böving]

Okay doc-gen is broken because of some lake stuff again let me fix that first and then I'll see how it plays with std4

[Henrik Böving]

So apparently this code:

  match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with

is broken now because:

invalid occurrence of universe level 'u_1' at 'DocGen4.lakeSetup', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  Lake.mkLoadConfig.{u_1}
    (Lake.LakeOptions.mk.{u_1} (FilePath.mk ".") Lake.defaultConfigFile leanInstall? lakeInstall?
      EmptyCollection.emptyCollection.{0} List.nil.{0} false Lake.Verbosity.normal.{u_1} false)

because: Lake.Verbosity is in Type u now? @Mac why is that?

inductive Verbosity : Type u
| quiet
| normal
| verbose
deriving BEq

and in general, how do I address this? It appears lean can (and I think rightfully so?) not infere the universe levels here?

I guess this works :D

  let t : Type 0 := Lake.Verbosity
  let config := Lake.mkLoadConfig {leanInstall?, lakeInstall?, verbosity := (Lake.Verbosity.normal : t)}

but that feels awful

[Sebastian Ullrich]

mkLoadConfig.{0} should work

[Henrik Böving]

Ah I tried the annotation directly at verbosity but it didn't like that...is there a reason we support it at the function but not like .verbose.{0}?

[Sebastian Ullrich]

Looks slightly cursed, but for consistency we probably should, yeah

[Henrik Böving]

@Adrien Champion just built locally after fixing the compilation issue with the latest version of lean:
image.png
looks fine to me.

[Adrien Champion]

Looks awesome!

[Henrik Böving]

Can you verify on your end?

[Adrien Champion]

On it

[Adrien Champion]

That's why you haven't been thanked yet

[Henrik Böving]

:D

[Henrik Böving]

you'll have to do a lake -Kdoc=on update then lake -Kdoc=on build Std:docs

[Adrien Champion]

It does work, thanks!

[Adrien Champion]

Minor remark however, the search feature seems to be broken

[Adrien Champion]

Searching array for instance yields

Screenshot-2022-12-02-at-18.25.59.png

[Adrien Champion]

Mario Carneiro said:

Possibly, if you can make it work I'll take a PR for that

I made it work! Slight problem with the search feature but I have my best guy on it

[Adrien Champion]

@Mario Carneiro is lake -Kdoc=on build Std:docs reasonable to you or do you want -Kenv=dev or something else?

[Mario Carneiro]

doc=on seems fine

[Henrik Böving]

Adrien Champion said:

Minor remark however, the search feature seems to be broken

Ehhh, its kind of a legacy feature specifically for mathlib that I should probably remove at some point, you're not supposed to actually use the search by pressing enter or the button but rather by clicking on the suggestions it provides you with.

[Adrien Champion]

I would be fine with that but I don't get any suggestions :confused:

Screenshot-2022-12-02-at-18.43.16.png

[Adrien Champion]

FYI: https://github.com/leanprover/std4/pull/50

[Henrik Böving]

Interesting, I do

[Henrik Böving]

image.png

[Adrien Champion]

I don't know what I'm doing wrong, maybe it just recognizes its master

[Henrik Böving]

Does your console show something maybe?

[Adrien Champion]

Was running on firefox, just tried on chrome, and console does not say anything helpful except maybe

Access to script at 'file:///Users/adrien/repos/std4/mine/build/doc/instances.js' from origin 'null' has been blocked by CORS policy: Cross origin requests are only supported for protocol schemes: http, data, isolated-app, chrome-extension, chrome, https, chrome-untrusted.

[Henrik Böving]

Ah, you're just opening these HTML files directly that's not gonna work because of this issue.

[Henrik Böving]

You need to host a local http server like for example python3 -m http.server in the directory doc/ in your std4 checkout

[Adrien Champion]

Oh I see, I did what I usually do with Rust docs my bad

[Henrik Böving]

If i was a better web developer I could probably fix this but I have to admit this website only looks so good because I cannibalized the original doc-gen massively I don't actually know what I'm doing in the browser :D

[Adrien Champion]

Well I can relate to that :smiley_cat: