Doc-gen no longer building

Stream: Analysis I

[Terence Tao]

I tried to update to a newer version of Mathlib but ran into some weird build issues (possiblyto do with the Verso book using a slightly different version of Mathlib than the main Lean source), so I tried undoing the change, but somehow I am now no longer able to make the doc-gen work despite several attempts to update the toolchain, lake manifest, etc. The most recent error messages include the following:

Some required builds logged failures:
- UnicodeBasic/UnicodeCLib
- DocGen4.Output.ToHtmlFormat
- DocGen4.Process.Attributes
- DocGen4.Process.Base
- UnicodeBasic.TableLookup:dynlib

with more specific errors like the following:

✖ [3149/6279] Building UnicodeBasic.TableLookup:dynlib
trace: .> c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.20.1\bin\clang.exe -shared -o C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\lib\lean\UnicodeBasic_TableLookup.dll @C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\lib\lean\UnicodeBasic_TableLookup.dll.rsp
info: stderr:
ld.lld: error: undefined symbol: unicode_case_lookup
>>> referenced by C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\ir\UnicodeBasic\TableLookup.c.o.export:(l_Unicode_CLib_lookupCase___boxed)
>>> referenced by C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\ir\UnicodeBasic\TableLookup.c.o.export:(l_Unicode_lookupCaseMapping)

ld.lld: error: undefined symbol: unicode_prop_lookup
>>> referenced by C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\ir\UnicodeBasic\TableLookup.c.o.export:(l_Unicode_CLib_lookupProp___boxed)
>>> referenced by C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\ir\UnicodeBasic\TableLookup.c.o.export:(l_Unicode_lookupGC)
>>> referenced by C:\Users\teort\Github\analysis\analysis\.lake\packages\UnicodeBasic\.lake\build\ir\UnicodeBasic\TableLookup.c.o.export:(l_Unicode_lookupGC___boxed)
>>> referenced 16 more times
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command 'c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.20.1\bin\clang.exe' exited with code 1

I must admit I am completely stumped as to what is going on. What is the best way to get back to a working build? I made the mistake of also adding some new content and implementing many housekeeping edits simultaneously with pushing attempted fixes, so I would prefer not to revert back to the last working version.

[Ruben Van de Velde]

If you revert analysis/lake-manifest.json back to the previous state, does that not solve it?

[Ruben Van de Velde]

Optionally with lake clean or removing .lake

[Terence Tao]

This gets me as far as having a working lean build, but doc-gen still is not working. I suspect the error messages on trying to update doc-gen are relevant:

PS C:\Users\teort\Github\analysis\analysis> lake update «doc-gen4»
warning: toolchain not updated; multiple toolchain candidates:
  leanprover/lean4:v4.23.0-rc2
    from «doc-gen4»
  leanprover/lean4:4.0.0
    from subverso
warning: subverso: ignoring missing manifest 'C:\Users\teort\Github\analysis\analysis\.lake\packages\subverso\lake-manifest.json'
info: mathlib: running post-update hooks
Mathlib repository: leanprover-community/mathlib4
No files to download
Decompressing 6772 file(s)
Unpacked in 64 ms
Completed successfully!

[Terence Tao]

After multiple reinstalls of elan and .lake, I am getting hung up on a missing Paths.olean file, whatever that means:

PS C:\Users\teort\Github\analysis\analysis> lake update
warning: toolchain not updated; multiple toolchain candidates:
  leanprover/lean4:v4.23.0-rc2
    from Analysis
  leanprover/lean4:4.22.0-rc4
    from MD4Lean
  leanprover/lean4:4.0.0
    from subverso
warning: subverso: ignoring missing manifest 'C:\Users\teort\Github\analysis\analysis\.lake\packages\subverso\lake-manifest.json'
info: mathlib: running post-update hooks
✖ [2/12] Building Cache.Lean
trace: .> LEAN_PATH=C:\Users\teort\Github\analysis\analysis\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\subverso\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\MD4Lean\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\build\lib\lean c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.23.0-rc2\bin\lean.exe C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\Cache\Lean.lean -o C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Lean.olean -i C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean\Cache\Lean.ilean -c C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\ir\Cache\Lean.c --setup C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\ir\Cache\Lean.setup.json --json
error: Cache/Lean.lean:7:0: object file 'c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.23.0-rc2\lib\lean\Lean\Util\Paths.olean' of module Lean.Util.Paths does not exist
error: Lean exited with code 1
Some required targets logged failures:
- Cache.Lean
error: build failed

[Terence Tao]

OK I am digging myself into an ever deeper hole; I can no longer locally run Lean on this repository, nor can I revert to a previous working version (and am willing at this point to abandon other code additions I have made today). I think this is the last time I will try attempting to update Mathlib on my own, this has been quite a negative experience. Any advice on how to get back to a working build would be greatly appreciated.

[Terence Tao]

Never mind, I got an AI to assist me with the rollback to the past working version. Still not sure why everything got so screwed up, but I'm not going to touch anything now that it is back to functional.

[Kim Morrison]

I'll try to take a look. I'd like to get started with https://github.com/teorth/analysis/pull/294, which provides reproducible built scripts, so it's at least easy to know if we are succeeding or failing at various points during upgrading.

[Kim Morrison]

Can anyone confirm for me that the instructions from the README are meant to work? When I run

cd analysis/
lake exe cache get
lake -R -Kenv=dev build Analysis:docs
lake build
cd ../book/
lake exe analysis-book
cd ../

I get an error in lake exe analysis-book with

✖ [83/117] Building Book.Analysis.Section_5_3
trace: .> LEAN_PATH=/home/kim/analysis/book/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/kim/analysis/book/.lake/packages/verso/.lake/build/lib/lean:/home/kim/analysis/book/.lake/packages/subverso/.lake/build/lib/lean:/home/kim/analysis/book/.lake/build/lib/lean /home/kim/.elan/toolchains/leanprover--lean4---v4.21.0-rc3/bin/lean /home/kim/analysis/book/.lake/build/src/Book/Analysis/Section_5_3.lean -R /home/kim/analysis/book/.lake/build/src -o /home/kim/analysis/book/.lake/build/lib/lean/Book/Analysis/Section_5_3.olean -i /home/kim/analysis/book/.lake/build/lib/lean/Book/Analysis/Section_5_3.ilean -c /home/kim/analysis/book/.lake/build/ir/Book/Analysis/Section_5_3.c --load-dynlib /home/kim/analysis/book/.lake/packages/MD4Lean/.lake/build/lib/libleanmd4c.so --plugin /home/kim/analysis/book/.lake/packages/MD4Lean/.lake/build/lib/libMD4Lean.so --json
error: .lake/build/src/Book/Analysis/Section_5_3.lean:5:0: Expected JSON array
error: Lean exited with code 1

[Kim Morrison]

Confusingly this doesn't seem to happen in CI: https://github.com/teorth/analysis/actions/runs/17029606461/job/48269985938?pr=294#step:8:1

[Kim Morrison]

I've been trying to debug this, but might need to ping @David Thrane Christiansen and see if they may have a chance to look.

The relevant code that is producing the "Expected JSON array" error message is in book/AnalysisBook/LiterateModule.lean:

  let f ← IO.FS.Handle.mk lakeConfig .read
  f.lock (exclusive := true)
  let jsonFile ←
    try

      let cmd := "elan"
      let args := #["run", "--install", toolchain, "lake", "build", s!"+{mod}:literate"]

      IO.println s!"Project directory: {projectDir}"
      IO.println s!"Running command: {cmd} {" ".intercalate args.toList}"
      let res ← IO.Process.output {
        cmd, args, cwd := projectDir
        -- Unset Lake's environment variables
        env := lakeVars.map (·, none)
      }
      if res.exitCode != 0 then
        reportFail projectDir cmd args res

      let args := #["run", "--install", toolchain, "lake", "query", s!"+{mod}:literate"]

      IO.println s!"Running command: {cmd} {" ".intercalate args.toList}"
      let res ← IO.Process.output {
        cmd, args, cwd := projectDir
        -- Unset Lake's environment variables
        env := lakeVars.map (·, none)
      }
      if res.exitCode != 0 then
        reportFail projectDir cmd args res
      IO.FS.readFile res.stdout.trim
    finally f.unlock

  let .ok (.arr json) := Json.parse jsonFile
    | throw <| IO.userError s!"Expected JSON array, got:\n{jsonFile}"
  match json.mapM deJson with
  | .error err =>
    throw <| IO.userError s!"Couldn't parse JSON from output file: {err}\nIn:\n{json}"
  | .ok val => pure val

(this includes a few debugging print statements I've just added.)

When the error is produced, jsonFile is empty. However the command that should have produced it is printed as

elan run --install leanprover/lean4:v4.20.1 lake query +Analysis.Appendix_A_5:literate

which for me (when running this inside book/) prints

/home/kim/analysis/analysis/.lake/build/literate/Analysis/Appendix_A_5.json

which is .... not empty!

[Kim Morrison]

Okay, without being able to build locally, I will switch to trying to debug remotely via CI.

[Kim Morrison]

https://github.com/teorth/analysis/pull/296 is a first attempt to tidy up the lakefiles, ensuring that we depend on libraries via pinned version tags, to make sure that everything stays in sync during updates.

Let's see if that passed CI before proceeding further.

[David Thrane Christiansen]

I will be back at the computer in an hour at the latest and will get it fixed. Thanks for the ping!

[Kim Morrison]

I've started upgrading to more recent Lean/Mathlib versions at https://github.com/teorth/analysis/pull/297. (I can only test the analysis/ part locally, so this may still fail in CI.)

I've only moved analysis/ to v4.21.0 so far. We can incrementally move it alone if that works.

[Terence Tao]

Thanks for looking into this! I see you're starting to run into the doc-gen issues that I had (which rapidly became worse the more I tried to "fix" it) though.

[Kim Morrison]

Yes, I think I know what's going on, and am trying again. I'll leave instructions in the README with whatever I learn, and then hopefully go fix some of the underlying problems.

Unfortunately, your lakefile uses a meta if statement to require doc-gen4: I have been trying to warn people that this is fragile for a long time now, but haven't quite succeeded in eradicating it. :-)

[David Thrane Christiansen]

The JSON deserialization issue is because the two subprojects were using different and incompatible versions of the library that extracts information from one for the other. PR #298 adds a check to CI that makes sure this doesn't happen, and there's a script to remedy the situation if it arises.

[David Thrane Christiansen]

PR #299 updates the book/ directory to use the latest RC of Lean and its corresponding Verso. I've verified locally that everything builds and the internal links work as they should.

[Terence Tao]

The bump seems to have caused random package lean files to stop building properly. Here is some sample errors from lake build (after doing the usual lake clean, update, cache get):

✖ [553/3132] Building Aesop.RulePattern
trace: .> LEAN_PATH=C:\Users\teort\Github\analysis\analysis\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\subverso\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\build\lib\lean c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.20.1\bin\lean.exe C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\Aesop\RulePattern.lean -R C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop -o C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\lib\lean\Aesop\RulePattern.olean -i C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\lib\lean\Aesop\RulePattern.ilean -c C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\ir\Aesop\RulePattern.c --json
error: C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\Aesop\RulePattern.lean:147:36: 'mvars' is not a field of structure 'AbstractMVarsResult'
error: C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\Aesop\RulePattern.lean:147:6: fields missing: 'numMVars'
error: Lean exited with code 1
Some required builds logged failures:
- Mathlib.Tactic.Linter.DirectoryDependency
- Qq.ForLean.ReduceEval
- Batteries.Linter.UnreachableTactic
- Batteries.Linter.UnnecessarySeqFocus
- Plausible.Random
- Batteries.Data.List.Basic
- Aesop.RulePattern
error: build failed

[Kim Morrison]

You say that you ran update: this is potentially a dangerous operation, and you shouldn't do it just to build the project. Only ever run update when you are about to embark on an update of your dependencies to newer versions.

Currently (i.e. on the a9e9324f5fa24a2c1456dd832c602ad842988eed commit which is currently the HEAD of main), when I run

cd analysis
lake clean
lake exe cache get
lake build

that succeeds. Is that working for you?

[Kim Morrison]

Now, when running those commands we do get a warning message:

warning: manifest out of date: git revision of dependency '«doc-gen4»' changed; use `lake update «doc-gen4»` to update it

which is not ideal.

To fix this we can run

lake update -Kenv=dev doc-gen4

which resolves that warning, without apparently breaking anything. I've made a PR from the change that command creates at https://github.com/teorth/analysis/pull/303.

[Kim Morrison]

In fact, after yesterday's PRs, it seems that it's safe to run lake update -Kenv=dev (i.e. without specifying to only update doc-gen4), and this also preserves the fact that lake build is working.

[Kim Morrison]

(In fact, even running lake update (i.e. with the -Kenv=dev), seems to leave lake build in a running state.)

[Kim Morrison]

Apologies about the -Kenv=dev needed when running lake update, we've been encouraging everyone to stop using setups that require this, but it seems you're still on a setup that needs it. :-(

[Terence Tao]

I get the same build errors even without lake update. A sample:

PS C:\Users\teort\Github\analysis\analysis> lake build
✖ [46/424] Building Mathlib.Tactic.Linter.DirectoryDependency
trace: .> LEAN_PATH=C:\Users\teort\Github\analysis\analysis\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\subverso\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\build\lib\lean c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.20.1\bin\lean.exe -Dpp.unicode.fun=true -DautoImplicit=false -DmaxSynthPendingDepth=3 -Dweak.linter.mathlibStandardSet=true -Dweak.linter.style.longFile=1500 C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\Mathlib\Tactic\Linter\DirectoryDependency.lean -R C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib -o C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean\Mathlib\Tactic\Linter\DirectoryDependency.olean -i C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean\Mathlib\Tactic\Linter\DirectoryDependency.ilean -c C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\ir\Mathlib\Tactic\Linter\DirectoryDependency.c --json
error: C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\Mathlib\Tactic\Linter\DirectoryDependency.lean:614:61: unknown identifier 'getLinterOptions'
error: Lean exited with code 1
✖ [83/520] Building Qq.ForLean.ReduceEval
trace: .> LEAN_PATH=C:\Users\teort\Github\analysis\analysis\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\packages\subverso\.lake\build\lib\lean;C:\Users\teort\Github\analysis\analysis\.lake\build\lib\lean c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.20.1\bin\lean.exe C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\Qq\ForLean\ReduceEval.lean -R C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq -o C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\lib\lean\Qq\ForLean\ReduceEval.olean -i C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\lib\lean\Qq\ForLean\ReduceEval.ilean -c C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\.lake\build\ir\Qq\ForLean\ReduceEval.c --json
warning: C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\Qq\ForLean\ReduceEval.lean:24:13: `Fin.ofNat` has been deprecated: use `Fin.ofNat'` instead
error: C:\Users\teort\Github\analysis\analysis\.lake\packages\Qq\Qq\ForLean\ReduceEval.lean:24:13: function expected at
  Fin.ofNat ?m.1731
term has type
  Fin (?m.1730 + 1)
error: Lean exited with code 1

[Terence Tao]

(this was after deleting .lake and then running lake clean and then lake exe cache get, which seemed to both run without difficulty.)

[Terence Tao]

... although lake exe cache get did print this warning.

PS C:\Users\teort\Github\analysis\analysis> lake exe cache get
Current branch: HEAD
Warning: Some Mathlib ecosystem tools assume that the git remote for `leanprover-community/mathlib4` is named `upstream`. You have named it `origin` instead. We recommend changing the name to `upstream`. Moreover, `origin` should point to your own fork of the mathlib4 repository. You can set this up with `git remote add upstream https://github.com/leanprover-community/mathlib4.git`.
Using cache from origin: leanprover-community/mathlib4
No files to download
Decompressing 6890 file(s)
Unpacked in 8396 ms
Completed successfully!

[Terence Tao]

Hmm, this is possibly an elan issue on my end, for some reason it is running c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.20.1\bin\lean.exe even though the project is now on leanprover/lean4:v4.21.0 . Don't really understand what is going on here though.

[Terence Tao]

Ah, I think the last time I was trying to debug things I followed AI advice to override elan's versioning to force 4.20.1 (which was the version at the time). Now I overrode it to 4.21.1 and it builds now, and now I'll unset the override.

[Kim Morrison]

Yeah, that was not a helpful :robot: :-)

[Terence Tao]

I mean, it did achieve the immediate goal at the time of getting lake to build, but at the cost of (a) modifying a setting that caused mysterious trouble later on, and (b) not giving me adequate understanding of what changes had just been made. It's a good thing I still had to cut and paste the AI provided solution otherwise I might not have recognized the issue at all...

[Ruben Van de Velde]

Can we make elan override print a big warning with a confirmation prompt and/or make it print a warning every time you build with it active?

[Dan Abramov]

I'm getting a different (maybe unrelated?) issue when rebasing on main:

Run ~/.elan/bin/lake -R -Kenv=dev build Analysis:docs
warning: manifest out of date: git url of dependency '«doc-gen4»' changed; use `lake update «doc-gen4»` to update it
info: doc-gen4: checking out revision '05a43fcf9c484d69252bbc3556ca0fdb2417048a'
error: external command 'git' exited with code 128
Error: Process completed with exit code 1.

See https://github.com/gaearon/analysis-solutions/actions/runs/17078118431/job/48426381566 for a failed run.

I sent https://github.com/teorth/analysis/pull/305 but I don't know if it's the right fix. The build doesn't fail anymore on my fork but it literally takes forever (https://github.com/gaearon/analysis-solutions/actions/runs/17078695472/job/48426708123).

[Dan Abramov]

I've cleaned the cache and I still can't get the CI to pass on my fork. I don't understand why it's passing in the upstream repo, maybe due to GH actions cache?

[Dan Abramov]

Updated https://github.com/teorth/analysis/pull/305 to a more minimal fix. I think this should work.

[Kim Morrison]

@Terence Tao, @Dan Abramov's analysis1#305 looks correct to me, if you'd like to merge that.

[Kim Morrison]

@Terence Tao, with significant help from @David Thrane Christiansen at #311, it looks like we've finally got everything upgraded to the latest toolchain.

The literate programming setup you're using here is a bit bleeding edge. This is all going to get easier in the nearish future! :-)