Zulip Chat Archive

Stream: std4

Topic: local documentation?


Adrien Champion (Dec 02 2022 at 14:27):

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 (Dec 02 2022 at 14:28):

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

Adrien Champion (Dec 02 2022 at 14:30):

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 (Dec 02 2022 at 14:31):

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

Adrien Champion (Dec 02 2022 at 14:33):

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 (Dec 02 2022 at 14:34):

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 (Dec 02 2022 at 15:24):

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 (Dec 02 2022 at 15:34):

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

Henrik Böving (Dec 02 2022 at 15:39):

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

Henrik Böving (Dec 02 2022 at 16:11):

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 (Dec 02 2022 at 16:18):

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 (Dec 02 2022 at 16:20):

mkLoadConfig.{0} should work

Henrik Böving (Dec 02 2022 at 16:22):

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 (Dec 02 2022 at 16:25):

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

Henrik Böving (Dec 02 2022 at 17:18):

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

Adrien Champion (Dec 02 2022 at 17:18):

Looks awesome!

Henrik Böving (Dec 02 2022 at 17:18):

Can you verify on your end?

Adrien Champion (Dec 02 2022 at 17:19):

On it

Adrien Champion (Dec 02 2022 at 17:19):

That's why you haven't been thanked yet

Henrik Böving (Dec 02 2022 at 17:20):

:D

Henrik Böving (Dec 02 2022 at 17:20):

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

Adrien Champion (Dec 02 2022 at 17:25):

It does work, thanks!

Adrien Champion (Dec 02 2022 at 17:25):

Minor remark however, the search feature seems to be broken

Adrien Champion (Dec 02 2022 at 17:26):

Searching array for instance yields

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

Adrien Champion (Dec 02 2022 at 17:27):

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 (Dec 02 2022 at 17:31):

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

Mario Carneiro (Dec 02 2022 at 17:32):

doc=on seems fine

Henrik Böving (Dec 02 2022 at 17:41):

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 (Dec 02 2022 at 17:44):

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 (Dec 02 2022 at 17:47):

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

Henrik Böving (Dec 02 2022 at 17:47):

Interesting, I do

Henrik Böving (Dec 02 2022 at 17:47):

image.png

Adrien Champion (Dec 02 2022 at 17:52):

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

Henrik Böving (Dec 02 2022 at 17:53):

Does your console show something maybe?

Adrien Champion (Dec 02 2022 at 17:56):

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 (Dec 02 2022 at 18:04):

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

Henrik Böving (Dec 02 2022 at 18:04):

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 (Dec 02 2022 at 18:11):

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

Henrik Böving (Dec 02 2022 at 18:11):

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 (Dec 02 2022 at 18:14):

Well I can relate to that :smiley_cat:


Last updated: Dec 20 2023 at 11:08 UTC