Lean companion to "Analysis I" - discussion

Stream: Analysis I

[Terence Tao]

I'm starting this thread for any feedback to a Lean companion to my textbook "Analysis I" that I just announced. (I also have a separate announcement on my blog.)

[Shreyas Srinivas]

Incidentally I was trying to do exactly this last year. Of course the issue is that technically the book uses set theory and spends a chapter developing those axioms and I got stuck on that

[Shreyas Srinivas]

Basically those sets in chapter 3 don’t need an interpretation as objects of a specific type

[Shreyas Srinivas]

Also, setting up Nat using an axiomatic structure meant foregoing all the tactics machinery around inductive types

[Terence Tao]

That took a while for me to figure out how to resolve! You can see my solution to that problem at https://github.com/teorth/estimate_tools/blob/d5839de68ffed426cdf702e7053396282fbf5553/EstimateTools/analysis/Section_3_1.lean . I created two bare-bones structures Set and Object, and bundled all the set theory axioms and other data relating these structures in a class SetTheory which I then created an instance of as a variable. This allowed me to then state the various set theory axioms as basic lemmas, which I then used to develop the rest of the theory. (This limits the set theory to only be able to handle these two specific structures Set and Object; if one wanted to extend the theory later, one should adopt a more polymorphic approach, but I decided instead to just use the Mathlib theory of sets going forward (sacrificing self-containedness of the text in favor of Mathlib compatibility).)

[Terence Tao]

Yes, the text deliberately forgoes the ability to use some powerful tactics and Mathlib lemmas initially, in order to force the student to prove certain things "by hand". But I believe it is still doable (I haven't actually done all the exercises though, just formalized their statement in Lean, so I am hoping that there will be some volunteers to "playtest" whether the exercises can in fact be established using the API provided without too much unnecessary pain).

[Shreyas Srinivas]

I am actually curious to find out how well the epsilon delta definitions work from scratch when one defines limits and continuity. Separately, is it ergonomic to define Riemann integrals?

[Terence Tao]

I'm several chapters away from being able to answer these questions :grinning:

[Eric Wieser]

Terence Tao said:

You can see my solution to that problem at https://github.com/teorth/estimate_tools/blob/d5839de68ffed426cdf702e7053396282fbf5553/EstimateTools/analysis/Section_3_1.lean .

I worry that this gets you into trouble since it forces your sets and objects to have the same cardinality. Is this problematic, or fine?

[Terence Tao]

If one was studying the model theory of ZFC this could eventually be a problem, but for the purposes of this Analysis text I doubt that this will be an issue. I think I could make things more polymorphic by having an extendible class for Set and Object (and then make SetTheory take those extended classes as parameters) but my choice here was guided by pedagogical considerations rather than generalizability; after this chapter I plan to switch over to Mathlib's Set types anyway, so there is no point developing the Chapter3.Set classes further once one reaches the end of that chapter. (Well, in Analysis II I do have a chapter discussing the axiom of choice that might revisit the Chapter3.Set structure, at which point I might wish to make things more polymorphic to make a distinction between set theory with choice and set theory without choice, but I will cross that bridge when I come to it.)

[Kevin Buzzard]

Why don't you put the work in a new repo? I think it's kind of strange that it's living in an existing one about something else. It's as simple as lake new AnalysisOne math, creating a new github repo, following the instructions on github for uploading a repo on your computer and then moving the files over, right? My instinct is that the current approach makes bumping twice as hard, for example.

[Kyle Miller]

Regarding epsilon/delta limits, in Patrick Massot's Lean tutorials about basic analysis, he defines the sequential limit and infinite sequential limit both directly. Then for example when the Bolzano-Weierstrass theorem is needed, he hooks the definition into the mathlib definitions easily enough to prove it.

[Kenny Lau]

I'm a little bit confused here, since in the version of ZFC that I am familiar with, objects and sets are not distinguished. (not that this would really affect anything)

[Terence Tao]

Kevin Buzzard said:

Why don't you put the work in a new repo? I think it's kind of strange that it's living in an existing one about something else. It's as simple as lake new AnalysisOne math, creating a new github repo, following the instructions on github for uploading a repo on your computer and then moving the files over, right? My instinct is that the current approach makes bumping twice as hard, for example.

Yeah, I should go and do that before the project gets too big. It's mostly laziness on my part, there's also the autogeneration of docs, blueprint, etc. that I didn't have time to get around to, but I guess I should go ahead and do that now.

[Kevin Buzzard]

I agree that blueprint makes it harder! I am not sure I would be able to confidently say "just do this" for a blueprint. Is the plan to have a blueprint? I thought you already wrote the book once!

[Terence Tao]

Kenny Lau said:

I'm a little bit confused here, since in the version of ZFC that I am familiar with, objects and sets are not distinguished. (not that this would really affect anything)

My text made the conscious choice to use ZFC with atoms, so that I didn't have to deal with the issue that (say) natural numbers are technically required to be sets in pure ZFC, which is conceptually confusing and also not really compatible with Mathlib's implementation of set theory.

[Terence Tao]

I don't plan to have a blueprint, but the only way I know how to automatically set up document generation is to run the blueprint script, so the project would then come with a placeholder blueprint. I don't own the copyright to the text outright, so unfortunately I can't just splat the textbook contents onto the blueprint, but hopefully the existing published text will suffice (I have an online copy of the first few chapters that can be downloaded for free, for instance.)

[Kyle Miller]

Maybe a way to address Eric's concern is

class SetTheory where
  Set : Type
  Object : Type
  set_to_object : Set ↪ Object
  [... the rest ...]

export SetTheory (Set Object)

and then when you define functions on Set, you write

abbrev SetTheory.Set.toObject (X:Set) : Object := X

instead of

abbrev Set.toObject (X:Set) : Object := X

The only other change seems to be that later the CoeSort instance would have Type rather than Type 1.

[Eric Wieser]

My concern with the original was more of there 'is there something contradictory / undecidable hiding here because the type of sets is too big", rather than worrying about it being too restrictive

[Kyle Miller]

Yeah, the goal here is to avoid the (potential) contradiction by avoiding saying exactly what the definitions of Set and Object are.

[Eric Wieser]

Yes, your version is certainly correct. I'm curious if my hunch is correct about the original, and if you really can derive False

[Terence Tao]

@Kyle Miller 's proposal is promising. I'll first work on migrating the companion to a separate repository and then test out the proposal. I didn't know about the export keyword - it seems to allow for the best of both worlds, providing a clean interface for students to start working on exercises without having to deal with the finer points of polymorphic instances etc., while also giving the flexibility to avoid contradictions and also allow for possible future extensions such as adding choice.

(I initially had Set and Object as purely empty structures, but then realized that then all objects were equal to each other under that implementation, hence the introduction of a dummy data attribute. But this solution is better.)

[Shreyas Srinivas]

You could actually experiment with verso here

[Shreyas Srinivas]

It allows for interesting write ups with text and lean code mixed in. Further you can interact with the lean code and see proof states for example.

[Terence Tao]

Hmm I have not worked with this platform before. If someone would volunteer to help set it up, I could migrate there instead of to a "standard" Github lean formalization repository.

[Shreyas Srinivas]

I haven’t done it before. I could give it a shot. I have been looking for an excuse to learn verso

[Terence Tao]

OK in that case I will keep working on making a separate Github repo but allow for the possibility of transitioning to a Verso repository if we can get to the point of that working well.

[Shreyas Srinivas]

I should also mention that verso has a small learning curve

[Terence Tao]

OK, the project is now migrated to its own repository: https://github.com/teorth/analysis

It appears to have passed CI on the repo, though I am currently experiencing a local issue due to not being able to install ProofWidgets, but I am currently trying (with LLM assistance) to work through that. In the meantime I will update links to point to this new repository.

[Kevin Buzzard]

I think the proofwidgets issue might be a current or recent problem with the set-up, it might be worth just searching this zulip for the error

[Terence Tao]

I'm seeing other people report the same issue, but so far none of the fixes are working. Time to try rm -rf .lake...

PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> npm -v
10.9.2
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake clean
error: permission denied (error code: 13)
  file: C:\Users\teort\OneDrive\Documents\GitHub\analysis\.lake\build\ir\Analysis
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake build
⚠ [689/937] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✖ [690/937] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake exe cache get
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1

[Justin Asher]

If you do not need the latest Mathlib declarations, you can try just using the stable versions of everything. For instance, here is what I had to do for LeanExplore (I deleted some irrelevant packages, for simplicity):

Example Imports

-- Require Batteries (a general-purpose utility library)
require batteries from git
  "https://github.com/leanprover-community/batteries" @ "v4.19.0"

-- Require ImportGraph (transitive dep, now made direct to override version)
require importGraph from git
  "https://github.com/leanprover-community/import-graph" @ "v4.19.0"

-- Require Mathlib (the comprehensive library of mathematics in Lean)
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.19.0"

-- Require Plausible (transitive dep, now made direct to override version)
require plausible from git
  "https://github.com/leanprover-community/plausible.git" @ "v4.19.0"

-- Require ProofWidgets4 (for interactive proof widgets)
require proofwidgets from git
  "https://github.com/leanprover-community/ProofWidgets4.git" @ "v0.0.57"

-- Require quote4 (transitive dep, now made direct to override version)
require Qq from git
  "https://github.com/leanprover-community/quote4" @ "v4.19.0"

[Terence Tao]

Do you know if the sorts of issues I am experiencing will likely also occur to anyone else downloading the repository (which is still passing CI, even if I can't get it to run currently locally), or if it is purely a problem at my end? If it is the latter then I would rather leave the lean files untouched while I work on a solution locally (although nuking .lake unfortunately did not work...)

[Justin Asher]

I presume the problem is because your Lean toolchain file says leanprover/lean4:v4.20.0-rc5, indicating that your project is trying to compile with the latest (unstable) version of Lean, while some imports (like ProofWidgets) have the latest commit being v4.20.0-rc2 (you can see this here). When you import Mathlib without fixing a version, it tries to use the latest version (i.e., v4.20.0-rc5), whereas other packages are not as well maintained.

I highly doubt this is a problem on your end of things. I would try fixing the versions of the packages that you want to use, and then create a clear commit message whenever you bump to a newer version of the imported packages. This also makes your code more reproducible, so that it should not cause any issues when it is run on anyone else's machine.

[Matt Diamond]

I created two bare-bones structures Set and Object

just wanted to note that opaque could've worked here (i.e. opaque Set : Type and opaque Object : Type) though I assume Kyle's suggestion (adding the types as fields on the class) is better

[Terence Tao]

From what you describe it sounds like the simplest solution would be to downgrade Lean to v4.20.0-rc2 for now and figure out how to bump later. EDIT: okay, this is basically what you are suggesting. I will try (with some LLM assistance) to implement this and see if it fixes things.

[Terence Tao]

Grr, even with all these pinned versions and the toolchain set to leanprover/lean4:v4.19.0 I am still getting the same error. Frustrating...

[Terence Tao]

The Lean Installation Game is significantly less fun to play than the Natural Number Game

[Julian Berman]

I'm trying to clone and build locally to see whether it reproduces -- but from the original error message it seems like something there is saying "passing -v might help see what the problem is". I know sometimes it's not clear which thing is the thing that wants -v passed because it can come from some arbitrarily lower down layer but hopefully it's lake build and cache? Can you try lake build -v and/or lake exe cache get -v?

[Justin Asher]

Try this:

Lakefile

import Lake
open Lake DSL

package «analysis» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- add any additional package configuration options here

-- Require Batteries (a general-purpose utility library)
require batteries from git
  "https://github.com/leanprover-community/batteries" @ "v4.19.0"

-- Require ImportGraph (transitive dep, now made direct to override version)
require importGraph from git
  "https://github.com/leanprover-community/import-graph" @ "v4.19.0"

-- Require Mathlib (the comprehensive library of mathematics in Lean)
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.19.0"

-- Require Plausible (transitive dep, now made direct to override version)
require plausible from git
  "https://github.com/leanprover-community/plausible.git" @ "v4.19.0"

-- Require ProofWidgets4 (for interactive proof widgets)
require proofwidgets from git
  "https://github.com/leanprover-community/ProofWidgets4.git" @ "v0.0.57"

-- Require quote4 (transitive dep, now made direct to override version)
require Qq from git
  "https://github.com/leanprover-community/quote4" @ "v4.19.0"

-- Require doc-gen4
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "v4.19.0"

@[default_target]
lean_lib «Analysis» where
  -- add any library configuration options here

meta if get_config? env = some "dev" then
-- Require checkdecls
require checkdecls from git
  "https://github.com/PatrickMassot/checkdecls.git"

[Justin Asher]

You probably do not need all the imports I just posted, but you need to fix the doc-gen4 import:

require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "v4.19.0"

When I did not, it kept trying to bump my toolchain to v4.20.0-rc5.

[Justin Asher]

When I ran lake update and then lake build on my local machine, everything worked (lots of sorrys!).

[Justin Asher]

It looks like doc-gen4 supports more recent versions if you want to try, for instance, setting all of your imports to v4.20.0-rc2:
https://github.com/leanprover/doc-gen4/tags

[Justin Asher]

Albeit, this may break the proofwidgets import...good luck!

[Julian Berman]

(I think FWIW that ProofWidgets didn't get releases for 4.20.0-rc5, but still works fine with it and is expected to -- or at least I noticed this when writing CI for another project that lean-toolchain in ProofWidgets had 4.20.0-rc2 but then it's clear Mathlib4 which uses rc5 is using ProofWidgets regardless.)

[Terence Tao]

Will try your fix now. At this point I'd be content to freeze the dependencies at a stable working version; there's nothing in this project that I envisage being upstreamed to anything else so bumping seems like nontrivial effort for negligible gain to me.

[Terence Tao]

Ugh, still having problems. Is your fix something that you can PR to the repository that I can download? Or is that not how lake works?

PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake update -v
trace: analysis: updating 'checkdecls' with {}
trace: .\.\.lake\packages\checkdecls> git fetch --tags --force origin
trace: analysis: updating 'Qq' with {}
trace: .\.\.lake\packages\Qq> git fetch --tags --force origin
trace: analysis: updating 'proofwidgets' with {}
trace: .\.\.lake\packages\proofwidgets> git fetch --tags --force origin
trace: analysis: updating 'plausible' with {}
trace: .\.\.lake\packages\plausible> git fetch --tags --force origin
trace: analysis: updating 'mathlib' with {}
trace: .\.\.lake\packages\mathlib> git fetch --tags --force origin
trace: stderr:
From https://github.com/leanprover-community/mathlib4
 + dc80c39735...422f1110b6 PicardGroup -> origin/PicardGroup  (forced update)
trace: analysis: updating 'importGraph' with {}
trace: .\.\.lake\packages\importGraph> git fetch --tags --force origin
trace: analysis: updating 'batteries' with {}
trace: .\.\.lake\packages\batteries> git fetch --tags --force origin
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache

[Terence Tao]

(here I am using your lakefile verbatim, with toolchain leanprover/lean4:v4.19.0).

[Justin Asher]

Yes, one minute.

[Terence Tao]

OK, I've merged your fix, but I'm having some weird git problem locally (fatal: '.lake/packages/BibtexQuery/.git' not recognized as a git repository). Sigh. I think I need to nuke my local repo and start over.

[Justin Asher]

Ah, if you just delete the local .lake folder, then I presume it will work.

[Justin Asher]

As an FYI: I also added a .gitignore to the repository to prevent uploading local files (like .lake).

[Terence Tao]

!! still not working

PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake update
info: toolchain not updated; already up-to-date
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '02dbd02bc00ec4916e99b04b2245b30200e200d0'
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache

[Justin Asher]

Are you on Windows?

[Terence Tao]

Yes

[Terence Tao]

@Kevin Buzzard Hopefully this answers your question 'Why don't you put the work in a new repo?'

[GasStationManager]

what tends to work for me when mathlib installation giving trouble:

• delete .lake
• delete lake-manifest.json (it will be re-generated)
• just require mathlib (say @ 4.19.0) in lakefile. Don't need to separately require proofwidgets etc
• make sure the lean-toolchain matches (e.g. 4.19.0)
• lake exe cache get

[Terence Tao]

Ok, trying now.

[Justin Asher]

GasStationManager said:

• just require mathlib (say @ 4.19.0) in lakefile. Don't need to separately require proofwidgets etc

@Terence Tao needs a couple other imports too:

require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"

meta if get_config? env = some "dev" then
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "v4.19.0"

I had a problem previously where I fixed all of my imports to v4.19.0, and yet the transitive imports still needed to be fixed. I figured fixing everything would work, and then we can reduce the number of imports afterwards.

[Justin Asher]

GasStationManager said:

• delete lake-manifest.json (it will be re-generated)

Does this still apply if the lake-manifest.json was generated on my local machine in a repository which built cleanly?

[Terence Tao]

Sigh. Still the same problem.

PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake exe cache get
info: analysis: no previous manifest, creating one from scratch
error: .\.\.lake\packages\mathlib: could not resolve 'HEAD' to a commit; the repository may be corrupt, so you may need to remove it and try again
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> Remove-Item -Recurse -Force .\.lake\packages\mathlib
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake exe cache get
info: analysis: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache

I'll try deleting the whole local repository again. I really have no clue what is going on at this point, since it seems it now builds locally elsewhere.

[Justin Asher]

I believe the problem is that the .lake folder needs to be deleted, both locally and on the repository.

[Justin Asher]

It seems to be working fine on my Windows machine after doing so. I was on Mac earlier.

[Justin Asher]

# macOS/Linux
rm -rf .lake

# Windows Command Prompt
rmdir /s /q .lake

# PowerShell
Remove-Item -Path .lake -Recurse -Force

[Terence Tao]

Trying this now.

[Terence Tao]

Fresh fetch of the repository + removing .lake + lake clean + lake update still failed to work. Am at a loss.

PS C:\Users\teort\OneDrive\Documents\GitHub> Remove-Item -Recurse -Force .\analysis
PS C:\Users\teort\OneDrive\Documents\GitHub> git clone https://github.com/teorth/analysis.git
Cloning into 'analysis'...
remote: Enumerating objects: 114, done.
remote: Counting objects: 100% (114/114), done.
remote: Compressing objects: 100% (73/73), done.
remote: Total 114 (delta 25), reused 104 (delta 19), pack-reused 0 (from 0)
Receiving objects: 100% (114/114), 164.65 KiB | 1.17 MiB/s, done.
Resolving deltas: 100% (25/25), done.
PS C:\Users\teort\OneDrive\Documents\GitHub> cd analysis
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> Remove-Item -Recurse -Force .\.lake
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake clean
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: checkdecls: checking out revision '3d425859e73fcfbef85b9638c2a91708ef4a22d4'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'fa4f7f15d97591a9cf3aa7724ba371c7fc6dda02'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4.git
info: proofwidgets: checking out revision 'c4919189477c3221e6a204008998b0d724f49904'
info: plausible: cloning https://github.com/leanprover-community/plausible.git
info: plausible: checking out revision '77e08eddc486491d7b9e470926b3dbe50319451a'
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'c44e0c8ee63ca166450922a373c7409c5d26b00b'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'e6a9f0f5ee3ccf7443a0070f92b62f8db12ae82b'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'f5d04a9c4973d401c8c92500711518f7c656f034'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '25078369972d295301f5a1e53c3e5850cf6d9d4c'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '5d50b08dedd7d69b3d9b3176e0d58a23af228884'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '02dbd02bc00ec4916e99b04b2245b30200e200d0'
PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake update
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache

[Justin Asher]

Can you try running with -v? lake update -v? I swear it worked on my Windows machine.

[Justin Asher]

Oh, there is another problem where if you do not connect it to your GitHub account, some imports will not work.

[Terence Tao]

It should be connected... with Github Actions enabled... is this something I have to set from the Github web site?

[Terence Tao]

PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake update -v
trace: analysis: updating 'checkdecls' with {}
trace: .\.\.lake\packages\checkdecls> git fetch --tags --force origin
trace: analysis: updating 'Qq' with {}
trace: .\.\.lake\packages\Qq> git fetch --tags --force origin
trace: analysis: updating 'proofwidgets' with {}
trace: .\.\.lake\packages\proofwidgets> git fetch --tags --force origin
trace: analysis: updating 'plausible' with {}
trace: .\.\.lake\packages\plausible> git fetch --tags --force origin
trace: analysis: updating 'mathlib' with {}
trace: .\.\.lake\packages\mathlib> git fetch --tags --force origin
trace: stderr:
From https://github.com/leanprover-community/mathlib4
   0634d16640..1ce9204c93  mjasper-flat-torsion-free -> origin/mjasper-flat-torsion-free
   9265da5cb8..6565d3168a  update-dependencies-bot-use-only -> origin/update-dependencies-bot-use-only
trace: analysis: updating 'importGraph' with {}
trace: .\.\.lake\packages\importGraph> git fetch --tags --force origin
trace: analysis: updating 'batteries' with {}
trace: .\.\.lake\packages\batteries> git fetch --tags --force origin
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache

[Terence Tao]

everything outside of proofwidgets seems to be working currently.

[Justin Asher]

I do not think that should be a problem here. I just remember it happening previously for me. Let me try forking and running your repository locally again to see if it still works.

[GasStationManager]

the errors seems to be about building proofwidgets? Try just remove the require proofwidgets... from lakefile.lean

[Terence Tao]

OK, I'll try this. I vaguely thought this was needed for the doc generation, but at this point I'll settle for at least being able to run Lean and figure out how to repair doc generation later.

[Terence Tao]

Deleting the explicit reference to proofwidgets produced the same error. I think it is a dependency of something else so it will get built regardless.

[Justin Asher]

@GasStationManager Do you know why it would work on my Windows and Mac machines and not on his? I just forked the repository and it worked fine again.

[GasStationManager]

@Terence Tao (you may also need to try delete .lake and lake-manifest again)

[Kevin Buzzard]

@Terence Tao I don't know what you've done, but I've just tried making a new Lean project with bleeding edge mathlib and it's worked fine:

buzzard@brutus:~$ mkdir crap
buzzard@brutus:~$ cd crap
buzzard@brutus:~/crap$ lake new Analysis math
info: downloading mathlib `lean-toolchain` file
buzzard@brutus:~/crap$ cd Analysis/
buzzard@brutus:~/crap/Analysis$ ls
Analysis  Analysis.lean  lakefile.toml  lean-toolchain  README.md
buzzard@brutus:~/crap/Analysis$ cat > Analysis.lean
import Mathlib

#check 2+2=4
#check RestrictedProduct
buzzard@brutus:~/crap/Analysis$ lake exe cache get
info: Analysis: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision '6565d3168aa73eaf276c9d9979da745fba34e481'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '304c5e2f490d546134c06bf8919e13b175272084'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '6c62474116f525d2814f0157bb468bf3a4f9f120'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'f5e58ef1f58fc0cbd92296d18951f45216309e48'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '632ca63a94f47dbd5694cac3fd991354b82b8f7a'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'a1cfb751fd148b5dedfc3ebe2f638d71d7ecad0c'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '36ce5e17d6ab3c881e0cb1bb727982507e708130'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'e5ffc6bd73d63d22e0f2ea9c4b3fa1d9761266b8'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '4f22c09e7ded721e6ecd3cf59221c4647ca49664'
info: mathlib: running post-update hooks
Mathlib repository: leanprover-community/mathlib4
Attempting to download 4897 file(s) from leanprover-community/mathlib4 cache
Downloaded: 4897 file(s) [attempted 4897/4897 = 100%] (100% success)
Decompressing 6762 file(s)
Unpacked in 16024 ms
Completed successfully!
Mathlib repository: leanprover-community/mathlib4
No files to download
Decompressing 6762 file(s)
Unpacked in 3734 ms
Completed successfully!
buzzard@brutus:~/crap/Analysis$ lake build
ℹ [6774/6775] Built Analysis
info: /home/buzzard/crap/Analysis/Analysis.lean:3:0: 2 + 2 = 4 : Prop
info: /home/buzzard/crap/Analysis/Analysis.lean:4:0: RestrictedProduct.{u_1, u_2} {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) (𝓕 : Filter ι) :
  Type (max u_1 u_2)
Build completed successfully.
buzzard@brutus:~/crap/Analysis$

Are you still working in a Dropbox folder?

[Kevin Buzzard]

@Terence Tao why have you committed a .lake directory? .lake is in the default .gitignore file which lake creates when you make a new project (in fact .lake is the only thing in .gitignore by default).

[Justin Asher]

@Terence Tao I just submitted a pull request to delete the .lake folder.

[Justin Asher]

@Kevin Buzzard The project earlier did not have a .gitignore file. I had to create one.

[Terence Tao]

I followed the instructions in https://leanprover-community.github.io/install/project.html to build a project. I don't know if those instructions automatically generate a .gitignore.

[Kevin Buzzard]

I have cloned the project locally and after deleting the .lake directory which I got when I cloned the project, re-creating the correct one with lake exe cache get and then running lake build everything is working absolutely fine for me.

[Justin Asher]

@Terence Tao What happens when you run:

lake update -K proofwidgets
lake build proofwidgets

I really think everything should be working fine.

[Kevin Buzzard]

I think the project should be working fine now.

[Terence Tao]

Incidentally the CI is now also broken, but that's a future problem

[Kevin Buzzard]

I can confirm that

$ git clone git@github.com:teorth/analysis.git
$ cd analysis/
$ lake exe cache get
$ lake build

is working fine for me locally now.

[Kevin Buzzard]

CI is a closed book to me unfortunately.

[Terence Tao]

OK, this is somewhat encouraging...

PS C:\Users\teort\OneDrive\Documents\Github\analysis> lake update -K proofwidgets
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache
PS C:\Users\teort\OneDrive\Documents\Github\analysis> lake build proofwidgets
⚠ [3/24] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
Build completed successfully.

[Kevin Buzzard]

If I type lake update proofwidgets then nothing changes, indicating that proofwidgets is on the right version I guess? I don't know what -K means.

[Justin Asher]

You can try running:

lake build mathlib

It will take a minute, but then Mathlib should build locally.

[Justin Asher]

If it is already built, it will just say Build completed successfully.

[Terence Tao]

It's trying to build a fair chunk of Mathlib now

[Kevin Buzzard]

The lake-manifest.json file currently says that it wants proofwidgets commit c4919189477c3221e6a204008998b0d724f49904 and if you change into .lake/packages/proofwidgets which looks to me to be the commit bumping the toolchain to v4.19.0 so proofwidgets looks good to me.

[Kevin Buzzard]

It's working fine at my end so you should probably just make sure that your version of the repo agrees with githubs, delete .lake, then lake exe cache get and lake build and you should be fine.

[Kevin Buzzard]

i.e. do git pull and then make sure git status is saying

On branch main
Your branch is up-to-date with 'origin/main'.

nothing to commit, working tree clean

and then rm -rf .lake and lake exe cache get and lake build and I am pretty sure that it will work.

[Terence Tao]

OK I will try this. I have a tentative theory that I am restoring from a cached version of the repository rather than the most recent build which is why I keep getting the same errors over and over again.

[GasStationManager]

I did just clone the current repo in Windows and can confirm that lake exe cache get and then lake build works

[Justin Asher]

Terence Tao said:

OK I will try this. I have a tentative theory that I am restoring from a cached version of the repository rather than the most recent build which is why I keep getting the same errors over and over again.

These should be in the .lake folder, which is why I suggested deleting it. If you can build the packages locally instead of using the precompiled versions, then that might solve your problem. I am just as confused as everyone else!

[Terence Tao]

In desperation I am reinstalling elan as nothing else seems to be working (git status confirms I match the online repo exactly and I still get the error)

[Justin Asher]

You can also try using WSL2 if you are that desperate...that's what I do on my Windows machine.

[Terence Tao]

in particular I have set elan default leanprover/lean4:4.19.0 though I do worry that this may screw up all my other Lean projects

[Justin Asher]

You should only need to set the Lean version in the toolchain file of the specific project, not any others. I do not think that should be necessary.

[Eric Taucher]

As a suggestion, instead of showing just the instructions, show a screen capture. I note this because the PS from Terry is for Windows PowerShell and the ~ used with Kevin is most likely on Mac or a Linux variant.

[Justin Asher]

@Eric Taucher I gave the same command for PowerShell earlier. It should be fine. But thanks for pointing this out. :working_on_it:

[Eric Taucher]

Justin Asher said:

You can also try using WSL2 if you are that desperate

WSL2 is a major step, something that Terry might have and that might be simpler is to bring up a Git Bash shell which will often convert Linux file paths correctly for Windows.

[Terence Tao]

OK, reinstalling elan didn't change anything. I had cancelled the previous lake build mathlib which followed a successful lake build proofwidgets so I will try that (lake exe cache get still fails to get proofwidgets)

[Eric Taucher]

When working on the Equational project I ran into a problem on Windows and Terry was the only other person to also run into it being on Windows.

It is noted here and might shed some light with this issue.

[GasStationManager]

@Terence Tao I think now that the current github repo seems to be in good shape (after removing .lake), perhaps you can also try in parallel to git clone the repo into a new directory and lake exe cache get

[Terence Tao]

Unfortunately lake build mathlibis absorbing all the CPU. Will report back in an hour or two. I've already deleted my local repository and restored multiple times, so am pessimistic that doing so again will be any different.

[Eric Taucher]

Using Windows 11 and a Git Bash shell

$ gh repo clone teorth/analysis
$ cd analysis/
$ lake exe cache get
$ lake build

results in Build completed successfully.

Git Bash Screen shots

Git_bash_001.png
Git_bash_002.png

Are there any more steps needed?

---

Also ran lake build mathlib which resulted in Build completed successfully.

Git Bash Screen shots

image.png

[Mac Malone]

I tried this on Windows 10 and cloning the repository and building work for me as well. Running lake update and then building with this simpler lakefile also worked:

lakefile.lean

import Lake
open Lake DSL

package «analysis» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
  ]
  -- add any additional package configuration options here

-- Require Mathlib (the comprehensive library of mathematics in Lean)
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ "v4.19.0"

-- Require Pantograph (a library for automated theorem proving)
-- require pantograph from git
--  "https://github.com/lenianiva/Pantograph.git" @ "v0.3.1"

@[default_target]
lean_lib «Analysis» where
  -- add any library configuration options here

require checkdecls from git "https://github.com/PatrickMassot/checkdecls.git"

meta if get_config? env = some "dev" then
require «doc-gen4» from git
  "https://github.com/leanprover/doc-gen4" @ "v4.19.0"

[Mac Malone]

I wonder if your local Mathlib cache may have been corrupted somehow. You can forcibly overwrite the local cache with lake exe cache get! (get with an exclamation point) and see if that helps.

[Justin Asher]

Mac Malone said:

I wonder if your Mathlib cache may have been corrupted somehow. You can forcibly overwrite the local cache with lake exe cache get! (get with an exclamation point) and see if that helps.

Where is the cache stored, in general? Is it separate from .lake and the toolchain directories?

[Justin Asher]

Also, in general, are there any good pages on addressing issues like these? Because I have had similar problems, and I feel like there should be a standard reference to point people to. This could just be an ordered list of things to try: update, build, clean, build Mathlib by itself, remove .lake, clean the cache, etc. when someone encounters an issue like this.

[Mac Malone]

Justin Asher said:

Where is the cache stored, in general? Is it separate from .lake and the toolchain directories?

Mathlib's lake exe cache stores its cache in a system-dependent location (which attempts to follow the standard for where similar cache directories on the system are stored).

• On Windows, this is %HOMEDRIVE%%HOMEPATH%\.cache\mathlib.
• On Unix, this is either $XDG_CACHE_HOME/mathlib (if set in the environment) or ~/.cache/mathlib.

This path can also be overriden with the MATHLIB_CACHE_DIR environment variable

[Justin Asher]

@Mac Malone Thanks for letting me know! This is probably the problem.

[Terence Tao]

Wow, even lake exe cache get! failed to eliminate the problem, which is really stumping me - clearly it is now a local problem since everyone else can build the project, but short of fully uninstalling and reinstalling Lean I am at a loss on what to do (other than continue the build of mathlib without cache, which looks like it will take a few more hours on my poor little laptop). Time for me to get a second device that can support Lean...

[Justin Asher]

You can always try WSL; it works well for me. If you run code lean-project-name it will open your project in VS Code (given that you have the extension installed), just like on Windows. I have a hard time imagining this not working.

[Justin Asher]

Here is a short guide via Gemini 2.5 Pro in case you are curious:

WSL Guide

Here's how to set up Lean 4 with WSL and VS Code:

• Install WSL (Windows Subsystem for Linux):
  * Open PowerShell or Command Prompt as Administrator.
  * Run wsl --install. This will install Ubuntu by default.
  * Restart your computer when prompted.
  * Complete the Ubuntu setup (username and password).

• Install Lean 4 and elan (Lean's version manager) in WSL:
  * Open your WSL terminal (Ubuntu).
  * Run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh.
  * Follow the on-screen instructions. It's usually safe to accept the defaults.
  * Close and reopen your WSL terminal or run source $HOME/.elan/env to update your path.
  * Verify installation by typing lean --version.

• Install VS Code and Extensions:
  * Download and install VS Code from the official website if you haven't already.
  * Install the WSL extension in VS Code.
  * Install the lean4 extension in VS Code.

• Open a Lean Project in VS Code via WSL:
  * Open your WSL terminal.
  * Navigate to or create a directory for your Lean projects (e.g., mkdir my_lean_project && cd my_lean_project).
  * Create a new Lean project: lake new my_lean_project.
  * Navigate into the project: cd my_lean_project.
  * Open the project in VS Code: code . (make sure you run this command from within the WSL terminal in your project directory).
  * VS Code should automatically detect it's a WSL environment and use the lean4 extension installed there. You might see a notification in the bottom-left corner indicating it's connected to WSL.

• Start Coding:
  * Open a .lean file (e.g., MyLeanProject.lean or create a new one).
  * The lean4 extension should provide features like syntax highlighting, error checking, and autocompletion.

[Jz Pan]

My personal experience with proofwidgets error on Windows is that it seems to be transient, re-run lake update several times should fix it.

[Terence Tao]

I was able to get Lean to work on this repo on a second (old and slow) computer, and the mathlib build for my primary computer is almost done, so I guess the problem is close to solved. I suspect that it was a local caching problem but hopefully it will not be an issue once the mathlib build completes.

[Pim Otte]

Something that might also be worthwhile to explore (in addition to Verso), is writing this in @Patrick Massots Verbose Lean (examples).

I think the advantage here is that it would make it easier to stay closer to the original text, making it more accessible to students. On the downside, the gap to regular Lean becomes bigger.

I'd be happy to try setting a proof of concept for this, if you think this is a worthwhile angle:)

[Kim Morrison]

I think using Verso is a great idea. (It's already lovely, and development work is likely to ramp up even more.)

Verbose Lean is cool, but realistically I don't think it's the right time, in terms of technological readiness, for this project to adopt it.

[Patrick Massot]

Kim, could you explain what is not technologically ready according to you?

[Patrick Massot]

Maybe you are mixing up Verbose Lean and Informal Lean?

[Patrick Massot]

Note also that the questions of using Verbose Lean and using Verso are completely orthogonal. You totally use both. And in both cases the main obstacle is insufficient documentation (but both are improving).

[Terence Tao]

For the record, I think I tracked down the issue that had been causing me so much grief yesterday. At one point I had deleted .lake, but there was a confirmation popup window asking if I was sure about deleting a certain number of files. But this window somehow got buried and I only discovered it today, after hours of dealing with issues with a corrupted .lake file. Note to self: add "reboot computer" to the list of things to try when dealing with weird lake issues.

[Terence Tao]

On the other hand, I still have the issue with document generation preventing CI from working currently - perhaps a consequence of messing around with the lakefile? The log says to run lake update «doc-gen4» (though I don't know if this is to be done locally), and unfortunately the same issue I had before sitll persists there:

PS C:\Users\teort\OneDrive\Documents\GitHub\analysis> lake update «doc-gen4»
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required builds logged failures:
- proofwidgets:release
error: build failed
uncaught exception: Failed to fetch ProofWidgets cloud release: lake failed with error code 1
error: mathlib: failed to fetch cache

[GasStationManager]

Locally on my checkout of the repo in Windows I was able to run lake update doc-gen4without errors; though that probably doesn't fix the CI issue.
For the local build issue, the best bet is probably lake exe cache get! suggested above, on a repo directory without .lake.

[Pim Otte]

I agree the Lean Verbose discussion is orthogonal. Since it seems Verso is a good idea in either case, I have taken the liberty of porting the existing content to Verso. It needs a little polishing, but this page is fairly representative for what it would look like. I'm not the most versed in Verso (pun intended), so suggestions for improvements are welcome.

Repository Hosted version

TODO:

• Fix up sections 2.2 and onwards (split up lean code, move documenting comments to documentation out of lean sections, shorten long lines) Used literate pages instead
• Investigate why this part gives a verso error Disappeared
• [ ] Generate and include doc-gen
• [ ] Link from Verso defs to doc-gen

@Terence Tao If, at any point, you'd like to adopt the verso version, I'm more than happy to transfer the whole repository to you or PR it to the existing repo, whichever you prefer.

[Terence Tao]

@Pim Otte That looks promising! Does Verso also function as a traditional Github repository - for instance are these pages auto-generated from the underlying Lean source files which one can make pull requests etc.? If one can also do the same sort of continuous integration available currently on Github (in particular, to autogenerate the Lean documentation for the methods) that would be great. Alternatively if Verso is able to auto-scrape from a separate Github repository (e.g., every 24 hours) then one could keep the current repository running as is and have the Verso page as a secondary visualization layer.

[Pim Otte]

This is indeed a traditional Github repository, people can contribute with pull requests and the pages are generated using CI from the source files. I have currently copied over and edited your original Lean files, so the auto-scraping option is not very attractive to me.

If I understand correctly, you're also looking for doc-gen style documentation. We could generate this, but I'm also wondering what you'd like to use that for? I think the idea is that we could do mostly everything we would want in the Verso-generated pages. (For example, the language reference is built using verso, and it has search built-in)

[Terence Tao]

I tend to use doc-gen both for search and also for direct access to the source code through the various "Source" hyperlinks, and also to be able to click on any term in the docstring one is currently viewing to see the corresponding docstring for that other term (from looking at your example pages, something similar occurs on hovering over a term, but one can't click through).

Pedagogically, given that a student going through the exercises here would also need to use Mathlib, it makes sense to me to offer at least one way to view the code for this repository in a format similar to the Mathlib documentation. But if one could offer both the Verso-style content and the doc-gen style content with links between the two (similar to how LeanBlueprint generates a LaTeX-PDF-like document with links to the corresponding doc-gen page) that would be the best of both worlds to me. If the links between the two require too much effort to set up, just having two independent pages would still be useful, I think.

[Pim Otte]

Clicking through in the hovers is something that might even be a good feature request for Verso in general/the manual genre.

Since your aim is to also get students acquainted to mathlib, then I'm totally on board with including the doc-gen. Generating the doc-gen and including it should definitely be doable. I think it should be possible to link to the doc-gen with a custom genre, perhaps even with some light customization. (If someone with more verso experience has any thoughts how to best architect this, feel free to pitch in)

[Shreyas Srinivas]

Doesn’t verso already offer search?

[Shreyas Srinivas]

I think on the lean reference manual one can already do a search for declarations

[Shreyas Srinivas]

Also @Pim Otte could you make this repository a template repository?

[Shreyas Srinivas]

Basically it has the right CI to deploy the compiled webpages

[Shreyas Srinivas]

And lakefile config to build verso + math projects

[Pim Otte]

Shreyas Srinivas said:

Doesn’t verso already offer search?

It needs some setup, but it should be doable.

Shreyas Srinivas said:

Also Pim Otte could you make this repository a template repository?

Once we've got it in a stable state, I think it should be easy to remove the analysis book specific parts for other people to use:)

[Shreyas Srinivas]

Making it a template repository allows people to start projects by clicking a button on GitHub

[Pim Otte]

Shreyas Srinivas said:

Making it a template repository allows people to start projects by clicking a button on GitHub

Gotcha, but I think it makes sense to do that once we're happy with the configuration and after I've removed the parts specific to this project from the template repo

[Jason Rute]

@Terence Tao I want to ask about what you mean by:

perhaps also serve as a data set to test various autoformalization techniques.

What do you envision here? Is this autoformalization of statements? Definitions? Proofs? Whole blogs/articles/chapters?

[Terence Tao]

In principle, all of these. I am limited to some extent by not holding the full copyright over the text of the book, but one could imagine using this project to build an annotated data set of informal statements/definitions/proofs and at least one proposed formalization of those texts, which could perhaps be useful training data. (Though I will disclose that some of the formalizations here were already AI-assisted, particularly in cases where there were a half-dozen similar statements to formalize, in which case Github Copilot was often able to formalize the last three or four more or less correctly after I had done the first few. Here it seems that the decision to use naming conventions similar to Mathlib's helps in this regard.)

Also, as this project contains a large number of sorrys that are relatively easy and/or standard, they could also potentially serve as a benchmark for any automated tools to complete short sorries.

[Pim Otte]

Since we want the combination doc-gen + Verso, we probably want the Lean files as is, and use the LiterateLean construction to include them in Verso. Other methods would involve keeping the documentation comments as comments in Verso, or not having them available for doc-gen.

@David Thrane Christiansen Some questions regarding Verso:

• Does the above make sense, or do you see a better way to approach this?
• The Literate Lean construction is only available for the Site/Blog genre, right? Or is there some way to embed this into the Manual genre?
• Is making the definitions in hovers clickable something that might be a good general feature request?

[David Thrane Christiansen]

I'll answer your bullet points one by one.

As far as the overall approach goes, I want to make sure I understand the goals of the document before I make a specific recommendation on how to set it up. The big one: is there ever any desire to have Lean code that exists, but isn't shown to users? Or should there be a 1:1 correspondence between the Lean code and the text?

The reason I ask is because Verso has a mechanism for naming parts of a file (basically just wrapping it in special comments) and including those in the document. These don't have to match the syntactic structure of the document - it can be used to show three lines from the middle of a definition, for instance - and they may overlap. This is very useful if you want to do things like show an example of using something prior to showing its definition, or if you want to elide certain details. The downside is, of course, thinking about what goes where!

I just used this to port Functional Programming in Lean to Verso, and I think it was quite pleasant.

[David Thrane Christiansen]

Pim Otte said:

• The Literate Lean construction is only available for the Site/Blog genre, right? Or is there some way to embed this into the Manual genre?

The literate Lean mechanism in Verso right now is only set up for blogs, but if you'd like to use it then I can port it fairly quickly to the manual genre. Verso is extensible, so this is also something that users can do themselves, but it should be there as a built-in feature. One downside of it is that it can't always map Lean code that occurs in Markdown to the correct thing - is it the x from the preceding scope, or the x from the subsequent scope? But it's close to the Lean file, and this aspect can be improved over time.

[David Thrane Christiansen]

Pim Otte said:

• Is making the definitions in hovers clickable something that might be a good general feature request?

Yes, that would be a useful improvement.

I do want to encourage people to write text that also works without hovers, though, for reasons of accessibility, readers on phones or other devices, and the glorious future where we have PDF and ePub backends.

[David Thrane Christiansen]

As far as the search box goes, that's currently a feature of the Lean Language Reference. It will eventually get upstreamed to Verso itself, but for now it's there.

It's really more of a "jump to this" box than it is a search box, because it searches the registered metadata for things like documented names, tactics, and tokens in syntax rules, rather than searching the full text. Full-text search would be great, but for now it's all metadata-driven.

[Pim Otte]

David Thrane Christiansen said:

I'll answer your bullet points one by one.

As far as the overall approach goes, I want to make sure I understand the goals of the document before I make a specific recommendation on how to set it up. The big one: is there ever any desire to have Lean code that exists, but isn't shown to users? Or should there be a 1:1 correspondence between the Lean code and the text?

The goals are to provide a formalization companion to Analysis I and a gateway to Lean and mathlib.
The Verso view is for online exploration, but for exercises, students would have to clone the repository.
The doc-gen serves as a reference while doing exercises.
A 1:1 correspondence is possible, but I'm definitely happy to hide some of the details, as long as we have the backing lean file available when students checkout the repo.
A nice-to-have would be auto-include links from the Verso-view to the doc-gen view.
The driving factor behind my structure is the wish to have a single source of truth for the material and then show the documenting comments in a sane way in both the Verso and doc-gen view.

[Jason Rute]

Terence Tao said:

Also, as this project contains a large number of sorrys that are relatively easy and/or standard, they could also potentially serve as a benchmark for any automated tools to complete short sorries.

In some sense we already have this benchmark by @Lenny Taelman. It is the SorryDB project: https://github.com/SorryDB/SorryDB by @Lenny Taelman and @Austin Letson . It indexes sorrys in repos like yours and turns them in a benchmark.

[Jason Rute]

https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning-for-Theorem-Proving/topic/SorryDB.20project

[Justin Asher]

@Jason Rute I do not think this is an entirely fair comparison regarding SorryDB, especially since it is updated nightly to reflect the current state of Lean repositories. Having a fixed set of "practice" sorry problems to test and train models at an introductory undergraduate level would be extremely helpful, and I think easier for people outside the Lean community to conceptualize. For instance, if I were to write a paper evaluating an agent, I think saying "Analysis I problems" would be a great and easy to understand benchmark.

[David Thrane Christiansen]

Pim Otte said:

The goals are to provide a formalization companion to Analysis I and a gateway to Lean and mathlib.
The Verso view is for online exploration, but for exercises, students would have to clone the repository.
The doc-gen serves as a reference while doing exercises.
A 1:1 correspondence is possible, but I'm definitely happy to hide some of the details, as long as we have the backing lean file available when students checkout the repo.
A nice-to-have would be auto-include links from the Verso-view to the doc-gen view.
The driving factor behind my structure is the wish to have a single source of truth for the material and then show the documenting comments in a sane way in both the Verso and doc-gen view.

This makes sense!

Here's how I'd organize it:

• Create a repository with two Lean packages in it, each in a subdirectory
• Put the example Lean code in one of the packages. It should depend on subverso but not Verso - this is the tool that is used to extract code metadata.
• Put the Verso text in the other package. Use the "anchor" mechanism to include the example code.

This provides more flexibility than you're asking for, but it works today without me building you any new features. It also lets the document be separate from the code, which can be nice, but you can still ensure that the code stays up to date WRT the document by using features that do things like checking Lean outputs against the expected text. It would be easy to transition to a system like the literate pages when that gets implemented, if you wanted to.

I think the biggest downside is that there would need to be comments in the Lean file that point at the different regions of it. Making the code downloadable without them would be doable with a quick sed script in CI, producing a "clean" tarball.

What do you think? I can also get on a quick call with you to figure it out sometime this week - sometimes a bit of screensharing is just what's needed to figure things out.

Automatic linking from Verso to doc-gen is totally doable. Right now, the function that maps names to their link targets is hard-coded, but that can very easily be made part of the configuration instead. I plan to make this more flexible soon anyway, so if you can wait a bit then it'll happen, and I'll take your use case into account as I update it.

[Pim Otte]

Do you have a link to some documentation/examples of the anchor feature? (edit: Found the examples in FPIL) I'll set up the structure with your guidance in mind, if I need a call I'll certainly ping you:)

[David Thrane Christiansen]

I just did the final release of the Verso version of FPiL, so that's one place to look.

It does a bit of gymnastics that aren't needed if you're not trying to pretend that List is universe-monomorphic in the first few chapters. @Patrick Massot has an early-stages manual for Verbose Lean here that has a simpler setup, which might be good to copy from.

Let me know how it goes!

[Li Xuanji]

Where do we leave playtest feedback?

My proof of Nat.mul_comm depended on Nat.mul_zero and Nat.mul_succ, so Nat.mul_comm is not available in the proofs of the later two

[Terence Tao]

Fair enough; I re-ordered these lemmas (and made the proofs of the latter into sorries). In general, the github issue and PR pages would be the best place to handle these sorts of errata and feedback.

[Jz Pan]

I didn't read your analysis book, but I assume that you have 3 axioms on natural numbers, and all of them are Prop, right? Currently I'm stuck on writing down the recursive definition:

universe u v

structure IsNat (N : Type u) (zero : N) (succ : N → N) : Prop where
  succ_ne_zero : ∀ n, succ n ≠ zero
  succ_injective : ∀ {m n}, succ m = succ n → m = n
  induction {motive : N → Prop} (t : N) (hzero : motive zero) (hsucc : (n : N) → motive n → motive (succ n)) : motive t

attribute [elab_as_elim] IsNat.induction

theorem Nat.isNat : IsNat Nat Nat.zero Nat.succ where
  succ_ne_zero := Nat.succ_ne_zero
  succ_injective := Nat.succ.inj
  induction := Nat.recOn

section IsNat

variable {N : Type u} {zero : N} {succ : N → N} (H : IsNat N zero succ)
include H

theorem unique_recurse {M : Type v} (mzero : M) (msucc : N → M → M) (r r' : N → M)
    (rzero : r zero = mzero) (rsucc : ∀ n : N, r (succ n) = msucc n (r n))
    (r'zero : r' zero = mzero) (r'succ : ∀ n : N, r' (succ n) = msucc n (r' n)) : r = r' := by
  ext1 x
  induction x using H.induction with
  | hzero => rw [rzero, r'zero]
  | hsucc x ih => rw [rsucc, r'succ, ih]

theorem exists_recurse {M : Type v} (mzero : M) (msucc : N → M → M) :
    ∃ r : N → M, r zero = mzero ∧ ∀ n : N, r (succ n) = msucc n (r n) := by
  sorry

end IsNat

OK find a solution: firstly construct a bijection to the actual natural numbers...

[EDIT] Use Nat.find to make everything computable, if DecidableEq N is present

Solution

import Mathlib.Data.Nat.Find
import Mathlib.Logic.Equiv.Defs
import Mathlib.Logic.Function.Iterate

structure IsNat (N : Type*) (zero : N) (succ : N → N) : Prop where
  succ_ne_zero : ∀ n, succ n ≠ zero
  succ_injective : Function.Injective succ
  induction {motive : N → Prop} (t : N) (hzero : motive zero)
    (hsucc : (n : N) → motive n → motive (succ n)) : motive t

attribute [elab_as_elim] IsNat.induction

theorem Nat.isNat : IsNat ℕ 0 Nat.succ where
  succ_ne_zero := Nat.succ_ne_zero
  succ_injective := Nat.succ_injective
  induction := Nat.recOn

namespace IsNat

variable {N : Type*} {zero : N} {succ : N → N} (H : IsNat N zero succ)
include H

def ofNat (_ : IsNat N zero succ) (n : ℕ) : N := succ^[n] zero

@[simp]
theorem ofNat_zero : H.ofNat 0 = zero := rfl

@[simp]
theorem ofNat_succ (n : ℕ) : H.ofNat (n + 1) = succ (H.ofNat n) := by
  simp_rw [ofNat, Function.iterate_succ_apply']

theorem ofNat_injective : Function.Injective H.ofNat
| 0, 0, _ => rfl
| m + 1, 0, h => by
  rw [ofNat_zero, ofNat_succ] at h
  exact False.elim (H.succ_ne_zero _ h)
| 0, n + 1, h => by
  rw [ofNat_zero, ofNat_succ] at h
  exact False.elim (H.succ_ne_zero _ h.symm)
| m + 1, n + 1, h => by
  rw [ofNat_succ, ofNat_succ] at h
  rw [ofNat_injective (H.succ_injective h)]

theorem ofNat_surjective : Function.Surjective H.ofNat := by
  intro x
  induction x using H.induction with
  | hzero => exact ⟨0, rfl⟩
  | hsucc x ih =>
    obtain ⟨n, hn⟩ := ih
    use n + 1
    rw [ofNat_succ, hn]

theorem ofNat_bijective : Function.Bijective H.ofNat := ⟨H.ofNat_injective, H.ofNat_surjective⟩

variable [DecidableEq N]

def toNat (n : N) : ℕ := Nat.find (H.ofNat_surjective n)

@[simp]
theorem toNat_ofNat (n : ℕ) : H.toNat (H.ofNat n) = n := by
  rw [toNat, Nat.find_eq_iff]
  exact ⟨rfl, fun m h ↦ H.ofNat_injective.ne (ne_of_lt h)⟩

@[simp]
theorem ofNat_toNat (n : N) : H.ofNat (H.toNat n) = n := Nat.find_spec (H.ofNat_surjective n)

@[simp]
theorem toNat_zero : H.toNat zero = 0 := by
  rw [← H.toNat_ofNat 0, H.ofNat_zero]

@[simp]
theorem toNat_succ (n : N) : H.toNat (succ n) = H.toNat n + 1 := by
  rw [← H.toNat_ofNat (H.toNat n + 1), H.ofNat_succ, H.ofNat_toNat]

@[simps apply symm_apply]
def equivOfNat : ℕ ≃ N where
  toFun := H.ofNat
  invFun := H.toNat
  left_inv := H.toNat_ofNat
  right_inv := H.ofNat_toNat

variable {M : Type*} (mzero : M) (msucc : N → M → M)

def recurse (t : N) : M :=
  Nat.recOn (motive := fun _ ↦ M) (H.toNat t) mzero (fun n ↦ msucc (H.ofNat n))

variable {mzero msucc}

@[simp]
theorem recurse_zero : H.recurse mzero msucc zero = mzero := by
  simp [recurse]

@[simp]
theorem recurse_succ (t : N) :
    H.recurse mzero msucc (succ t) = msucc t (H.recurse mzero msucc t) := by
  simp [recurse]

theorem eq_recurse (r : N → M)
    (rzero : r zero = mzero) (rsucc : ∀ n : N, r (succ n) = msucc n (r n)) :
    r = H.recurse mzero msucc := by
  ext1 x
  induction x using H.induction with
  | hzero => rw [rzero, recurse_zero]
  | hsucc x ih => rw [rsucc, recurse_succ, ih]

end IsNat

[Kim Morrison]

Patrick Massot said:

Kim, could you explain what is not technologically ready according to you?

Mostly just that I wasn't aware of "external" users, i.e. a project independent of the authors already using it, and I was hesitant to suggest Terry becomes the first such. Very happy to have pointers to corrections to this!

[Pim Otte]

@David Thrane Christiansen I have experimented a bit, and I don't think anchors cover quite everything we want. In particular, I think it makes sense to have docstrings in a nice format in the Verso view, and I can't figure out how to do that with anchors. The reason I want this is because the docstrings are a key part of the doc-gen view, and maintaining two versions of explanatory text seems undesirable. See this commit I based on Patrick's setup for the experimentation.

I see a couple of ways forward:

• Implement ```literateAnchor, which reformats docstrings to normal text.
• Implement Literate Lean for the Manual Genre
• Use LiterateLean with the Site Genre for this project

I strongly suspect the first two are beyond me at this point in time, so I'd ask you to do the implementation. The last one I could probably work out myself. Depending your availability, I could also start on option 3 and migrate to one of the others later. Especially if it's feasible to use literateAnchor on large parts of examples, the main migration work would be in the glue-code.

What do you think?

[Pim Otte]

In addition, it seems that the anchor construct requires manually moving the text from examples to the location? I'm not missing automatic tooling that does this, right? I don't think it's a blocker, but it is something that I can see getting annoying quickly, especially since building the full docs is quite a heavy operation. (The literate page construct, where the inclusion is by-reference, seems nicer to work with from my point of view).

[Pim Otte]

Kim Morrison said:

Mostly just that I wasn't aware of "external" users, i.e. a project independent of the authors already using it, and I was hesitant to suggest Terry becomes the first such. Very happy to have pointers to corrections to this!

I've done some small scale experimentation a while back, and it worked pretty cleanly. The main technical constraint at that point was matching toolchain versions with Verso, which is definitely something that can be overcome. That being said, with Terry's clarifications, it's clear that the gateway to formalization and mathlib is a specific goal for this project. Using Verbose Lean widens the gap to that, so I don't think starting with it is the way to go. I still think it could be a really nice follow-up project to produce a variant for students that don't necessarily want to go into formalization.

[Jason Rute]

Justin Asher said:

Jason Rute I do not think this is an entirely fair comparison regarding SorryDB, especially since it is updated nightly to reflect the current state of Lean repositories. Having a fixed set of "practice" sorry problems to test and train models at an introductory undergraduate level would be extremely helpful, and I think easier for people outside the Lean community to conceptualize. For instance, if I were to write a paper evaluating an agent, I think saying "Analysis I problems" would be a great and easy to understand benchmark.

I think I misunderstood what the sorrys were doing here. If these are exercises or other intentional sorries that are not supposed to be eventually filled in (except as a learning exercise), then I agree it is different from the aim (as I understand it) of the SorryDB project.

[Pim Otte]

@David Thrane Christiansen I've pushed a proof of concept for option 3 described above #general > Lean companion to "Analysis I" - discussion @ 💬 on this branch

It's missing some of the nice infra of the manual, but I'm totally fine handcrafting a menu. The major issue is that only module docstrings are translated. Would also including docComments in the literate page be a possibility? Another minor issue is that the unicode symbols are slightly broken, but that might be something on my end.

[David Thrane Christiansen]

I'm completely slammed this month, so I'm not able to implement substantial new features right away. I'll do my best to guide you with what's present, though, and point you in the direction of implementing any missing parts that you need in the meantime.

For the anchor system, including examples in the text provides a code action to fix them if they get out of sync. The idea is to make sure the author of the document knows what's changing and can know when the text needs updating, rather than having things silently get out of sync. So it does take a bit of explicit consideration, but hopefully inserting the code is not more than just clicking OK repeatedly.

Can I check my understanding of your goal? Is it right that your goal is to have the contents of a Lean development, with module docs and docstrings rendered, with the document adhering very closely to the structure of the underlying code? Essentially "doc-gen plus definitions, with a navigation superstructure added"? Or is it more to write a higher-level overview that's decoupled from the structure of the source files, to help readers find their way to the right place? Most of Verso has thus far been designed for documents that aren't very closely coupled to the module structure and definition order of the code being described. There's no reason it can't support the other use cases, but they've not yet been developed.

As far as matching versions goes, the SubVerso library exists to allow Verso to document code that's written in any version of Lean. The anchor-based code inclusion feature works this way, as does the literate page feature. So matching toolchains shouldn't be a big issue going forward.

It almost sounds to me like you'd be best served by something that just slurps in a Lean package and emits fancy HTML with clickable cross-references, with docstrings and module docs rendered specially. Is that an accurate understanding?

[Terence Tao]

@Jz Pan Nice! In the current writeup I did not adhere to a fully axiomatic approach, and instead "cheated" by working with a specific inductive type of natural number for which it was much easier to construct the recursor, but it is nice to know that it is possible to obtain that recursor directly from the axioms, as well as the equivalence with ℕ, within type theory. I might create a second epilogue to Chapter 2 in which one introduces a fully axiomatic form of the natural numbers along the lines of your proposal and show that they can be identified with either ℕ or my existing Chapter2.Nat.

EDIT: I have now expanded the Chapter 2 epilogue at https://teorth.github.io/analysis/docs/Analysis/Section_2_epilogue.html to flesh out this approach.

[Pim Otte]

David Thrane Christiansen said:

...

It almost sounds to me like you'd be best served by something that just slurps in a Lean package and emits fancy HTML with clickable cross-references, with docstrings and module docs rendered specially. Is that an accurate understanding?

I think your conclusion here here is correct.

The adherence to the document structure is more something that results from not wanting to maintain multiple sources: We'll just write the lean file to be in the order we want to present it in. The docstring requirement stems for wanting both the doc-gen and Verso view.

Given your availability, I'll try to see if I can implement the docstring conversion myself, this seems like the most doable route for me right now:)

[David Thrane Christiansen]

Thanks for your understanding!

The code to do it should be able to re-use that of the module docstrings. I'd do it such that it emits a sequence of three Verso blocks - one for the part of the command before the docstring (as Block.highlightedCode), then a paragraph sequence for the contents, then one for the rest. Wrap the whole thing in an HTML span, and it should be reasonably stylable. Please let me know if you get stuck!

[David Thrane Christiansen]

Also, most of that complexity is coming from handling headers. If you translate Markdowns headers in docstrings to something other than Verso headers (like HTML or bold) then that code I linked becomes like 3 lines instead of 20.

[David Thrane Christiansen]

Pim Otte said:

the unicode symbols are slightly broken

It occurred to me that I didn't address this part. I'm assuming that it's a tofu problem.

In the language reference, the Noto fonts are used as fallbacks for Unicode ranges that aren't covered by our default code font. Let me know if doing something like this resolves it for you.

[Pim Otte]

Yep, that worked!

[David Thrane Christiansen]

Great!

I'll be out for the next four days (Constitution Day and Ascension Day, w/ associated daycare closures). Is there anything I can help with to set you up today?

[Pim Otte]

A couple small questions:

• I have the literate doc comments fix here, but without wrapping it in a span. Would you accept a PR without that?
• A pointer to the code I would need to adapt to redirect links to a doc-gen view would be nice:)

For reference: Latest version of the whole thing is on the literate_website branch

[David Thrane Christiansen]

Pim Otte said:

• I have the literate doc comments fix here, but without wrapping it in a span. Would you accept a PR without that?

Yes, that's fine. Thanks!

But I do think it should be configurable - using module docstrings for text that explains ordinary Lean code that uses doc comments as usual is an important use case. Could you add a parameter that controls this feature?

[David Thrane Christiansen]

Pim Otte said:

A pointer to the code I would need to adapt to redirect links to a doc-gen view would be nice:)

Right here: https://github.com/leanprover/verso/blob/5ff418fa7932b3eefcc8858746ab5c52a0deb4f4/src/verso-blog/VersoBlog.lean#L803

The linkTargets parameter determines how to add hyperlinks to rendered source code. It's a no-op in the blog genre right now.

The LinkTargets structure is a record of functions - the idea is that you initialize it with a suitable set of functions whose closure includes the table in which you've got the mapping from names to doc-gen link URLs

[Pim Otte]

@Terence Tao I have a new version up here. The last major thing on my TODO list is implementing the links from the Verso-view to the Documentation part.

The way it is setup, it keeps a large part of the structure of your current repository, the difference is that the formalization is a project in the subfolder analysis.

Feel free to let me know if you have any other requests/ideas:)

[Terence Tao]

Looks good! So it is now set up that the Verso pages are auto-generated from the Lean files, similarly to how the doc-gen files are auto-generated? Ideally this means that any update only needs to touch the Lean files and continuous integration will do the rest.

It is not immediately clear from the current formatting that each docstring is meant to refer to the Lean statement immediately following it, rather than preceding it (compare with the doc-gen file where there are horizontal lines between each statement+docstring pair that make it clearer).

Is there the ability to add additional comments to the Lean file that will render as plain text in the Verso file (similarly to how docstrings are currently rendered)?

I'll stop work on the old repository for now (I managed to reach a reasonably good stopping point at any rate, having constructed most of the real number system) to allow for a smooth transfer over to the new system.

[Pim Otte]

Terence Tao said:

Looks good! So it is now set up that the Verso pages are auto-generated from the Lean files, similarly to how the doc-gen files are auto-generated? Ideally this means that any update only needs to touch the Lean files and continuous integration will do the rest.

Yes, with the exception of adding a page, for which it is needed to:

1. Add an import inanalysis/Analysis.lean
2. Add two lines of code to book/AnalysisBook.lean

[Pim Otte]

Terence Tao said:

It is not immediately clear from the current formatting that each docstring is meant to refer to the Lean statement immediately following it, rather than preceding it (compare with the doc-gen file where there are horizontal lines between each statement+docstring pair that make it clearer).

I can add some formatting to address this:)

[Pim Otte]

Terence Tao said:

Is there the ability to add additional comments to the Lean file that will render as plain text in the Verso file (similarly to how docstrings are currently rendered)?

Yes, all module docstrings, marked with /-! ... -/are rendered, just like the first one that's there right now. (In fact, the module docstrings are a little bit more flexible, since you can use headers inside of them, which currently doesn't work for the docstrings.)

[Shreyas Srinivas]

In general, verso is meant to allow you to mix text and lean code and render them both.

[Shreyas Srinivas]

This is a concept already known in the functional programming world, and has been used for instance, in the unimath project in agda

[Shreyas Srinivas]

@Pim Otte : It seems the webpage design has changed to look more like plain text since the last time. The code snippets are now printed in a very small font size making them harder to read relative to the text.

[Shreyas Srinivas]

This is what I see on firefox on ubuntu:
Screenshot from 2025-06-06 15-24-38.png

[Pim Otte]

Terence Tao said:

I'll stop work on the old repository for now (I managed to reach a reasonably good stopping point at any rate, having constructed most of the real number system) to allow for a smooth transfer over to the new system.

The options for transfer are: Making a PR to your current repository, or transferring the entire repository to you. The first is a little bit more work, and the site could be offline for a bit, but the url will be stable at teorth.github.io/analysis/. The second is easier, but the url would be teorth.github.io/analysis-book/ unless we also renamed the repository. I'm tempted to say the first one is probably the way to go, and I'd be happy to prepare the PR for that.

[Pim Otte]

Shreyas Srinivas said:

Pim Otte : It seems the webpage design has changed to look more like plain text since the last time. The code snippets are now printed in a very small font size making them harder to read relative to the text.

Sure, I can bump the font size of the code a bit:)

[Terence Tao]

I'm fine with either option - the project is still in its early stages and is not experiencing massive traffic, so a move is not problematic, but if you are willing to go with the first option that works for me as well. Will you need any administrator privileges for this, or can it be done purely through PRs?

[Pim Otte]

I think it's just a PR, nothing special needed.

[Shreyas Srinivas]

Also could we have a different font? The font used by the lean reference manual or the new FPIL seems to be a better fit (for me the blurriness in that font is lower than this one).

[Pim Otte]

@Terence Tao PR is here. Since the Github Actions also change in a big way, they don't trigger on this PR. I think it should work, but there might be some issues left due to the refactoring. If you want me to be able to do a quick fix if something breaks, I would hold off merging until after the weekend and merge during daytime in Europe, since I'm logging off soon.

[Terence Tao]

OK. I merged, but it appears that the new files were not automatically built by the CI, so I reverted for now.

[Pim Otte]

Terence Tao said:

OK. I merged, but it appears that the new files were not automatically built by the CI, so I reverted for now.

Alternatively, this should fix it (nvm, some other outstanding issues, feel free to revert)

[Terence Tao]

This message is for anyone encountering the cache issues I was having last week. I finally tracked down the issue to a newly installed antivirus software that was intercepting the cache retrieval. The fix in #mathlib4 > lake exe cache get errors @ 💬 worked for me.

[Marc Huisinga]

Thanks! It's very useful to know that this was also caused by an anti-virus. I think I'll adjust the error message to suggest this as a potential cause when lake exe cache get (or Lake's own caching mechanism) fails from within VS Code on Windows next week.

[Pim Otte]

@David Thrane Christiansen some more questions:

1. The def_literate_page command is quite heavy. Larger sections go past maxHeartbeats (see this issue). CI builds go past 25 minutes.
   a. Are you aware of anything that I could fix in Verso that would (likely) increase performance?
   b. Would the following setup work (well) for caching in CI? (I have had situations where just editing the examples doesn't propagate to the verso view)

   - Split off each `def_literate_page` call to a separate file
   - Cache .lake folders in both the `book` and `analysis` projects
   - Run lake build in `analysis` followed by `lake build && lake exe analysis-book` in `book`

2. I have a commit for the linking to doc-gen support, is the architecture here right for a PR to verso?

3. Currently, the above doesn't link definitions themselves, only references. Am I right that we would need to extend LinkTargets to also support this? Would you be interested in a Verso PR for this? (Either separately or joined with the above)

[David Thrane Christiansen]

Pim Otte said:

• The def_literate_page command is quite heavy. Larger sections go past maxHeartbeats (see this issue). CI builds go past 25 minutes.

Yes, this is unfortunate - it's running quite a lot of code in the interpreter from one Lean command. I think it needs to be rearchitected to become fast. A few things can be done to start, though:

1. Caching of elaborated Lean files - right now, it's going out and re-elaborating each file, which is wasteful. I'll have a look at making it cache these results tomorrow. This should greatly improve wall-clock time, even if it doesn't address the heartbeat issue.
2. Can you live with simpler rendering of the Markdown for a while? Right now, it's also launching a subprocess and having a little "conversation" about each embedded term. Skipping this, and rendering the Markdown with less metadata, would make things much faster. This should buy some time until I can go make it really fast!

Your proposed CI setup sounds like a good one. It shouldn't be necessary, but it probably is until I get a chance to greatly improve this side of Verso.

[David Thrane Christiansen]

Pim Otte said:

• I have a commit for the linking to doc-gen support, is the architecture here right for a PR to verso?

Thanks for checking!

I think I'd rather see an approach that allows users to pass any LinkTargets that they want to their blogMain. Some may want to link to other posts on their blog, some might want to link to docgen (as here), and some might want to link to both.

Does that make sense?

[David Thrane Christiansen]

Pim Otte said:

Currently, the above doesn't link definitions themselves, only references. Am I right that we would need to extend LinkTargets to also support this? Would you be interested in a Verso PR for this? (Either separately or joined with the above)

Probably - can you say more about what you mean? Do you mean that the definition site of a name should be able to link to e.g. the corresponding doc-gen page? Customized destinations for definition sites definitely seems like a good thing to have.

[Pim Otte]

David Thrane Christiansen said:

Pim Otte said:

• The def_literate_page command is quite heavy. Larger sections go past maxHeartbeats (see this issue). CI builds go past 25 minutes.

2. Can you live with simpler rendering of the Markdown for a while? Right now, it's also launching a subprocess and having a little "conversation" about each embedded term. Skipping this, and rendering the Markdown with less metadata, would make things much faster. This should buy some time until I can go make it really fast!

Probably yes. I don't think we're doing anything particularly fancy, this might depend on what exactly this disables.

[Pim Otte]

David Thrane Christiansen said:

Probably - can you say more about what you mean? Do you mean that the definition site of a name should be able to link to e.g. the corresponding doc-gen page? Customized destinations for definition sites definitely seems like a good thing to have.

Yes, that's exactly what I mean

[David Thrane Christiansen]

Pim Otte said:

Probably yes. I don't think we're doing anything particularly fancy, this might depend on what exactly this disables.

Mostly, it would mean that identifiers in the text weren't automatically becoming links. For a while.

[Pim Otte]

David Thrane Christiansen said:

Pim Otte said:

Probably yes. I don't think we're doing anything particularly fancy, this might depend on what exactly this disables.

Mostly, it would mean that identifiers in the text weren't automatically becoming links. For a while.

Yeah, we're not using this anyway (since we're linking to doc-gen instead). The hovers are key though, so if we would lose those that would be a no-go

[David Thrane Christiansen]

Just to be sure I'm understanding, do you mean the hovers on the code, or the hovers in the text?

[Pim Otte]

Both the hovers on code and the hovers on inline code in text, hovers in the text we could probably go without for a bit, but they are also nice to have.

From my point of view, the priorities are as follows:

I'll implement the CI-based caching strategy and add sections with higher maxHeartbeats for now.

If you have time to implement 1) above, that's really nice and I think somewhat stacks with the CI cache. (If not, I could put it on my backlog)

If these are not enough, we could reconsider 2).

[David Thrane Christiansen]

Sounds good - and I'll work on clearing out enough backlog to build the feature that I think you _really_ want, rather than the one you've got. I think it'd be generally useful.

[Pim Otte]

I'm not sure the CI setup actually works. The issue I'm running into is that changing the underlying literate page does not invalidate the cache for the Verso page. I've reproduced this in the verso repo example:

1. Build the whole repository and run lake exe demosite
2. Edit examples/website-literate/LitLean.lean
3. Rebuild the whole repository, rebuild the examples/website-literate project
4. Change in LitLean is not reflected in built html.
   (5. Changing examples/website/DemoSiteMain.lean invalidates the cache, and rebuilding now propagates the change.)

@David Thrane Christiansen Do you have any thoughts how to fix this without resorting to rebuilding the verso pages every time?

[David Thrane Christiansen]

There's a new Lake feature that should help here. The needs option allows extra dependencies to be added to a target, and input_file or input_dir should allow you to give the Lean file an extra external dependency on the files that it references. It's not in the reference manual yet, and I haven't done it myself, but it should do the job. I can experiment with it tomorrow and give you better guidance, but I figured something soon was better than more later

[David Thrane Christiansen]

It does require manual tracking, unfortunately

[David Thrane Christiansen]

But it should be possible to generate these rules, or check in CI that they're correct

[Pim Otte]

Is the manual tracking something along the lines of splitting every section in its own package and then using input_file and needs to link them to the example .lean files?

[David Thrane Christiansen]

Let me see if I can write a lakefile.lean that does this automatically and I'll get back to you

[David Thrane Christiansen]

Just an update so you don't think I forgot you: I looked at the problem, and I think there's a better way. I'm working on a PR that I hope you can take over once the basics are in place. Here's what it does now:

1. There's a custom executable for extracting code relevant for literate page rendering. It uses a Markdown parser to retrieve all code elements in all docstrings and module docs, and elaborates them in the final environment of the module, returning a mapping from the string in the code block to Verso highlighted code value.

2. A Lake facet incrementally rebuilds modules' extractions

The remaining step is to write a modified literate code renderer that just uses these extracted JSON snippets instead of calling a Lean subprocess. That should be much, much faster, and have good cache behavior

[David Thrane Christiansen]

I suspect this will be fast and convenient, and I think it should be easy enough for you to maintain

[Pim Otte]

Awesome, thanks so much!

[Shreyas Srinivas]

@David Thrane Christiansen and @Mac Malone : Is it possible to have a project template named something like math-verso that finds matching mathlib and verso toolchains and sets up a math project with verso and includes all the bells and whistles that math projects have? Writing literate code seems like a sufficiently basic task to justify such a template

[David Thrane Christiansen]

@Shreyas Srinivas I think this will be a good thing to have, but we need to do a bit of preliminary work first. There's not just one style of literate programming that works with Verso, so I think we need to do a bit of mapping of the best-supported use cases and some communication with users to figure out and address gaps before making template projects.

[David Thrane Christiansen]

@Pim Otte https://github.com/teorth/analysis/pull/43 contains the state of the updates so far. It demonstrates how to get incremental rebuilds of the section pages when the underlying Lean code changes, and it makes the build take much less time on my machine. It has some bureaucratic overhead at the moment that I'll look into eliminating tomorrow using a technique that @Mac Malone just showed me.

[Pim Otte]

Edit: Fixed the issues below locally, except runtime is still quite a lot longer than described in the PR

I don't know if this was ready to be run by me, and I might be doing something silly, but some information:

Running lake build in book errors, because the literate json files in analysis/.lake/build/literate/ are empty.

Running lake build Analysis:literate in analysis takes quite long for me (~ at least 45 min, seems to run all of mathlib for some reason) and fails with errors like:

error finding highlighted code: Could not find native implementation of external declaration 'IO.getRandomBytes' (symbols 'l_IO_getRandomBytes___boxed' or 'l_IO_getRandomBytes').
For declarations from `Init`, `Std`, or `Lean`, you need to set `supportInterpreter := true` in the relevant `lean_exe` statement in your `lakefile.lean`.
error: external command '/home/pim/projects/lean/analysis/analysis/.lake/build/bin/literate-extract' exited with code 2

I'm currently rerunning with the supportInterpreter := true added to the literate-extract exe in analysis/lakefile.lean (Edit: This works and yields json files with content. Runtime of lake build in analysis is quite long still )

Edit: Running lake build in book is stuck on [64/64] Running Job computation for a long time too.

Edit: Cache is working nicely:)

[Pim Otte]

I have some fixes with respect to rendering and content available on this branch.

[David Thrane Christiansen]

Thanks for the feedback! I think it's ready for you to take over now, with the latest pushes. It now generates all the modules automatically, so you don't need to import them by hand. All you need to do to add a section is to add it to a list in the Lake config under book and place it in the URL hierarchy somewhere.

It definitely spends time on "Running job computation" - I think that's because the code gen step is happening there, and it's needing to create all the files before processing the imports for the actual site.

I've verified locally that it rebuilds reasonably efficiently, and that the cache is invalidated correctly upon changes to the Lean code. Here's what I did to test it:

1. Delete the .lake directories in analysis and book
2. Run lake exe cache get in analysis
3. Run lake build verso in book (just so we're testing the time to build the site, rather than the time to build Verso)
4. Run time lake build in book

This includes the time to build analysis in the time to build the book, but it didn't rebuild Mathlib. I got:

> time lake build
Build completed successfully.

________________________________________________________
Executed in  170.98 secs    fish           external
   usr time  299.06 secs    0.18 millis  299.06 secs
   sys time   57.25 secs    1.60 millis   57.25 secs

Redoing it was very fast:

> time lake build
Build completed successfully.

________________________________________________________
Executed in  496.02 millis    fish           external
   usr time  366.47 millis    0.16 millis  366.31 millis
   sys time  236.72 millis    1.57 millis  235.16 millis

I then added a random blank line in Section_2_3.lean, saved the file, and rebuilt. Visually, I could see that it rebuild the corresponding section of the web page, but not the others, and the timing is reasonable:

> time lake build
Build completed successfully.

________________________________________________________
Executed in   12.51 secs    fish           external
   usr time   11.36 secs    0.22 millis   11.36 secs
   sys time    4.12 secs    1.75 millis    4.12 secs

To see how much time is due to building analysis, I then deleted all the JSON caches from analysis/.lake/build/literate, ran lake build in analysis, deleted book/.lake/build, and saw this in book:

> time lake build
Build completed successfully.

________________________________________________________
Executed in  118.26 secs    fish           external
   usr time  230.63 secs    0.20 millis  230.62 secs
   sys time   42.98 secs    1.50 millis   42.98 secs

If I just remove book/.lake/build, then we can see how much overhead was due to generating the JSON files:

> time lake build
Build completed successfully.

________________________________________________________
Executed in   56.55 secs    fish           external
   usr time  188.11 secs    0.21 millis  188.11 secs
   sys time   34.97 secs    1.40 millis   34.97 secs

So, from this, I think we can conclude that the CI setup should do the following:

1. Get the Mathlib cache in analysis
2. Run lake build in analysis
3. Run lake build in book
4. Cache the contents of analysis/.lake/build and book/.lake

I think this should get you acceptable performance and incrementality until I have time to revisit this use case and make it better.

When you were getting rebuilds of Mathlib, is it possible that you skipped the lake exe cache get step in analysis?

[Pim Otte]

Awesome, works exactly as advertised. (I guess I indeed was missing a lake exe cache get)

I've made this PR which should make all of this ready to be merged.

@David Thrane Christiansen (and @Mac Malone behind the scenes), thanks so much! Depending on your preferences, I would be happy to help upstream this to Verso/Subverso and/or make it into a template repo at some point. There's no rush for me on this part, so it would be a bit of a slower project to do this anyway. I can also imagine some of this gets superseded by other stuff you're working on, or it might be easier to upstream it yourself, so feel free to let me know whatever helps you best:)

[David Thrane Christiansen]

I'm happy to help!

How about we get in touch again in a couple of weeks? That gives me time to clear out some other things that need doing, and it gives you time to figure out what works well and not so well with your current setup. That can become input into a proper user-friendly tool for this kind of project.

[Pim Otte]

@David Thrane Christiansen A small bug popped up. We have a workaround, so it's not too urgent to properly fix this. That being said, it might be a subverso issue, so I did want to let you know:)

When highlighting a pattern of the form obtain ⟨⟨x, hx⟩, hx1⟩ := this, LiterateExtract errors with error finding highlighted code: unexpected internal error: unknown free variable '_fvar.105'. Minimal example here

The error originates from somewhere in this function, with the above example when trying to highlight hx1.

[David Thrane Christiansen]

Thanks! This is probably SubVerso using the wrong local context at some point. I'll investigate, and thanks for a great minimization!

[David Thrane Christiansen]

It seems that the language server agrees!

Screenshot 2025-06-17 at 14.16.00.png

I'll make SubVerso more robust against this kind of thing, though.

[David Thrane Christiansen]

OK, this should do the trick.

[Pim Otte]

I think so; I've tested the LiterateExtract with this version of subverso and it doesn't error, I haven't managed to get it to work with verso by hacking it together, but that's of orthogonal issues concerning my Verso fork. I think I'll try to migrate to mainline Verso once you've bumped SubVerso there, I'm pretty sure we don't have anything right now that I couldn't include in the project itself instead.

[David Thrane Christiansen]

Verso being a library rather than a tool is intended to make it so that you don't need to fork it, but can rather call a different function if you want :-) I'll ping you when the dep is bumped

[David Thrane Christiansen]

@Pim Otte It's merged

[Pim Otte]

I think you may have bumped before merging this PR :) (The bump you did made it easy for me to move back to the main branch, so I put together this PR for the proper fix, no need to rush another subverso bump)

[Hanson Char]

Apparently the Build book workflow has been broken since about 3 days ago. Is this something being fixed? This appeared to be the first commit to main after which the failure started.

[Terence Tao]

I've not been able to resolve the issue; it's some sort of heartbeats problem, possibly related to the previous book issue.

[David Thrane Christiansen]

I can see that @Pim Otte has a PR that bumps the limit. Thanks!

In the next few months, I'll be working on better ways to do this kind of project in Verso, without these challenges.

[Pim Otte]

@David Thrane Christiansen I was looking into are errors like on this page. It's reasonable that they error, since the stuff it concerns is not defined yet. Maybe for the better version it might be nice to have an option to elaborate inline elements in the context of the full module?

If you have a thought on how to best-effort fix this for now, I'd appreciate a pointer how you'd approach it:)

[David Thrane Christiansen]

Elaborating them in the context of the module seems like it's definitely the right way to do it today. In the future, I hope to have a way to specify the scope a bit better - perhaps documents should also be able to forward-reference the contents of other modules, after all!

[David Thrane Christiansen]

As far as fixing up the current project quickly, the way to do it is to modify LiterateExtract.lean in the analysis subproject. Right now, for each command, it extracts the set of terms in the Markdown and sticks their elaborated forms in the terms field. This process should be delayed until the end, and occur globally for the complete syntax of the module rather than be one command at a time.

[David Thrane Christiansen]

Does that make sense?

[Pim Otte]

Thanks, I think I get that enough to take a shot at it:)

[David Thrane Christiansen]

I'll be out for two weeks, and pretty far away from the keyboard, but when I get back we could set up a little check-in if that would be useful for you. Let me know!

[Pim Otte]

I'm relatively unavailable the two weeks after that, so I'll probably ping you somewhere after the start of August

[Andrii Kurdiumov]

I notice that https://teorth.github.io/analysis/sec34/
Not very friendly to mobile readers. What do you think about submitting changes which make it like this https://kant2002.github.io/analysis/sec51/

Also I notice that all Verso templates does not pretend to be mobile friendly. Maybe I can improve that as well. did not checkout how exactly templates looks tbh.

[Terence Tao]

Can you be more specific about what changes you are proposing? The Verso framework is experiencing some other unrelated technical issues right now and it would be good to make sure that any formatting changes do not intefere with the resolution of those issues.

[Pim Otte]

I think what @Andrii Kurdiumov is proposing is mostly css changes, which are more-or-less orthogonal to the current Verso framework issues. I'd be happy to review a PR to make it more mobile friendly. If you take the Lean Language Reference as inspiration it might also make it easier to upstream that later to a potential "Literate Lean Module template"

[Terence Tao]

There are now a number of separate threads

• #new members > Can this proof related to Set replacement be shorter?
• #new members > Tao's Analysis Ch3.3
• #new members > ✔ help with Tao's Analysis Ch3.1 exercise
• #new members > Why is equivalence of type, zero, and succ sufficient here?
• #new members > ✔ Why doesn't rw match my pattern?
• #new members > Help with solving Tao's Analysis Chapter 2 epilogue problem

regarding various aspects of this companion besides this current one. Would it make sense to create a dedicated Zulip channel for this companion and move these discussion threads to it?

[Patrick Massot]

Sure I can create that for you. You simply need to give me a title, description and visibility settings. The possible settings are
image.png

[Terence Tao]

I'll wait to see if there is actually any community interest in having such a channel

[Hanson Char]

Perhaps the administrators can create a poll?

[Terence Tao]

/poll Should we create a dedicated channel for discussion of the Analysis I Lean companion?
Yes, and move previous discussion over to the new channel
Yes, but leave previous discussion as is
No; use existing channels to handle any future discussion
Other

[Terence Tao]

Here I would say the "Yes" options would default to a web-public channel; any other options should be under "Other".

[Terence Tao]

OK, I think this is sufficient indication that there will be an audience for this channel. @Patrick Massot , I would like to go ahead and create a channel "Analysis I", with the description "Discussion about all topics related to the Lean companion to the "Analysis I" textbook", and set to web-public.

I envisage a broad set of topics, ranging from the actual math content itself, to Lean-specific questions, to pedagogical strategy, to technical discussion about various components of the companion such as the Verso pages.

[Patrick Massot]

I created a channel at #Analysis I.

[Terence Tao]

Thanks!

I just realized that I don't have permission to move this thread, and the other threads listed at #general > Lean companion to "Analysis I" - discussion @ 💬 , to the new channel. Would you be able to do that?

[Johan Commelin]

@Terence Tao I've managed to move all the threads that you listed a few posts up. But when I try to move this thread itself, zulip thinks for 37 seconds, and then tells me "Failed"...

[Kevin Buzzard]

Moving them in small batches works and (thankfully!) preserves order. I'm in the process of moving this final thread now, although its title is sufficiently generic that probably people should be discouraged from posting any more stuff here now the topic has its own channel.

[Notification Bot]

64 messages were moved here from #general > Lean companion to "Analysis I" - discussion by Kevin Buzzard.