Zulip Chat Archive

Stream: general

Topic: Lean 4 project blueprint

Yaël Dillies (Sep 20 2023 at 19:42):

Has anyone gone around to doing a version of plastex (cc @Patrick Massot) for Lean 4? I'm almost done porting LeanAPAP to Lean 4 but I don't want to switch over if that means losing the blueprint.

Yaël Dillies (Sep 20 2023 at 19:42):

cc @Sky Wilshaw who has a similar problem with Con(NF)

Johan Commelin (Sep 20 2023 at 19:43):

You mean a Lean 4 plugin for plasTeX?

Sky Wilshaw (Sep 20 2023 at 19:45):

We were talking about a Lean 4-compatible version of leanblueprint.

Patrick Massot (Sep 20 2023 at 19:45):

I haven't heard anything about this. It should be at most one day of work, but someone needs to do it.

Utensil Song (Oct 01 2023 at 05:00):

Recently I also needed a lightweight solution to use blueprint for Lean 4/Mathlib 4, so I hacked one here in a minimal setting:

  1. Use \leanfour{SomeTheorem} to jump to Mathlib4 doc like https://leanprover-community.github.io/mathlib4_docs/find/?pattern=SomeTheorem#doc and the base url can be configured by \dochome{https://your-docgen4-url-base/} in your web.tex file
  2. All original \lean{some_theorems} still work alongside the Lean 4 button, provided you install leanblueprint with leanblueprint[lean3] @ git+https://github.com/utensil/leanblueprint.git@lean4 in your requirements.txt via pip install -r requirements.txt (note the extra [lean3] here to indicate legacy Lean 3 support together with Lean 4 support)

Utensil Song (Oct 01 2023 at 05:01):

A few considerations:

1. Should it drop Lean 3 support immediately?

I choose to make them work together for the transition period because converting all \lean{some_theorems} to \leanfour{SomeTheorem} or just \lean{SomeTheorem} could be as easy as replacing them with CamelCase or they could end up somewhere quite different with some different name, it's better to provide a transition period, at least I need it in a scenario that the dependency is changed to Mathlib 4 but the project itself is still in Lean 3 and porting, so it makes sense for the blueprint to accommodate that.

It's likely the official leanblueprint will drop Lean 3 support without hesitation and use \lean{SomeTheorem}, but it's easy to port \leanfour to \lean as it's just a simple global replacement without ambiguity. So this solution is future-proof.

During the transition period, mathlibtools installation has been made optional, as long as you don't use the old \lean and stick to \leanfour in your Lean 4 project, you are safe to just use leanblueprint @ git+https://github.com/utensil/leanblueprint.git@lean4 (if there's consensus on the approach I will open a PR).

2. Where should it jump?

I prefer to jump to the doc, but it can be made jumping to source with an option to replace the trailing #doc to #src as this is supported by docgen4. But I think this is a loss of information, because one can jump to the source from the doc if needed but not vice versa.

The old leanblueprint requires running a Lean 3 script to collect the declarations to make a precise jump, this can be done for Lean 4 in principle, but I fail to see the necessity in a minimal setting and I need to figure out how to do it idiomatically in Lean 4. So this part is left out, but the UX is almost not affected, the only difference is that it might not jump to the precise one if there is ambiguity but this can be considered a feature to find similar theorems or definitions.

EDIT: One requirement difference is that the target project needs to use docgen4, because the old one supports jumping to Github source without a docgen setting. But this requirement is towards a better practice.

3. Why \leanfour instead of \lean4?

Unfortunately, LaTeX doesn't directly support digits in macro names. There are workarounds, but they make the solution more fragile. So I stick to \leanfour and also it's easier to replace it without ambiguity and reasonably simple to type.

Anyway, this fits my own need for now, and it's easy for anyone else to make one with some different preference by reading the diff here.

Utensil Song (Oct 01 2023 at 05:05):

It looks like this:

image.png

(Maybe I should change L∃∀N to L∃∀N 3 or L∃∀N 4 to :lucky: )

Kevin Buzzard (Oct 01 2023 at 06:28):

I don't see any reason why you should still support lean 3. If someone wants to make a project then they won't be using both systems, and lean 3 already has its own blueprint software.

Utensil Song (Oct 01 2023 at 07:24):

Besides the reasons I explained above that I need to reference Mathlib 4 and Lean 3 project in one Blueprint for the time being, use \lean to mean lean4 will break Blueprint CI for existing Lean 3 projects (but it's also an easy fix). It's easy to drop Lean 3, and equivalently easy to remain compatibility so I did it.

Utensil Song (Oct 01 2023 at 07:37):

If dropping Lean 3 is preferred and using \lean to mean Lean 4 is ok, I can easily make it so and submit a PR.

Yaël Dillies (Oct 01 2023 at 07:40):

LeanAPAP is currently in Lean 3 because I don't want the blueprint to break. But all the code has been ported to Lean 4 on a branch and I don't need any transition period for my blueprint.

Utensil Song (Oct 01 2023 at 07:41):

Consideration 2 is also opinionated.

Utensil Song (Oct 01 2023 at 07:45):

@Yaël Dillies Do you have doc-gen4 for your Lean 4 project?

Yaël Dillies (Oct 01 2023 at 07:48):

Yes.

Utensil Song (Oct 01 2023 at 07:52):

Then consideration 2 won't be an issue.

Yaël Dillies (Oct 01 2023 at 07:54):

I think you should have both a "Lean docs" and a "Lean source" button, with the "Lean docs" one on only if doc-gen4 is used.

Utensil Song (Oct 01 2023 at 07:58):

Unfortunately the old leanblueprint relies on the Lean script to gather source location while my branch relies on doc-gen4 to do the same. I can provide both buttons if doc-gen4 is available but none of them if doc-gen4 is not.

Yaël Dillies (Oct 01 2023 at 08:03):

Ah I see. I think that's fine to keep it like that until someone complains.

Utensil Song (Oct 01 2023 at 08:09):

One in need could port the Lean 3 script to Lean 4 but maybe better to use yaml etc. instead of pickle.

Utensil Song (Oct 01 2023 at 08:10):

Lean 4 only branch: https://github.com/utensil/leanblueprint/tree/lean4-only

It works with leanblueprint @ git+https://github.com/utensil/leanblueprint.git@lean4-onlyin the requirements.txt via pip install -r requirements.txt.

PR WIP, need to add some doc

Utensil Song (Oct 01 2023 at 17:53):

PatrickMassot/leanblueprint#5

Utensil Song (Oct 01 2023 at 17:58):

I don't know what to add in the doc, as there were little and people follow example projects anyway. I end up writing a migration guide assuming the readers know what to do for Lean 3, only need some clue to achieve the same for Lean 4.

Eric Wieser (Oct 02 2023 at 04:50):

Utensil Song said:

2. Where should it jump?

I prefer to jump to the doc, but it can be made jumping to source with an option to replace the trailing #doc to #src as this is supported by docgen4. But I think this is a loss of information, because one can jump to the source from the doc if needed but not vice versa.

The advantage of a src jump is that you can permalink to a specific commit, unlike a doc link that can break.

Chris Birkbeck (Oct 02 2023 at 14:05):

Utensil Song said:

I don't know what to add in the doc, as there were little and people follow example projects anyway. I end up writing a migration guide assuming the readers know what to do for Lean 3, only need some clue to achieve the same for Lean 4.

Is there a sample project for lean 4 that I can look at? I wanted to try and do this for the flt blueprint, but even though I at somepoint knew how to do it for lean 3 I don't really know how to do it now for lean 4. I remember using the instructions here when I made a lean 3 blueprint, but I'm not sure how much carries over.

Patrick Massot (Oct 02 2023 at 14:07):

@Utensil Song thanks for your work. I'll take a look soon. In the mean time I'd be really interested in reading what existing and future users of the blueprint infrastructure think about the link targets (doc-gen vs GitHub). Indeed the doc-gen solution is infinitely simpler to implement.

Patrick Massot (Oct 02 2023 at 14:08):

Eric Wieser said:

Utensil Song said:

2. Where should it jump?

I prefer to jump to the doc, but it can be made jumping to source with an option to replace the trailing #doc to #src as this is supported by docgen4. But I think this is a loss of information, because one can jump to the source from the doc if needed but not vice versa.

The advantage of a src jump is that you can permalink to a specific commit, unlike a doc link that can break.

I think it means the blueprint must link only to documentation hosted on the same website and generated at the same time. So a project depending on mathlib needs to rebuild and host mathlib documentation. Does that sound reasonable? @Henrik Böving

Utensil Song (Oct 02 2023 at 14:34):

Yes, keeping doc-gen4 consistent with blueprint and ensured by a CI is the practice I was imagining.

Somehow I begin to realize the usability cost for the simplicity of implementation. Maybe the Lean script to collect declarations is already a minimal dependency and worth porting to meet functionality equivalence then jumping to doc-gen4 could be an extra feature.

Utensil Song (Oct 02 2023 at 14:51):

Chris Birkbeck said:

Utensil Song said:

I don't know what to add in the doc, as there were little and people follow example projects anyway. I end up writing a migration guide assuming the readers know what to do for Lean 3, only need some clue to achieve the same for Lean 4.

Is there a sample project for lean 4 that I can look at? I wanted to try and do this for the flt blueprint, but even though I at somepoint knew how to do it for lean 3 I don't really know how to do it now for lean 4. I remember using the instructions here when I made a lean 3 blueprint, but I'm not sure how much carries over.

Sorry I'm out these two days, I can make a minimal sample project when I'm back.

Chris Birkbeck (Oct 02 2023 at 14:55):

That would be great, thank you! I'll have a closer look to see if I can figure it out, but I'm sure a sample project will be useful to others as well :)

Utensil Song (Oct 02 2023 at 14:58):

Meanwhile you can check out here particularly tasks.py, .github, requirements.txt which runs blueprint lean4 only version. You can use the relevant part in your Lean 4 project and safely ignore the fact that lean-ga is still a Lean 3 project which doesn't affect the new blueprint plugin as it's simply jumping to a doc-gen4 link.

Kevin Buzzard (Oct 02 2023 at 15:04):

If I want to use this stuff to make a Fermat's Last Theorem project like the liquid tensor experiment, hosted at eg Imperial College's GitHub, then what does jumping to doc-gen mean for me? Do I also have to host docs somehow?

Wasn't the dream to jump to leanink?

Utensil Song (Oct 02 2023 at 15:19):

Yes, hosting the doc makes this approach work naturally. I'll show the POC of how it works in the sample project. It could be as easy as some copy-pasting(from the sample project).

Patrick Massot (Oct 02 2023 at 15:20):

Kevin Buzzard said:

If I want to use this stuff to make a Fermat's Last Theorem project like the liquid tensor experiment, hosted at eg Imperial College's GitHub, then what does jumping to doc-gen mean for me? Do I also have to host docs somehow?

Yes, if we want links to doc-gen rather than GitHub then you need to host docs. But there is no need for a fancy server, they are html pages with javascript. It is not more complicated than hosting NNG3.

Utensil Song (Oct 02 2023 at 15:21):

As for LeanInk, my dream would be directly embed LeanInk generated Lean 4 proof with intermediate goal states in the blueprint, maybe with click to expand.

Patrick Massot (Oct 02 2023 at 15:21):

Wasn't the dream to jump to leanink?

Very good question. The original dream was indeed to jump to some version of leanink. But leanink is abandonned. Even doc-gen no longer includes links to leanink-generated pages. I hope someone will pick up this project at some point.

Utensil Song (Oct 02 2023 at 15:26):

Oh I didn't know LeanInk is abandoned (only in the sense of maintenance, right? as it seems to work fine for proofs I tried) and docgen4 used to link to it. Then if LeanInk is revived, blueprint → doc gen4 → LeanInk is still there.

Patrick Massot (Oct 02 2023 at 15:29):

It is not officially abandoned, but this was a student project, the student moved along and nobody took up the task. The main difficulty is that it was built on top of a tool, Alectryon, that is also mostly abandoned (the main author was a post-doc but got an actual job involving teaching and presumably administrative duty and no longer has enough time). In the beginning relying on Alectryon was a big win because it allowed to focus on Lean with worrying with user-facing stuff, but now this dependency should probably be removed.

Patrick Massot (Oct 02 2023 at 15:31):

All of this is public information by the way, you only need to look at https://github.com/leanprover/LeanInk/commits/main, https://github.com/leanprover/LeanInk/issues, https://github.com/cpitclaudel/alectryon/commits/master, https://github.com/cpitclaudel/alectryon/issues

Utensil Song (Oct 02 2023 at 15:54):

Thanks for the thorough explanation. I checked the issues of both repos and they seem to be mostly enhancements and only few are bugs for edge cases, so overall LeanInk is in good shape and the major issue is to make LeanInk work with something else to produce the HTML instead of relying on alectryon? As LeanInk already produces JSON, these something else could be as simple as just one html with some js to consume that JSON directly as opposed to the current approach of using alectryon to generate some HTML tags then use CSS/JS to render these tags.

Henrik Böving (Oct 02 2023 at 16:23):

Patrick Massot said:

Eric Wieser said:

Utensil Song said:

2. Where should it jump?

I prefer to jump to the doc, but it can be made jumping to source with an option to replace the trailing #doc to #src as this is supported by docgen4. But I think this is a loss of information, because one can jump to the source from the doc if needed but not vice versa.

The advantage of a src jump is that you can permalink to a specific commit, unlike a doc link that can break.

I think it means the blueprint must link only to documentation hosted on the same website and generated at the same time. So a project depending on mathlib needs to rebuild and host mathlib documentation. Does that sound reasonable? Henrik Böving

Yes. Although I would hope we eventually converge towards a docs.rs style solution that everyone can just link to.

Patrick Massot (Oct 02 2023 at 17:41):

Utensil Song said:

Thanks for the thorough explanation. I checked the issues of both repos and they seem to be mostly enhancements

Some enhancements are really fundamental. Currently Alectryon and LeanInk are fundamentally tools handling one Lean file at a time. There is no way you can get links between files. So you don' t have the html analogue of jump to definition, or even preview lemma statement, so it is not really usable. I'm also pretty sure there were more serious bugs, but maybe nobody opened issues because it seemed abandoned.

and only few are bugs for edge cases, so overall LeanInk is in good shape and the major issue is to make LeanInk work with something else to produce the HTML instead of relying on alectryon? As LeanInk already produces JSON, these something else could be as simple as just one html with some js to consume that JSON directly as opposed to the current approach of using alectryon to generate some HTML tags then use CSS/JS to render these tags.

Yes, that would be the minimal version. But I think it's less simple than it appears.

Utensil Song (Oct 03 2023 at 00:39):

To be able to handle multiple Lean files or a Lean project as a whole, then distilling the relevant part of LeanInk into doc-gen4 might be the way to go, then facilities there handling cross-reference, markup and frontend etc. can be reused. This would be like Doxygen, which can generate API document as well as source code cross-reference, in one place.

As for blueprint, once I thought it would become less used when doc-gen4 becomes more powerful and integrated, but its value is to first chart uncharted territories in an informal and Lean-neutral way, then provides portals to the later formalized doc and source. So keeping it independent from doc-gen4 makes sense.

Mac Malone (Oct 03 2023 at 06:00):

Henrik Böving said:

Yes. Although I would hope we eventually converge towards a docs.rs style solution that everyone can just link to.

I contemplated doing this in Reservoir, but I was not sure how to make this work. The main issue is that doc-gen4 currently has a lot of workspace global data, which does not translate nicely to atomized packages. For example, if we run doc-gen on each package it produce documentation for all its dependencies which means a lot of duplicated data across packages (and very large data for packages which depend on mathlib). How would you see this working?

Henrik Böving (Oct 03 2023 at 10:03):

Right, I do think the current doc gen design is not so easily compatible with having multiple separate packages either. In particular features like the global list of instances definitely dont work out on a larger scale. I think the answer here is to basically give up on the idea of having a list of all instances in the Eco system on the type class itself and instead limit these global information features to local package information.

In addition to that we would need a slightly more intelligent linking feature that tells doc-gen some sort of template string to use for linking to external packages. Reservoir could then provide such a string that conforms with its own structure.

Do you see additional problems here? @Mac Malone

Eric Wieser (Oct 03 2023 at 15:11):

If I publish a package that depends on a particular version of mathlib, then I'm going to want to be able to permalink to docs for that particular mathlib version; and by far the easiest way to do that is just to regenerate all those docs myself and host them alongside my docs (in which case the instance lists in their current form are fine)

Eric Wieser (Oct 03 2023 at 15:13):

The alternative is to centrally host a copy for every mathlib "release", but that seems far more resource intensive than each package hosting the one copy they need.

Eric Wieser (Oct 03 2023 at 15:13):

(at least while every commit is a release)

Eric Wieser (Oct 03 2023 at 15:14):

It would be great if doc-gen4 could distinguish "this is the documentation for this package" vs "you are looking at an old version of the documentation for a dependency of another package"

Eric Wieser (Oct 03 2023 at 15:15):

(doc-gen3 did this with link rel="canonical", which avoids SEO problems caused by duplication)

Utensil Song (Oct 03 2023 at 15:22):

Yes, I've also made used of this fact (generating doc for a project generates doc for the exact version of mathlib, std, core it uses) so there is only one base url to jump to, the doc of the project.

Utensil Song (Oct 03 2023 at 15:24):

I could not imagine a docs.rs for Lean as it's so decentralized in regard to versions of dependencies, and little compatibility can be preserved when they evolve, unlike traditional software developments.

Utensil Song (Oct 04 2023 at 08:37):

@Chris Birkbeck The minimal Lean 4 blueprint project is here: https://github.com/utensil/LeanBlueprintExample/ which has a minimal CI that generates a blueprint here ( https://utensil.github.io/LeanBlueprintExample/blueprint/sec-subdemo.html ) that can jump to its doc-gen4 docs ( https://utensil.github.io/LeanBlueprintExample/doc/ ) .

Chris Birkbeck (Oct 04 2023 at 08:37):

Amazing! Thank you very much! I'll check it out now

Chris Birkbeck (Oct 04 2023 at 08:48):

@Utensil Song In step 3, is there a command missing? should I add

meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

to the lakefile.lean?

Utensil Song (Oct 04 2023 at 09:37):

Yes, I was about to update readme after ci pass but forgot (before went out to play with my kids)

Chris Birkbeck (Oct 04 2023 at 10:23):

So I'm getting the following error when I try to test locally, running lake -Kenv=dev build YourProject:docs it says
"error: unknown library facet docs"

Utensil Song (Oct 04 2023 at 10:36):

It would appear if you haven't run lake -Kenv=dev update which installs and configures doc-gen4

Utensil Song (Oct 04 2023 at 10:36):

README updated.

Chris Birkbeck (Oct 04 2023 at 10:37):

Hmm, no I did run that: 

PS C:\Users\chris\FLT_regular_blueprint\FltRegular> lake -Kenv=dev update
mathlib: updating repository '.\lake-packages\mathlib' to revision '39a866a8658151890d84106ca8edd9fbebfe9df1'
PS C:\Users\chris\FLT_regular_blueprint\FltRegular> lake -Kenv=dev build FltRegular:docs
error: unknown library facet `docs`

Utensil Song (Oct 04 2023 at 10:38):

Weird, it should show:

% lake -Kenv=dev update
cloning https://github.com/leanprover/doc-gen4 to ./lake-packages/doc-gen4
cloning https://github.com/xubaiw/CMark.lean to ./lake-packages/CMark
cloning https://github.com/fgdorais/lean4-unicode-basic to ./lake-packages/lean4-unicode-basic
cloning https://github.com/hargonix/LeanInk to ./lake-packages/leanInk
warning: improperly formatted manifest: incompatible manifest version `4`

Chris Birkbeck (Oct 04 2023 at 10:39):

now it just does nothing: 

PS C:\Users\chris\FLT_regular_blueprint\FltRegular> lake -Kenv=dev update
PS C:\Users\chris\FLT_regular_blueprint\FltRegular>

Utensil Song (Oct 04 2023 at 10:41):

Let me try this from scratch again

Chris Birkbeck (Oct 04 2023 at 10:42):

I did add that line to the lakefile.lean. I also cloned the blueprint example repo and tried running it there and nothing. Also I don't know if this matters but I'm using windows...

Utensil Song (Oct 04 2023 at 10:50):

Seems to work from scratch on my end. Sorry, I can't test this on Windows at the moment.

Chris Birkbeck (Oct 04 2023 at 10:51):

hmm ok, let me try with my WSL

Utensil Song (Oct 04 2023 at 10:51):

Maybe try remove meta if get_config? env = some "dev" then -- dev is so not everyone has to build it and leaves only require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" in the lakefile.lean, then run lake update and lake build YourProject:docs?

Utensil Song (Oct 04 2023 at 10:52):

I can only assume maybe get_config? has some issue on Windows, the rest seems platform-independent.

Chris Birkbeck (Oct 04 2023 at 10:53):

Utensil Song said:

Maybe try remove meta if get_config? env = some "dev" then -- dev is so not everyone has to build it and leaves only require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" in the lakefile.lean, then run lake update and lake build YourProject:docs?

Oh that did something. I got the output you said I should get. Let me see if the rest works now

Chris Birkbeck (Oct 04 2023 at 14:48):

OK I think I almost have it all running. I ran the github workflow and made a doc and blueprint folder in the gh-pages branch which look good. The only thing I dont know how to do is to get github to host the pages from these subfolders. Is there a way to do this? I guess I could just put the contents in some other branch and use that, but I wanted to know if there is something I'm missing.

Utensil Song (Oct 04 2023 at 14:56):

Congratulations! CI has been set up to publish Github pages, Step 8 & 9 in the updated README is about that.

Utensil Song (Oct 04 2023 at 14:58):

In .github/workflows/push.yml, step "Copy documentation" and "Deploy doc & blueprint" are there to make this work, along with permissions at the beginning of the file.

Chris Birkbeck (Oct 04 2023 at 15:05):

Oh nice, I hadn't refreshed the readme. Thank you very much!

Utensil Song (Oct 04 2023 at 15:05):

You can add more steps to make an extra project page to link to doc and blueprint like https://github.com/YaelDillies/LeanAPAP did (using its docs folder for a Jekyll website, and step "Bundle dependencies" and "Bundle website" to generate the website, then you just need to copy or move things to be under _site then it's published together with doc and blueprint). I didn't include that part as I think that won't be minimal to include something that depends on Ruby.

Chris Birkbeck (Oct 04 2023 at 20:17):

OK I think I got this working now, thank you so much for making the example blueprint. One last thing that I'm unsure of is, with doc4 links to things that are already in mathlib, should the link direct you to https://leanprover-community.github.io/mathlib4_docs/etc.. or to the one I created? Since it seems either I can link to the mathlib4 ones but then ones that aren't in mathlib wont work or only to the ones in the project but the ones to things in mathlib don't work. You can see here where some of LEAN links work and some don't.

Kevin Buzzard (Oct 04 2023 at 20:27):

I guess you need to consider what this looks like in 5 years when your project is finished but mathlib is still racing on, definitions and theorems have moved or been removed or generalised etc.

Ruben Van de Velde (Oct 04 2023 at 20:28):

Yeah, I think you want to have a copy of the docs for the exact mathlib version you depend on

Yaël Dillies (Oct 04 2023 at 21:17):

Why change the way it worked in Lean 3? namely host the docs for all the mathlib files imported by your project, at the version used by your project.

Chris Birkbeck (Oct 04 2023 at 22:55):

Aha I see, I hadn't thought about how this would age. I agree maybe a copy of the exact version would be best then.

Utensil Song (Oct 04 2023 at 23:33):

Wait, why isn't Mathlib4 documentation of the used version generated together with the project itself?

Utensil Song (Oct 04 2023 at 23:34):

Lean, Lake, Init are, why not Mathlib?

Utensil Song (Oct 04 2023 at 23:36):

I thought they would be, so they would naturally be linked inside the project doc, at least the part that's used.

Utensil Song (Oct 04 2023 at 23:38):

There was this PR discussing generating the document for dependencies but only handles Init/Lean/Lake: https://github.com/leanprover/doc-gen4/pull/19

Utensil Song (Oct 04 2023 at 23:45):

If you have multiple libraries you want to generate documentation for the recommended way right now is to run it for each library.

From doc-gen4 README. But do they link together? I'll have to experiment this the day after tomorrow as I'm out hiking again today and tomorrow.

Has anyone get this to work? From FLT's doc, it can't jump to something in Mathlib, e.g. AddCommMonoid from https://cbirkbeck.github.io/FltRegulartest/doc/FltRegular/ReadyForMathlib/Homogenization.html nor can it be found using find

Eric Wieser (Oct 04 2023 at 23:47):

I think this is just an accident

Utensil Song (Oct 04 2023 at 23:56):

How so? Can you elaborate a bit? :confused:

Utensil Song (Oct 05 2023 at 00:30):

Observing https://cbirkbeck.github.io/FltRegulartest/doc/Mathlib/Algebra/Group/Defs.html#AddCommMonoid it seems linking is possible, just need to place the generated Mathlib doc at the right place (EDIT: already so)

Utensil Song (Oct 05 2023 at 00:32):

I can ge this fixed in the minimal example when I'm back. The same applies to Std etc.

Utensil Song (Oct 05 2023 at 00:41):

And it seems just a little tweak can make find work too

Henrik Böving (Oct 05 2023 at 07:06):

Utensil Song said:

If you have multiple libraries you want to generate documentation for the recommended way right now is to run it for each library.

From doc-gen4 README. But do they link together? I'll have to experiment this the day after tomorrow as I'm out hiking again today and tomorrow.

Has anyone get this to work? From FLT's doc, it can't jump to something in Mathlib, e.g. AddCommMonoid from https://cbirkbeck.github.io/FltRegulartest/doc/FltRegular/ReadyForMathlib/Homogenization.html nor can it be found using find

You just run

lake build Std:docs Mathlib:docs Whatever:docs

and it figures the linking out for you, you only have to copy paste the doc folder somewhere and done

Chris Birkbeck (Oct 05 2023 at 08:17):

Henrik Böving said:

Utensil Song said:

If you have multiple libraries you want to generate documentation for the recommended way right now is to run it for each library.

From doc-gen4 README. But do they link together? I'll have to experiment this the day after tomorrow as I'm out hiking again today and tomorrow.

Has anyone get this to work? From FLT's doc, it can't jump to something in Mathlib, e.g. AddCommMonoid from https://cbirkbeck.github.io/FltRegulartest/doc/FltRegular/ReadyForMathlib/Homogenization.html nor can it be found using find

You just run

lake build Std:docs Mathlib:docs Whatever:docs

and it figures the linking out for you, you only have to copy paste the doc folder somewhere and done

Ahn nice! I'll try doing this then. Thanks!

Chris Birkbeck (Oct 05 2023 at 16:21):

Ok I tried doing this on the github workflow (i.e. ran ~/.elan/bin/lake -Kenv=dev build Std:docs Mathlib:docs FltRegular:docs), but it seems to take a very long time (which is maybe not suprising?) and then fails giving the message System.IO.IOException: No space left on device. It seems to be making the doc for all of mathlib instead of just the ones I need for the repo. Am I doing something wrong?

Utensil Song (Oct 07 2023 at 04:17):

@Chris Birkbeck I've tried this locally, the link and find seems to work.

I'll try doing this in CI with the help from https://github.com/jlumbroso/free-disk-space .

Utensil Song (Oct 07 2023 at 04:38):

doc-gen4 seems to be smart enough to pick up all declarations generated by previous lake Whatever:docs runs under build/doc/declarations, index them into one declaration-data.bmp (~32MB with mathlib etc.), not only the last run. That's why find works in this case. Related source code: htmlOutputIndex in DocGen4.Output. So no tweak required at all.

Utensil Song (Oct 07 2023 at 06:17):

It takes 1h19m to run lake build Mathlib:docs Whatever:docs in CI, barely acceptable. For now, it can be accelerated by caching Mathlib docs for the commit. But indeed we need a way to only build the doc for the part that is used.

Utensil Song (Oct 07 2023 at 08:22):

My 1h35m CI failed with:

  /usr/bin/git push origin gh-pages
  remote: error: Trace: bdbeb905b93ebbfade683a8bd626cf4d052ac40891b9622c6f33a00dcb598006
  remote: error: See https://gh.io/lfs for more information.
  remote: error: File doc/declarations/header-data.bmp is 449.71 MB; this exceeds GitHub's file size limit of 100.00 MB
  remote: error: GH001: Large files detected. You may want to try Git Large File Storage - https://git-lfs.github.com.
  To https://github.com/utensil/LeanBlueprintExample.git
   ! [remote rejected] gh-pages -> gh-pages (pre-receive hook declined)
  error: failed to push some refs to 'https://github.com/utensil/LeanBlueprintExample.git'
  Error: Action failed with "The process '/usr/bin/git' failed with exit code 1"

so using gh-pages is probably no longer a good idea, should use actions/deploy-pages directly instead.

Utensil Song (Oct 07 2023 at 13:26):

I've hacked doc-gen4 locally, it seems that I only need to bypass the following lines in DocGen4.Process.process:

    if !relevantModules.contains moduleName then
      continue

and change it to:

    if !relevantModules.contains moduleName && !moduleName.toString.startsWith "Mathlib" then
      -- println! "Skipping {name} because it is not in the relevant modules"
      continue

then I can generate the part of Mathlib that this package has actually imported by Whatever when running lake build Whatever:docs. This can reduce the document size and build time significantly (before: 487M, after: 223M, for minimal example that imported Mathlib.Tactic which is already a big import).

Utensil Song (Oct 07 2023 at 13:38):

@Henrik Böving As it's technically feasible, is it desired for doc-gen4 to generate imported part of Mathlib for a math project (with an addtional flag)?

IMHO, a math project is better to host the exact version of Mathlib it uses, but only the part it uses instead of the whole Mathlib which might contain totally unrelated math branches. I estimate this should be able to reduce the size/build time to 1/3 or less, as a math project is likely only depend on that much of human math.

Henrik Böving (Oct 07 2023 at 13:52):

Utensil Song said:

doc-gen4 seems to be smart enough to pick up all declarations generated by previous lake Whatever:docs runs under build/doc/declarations, index them into one declaration-data.bmp (~32MB with mathlib etc.), not only the last run. That's why find works in this case. Related source code: htmlOutputIndex in DocGen4.Output. So no tweak required at all.

This is phenomenon is a combination of lake knowing when to build what and doc-gen just using the stuff that is already there without thinking, doc-gen itself is not actually aware of the fact what is going on, it is merely instructed by lake to generate documentation for this and that module if lake deems that necessary.

Utensil Song said:

My 1h35m CI failed with:

  /usr/bin/git push origin gh-pages
  remote: error: Trace: bdbeb905b93ebbfade683a8bd626cf4d052ac40891b9622c6f33a00dcb598006
  remote: error: See https://gh.io/lfs for more information.
  remote: error: File doc/declarations/header-data.bmp is 449.71 MB; this exceeds GitHub's file size limit of 100.00 MB
  remote: error: GH001: Large files detected. You may want to try Git Large File Storage - https://git-lfs.github.com.
  To https://github.com/utensil/LeanBlueprintExample.git
   ! [remote rejected] gh-pages -> gh-pages (pre-receive hook declined)
  error: failed to push some refs to 'https://github.com/utensil/LeanBlueprintExample.git'
  Error: Action failed with "The process '/usr/bin/git' failed with exit code 1"

so using gh-pages is probably no longer a good idea, should use actions/deploy-pages directly instead.

These issues are solved in the mathlib4_docs repo

Utensil Song said:

Henrik Böving As it's technically feasible, is it desired for doc-gen4 to generate imported part of Mathlib for a math project (with an addtional flag)?

IMHO, a math project is better to host the exact version of Mathlib it uses, but only the part it uses instead of the whole Mathlib which might contain totally unrelated math branches. I estimate this should be able to reduce the size/build time to 1/3 or less, as a math project is likely only depend on that much of human math.

Right now doc-gen is simply instructed by lake on what modules to build docs for and just does that. It is not intended for a doc-gen task for one module to build documentation for others due to two reasons:
a) races with other lake tasks. Say you give lake two things that rely on some shared files in mathlib and use this discovery mechanism. You end up doing the same documentation computation twice for no reason.
b) this reduces parallelism drastically (this was the main motivator to use lake instead of orchestrating the build process on its own in this "dynamically discover what to do fashion" which was the previous implementation)
Regarding the parallelism, if you check the mathlib4_docs actions you will see that due to the large amount of cores that we have on these machines generating documentation for mathlib4 + all of its dependencies + core is a thing of just 20 minutes. If we fall back to this discovering mechanism we would in fact end up having worse run time compared to the current mechanism the larger of a mathlib fragment you depend on.

Which is not to say that the idea of only building the stuff you need is necessarily invalid, but it should not be part of doc-gen itself to decide on what to build in order to keep making use of maximum parallelism.

Henrik Böving (Oct 07 2023 at 13:56):

Oh and another comment/idea, the Mathlib import graph always seemed very densely connected to me from the pictures but you only did a benchmark using Mathlib.Tactic which is a mostly self contained meta programming part. How big are the savings that you get through this mechanism if you actually try to look at the transitive closure of some files that a mathematics interested consumer would import? So for example besides Mathlib.Tactic also import some important group theory/analysis/graph theory w/e

Utensil Song (Oct 07 2023 at 14:26):

These issues are solved in the mathlib4_docs repo

Thanks, I'll check out mathlib4_docs's solution. Previously I thought these are just issues that can be mitigated, the crucial issue is to figure out the imported part so I went straight looking for a solution to do so. As I guess that the relevant code (to find the locations of all imported declarations) is already in doc-gen4, so porting the old decls from mathlibtools would not make sense, I went straight to the doc-gen4 source.

It is not intended for a doc-gen task for one module to build documentation for others due to two reasons

Thanks for the explanations, I understand these two reasons, and they make perfect sense for Mathlib itself, but for projects of small to medium size that depends on Mathlib, they are very irrelevant:

  • issue a is less a problem due to the significantly lower complexities
  • issue b: these project will have to use a low core free Github Actions runner, but can't afford a long CI runtime (of course this can be mitigated by running the Mathlib build nightly then cache the result, and the project only bumps to cached mathlib docs, so push/pr CI of the project itself can have a short run time); also there are simple technical solutions to increase parallelism or avoid duplications on the end of doc-gen4

That said, as now the design decision has already been made to move these responsibilities to lake, and it's more efficient for Mathlib this way, I can see that it's not desired to go back to the "discover" design for doc-gen4, nor adding a flag to do so. For now I'll choose to only mitigate the CI run time issue.

Utensil Song (Oct 07 2023 at 14:32):

How big are the savings that you get through this mechanism if you actually try to look at the transitive closure of some files that a mathematics interested consumer would import? So for example besides Mathlib.Tactic also import some important group theory/analysis/graph theory w/e

I assume more saving for a normal math project that use exact import for what it wants, as I know tactics imports quite some group theory/analysis/graph theory etc. I was trying @Chris Birkbeck 's https://github.com/CBirkbeck/ModularForms_Lean4/, but it's only partly ported to Lean 4, so I don't have an actual figure yet.

If we push this thought experiment further, when Lean has solved its transitive import issues ( A -> B.b1 -> C.c1 but Lean pulls all of A, B, C), this could be a much significant saving, compared to parallelism savings which, I might argue, are only time savings not computation power savings.

Chris Birkbeck (Oct 07 2023 at 14:47):

Utensil Song said:

Chris Birkbeck I've tried this locally, the link and find seems to work.

I'll try doing this in CI with the help from https://github.com/jlumbroso/free-disk-space .

Ok nice, I'll try this locally as well then.

Chris Birkbeck (Oct 07 2023 at 14:49):

I think the stuff in https://github.com/CBirkbeck/ModularForms_Lean4/ is all in ported to lean 4, but has some new stuff in progress that need doing before starting to PRing. Maybe looking at the FTL regular repo here might be more useful (there is a mathlib 4 branch containing the ported files)

Utensil Song (Oct 07 2023 at 14:51):

These issues are solved in the mathlib4_docs repo

The solution at https://github.com/leanprover-community/mathlib4_docs/blob/main/.github/workflows/docs.yaml is an easy fix for the bmp file size issue, but the build time is only solved with more powerful runner :joy:

Utensil Song (Oct 07 2023 at 14:55):

Chris Birkbeck said:

I think the stuff in https://github.com/CBirkbeck/ModularForms_Lean4/ is all in ported to lean 4, but some I have some new stuff in progress that need doing before starting to PRing. Maybe looking at the FTL regular repo here might be more useful (there is a mathlib 4 branch containing the ported files)

It seems that things under Modformsported/ForMathlib/EisensteinSeries are not ported yet.

Chris Birkbeck (Oct 07 2023 at 14:58):

Hmm ok maybe I'm not sure what you mean by ported. All the code is in lean 4 right? but it has some things in progress which still have (or should have!) sorries

Chris Birkbeck (Oct 07 2023 at 14:59):

In any case, the FLT repo is more stable at the moment, if that helps :)

Utensil Song (Oct 07 2023 at 15:15):

Thanks, I'll check FLT instead for now.

Henrik Böving (Oct 07 2023 at 15:23):

Utensil Song said:

These issues are solved in the mathlib4_docs repo

Thanks, I'll check out mathlib4_docs's solution. Previously I thought these are just issues that can be mitigated, the crucial issue is to figure out the imported part so I went straight looking for a solution to do so. As I guess that the relevant code (to find the locations of all imported declarations) is already in doc-gen4, so porting the old decls from mathlibtools would not make sense, I went straight to the doc-gen4 source.

It is not intended for a doc-gen task for one module to build documentation for others due to two reasons

Thanks for the explanations, I understand these two reasons, and they make perfect sense for Mathlib itself, but for projects of small to medium size that depends on Mathlib, they are very irrelevant:

  • issue a is less a problem due to the significantly lower complexities
  • issue b: these project will have to use a low core free Github Actions runner, but can't afford a long CI runtime (of course this can be mitigated by running the Mathlib build nightly then cache the result, and the project only bumps to cached mathlib docs, so push/pr CI of the project itself can have a short run time); also there are simple technical solutions to increase parallelism or avoid duplications on the end of doc-gen4

That said, as now the design decision has already been made to move these responsibilities to lake, and it's more efficient for Mathlib this way, I can see that it's not desired to go back to the "discover" design for doc-gen4, nor adding a flag to do so. For now I'll choose to only mitigate the CI run time issue.

I would hope that we can teach the facet that doc-gen uses to build things (refer to doc-gens lakefile.lean for the implementation) about this "only build the stuff you need feature" somehow. My basic idea here would be like this: If we are in the module_facet of some module somehow get access to the dependency tree of our current module and request the doc facet to be built for all the imported modules in addition as well. This would effectively mimic the "discover" approach without the drawbacks that it has when doing this directly in doc-gen. But my lake-facet-fu is not sufficient to implement this. @Mac Malone is what I am dreaming up here possible?

Utensil Song (Oct 07 2023 at 16:12):

That seems reasonable, doc-gen4 do the lite discovering, lake orchestrates the heavy lifting.

Notification Bot (Oct 07 2023 at 17:19):

A message was moved from this topic to #new members > Help declaring Huntington postulates by Mario Carneiro.

Mac Malone (Oct 07 2023 at 17:21):

Henrik Böving said:

My basic idea here would be like this: If we are in the module_facet of some module somehow get access to the dependency tree of our current module and request the doc facet to be built for all the imported modules in addition as well. This would effectively mimic the "discover" approach without the drawbacks that it has when doing this directly in doc-gen. But my lake-facet-fu is not sufficient to implement this. Mac Malone is what I am dreaming up here possible?

Yes! After all, Lake needs to do this to a build a module's dependency tree in the first place. :smile: The mod.imports.fetch will provide the ordered set of imports of the module (as an Array). You can then loop through these and call fetch <| mod.facet `docs to recursively generate the docs of the dependency tree.

Henrik Böving (Oct 07 2023 at 18:58):

@Mac Malone do I also get imports like Init and Lean in this thing? Or do I need to keep this job that always build the compiler documentation extra and is pulled in by every module job? My result so far indicate the latter.

Henrik Böving (Oct 07 2023 at 19:13):

@Utensil Song https://github.com/leanprover/doc-gen4/commit/fa8c9d771aa6a06e25468c92b049fecc3e482b99 When running lake build DocGen4:docs this also generates docs for all of the doc-gen4 deps, does it work for you as well?

Mac Malone (Oct 07 2023 at 19:16):

Henrik Böving said:

Mac Malone do I also get imports like Init and Lean in this thing? Or do I need to keep this job that always build the compiler documentation extra and is pulled in by every module job? My result so far indicate the latter.

You are correct. Init and Lean are will note be caught by this because they are not proper modules in Lake.

Utensil Song (Oct 08 2023 at 01:52):

@Henrik Böving @Mac Malone Amazing ! Thank you both, I'm giving it a try now.

Utensil Song (Oct 08 2023 at 04:39):

Cool, now doc build time is significantly reduced: 1h19m ⇒ 28m for LeanBlueprintExample only importing Mathlib.Tactic, and 1h12m ⇒ 37m for FltRegular with actual mathematically interesting imports.

Utensil Song (Oct 08 2023 at 04:47):

@Chris Birkbeck You can directly use my adjusted code at the PR here

Utensil Song (Oct 08 2023 at 04:49):

Or is the reduced build time partially caused by https://github.com/leanprover/doc-gen4/commit/fa8c9d771aa6a06e25468c92b049fecc3e482b99#r129427912 ?

Mac Malone (Oct 08 2023 at 06:22):

@Utensil Song I am not exactly sure what happens to jobs that are not waited on. I think they may be killed when Lake terminates but I am not certain. One way to check if that is the causes is to look through the generated docs and see if anything is missing / partially complete.

Utensil Song (Oct 08 2023 at 06:50):

I sample-walkthrough https://utensil.github.io/LeanBlueprintExample/doc//Mathlib/Tactic/Ring.html (EDIT: and https://utensil.github.io/FltRegulartest/doc/FltRegular/FltRegular.html ) and their imports, seems not missing anything. So maybe it's not terminated prematurely.

But when I check https://utensil.github.io/FltRegulartest/blueprint/ and https://utensil.github.io/FltRegulartest/doc/ , mathlib doc is not there, I'm still investigating why. It uses exactly the same approach.(EDIT: because \dochome is still pointing to cbirkbeck's pages)

Utensil Song (Oct 08 2023 at 07:04):

@Henrik Böving I wonder if doc for theorems can be improved, showing Prop is not really helpful:

image.png

Is it possible to show the Lean statement for the Prop? It's quite readable:

image.png

Utensil Song (Oct 08 2023 at 07:36):

Weird, other theorems seem to be doing fine:

image.png

just not Fermat's last theorem :joy:

Utensil Song (Oct 08 2023 at 07:38):

Oh, I see, it has special treatment for theorems, but not theorems defined by def.

Yaël Dillies (Oct 08 2023 at 07:40):

Yeah, it's not a theorem, it's a def. We used to be able to expand the definition of a def in the docs. But now we can't. It's a shame.

Ruben Van de Velde (Oct 08 2023 at 07:52):

Has anyone filed an issue about that?

Utensil Song (Oct 08 2023 at 08:03):

No, I searched issues with def, theorem, Prop, no result. Filing one.

Utensil Song (Oct 08 2023 at 08:04):

I think it's fixable by adding a branch for DocGen4.Process.DocInfo.ofConstant or DocGen4.Process.DefinitionInfo.ofDefinitionVal.

Utensil Song (Oct 08 2023 at 08:35):

https://github.com/leanprover/doc-gen4/issues/155

Henrik Böving (Oct 08 2023 at 09:38):

Yaël Dillies said:

Yeah, it's not a theorem, it's a def. We used to be able to expand the definition of a def in the docs. But now we can't. It's a shame.

I had gotten rid of the feature to just expand definitions because for the majority of definitions I looked at it just produces unreadable garbage. But I guess I just look at programming definitions too much :D Added it back

Henrik Böving (Oct 08 2023 at 09:40):

Mac Malone said:

Utensil Song I am not exactly sure what happens to jobs that are not waited on. I think they may be killed when Lake terminates but I am not certain. One way to check if that is the causes is to look through the generated docs and see if anything is missing / partially complete.

And I fixed this but now I am a bit unsure. This does not accurately reflect the dependency graph anymore. If module A imports module B that does not mean I need to regenerate documentation for A if B changes, it only means I need to run the indexing again after I built B's doc...is there a way to reflect this as well?

Henrik Böving (Oct 08 2023 at 10:05):

Deployed on mathlib4_docs now again

Chris Birkbeck (Oct 08 2023 at 10:41):

Utensil Song said:

Chris Birkbeck You can directly use my adjusted code at the PR here

Ah amazing, thank you! I've merged the PR now and will wait to see what come out after the workflow runs :)

Utensil Song (Oct 08 2023 at 10:44):

Ah you need to wait a bit

Utensil Song (Oct 08 2023 at 10:45):

I need to update doc-gen4 in it again

Chris Birkbeck (Oct 08 2023 at 10:45):

Oh ok no worries :)

Utensil Song (Oct 08 2023 at 10:46):

to include the new fixes, particularly for the FLT def

Chris Birkbeck (Oct 08 2023 at 10:46):

I invited you to the repo in case that helps at all

Utensil Song (Oct 08 2023 at 10:49):

Re-PRed :handshake:

Utensil Song (Oct 08 2023 at 10:50):

You may want to cancel the previous workflow to wait on the one after this merge

Utensil Song (Oct 08 2023 at 12:00):

Oh, the proposition is now shown in Equations, is there a reason or a background? Like when would it have multiple equations?

Utensil Song (Oct 08 2023 at 12:01):

@Yaël Dillies Is this what you expected?

Utensil Song (Oct 08 2023 at 12:02):

D1BF4B48-A111-42DC-9DF6-A6C51BB00520.jpg

Yaël Dillies (Oct 08 2023 at 12:02):

Yes, why?

Yaël Dillies (Oct 08 2023 at 12:03):

It would have multiple equations if it were defined by pattern-matching, eg docs#List.length

Utensil Song (Oct 08 2023 at 12:03):

Ah yes

Utensil Song (Oct 08 2023 at 12:05):

I guess showing equations is indeed better than showing raw pattern matching, the rationale is less obvious for a single definition

Utensil Song (Oct 09 2023 at 02:34):

@Chris Birkbeck Hi, I merged my PR yesterday and the CI failed to deploy to Github Pages, the new workflow requires configuringthe settings, changing it from deploying from a branch gh-pages to deploy directly from the actions, the official guide is Publishing with a custom GitHub Actions workflow and I've updated the example README to reflect this.

Sorry I only checked the Pages build on my fork then went to work on other stuff and didn't realize this.

Henrik Böving (Oct 09 2023 at 07:42):

@Utensil Song I just pushed a doc-gen4 commit that pushes the doc-gen time from ~17min to ~9min on the mathlib4_docs runner, might wanna try your thing again^^

Chris Birkbeck (Oct 09 2023 at 08:06):

OK no problem, I updated the setting to deploy from actions.

Utensil Song (Oct 09 2023 at 08:11):

Henrik Böving said:

Utensil Song I just pushed a doc-gen4 commit that pushes the doc-gen time from ~17min to ~9min on the mathlib4_docs runner, might wanna try your thing again^^

Fantastic! I'll try it now.

Utensil Song (Oct 09 2023 at 08:17):

By the way, today I was trying to add --ink flag to the single command like the reverse modification of https://github.com/leanprover/doc-gen4/commit/9af4c720f08e9c694e574fc35cf59b385be47175 and I got the panic when running this command

[620/2525] Documenting module: Qq.ForLean.ReduceEval
LEAN_PATH=./lake-packages/std/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./lake-packages/Cli/build/lib:./lake-packages/proofwidgets/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/CMark/build/lib:./lake-packages/lean4-unicode-basic/build/lib:./lake-packages/leanInk/build/lib:./lake-packages/doc-gen4/build/lib:./build/lib:/Users/utensil/.elan/toolchains/leanprover--lean4---v4.2.0-rc1/lib/lean lldb ./lake-packages/doc-gen4/build/bin/doc-gen4 -- single Qq.ForLean.ReduceEval --ink
INTERNAL PANIC: out of memory

LLDB bt result

which seems quite innocent, is this similar to the weird panic you mentioned in the commit log?

Henrik Böving (Oct 09 2023 at 08:23):

No the panics were coming from LeanInk itself, I would not expect a panic to occur at this position

Utensil Song (Oct 09 2023 at 08:24):

OK, so this is something different, maybe only related to Mac M1, I'll try this on Ubuntu later.

Utensil Song (Oct 09 2023 at 08:25):

Blazing fast: 187.18s for a local doc build

Henrik Böving (Oct 09 2023 at 08:25):

I'm in general surprised that this would panic only wiht --ink as this code path should definitely not be influenced by the flag. Either way this code path is removed in the new version as it doesn't talk with lake anymore from within DocGen

Henrik Böving (Oct 09 2023 at 08:26):

Utensil Song said:

Blazing fast: 187.18s for a local doc build

what was the base line?

Utensil Song (Oct 09 2023 at 08:32):

Henrik Böving said:

I'm in general surprised that this would panic only wiht --ink as this code path should definitely not be influenced by the flag. Either way this code path is removed in the new version as it doesn't talk with lake anymore from within DocGen

I've just noticed that the same panic also appear in the old doc-gen4 normal build (i.e. w/o --ink), it just won't terminate the whole process and proceed to other modules.

Utensil Song (Oct 09 2023 at 08:32):

It looks like this

Utensil Song (Oct 09 2023 at 08:33):

and yes, I just read the code diff in the latest commit and the whole related code are gone

EDIT: The same error is still there for normal doc build without --ink.

Utensil Song (Oct 09 2023 at 08:34):

Henrik Böving said:

Utensil Song said:

Blazing fast: 187.18s for a local doc build

what was the base line?

380.59s for commit 402cfda104da78727a4ead99992abe638b8c14ef

Utensil Song (Oct 09 2023 at 08:53):

418.96s → 231.37s for a full lake -R -Kenv=dev build Mathlib:docs

Utensil Song (Oct 09 2023 at 09:15):

The PANIC issue is still there, but if I try to minimalize it to build docs for Qq as a standalone project, the PANIC is gone

quote4 % export LEAN_HOME=~/.elan/toolchains/leanprover--lean4---v4.2.0-rc1
ELAN_HOME=~/.elan ELAN_TOOLCHAIN=leanprover/lean4:v4.2.0-rc1 LAKE=$LEAN_HOME/bin/lake LAKE_HOME=$LEAN_HOME LEAN_SYSROOT=$LEAN_HOME LEAN_AR=$LEAN_HOME/bin/llvm-ar LEAN_CC= LEAN_PATH=./lake-packages/Cli/build/lib:./lake-packages/CMark/build/lib:./lake-packages/lean4-unicode-basic/build/lib:./lake-packages/leanInk/build/lib:./lake-packages/doc-gen4/build/lib:./build/lib:$LEAN_HOME/lib/lean LEAN_SRC_PATH=./lake-packages/Cli/./.:./lake-packages/CMark/./.:./lake-packages/lean4-unicode-basic/./.:./lake-packages/leanInk/./.:./lake-packages/doc-gen4/./.:././.:$LEAN_HOME/src/lean/lake DYLD_LIBRARY_PATH=./lake-packages/std/build/lib:./lake-packages/Cli/build/lib:./lake-packages/CMark/build/lib:./lake-packages/lean4-unicode-basic/build/lib:./lake-packages/leanInk/build/lib:./lake-packages/doc-gen4/build/lib:./build/lib:$LEAN_HOME/lib/lean:$LEAN_HOME/lib ./lake-packages/doc-gen4/build/bin/doc-gen4 single Qq.ForLean.ReduceEval https://github.com/gebner/quote4/blob/a387c0eb611857e2460cf97a8e861c944286e6b2//Qq/ForLean/ReduceEval.lean

It runs fine.

Chris Birkbeck (Oct 10 2023 at 09:43):

The github action seems to be breaking again, with the same error msg I had before System.IO.IOException: No space left on device... . I don't think I've changed anything in the action, all I did was add more maths to the latex file.

Chris Birkbeck (Oct 10 2023 at 09:46):

Did I maybe need to first run something locally?

Utensil Song (Oct 10 2023 at 13:46):

Weird, I'll check it now.

Utensil Song (Oct 10 2023 at 13:48):

I'm trying a new run here which will free disk space and install only texlive-latex-extra (ref )

Utensil Song (Oct 10 2023 at 18:23):

It's green now, PRed and merged.

Chris Birkbeck (Oct 11 2023 at 08:17):

Ok great! thank you :) what was the problem?

Utensil Song (Oct 11 2023 at 08:52):

The main source of problem is the full installation of TeXLive. I tried using a less large installation texlive-latex-extra (ref ) but it doesn't include xelatex. So I only mitigate the issue by deleting unnecessary stuff in the container images of a default Github runner with the help from https://github.com/jlumbroso/free-disk-space which I thought I did it for your repo but only my example repo.

Utensil Song (Oct 11 2023 at 09:00):

My personal blueprint CI uses less traditional TeX toolchain tectonic which is rewritten in Rust, and incrementally download what is needed during compiling a LaTeX document from TeXLive distribution.

It's much smaller and haven't failed me for compatibility yet, so I'm free of this disk space issue. You can check the bp task in my task.py here and its setup in CI here.

Utensil Song (Oct 11 2023 at 09:03):

Another way to avoid this is to use your old method, run xu-cheng/texlive-action/full@v1 which doesn't occupy your disk space, but the downside is to use apk instead of apt to install dependencies. Although I have done this before, I was too lazy and less motivated to use it (and fix potential compatibilitiy issues) when I made the example.

Utensil Song (Oct 11 2023 at 09:16):

Although depending on doc-gen4 minimized the implementation of blueprint, and it becomes more loosely couple to Lean (You may ask: why would some one want blueprint to be loosely coupled with Lean? Because it's indeed a good fit for formalization, even for pen-and-paper, that's why there was a noleanblueprint), and I'm comfortable with the solution, I still wish to parse Lean 4 and provide information to blueprint (although optionally this time), the main gain would be directly list the related Lean code in the blueprint.

But there are quite some issues (e.g. evaluate if it's a good idea, what the code should look like, is it like the expaned version of doc-gen4? How to pull in the depended code? How to handle line-by-line comments inside the proof? Is @Patrick Massot 's informal Lean project coming out recently? ) to address before this, so this would come later on my TODO list.

Chris Birkbeck (Oct 11 2023 at 09:35):

Aha I see, thank you for the explanation and for getting it working again!

Patrick Massot (Oct 11 2023 at 12:45):

Informal Lean isn't really making progress currently. We are too busy with other things. I know I also need to find time for the blueprint thing. But days aren't long enough.

Utensil Song (Oct 11 2023 at 12:54):

How would you imagine the blueprint for Lean 4 if you have time to work on it?

Patrick Massot (Oct 11 2023 at 13:13):

The first target is to uncouple Lean and the graph generating stuff as much as possible. Then there is a bit of Lean meta-programming to do to get access to file position information for all declaration and then the python part must be adjusted.

Utensil Song (Oct 11 2023 at 13:30):

I thought graph generating stuff doesn't depend on lean now. As for the Lean meta-programming code decls, similar code exists in doc-gen4, I hesitate to make a less maintained duplicate without additional gain.

Ramon Fernández Mir (Oct 12 2023 at 15:32):

Utensil Song said:

It looks like this


Did you manage to fix this? I'm getting the exact same error when I run this locally to generate docs for a project that depends on mathlib.

Utensil Song (Oct 12 2023 at 15:42):

For now, it does not interfere with normal doc gen without --ink, just a log, and failure to generate it for Qq.ForLean.ReduceEval so I haven't look into it yet.

Utensil Song (Oct 15 2023 at 05:19):

The coverage report seems to be broken, it's not linked from home, and the generated html doesn't render properly, this can be confirmed for:

The best rendered ones are

Will look into it later.

Patrick Massot (Oct 15 2023 at 14:02):

Indeed I saw very early that this tool wasn't used, people used the graph directly. So I removed the link and then forgot to update the corresponding code when other things changed. The result is this became broken dead code that should be removed.

Yaël Dillies (Oct 15 2023 at 15:09):

In fact, @Sky Wilshaw reimplemented something akin to your coverage for Con(NF).

Sky Wilshaw (Oct 15 2023 at 15:13):

I don't think I remember doing anything like this - I did implement a dynamic sorry counter with markdown and GH actions.

Yaël Dillies (Oct 15 2023 at 15:15):

The dynamic sorry counter is what I meant.

Bhavik Mehta (Oct 15 2023 at 20:24):

Utensil Song said:

The coverage report seems to be broken, it's not linked from home, and the generated html doesn't render properly, this can be confirmed for:

The best rendered ones are

Will look into it later.

I'll be honest, I had no idea that the coverage page existed for unit-fractions! The only reason it works is because I copied the setup from sphere-eversion

Yaël Dillies (Oct 22 2023 at 18:24):

@Utensil Song, what's the status of the Lean 4 blueprint? Is it usable now?

Utensil Song (Oct 22 2023 at 18:41):

Yaël Dillies said:

Utensil Song, what's the status of the Lean 4 blueprint? Is it usable now?

It's usable to the extent that

As the implementation is so simple, having consistent behaviors with its Lean 3 version, and mostly relying on doc-gen4, I think it will be future-proof to use it. If you run into any issue, I'm happy to assist.

Yaël Dillies (Oct 22 2023 at 18:46):

I think the problem here is that LeanAPAP contains a lot of tweaks to the CI which I don't want to just throw away.

Yaël Dillies (Oct 22 2023 at 18:49):

I'm out of Lean time for today but here's the repo if you want to try it out (and open a PR fixing my beautiful blueprint please :pray:): https://github.com/YaelDillies/LeanAPAP

Utensil Song (Oct 22 2023 at 18:50):

You don't need to throw away those CI tweaks to use it, just need to incorporate something from the example CI.

Yaël Dillies (Oct 22 2023 at 18:51):

Yes precisely. But it's not obvious to me what I should incorporate and what I should throw away. You will know, however.

Utensil Song (Oct 22 2023 at 18:53):

OK, I'll give it a try tomorrow.

Utensil Song (Oct 23 2023 at 01:06):

https://github.com/YaelDillies/LeanAPAP/compare/master...utensil:LeanAPAP:master

It's pretty much what needs to be incorporated.

I'm testing this on my Pages, but the build failed due to an undefined \C in LaTeX, I believe it means \mathbb {C} but not found in blueprint/src/macros_common.tex etc.

Here is the build log. Now I'm testing locally.

UPDATE: got past the LaTeX compilation, new error building jekyll: missing sorries.md. I added an ad hoc fix, CI running.

UPDATE: CI passed, but published to wrong directory due to subtle reasons. Fixed, CI running.

Utensil Song (Oct 23 2023 at 10:07):

@Yaël Dillies CI passed and blueprint and doc are published to https://utensil.github.io/LeanAPAP/.

Links to Blueprint or Documentation are working, and jumping from blueprint/depgragh to doc is also working (for theorems, because their names are all in lower case, unchanged from Lean 3 to Lean 4).

Please let me know if you have observed any issues. :smiley:

( P.S. Starting from tomorrow, I have a 5-day trip involving hiking in a desert, so it's likely that I can only work on it when I'm back.)

Utensil Song (Oct 23 2023 at 10:12):

CI takes around 26min because I have cached the Mathlib doc. If you change lake-manifest.json, CI would be much longer ( + 15min ) .

Utensil Song (Oct 23 2023 at 10:34):

More info in YaelDillies/LeanAPAP#2 , let's continue discussions there.

Last updated: Dec 20 2023 at 11:08 UTC