doc-gen4 broken

Stream: lean4

[Siddhartha Gadgil]

@Henrik Böving I was trying to use doc-gen4 the other day, and I cannot build it due to its dependency on Cli which is far behind lean updates. Any suggestions?

[Henrik Böving]

Yeah it's always a little annoying with the breaking nightly changes, getting it to 30-06 already took me half a day to get right and a bunch of PRs and diffs. However due to the fact that the getOp issue is currently very much undecided and might continue to experience breaking changes in the following nightlies and the fact that I'm busy learning for my exams I did not plan on fixing the mess again until this section of Lean has stabilized. I'll get to fixing it at the 24.7 most likely since that's the day after my last exam for this semester so I'll be all free again. By then the nightlies will hopefully be a little more stable again^^

In the mean time it will just be broken for ~20 days unless someone else fixes it, sorry :/

[Siddhartha Gadgil]

No problem. But do you happen to know which was the last (or close to last) version that was not broken @Henrik Böving ? I will checkout that and build (I made a couple of random guesses but failed).

[Henrik Böving]

In general when I push something to main it did always build at the time when I pushed if you use the compiler version that is in lean-toolchain (the mentioned 30-06) compiling that from scratch and running it against another project that is using 30-06 (the fact that the compiler versions match up can be quite important in times of frequent change^^) does yield good results on the mini project I use for testing before running it against mathlib:

image.png

[Siddhartha Gadgil]

Thanks.
But presumably since I am using a fairly recent version of lean, if I use something that can handle Cli (which uses OptionM for example) I cannot build.
I will wait for the eventual stable doc-gen4.

[Henrik Böving]

Hopefully after the first real release of Lean the simple-ish libraries doc-gen depends on won't be broken so often anymore and everything will be stable-ish^^

[Marc Huisinga]

Siddhartha Gadgil said:

Henrik Böving I was trying to use doc-gen4 the other day, and I cannot build it due to its dependency on Cli which is far behind lean updates. Any suggestions?

Just to be clear, the lean4-cli nightly branch is up to date and main is in sync with the milestone releases.

[Henrik Böving]

It's definitely not only related to lean4-cli (if at all) yeah, there is some funky linker issues I'm seeing, other dependencies break due to getOp etc.

[Siddhartha Gadgil]

Marc Huisinga said:

Siddhartha Gadgil said:

Henrik Böving I was trying to use doc-gen4 the other day, and I cannot build it due to its dependency on Cli which is far behind lean updates. Any suggestions?

Just to be clear, the lean4-cli nightly branch is up to date and main is in sync with the milestone releases.

Thanks. Good to know that.
I planned to use lean4-cli but did not because of seeing the last commit on github being from a while back. I will use it (via the nightly).

[Henrik Böving]

Exams done onwards to fixing everything!

[Henrik Böving]

@Siddhartha Gadgil main compiles and works with 07-20 now^^, the documentation for current mathlib4 should deploy within the next few minutes.

[Siddhartha Gadgil]

@Henrik Böving There are mathlib4 versions for 07-19, 07-24 and 07-28. Can you sync a DocGen4 version to one of them (I do not see mathlib4 for 07-20).

Thanks.

[Henrik Böving]

I did see the bulid failure yesterday evening yeah I just didn't get to fixing it yet, wait a sec.

[Henrik Böving]

@Siddhartha Gadgil fixed and deploying

[Siddhartha Gadgil]

Thanks

[Siddhartha Gadgil]

Unfortunately I am still not able to build, though probably the issue is with some os-level setup. I am using Ubuntu 20.04. With lake build I get the following error.

> /home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/bin/leanc -shared -o ./lean_packages/CMark/build/cmark/libleancmark.so -Wl,--whole-archive ./lean_packages/CMark/build/cmark/libleancmark.a -Wl,--no-whole-archive
error: stderr:
ld.lld: error: relocation R_X86_64_PC32 cannot be used against symbol 'stderr'; recompile with -fPIC
>>> defined in /home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib/glibc/libc.so
>>> referenced by buffer.c
>>>               buffer.o:(cmark_strbuf_grow) in archive ./lean_packages/CMark/build/cmark/libleancmark.a

ld.lld: error: relocation R_X86_64_PC32 cannot be used against symbol 'stderr'; recompile with -fPIC
>>> defined in /home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib/glibc/libc.so
>>> referenced by cmark.c
>>>               cmark.o:(xcalloc) in archive ./lean_packages/CMark/build/cmark/libleancmark.a

ld.lld: error: relocation R_X86_64_PC32 cannot be used against symbol 'stderr'; recompile with -fPIC
>>> defined in /home/gadgil/.elan/toolchains/leanprover--lean4---nightly-2022-07-24/lib/glibc/libc.so
>>> referenced by cmark.c
>>>               cmark.o:(xrealloc) in archive ./lean_packages/CMark/build/cmark/libleancmark.a
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Any help is appreciated. Maybe I should run lake with some flags to debug further?

[Henrik Böving]

I already fixed that cmark issue a while ago, you're cloning or updating doc-gen in a wrong way if it still does this, this indicates that the cmark dependency you are using for it is out of date

[Henrik Böving]

And FYI the fix was to actually add -fPIC to the cmark compilation call, C compiler error messages can actually be useful sometimes :D

[Siddhartha Gadgil]

Thanks. I am nuking the build, lean_packages etc and trying again.

[Siddhartha Gadgil]

I cloned afresh and I am now getting a different error, this time with leanInk

info: updating ./lean_packages/leanInk to revision cb529041f71a4ea8348628a8c723326e3e4bdecc
error: stderr:
fatal: reference is not a tree: cb529041f71a4ea8348628a8c723326e3e4bdecc
error: git exited with code 128

Indeed if I navigate to https://github.com/hargonix/LeanInk/tree/cb529041f71a4ea8348628a8c723326e3e4bdecc I see a warning on Github: "This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository"

[Henrik Böving]

oh shitttt

[Henrik Böving]

that's totally on me i force pushed over that like 30 min ago on another branch because that diff isn't needed, let me fix that

[Henrik Böving]

Phew my reflog still got that commit close one :sweat_smile: Can you pull and try again now? That was really dumb of me sorry @Siddhartha Gadgil

[Siddhartha Gadgil]

Thanks @Henrik Böving - it builds fine now.

[Henrik Böving]

Phew, what happened was that LeanInk on its doc-gen branch has a diff to serialize some internal datastructures to Json so i can use them but for the LeanInk link back feature I don't need that anymore so I removed it from that branch in order to avoid having to change the branch name etc...which of course breaks the doc-gen main branch that still relies on its existence /o\

[Siddhartha Gadgil]

Just ran it on my code (with @Anand Rao ) - the output is splendid. Thanks a lot @Henrik Böving for this.

[Siddhartha Gadgil]

If you want to see another product of doc-gen4 publicly hosted, I have deployed at http://math.iisc.ac.in/~gadgil/unit_conjecture//Polylean/TorsionFree.html
(link is not to the top level).

[Siddhartha Gadgil]

Actually for some reason we had not made things doc-strings. Will do so and get better docs.

[Henrik Böving]

http://math.iisc.ac.in/~gadgil/unit_conjecture/Polylean/ModArith.html#instHomomorphismIntFinOfNatNatInstOfNatNatToAddCommGroupToRingInstCommRingIntInstCommRingFinInstNonemptyInstInhabitedFinHAddNatInstHAddInstAddNatOfNatMod2

that's gonna be the longest instance name i've seen so far

[Kevin Buzzard]

This was auto-generated right? You probably can't refer to it explicitly whilst staying under the 100 char per line limit

[Siddhartha Gadgil]

Kevin Buzzard said:

This was auto-generated right? You probably can't refer to it explicitly whilst staying under the 100 char per line limit

Yes, auto-generated.

[Mario Carneiro]

That gives me cause to worry about the instance name generator then, since the input is fairly small (at least from the user perspective)

[Mario Carneiro]

You might think, why does it matter if instances have long names since they are usually anonymous? But remember that when you are debugging and looking at pp.all output, you will commonly see an instance name like this in a stack with 6 others, repeated hundreds of times in the proof term. Instances tend to dominate the output in this case

[Mac]

Mario Carneiro said:

since the input is fairly small (at least from the user perspective)

I believe this is the problem. The input looks small, but actually isn't. The AddCommGroup.Homoroprhism class has two instance-implicit parameters that have to be synthesized on every use (here for Int and Fin) and those specific instances are what is resulting in the very long name.

[Mario Carneiro]

I don't think the naming system should make use of implicit arguments for this reason

[Mario Carneiro]

If the arguments are canonical instances then they are uniquely defined from the other arguments anyway

[Siddhartha Gadgil]

Mac said:

Mario Carneiro said:

since the input is fairly small (at least from the user perspective)

I believe this is the problem. The input looks small, but actually isn't. The AddCommGroup.Homoroprhism class has two instance-implicit parameters that have to be synthesized on every use (here for Int and Fin) and those specific instances are what is resulting in the very long name.

That is exactly the case - we use a fair amount of typeclass inferences so instances built from other instances.

[Matej Penciak]

Sorry to bring this up again, but I think something in the last couple weeks might have broken doc-gen4 again. I tried running it on some personal repos and I'm either getting segfault errors or lakefile errors.

I also tested it on mathlib4 thinking something about my repositories might be messing it up, but I get the following error when running doc-gen4 Mathlib

error: ./lakefile.lean:1:0: error: invalid parser attribute implementation builder arguments
error: ./lakefile.lean:3:0: error: unknown namespace 'Lake'
error: ./lakefile.lean:5:0: error: expected command
error: ./lakefile.lean:8:0: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'example', 'inductive', 'initialize', 'instance', 'opaque', 'structure', 'syntax' or 'theorem'
error: ./lakefile.lean:11:0: error: expected 'abbrev', 'axiom', 'builtin_initialize', 'class', 'def', 'example', 'inductive', 'initialize', 'instance', 'opaque', 'structure', 'syntax' or 'theorem'
uncaught exception: ./lakefile.lean: package configuration has errors

[Matej Penciak]

Does doc-gen4 have to be built with the same release as the repository it's going to generate the documentation for?

[Henrik Böving]

It's a little more intricate than that but generally speaking since Lean is very unstable right now that is usually a good idea. However this is not really enough in this case. What I would have to do here is also upgrade the Lake dependency, I last looked at this on the weekend and there Lake changed its API In a way that I had to figure out new stuff again and to be quite honest I couldn't be bothered to at that time since I saw the same API was again changed in one of the next nightlies :D however I see that mathlib has now pushed further as well so I will reinvestigate...I think I also saw some bugs with LeanInk and what not, I'll see how it goes.

Either way, yes in general its a good idea to build doc-gen with the same Lean version as the project you are trying to document because of quickly changing API stuff, once we have a Lean stable release this should become much much better. Right now you can basically assume if your project version does not match doc-gens current version it will blow up in at least a significant amount of cases.

[Henrik Böving]

@Mac the current nightly breaks the lakefile of https://github.com/xubaiw/CMark.lean/blob/main/lakefile.lean (a doc-gen dependency)

error: ./lakefile.lean:19:19: error: unknown identifier 'inputFileTarget'
error: ./lakefile.lean:20:2: error: unknown identifier 'fileTargetWithDep'
error: ./lakefile.lean:25:19: error: unknown identifier 'inputFileTarget'
error: ./lakefile.lean:26:2: error: unknown identifier 'fileTargetWithDep'
error: ./lakefile.lean:31:2: error: unknown identifier 'staticLibTarget'

are these functions still somewhere? Does it have to be done in a completely different way?

It also broke your by file facet which I will just remove for now, it is not exactly useful in its own right anyways and if you are still working the API it's just additonal unnecessary maintenance effort

[Mac]

@Henrik Böving yeah, the entire API has changed (for all custom builds).

[Mac]

Everything now is in a essentially stable final state including facets and excluding, of course, necessary maintenance to fix bugs.

[Henrik Böving]

s/no/now ?

[Mac]

With the addition of library facets, the doc-gen4 docs facet should be implementable on a file and library level.

[Henrik Böving]

In that case, is there a nice migration path or does there have to happen some fundamental change to CMarks lakefile? I would assume that the lake FFI example shows how to do this type of stuff?

And my follow up question would have been whether its sensible for me to update doc-gen now or whether you are planning to throw things overboard again in the coming days, then I'd just leave it be as is. But from your remark I'm assuming this is not the case and I can just fix things right now and expect them not to be broken in the next few nightlies right?

[Mac]

Henrik Böving said:

In that case, is there a nice migration path or does there have to happen some fundamental change to CMarks lakefile? I would assume that the lake FFI example shows how to do this type of stuff?

Unforunately, yes, CMark needs to update to be compatible (the FFI example has been update to show what is necessary, though).

[Mac]

Henrik Böving said:

or whether you are planning to throw things overboard again in the coming days, then I'd just leave it be as is. But from your remark I'm assuming this is not the case and I can just fix things right now and expect them not to be broken in the next few nightlies right?

Yep I am done with major changes, I will hopefully doing a maintenance release to fix any bugs / missing features at the end of the month, but no more major changes. In fact, I will largely be bowing out of Lean until next Spring/Summer as I have to work on my dissertation. So things are pretty final as they are for the foreseeable future.

[Mac]

For the doc-gen4 facets, here is how they should probably look updated:

module_facet docs (mod) : FilePath := do
  let some docGen4 ← findLeanExe? `«doc-gen4»
    | error "no doc-gen4 executable configuration found in workspace"
  let exeJob ← docGen4.exe.fetch
  let modJob ← mod.leanBin.fetch
  let buildDir := (← getWorkspace).root.buildDir
  let docFile := mod.filePath (buildDir / "doc") "html"
  exeJob.bindAsync fun exeFile exeTrace => do
  modJob.bindSync fun _ modTrace => do
    let depTrace := exeTrace.mix modTrace
    let trace ← buildFileUnlessUpToDate docFile depTrace do
      proc {
        cmd := exeFile.toString
        args := #["single", mod.name.toString]
        env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
      }
    return (docFile, trace)

library_facet docs (lib) : Unit := do
  BuildJob.mixArray (α := FilePath) <| ← lib.recBuildLocalModules #[`docs]

[Henrik Böving]

Very cool, I'll fix CMark then and finally switch to the new doc-gen approach as well.

One more question though, the FFI example demonstrates how to build for a single FFI C target, and as far as I can see targets are identified by name (https://github.com/leanprover/lake/blob/master/examples/ffi/lib/lakefile.lean#L24) do you have an example that showcases how one might dynamically generate multiple targets? or should I have one big target that iterates over all C files and builds them

[Matej Penciak]

Thanks for working on this! I tried to hack away at it to bump it to a more recent nightly, but I obviously got stuck since I didn't know the codebase at all.

[Mac]

Henrik Böving said:

do you have an example that showcases how one might dynamically generate multiple targets? or should I have one big target that iterates over all C files and builds them

This is non-trivial as what this would really want is a non-Lean LeanLib-like target that specifies the targets to collect. Currently, the simplest solution is just to have one Lake-facing target that collects the builds jobs of the smaller targets. Alternatively, you could do some metaprogramming and generate target declarations for each file to build. The later has the advantage of making the targets accessible to Lake (which provides e.g., CLI support). The former has the advantage of simpler (i.e., no metaprogramming shenanigans).

[Henrik Böving]

Eh, I would hope nobody wants to build those C files manually...I'll try to get the big target going then and to the rest as build jobs

[Mac]

@Henrik Böving looking at CMark's source, it can largely just be an API-to-API translation, there is no real need to reorganize it.

[Mac]

One thing to keep in mind is the pkg caveat for parameterized targets that tripped @Wojciech Nawrocki up in yesterday's thread, which he recorded in lake#114.

[Henrik Böving]

import Lake
open System Lake DSL

package CMark

def cmarkDir : FilePath := "cmark"
def wrapperDir := "wrapper"
def srcNames := #[
  "blocks", "buffer", "cmark_ctype", "cmark",
  "commonmark", "houdini_href_e", "houdini_html_e",
  "houdini_html_u", "html", "inlines", "iterator",
  "latex", "man", "node", "references", "render",
  "scanners", "utf8", "xml"]
def wrapperName := "wrapper"
def buildDir := defaultBuildDir

def cmarkOTarget (pkg : Package) (srcName : String) : IndexBuildM (BuildJob FilePath) := do
  let oFile := pkg.dir / buildDir / cmarkDir / ⟨ srcName ++ ".o" ⟩
  let srcTarget ← inputFile <| pkg.dir / cmarkDir / ⟨ srcName ++ ".c" ⟩
  buildFileAfterDep oFile srcTarget λ srcFile => do
    let flags := #["-I", (pkg.dir / cmarkDir).toString, "-fPIC"]
    compileO (srcName ++ "c") oFile srcFile flags

def wrapperOTarget (pkg : Package) : IndexBuildM (BuildJob FilePath) := do
  let oFile := pkg.dir / buildDir / wrapperDir / ⟨ wrapperName ++ ".o" ⟩
  let srcTarget ← inputFile <| pkg.dir / wrapperDir / ⟨ wrapperName ++ ".c" ⟩
  buildFileAfterDep oFile srcTarget λ srcFile => do
    let flags := #["-I", (← getLeanIncludeDir).toString, "-I", (pkg.dir / cmarkDir).toString, "-fPIC"]
    compileO (wrapperName ++ "c") oFile srcFile flags

@[defaultTarget]
lean_lib CMark

extern_lib cmark (pkg : Package) := do
  let libFile := pkg.dir / buildDir / cmarkDir / "libleancmark.a"
  let oTargets := (←srcNames.mapM (cmarkOTarget pkg)) ++ #[←wrapperOTarget pkg]
  buildStaticLib libFile oTargets

was completely painless indeed^^ Amazing, Putting this here in case someone has similar needs.

[Henrik Böving]

@Mac Two more things and you'll be rid off me for quite some time again :D, the main doc-gen still attempts to build the lake root package with:

    let ctx ← Lake.mkBuildContext ws true
    (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx

which broke again now, I know that the facet will fix this but I'd like to fix the main build first for now and get to the facet multi file stuff when I have more time...is there a quick way to do this right now?

Secondly my SourceLinker is broken again:

  for pkg in ws.packageArray do
    for dep in pkg.dependencies do
      let value := match dep.src with
        | Lake.Source.git url commit _ => (getGithubBaseUrl url, commit.getD "main")
        -- TODO: What do we do here if linking a source is not possible?
        | _ => ("https://example.com", "master")
      gitMap := gitMap.insert dep.name value

pkg.dependencies doesn't seem to be a thing anymore, can I still somehow construct my gitMap? (This is an issue that I cannot simpl solve with the facet, lake graph would be the proper solution here)

I know I could start grepping for both in the Lake repo to probably figure out what I want but I figured since I already have you here I might as well ask :P

[Mac]

Henrik Böving said:

Mac Two more things and you'll be rid off me for quite some time again :D, the main doc-gen still attempts to build the lake root package with:

    let ctx ← Lake.mkBuildContext ws true
    (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx

which broke again now, I know that the facet will fix this but I'd like to fix the main build first for now and get to the facet multi file stuff when I have more time...is there a quick way to do this right now?

Take a look at printPaths to see how to format this: https://github.com/leanprover/lake/blob/6db611df8a814d6a9f8962205384b1659791354a/Lake/CLI/Actions.lean#L35-L37

[Mac]

Henrik Böving said:

pkg.dependencies doesn't seem to be a thing anymore, can I still somehow construct my gitMap? (This is an issue that I cannot simpl solve with the facet, lake graph would be the proper solution here)

Package themselves now have a remoteUrl? field that you can just use directly.

[Mac]

Also, you should probably be defaulting the commit to master rather than main, since that is what Lake does.

[Henrik Böving]

And the gitTag?is the commit then I assume?

[Henrik Böving]

Mac said:

Also, you should probably be defaulting the commit to master rather than main, since that is what Lake does.

will do

[Mac]

Henrik Böving said:

And the gitTag?is the commit then I assume?

Not exactly, the tag is the tag if it the resolved commit has an associated Git tag.

[Henrik Böving]

How can I get the commit then?

[Mac]

You realistically need to read the manifest for this. Your old solution was actually wrong, as the revision in the lakefile is not necessarily related to the revision actually used.

[Mac]

Honestly, reading the manifest would probably be the best solution anyway as it has all the package source information in a nice JSON format.

[Matej Penciak]

Henrik Böving said:

pkg.dependencies doesn't seem to be a thing anymore, can I still somehow construct my gitMap? (This is an issue that I cannot simpl solve with the facet, lake graph would be the proper solution here)

I know I could start grepping for both in the Lake repo to probably figure out what I want but I figured since I already have you here I might as well ask :P

So this is actually something I managed to fix by hand when I was hacking away at trying to get doc-gen4 to work. I just cded into the package directory, and copied the command from getProjectCommit

[Matej Penciak]

Mac said:

Honestly, reading the manifest would probably be the best solution anyway as it has all the package source information in a nice JSON format.

But this is almost certainly the right solution...

[Henrik Böving]

Mac said:

Honestly, reading the manifest would probably be the best solution anyway as it has all the package source information in a nice JSON format.

https://github.com/leanprover/lake/blob/6db611df8a814d6a9f8962205384b1659791354a/Lake/Load/Manifest.lean#L104-L110 with this then yes? I can assume the manifest.json always exists in lean_packages (if there are dependencies) after a lake build equivalent right?

[Mac]

@Henrik Böving actually, the path of the manifest file is changing due to request lake#111. The future-proof way to do this is just read ws.root.manifestFile.

[Henrik Böving]

@Matej Penciak CI just passed on doc-gen and it worked fine on my local test project so I would assume you can use it again now!

Thanks a lot for the help Mac!

[Matej Penciak]

Thank you! I will now give it a shot!

[Chris Lovett]

In the latest Mathlib4 building docs with:

https://github.com/leanprover-community/mathlib4.git
cd mathlib4
lake -Kdoc=on build Mathlib:docs --verbose

fails with:

error: > LEAN_PATH=./lean_packages/Cli/build/lib:./lean_packages/leanInk/build/lib:./lean_packages/doc-gen4/build/lib:./lean_packages/Unicode/build/lib:./build/lib:./lean_packages/lake/build/lib:./lean_packages/CMark/build/lib LD_LIBRARY_PATH=/home/chris/.elan/toolchains/leanprover--lean4---nightly-2022-08-18/lib:./lean_packages/doc-gen4/build/lib /home/chris/.elan/toolchains/leanprover--lean4---nightly-2022-08-18/bin/lean ./lean_packages/doc-gen4/././DocGen4/Output/DocString.lean -R ./lean_packages/doc-gen4/./. -o ./lean_packages/doc-gen4/build/lib/DocGen4/Output/DocString.olean -i ./lean_packages/doc-gen4/build/lib/DocGen4/Output/DocString.ilean -c ./lean_packages/doc-gen4/build/ir/DocGen4/Output/DocString.c
error: stdout:
./lean_packages/doc-gen4/././DocGen4/Output/DocString.lean:131:29: error: invalid field 'map', the environment does not contain 'DocGen4.Output.HtmlM.map'
  modifyElement e
has type
  HtmlM Element

and I get the same thing if I edit lean-toolchain to match what doc-gen4 is using leanprover/lean4:nightly-2022-08-18 but I guess I'm a bit surprised doc-gen4 is doing this:

require lake from git
  "https://github.com/leanprover/lake" @ "master"

What if master doesn't match leanprover/lean4:nightly-2022-08-18 ? Why isn't doc-gen4 just using whatever version of lake is specified in it's lean-toolchain?

[Henrik Böving]

It is more nuanced than this doc-gen's real master is working right now. However lake is more clever than to just use the master branch if it is written in the lakefile, it will lock a certain version of the master branch that was at use at the time, doc-gen has already moved on by exactly one important functional and a few CI related commits and one would have to run lake update in mathlib before running it (the changed lockfile in lean_packages/manifest.json could also be a PR to mathlib)

The reason that lake does only respect the lean-toolchain version from the top level project it is building is (I dont konw this for sure but this would be my first concern), the Lean compiler does not care about backwards compatability across nightlies, if you compile one lean file with todays nightly and another with yesterdays there is absolutely nothing guaranteeing you that they will work together so instead lake will always use one lean version, the one specified in the top level.

The doc-gen CI does get around this issue with this beautiful line of sed: https://github.com/leanprover/doc-gen4/blob/main/deploy_docs.sh#L26

[James Gallicchio]

I don't really understand what was discussed in this thread, but wondering if this issue is related:

My repo's doc generation succeeds locally but was failing on CI, so I now have the CI build the library before building the docs. Both steps succeed.

I hard-coded the commits for the mathlib/docgen dependencies to ensure everything is on the same Lean version but it seems like a version mismatch bug to me.

Before pre-compiling library: https://github.com/JamesGallicchio/LeanColls/runs/7946219736?check_suite_focus=true#step:5:69
Now: https://github.com/JamesGallicchio/LeanColls/runs/7946544943?check_suite_focus=true#step:6:358

[Henrik Böving]

You should use/push the auto generated lean_packages/manifest.json instead of hard pinning dependencies to certain commits. Looking at your lean-toolchain you are 9 days behind doc-gens current toolchain which can easily cause bugs already, in general you want to always be in sync with the toolchain I used to develop the doc-gen commit you are using, otherwise I can basically guarantee for nothing :P There is also no real point in debugging things at this point for me since it could be anything related to a nightly breaking something still really.

Anyways I did it either way now xD. After updating your toolchain and pinning everything to master/main in the lakefile:

λ cat lean-toolchain
leanprover/lean4:nightly-2022-08-18
λ cat lakefile.lean
import Lake
open System Lake DSL

package leancolls {
  precompileModules := false
}

@[defaultTarget]
lean_lib LeanColls {
  srcDir := __dir__
  roots := #[`LeanColls]
}

@[defaultTarget]
lean_exe test {
  root := `Main
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "master"

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

we now need to run:

lake -Kenv=dev update

to get manifest.json up to date properly. Then run

lake -Kenv=dev build LeanColls:docs

and it will work.

So yeah if you are observing a bug with doc-gen please always make sure that:

• you are at the latest master
• your toolchain is in sync
• your manifest.json reflects this by running the proper lake update command
• to commit your manifest.json so things are actually reproducible for anyone wanting to help you

[James Gallicchio]

That makes sense, thanks! :) Updated and looks like it's working fine now

[Chris Lovett]

@Henrik Böving that would make an excellent addition to your doc-gen4 readme perhaps...

[Arthur Paulino]

Henrik Böving said:

And FYI the fix was to actually add -fPIC to the cmark compilation call, C compiler error messages can actually be useful sometimes :D

How can I do this? I'm hitting the same error on another repo

[Henrik Böving]

Take a look at the lakefile of CMark.lean I think it was? Its just adding a compiler option to the c compiler call there really

[Arthur Paulino]

Henrik Böving said:

Take a look at the lakefile of CMark.lean I think it was? Its just adding a compiler option to the c compiler call there really

I tried to mimic it without success. See https://github.com/leanprover/lake/issues/126 for more details

[James Gallicchio]

RE: https://github.com/leanprover/doc-gen4/pull/82 is there a reason why doc-gen4 still generates mathlib docs instead of them being generated by the mathlib repo CI? it seems like this is making it harder than necessary to keep doc-gen4 main branch up to date

[Henrik Böving]

Yes there is a reason, this would break mathlib's CI if doc-gen cannot keep up with their upgrade frequency of the lean compiler and this is not a burden mathlib should take but I should.

[James Gallicchio]

@Henrik Böving So, poking around, it seems like Lake won't update a dependency if it's locked by a different dependency? And mathilb's manifest.json locks a bunch of packages that doc-gen4 depends on, because mathlib's lakefile lists doc-gen4 as a dependency itself

[James Gallicchio]

but even manually updating lean_packages/mathlib/lean_packages/manifest.json doesn't seem like enough to get doc generation running, since this lake PR hasn't been merged yet: https://github.com/leanprover/lake/pull/127/files

[Henrik Böving]

Yes that is indeed an issue but I can also not just run lake update in the CI because this might update the std4 dependency as well and if mathlib4 doesnt like the master of std4 stuff blows up.

[James Gallicchio]

Oh yeah this isn't doc-gen4 CI issue. I think lake's handling of transitive dependencies could be improved. And mathlib should be keeping an up to date manifest (@Mario Carneiro is the manifest being updated without -Kdocs=on set?)

[Mario Carneiro]

I'm not sure why mathlib4 has all those dependencies. As far as I know it doesn't use them at all, but I think lake added them automatically?

[Mario Carneiro]

std4 should have zero dependencies (other than lake), and mathlib4 should only depend on std4

[Mario Carneiro]

But I was afraid to make changes without some confirmation from someone who understands lake better

[Henrik Böving]

Lake added them automatically because doc-gen uses them and lake locks all transitive dependencies.

My point is, I can run lake -Kdocs=on update to update the manifest so it reflects the changes that doc-gen made to its own dependencies but that might in the process also change the commit hash of std4 and if that is incompatible with mathlib4 stuff will blow up during the build anyways so I'm not really sure how to proceed here.

[Mario Carneiro]

mathlib4 should be using an up to date std4

[Mario Carneiro]

I will do lake -Kdocs=on update for the bump-09-26 branch

[Mario Carneiro]

it didn't do anything, is that expected?

[Mario Carneiro]

that is, it used version https://github.com/leanprover/doc-gen4/commit/a2345380e861332fabecc61591cb274e61163a97

[Henrik Böving]

Sure since doc-gen's master didn't change yet that is expected^^ Right now the CI of doc-gen is broken because of the issue updated above so I didn't merge the PR that would fix it yet...if you are saying that I have a guarantee that mathlib4 always uses an up to date std4 I'll add the lake update to the CI and we'll see how that goes,

[Mario Carneiro]

oh oops it's -Kdoc=on for mathlib

[Mario Carneiro]

we should try to standardize those config flags

[Mario Carneiro]

I wouldn't say that it's always exactly up to date, but changes are usually propagated within a day

[Mario Carneiro]

pinning your versions is probably the right thing to do unless it's for a speculative build

[Henrik Böving]

It is for a speculative build, the doc-gen CI attempts to slip the new doc-gen into mathlib and build it in order to deploy docs4#, I added the update to the CI now let's see if it passes this time...

[Mario Carneiro]

I think what we need is a way to tell lake update to only update specified packages to the latest version and update other packages only to the versions required

[Henrik Böving]

Yes that would be awesome.

[Mario Carneiro]

in fact, I think that should be the default behavior, since lake knows which packages are requested by the user and which are transitive dependencies

[James Gallicchio]

Maybe worth discussing in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.22Perfect.20world.22.20dependency.20management :joy:

[James Gallicchio]

(Although that still feels a bit like a hacky heuristic, perhaps that's not so perfect-world...)

[Henrik Böving]

https://github.com/leanprover/doc-gen4/actions/runs/3138157000/jobs/5097168181 stil blowing up /o\

[Mario Carneiro]

note: bump-07-26 hasn't merged yet

[James Gallicchio]

It's so hard to parse what this log is saying when mathlib depends on doc-gen4 and doc-gen4 depends on mathlib :worried:

[James Gallicchio]

@Henrik Böving is it possible to split the CI job out from doc-gen4? and maybe have the mathlib4_docs repo run the CI job nightly?

[Mario Carneiro]

How exactly does doc-gen4 interact with other projects? Why does it need to be a dependency of mathlib?

[Mario Carneiro]

Is there some stub that std4 can ship that marks things up such that doc-gen4 has what it needs without having to be a dependency?

[James Gallicchio]

I think the idea is that doc-gen4 is a "dependency" of your project so that you can have docs as a build target. So, mathlib can generate its documentation by lake -Kdoc=on build mathlib:docs

[Mario Carneiro]

That sounds like it should be a lake feature

[James Gallicchio]

Probably, yeah

[Henrik Böving]

Okay one after the other

"and maybe have the mathlib4_docs repo run the CI job nightly?" I am already doing this already becuase: If mathlib4 pushes an update it does not have a job to push mathlib4_docs because: mathlib4 should not depend on doc-gen4 working all the time

"is it possible to split the CI job out from doc-gen4?" Yes, but for me building the docs of mathlib4 is sort of an integration test since its the only large scale Lean 4 project out there right now

Mario: It is a dependency because doc-gen4 provides something Mac calls a "facet" where I as a dependency can basically provide additional build targets (namely the docs one) to my dependent in order to allow you to build the docs directly yourself from lake without having to:

1. clone, build and run doc-gen yourself
2. ship doc-gen via elan which would actually require it to work on each nightly of course (and that's effort I cannot do)

[Mario Carneiro]

Thinking about how rust does it, it feels like we actually want doc-gen to be part of the core distribution - anyone should be able to get documentation for their project

[Henrik Böving]

Now to explain what is confusing me:

doc-gen does right now compile for me locally with the same nightly as master mathlib4
mathlib4 obviously also compiles
but: If i declare doc-gen as a dependency of mathlib, run lake update and lake build again stuff blows up hard, why is this happening?

[Mario Carneiro]

adding it to the bootstrap is not very attractive, but at least we should be able to get it working with high availability somehow

[Mario Carneiro]

I put the bump-07-26 on the queue, so maybe try your test again once it lands

[Henrik Böving]

Mario Carneiro said:

Thinking about how rust does it, it feels like we actually want doc-gen to be part of the core distribution - anyone should be able to get documentation for their project

We can do this, but I cannot make doc-gen4 work every day on my own, somedays its like...Lean broke some syntax so i have to land PRs in the doc-gen dependencies (I got commit permission in some by now which makes this easier), then Mac had some funky idea for Lake again and threw his whole API overboard and I have to rework the Lake integration and then there are of course sometimes just Lean API changes that are there and blow doc-gen up.

[Mario Carneiro]

that is one reason to add it to the bootstrap...

[James Gallicchio]

Yeah, I don't think the core team has the time to maintain it either right now :joy:

[Henrik Böving]

I mean if anyone wants to put put up with it in this state we can go ahead and put it into the core distribution but sometimes it takes me like a whole afternoon to break the stuff that's broken again and I don't see where we are pulling the manpower from to make this happen

[Mario Carneiro]

I've been trying to update std4, mathlib4 and mathport in "waves" where they all use the same nightly to make dependencies easier

[Mario Carneiro]

maybe doc-gen4 also needs to be part of that

[Marc Huisinga]

... FWIW, lean4-cli also appears to be broken since 09-25 due to "LCNF local context contains unused local variable declaration" errors.

[Mario Carneiro]

Oh, that's a good one to report

[Henrik Böving]

doc-gen4 usually tries to aim at whatever nightly I'm seeing on mathlib4 (because of course: doing meta analysis on the .elan files of mathlib4 is due to API/ABI breaking changes only possible on the same nightly) its just that sometimes I take a while to find time for that

[Henrik Böving]

Marc Huisinga said:

... FWIW, lean4-cli also appears to be broken since 09-25 due to "LCNF local context contains unused local variable declaration" errors.

If you could minimize that and report it to leanprover/lean4 that would be lovely!

[Mario Carneiro]

09-25 broke the world as a way to get feedback on the new code generator

[Marc Huisinga]

I didn't notice because it's in the example and test files, which don't get built :sweat_smile:

[James Gallicchio]

Mario Carneiro said:

I've been trying to update std4, mathlib4 and mathport in "waves" where they all use the same nightly to make dependencies easier

I think this is actually the only setup in which Lake works correctly :joy: handling other situations correctly requires much more sophisticated dependency management a la Rust cargo... A project I'd be happy to work on after grad applications are in :sweat:

[James Gallicchio]

Mario Carneiro said:

09-25 broke the world as a way to get feedback on the new code generator

ooh, that landed? awesome, I was wondering why my inline'd code broke :)

[Henrik Böving]

No the new code generator isn't active yet as in actively producing the binary, stage 1 of 3 are active and trying to do their job in addition to the current code generator. If you get any issue from updating to this that mentions stuff like "LCNF" do report it here we did it exactly because of this

[Mac]

Henrik Böving said:

then Mac had some funky idea for Lake again and threw his whole API overboard and I have to rework the Lake integration

Sorry, that I do have a tendency to do that. :rofl:

[Mac]

James Gallicchio said:

Mario Carneiro said:

I've been trying to update std4, mathlib4 and mathport in "waves" where they all use the same nightly to make dependencies easier

I think this is actually the only setup in which Lake works correctly :joy: handling other situations correctly requires much more sophisticated dependency management a la Rust cargo

While true, it should be noted that (outside of bugs) the problem here is not exactly the algorithm. Programmatically, Lake could be adapted rather easily to use a more common dependency algorithm. The main problem is that most of these algorithms are not compatible with Lean.

For instance, we can't use an NPM or cargo style algorithm because the dependency tree cannot have multiple versions of the same package. Furthermore, due to metaprogramming and the Lean core's frequent changes most updates are not generally backwards compatible meaning there is not as much leeway as there is in other languages for disparate versioning or proper semantic versioning..

[Mario Carneiro]

(Given infinite time,) I would really like to go over lake and find ways to simplify both the API and the internal implementation, but the main blocker is that I don't know how much of lake is considered "public external API" / features people are relying on vs things that are only there to hold the rest of it up.

[Mario Carneiro]

So stuff like documentation about what is public and what is not, and what the public functions are intended to do, is very valuable information

[Mac]

Mario Carneiro said:

I don't know how much of lake is considered "public external API" / features people are relying on vs things that are only there to hold the rest of it up.

This is a problem I actually had as well. That is, in the past, when I broke some things that I though were just "there to hold the rest of it up", I found that some users were already relying on them (e.g., mathport early on).

[Mario Carneiro]

Also information about how much use the more elaborate stuff gets in practice

[Mac]

Mario Carneiro said:

Also information about how much use the more elaborate stuff gets in practice

I would love this data! If we could figure out how to collect it, that would be great!

[Mac]

Until v4, I considered the API to be entirely unstable (i.e., only the DSL helpers were the public features). After v4, I consider the build API pretty stable. The one exception being a fix to avoid the Fact in examples like lake#114 that I hope to include in the next maintenance (which I hope to do soon -- ideally this weekend).

[Mario Carneiro]

There are currently 103 projects listed in https://github.com/topics/lean4, we could just pull all the lakefiles

[Mario Carneiro]

what is the "Build API", formally? Is there a specific list of functions you can enumerate?

[Mario Carneiro]

Is the definition of the monad itself considered part of that public API?

[Mac]

the files in Lake.Build and its imports

[Mario Carneiro]

see that's not a great list, unless you are being very careful about putting private on things

[Mario Carneiro]

you can't just say "all dependencies of X"

[Mario Carneiro]

that's going to have tons of crap in it

[Mac]

I would not say there is much in Lake that is non-public, most of it is useful in performing some action of some kind that a user might also want to replicate.

[Mario Carneiro]

I would hope it's more like "the functions in Lake.Build and only that"

[Mario Carneiro]

It's okay to have things public and unstable, that just means that users who use the feature have to be prepared for it to change

[Mario Carneiro]

but messaging around that is very important

[Mario Carneiro]

that allows you to draw a line between users who use the stable stuff and can enjoy a relatively pain-free upgrade process, and those who integrate tightly with the lake implementation and are hopefully either pinned or coordinate with lake itself

[Mac]

Yeah, I agree. For me, right now, the unstable parts are: The issue I mentioned around Fact and the package argument to targets/facets, the implementation of logging (but the log methods themselves are stable), the dependency resolution code, and the CLI code.

[Mario Carneiro]

is the CLI itself stable?

[Mac]

All CLI commands mentioned in the lake help are considered stable (i.e., breaking them is a major breaking change).

[Mac]

So not things like print-paths as that is tied to whatever is going on in the Lean core (or the undocumented check-self and resolve-deps).

[Mario Carneiro]

Looking at the stuff in Lake.Build.Monad, I don't see a single function people would want to call. Lake.Build.Context has a ton of monads and I really hope users don't have to interact with this. Maybe I'm just lacking imagination, what kind of project would actually use this stuff?

[Mario Carneiro]

Lake.Build.Actions, okay it's a little low level but I can imagine users calling these functions. It would be better to have a simpler API here though

[Mac]

Most of the monads end up being used a some point in a build code, so they are definitely relevant to end users to some degree (at least in what actions they support). Also, to clarify, as I allude to when mentioning logging, the definitions of the monad themselves are unstable (even if the monad itself is).

[Mario Carneiro]

Lake.Build.Index, those functions have some intimidating type signatures but I suspect they are actually user-facing.

[Mario Carneiro]

I'm guessing these functions are where the monad soup comes from

[Mario Carneiro]

But seriously I would like to see some non-toy code that uses these

[Mario Carneiro]

It seems like none of the lake tests call any of these functions

[Mac]

Mario Carneiro said:

Looking at the stuff in Lake.Build.Monad, I don't see a single function people would want to call.

Essentially all of these functions are needed to run a build from scratch, which a user may wish to do in a Lake script. For example, in the test script @Wojciech Nawrocki discussed in another thread.

[Mac]

Mario Carneiro said:

It seems like none of the lake tests call any of these functions

Yeah, I very lacking in non-trivial test coverage. :sad: Prior to v4, all of this code was considered internal (hence no tests). Now that the API is key part of v4,, I should add some tests (I just have not got around to doing so). There are some challenges as well: I am still what many of the uses cases of build API would look like, and many of the existing examples (e.g., doc-gen4, alloy, FFI code) have complex dependencies and are thus hard to reduce to tests.

[Mac]

One thing that might be nice is to have in the future is some new attributes that record the API characteristics of definitions (e.g., marking the names/types/bodies as stable/unstable).

[Mario Carneiro]

it's easy enough to define an unofficial attribute to that effect and use it on your own API

[Mac]

Definitely.

[James Gallicchio]

If you do, put it in a separate repo so I can use the same :) maybe at some point we can have linting that,

• for libraries, ensures "stable" identifiers' types only change when the package semver has a major change
• for users, warns usages of unstable types (and maybe unfolding any other package's definition, since terms are super brittle)

I'm not sure how this would interact particularly with stuff like simp lemmas, but I think with enough careful engineering this could be workable

[James Gallicchio]

@Mario Carneiro could you remove doc-gen4 from the mathlib lakefile entirely? since the CI isn't building docs anyways, I don't think it should break anything, and it's locking doc-gen4 dependencies (e.g. xubaiw unicode) to month-old revisions, since the doc-gen4 revision is the old one.

[James Gallicchio]

(after it's removed, I think doc-gen4 CI should be building again)

[Mario Carneiro]

shouldn't the fix be to upgrade it then?

[James Gallicchio]

The upgraded doc-gen4 revision isn't on doc-gen4 main. So I guess you could also switch the lakefile to depend on the upgrade-lean branch of doc-gen4. But if mathlib isn't using doc-gen4 right now it seems overly complicating things for it to still pin dependency versions.

[Mario Carneiro]

Can't this be done on a branch?

[Mario Carneiro]

and/or using the config parameter which exists exactly for the purpose

[James Gallicchio]

(which config parameter?)

[Mario Carneiro]

the mathlib lakefile has this:

meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

[Mario Carneiro]

AFAICT that's the correct invocation so I'd rather not change it unless the official recommendation changes

[Mario Carneiro]

but if you need a mathlib commit that changes it you should be able to do so on a branch

[James Gallicchio]

Mario Carneiro said:

the mathlib lakefile has this:

meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

Ah, yeah, but the manifest still lists the revisions (and lake doesn't distinguish between manifest entries that are/aren't used when doing dependency resolution)

I can make a branch and see if I can figure out how to get this unstuck -- could I get push perms on mathlib?

[Henrik Böving]

Okay I think I'm starting to see an issue here. If I modify the lakefile of mathlib4 like so in my CI:

require «doc-gen4» from ".." / "doc-gen4" with NameMap.empty

and run lake update with the doc flag on I get:

 info: Found dependency `doc-gen4`
Using `main` at `b07faa65fe58882da6322aa9bfe480509fee8c76`

Which is indeed master but I am expecting lake here to just use the revision in the doc-gen4 directory which is most definitely not master but the update-lean branch.

[Henrik Böving]

@Mac is this behaviour inteded? If it is, how can I force lake to actually use the revision in that directory?

[James Gallicchio]

I wonder if it'd work for the CI to replace "main" in the mathlib lake file with the doc-gen4 commit's git hash

[Henrik Böving]

Most likely yes but then the CI will not be able to review PRs anymore correctly (assumming of course that anyone will ever write significant PRs /o\)

[James Gallicchio]

Doesn't the CI have access to the git commit that it is being run on? i.e. on a PR we could inject the PR's git hash

[James Gallicchio]

It would bar you from testing locally which is unfortunate

[Henrik Böving]

Declaring a git dependency in lake requires a URL though...I guess we could try to tickle that one out of git remote get-url as well though...

[James Gallicchio]

lemme see what the github actions CLI exposes

[James Gallicchio]

The URL can be passed into the script as $GITHUB_SERVER_URL/$GITHUB_REPOSITORY, and the commit hash as $GITHUB_SHA

[James Gallicchio]

which might be cleaner than pulling from git log/remote. unsure

[Henrik Böving]

Hah, of course sed wont like if i just sed -i "s/\"https:\/\/github.com\/leanprover\/doc-gen4\" @ \"main\"/\"$docgen_url\" @ \"$GITHUB_SHA\"/" lakefile.lean because $docgen_url contains slashes...how do you automatically escape slashes in a variable in a shell script? :D

[Henrik Böving]

Hah, one could of course also use another delimiter, what a wonderful tool sed is...

[James Gallicchio]

This is beyond my knowledge. Time to consult the stackoverflow texts.

[Henrik Böving]

The solution is of course the other delimiter as mentioned above: sed -i "s|\"https://github.com/leanprover/doc-gen4\" @ \"main\"|\"$docgen_url\" @ \"$GITHUB_SHA\"|" lakefile.lean

[Damiano Testa]

You like living dangerously: really the pipe symbol |? I normally shift to =!

[James Gallicchio]

My oh my. I'm excited for the day when we can write CLI scripts in Lean instead.

[Henrik Böving]

Gaaaahh, GITHUB_SHA is not the current commit in a pull request ffs... https://github.com/orgs/community/discussions/26325

[James Gallicchio]

corentingiraud coming in clutch :joy: this is impressively hard

[Henrik Böving]

He is lying though (well probably not on purpose) that variable is empty as well for whatever reason.

[Mac]

Henrik Böving said:

Declaring a git dependency in lake requires a URL though...

It doesn't have to be a full URL, you can just use a filepath. See, for instance, Lake's own git example.

[Mac]

Henrik Böving said:

Hah, of course sed wont like if i just sed -i "s/\"https:\/\/github.com\/leanprover\/doc-gen4\" @ \"main\"/\"$docgen_url\" @ \"$GITHUB_SHA\"/" lakefile.lean

You could also just pass these vairables to Lean/Lake as configuration options via -K and use get_config to access them. The elements of the syntax support arbitrary terms.

[Henrik Böving]

@Mac I have another question regarding the update mechanism, so I have convinced lake in mathlib to use the proper doc-gen version now, then I run this in the mathlib repo:

λ lake -Kdoc=on update
Found dependency `Cli`
`«doc-gen4»` locked `nightly` at `80b783a8905a4e8a29ced841abb64f710bc86f06`
Using `master` at `112b35fc348a4a18d2111ac2c6586163330b4941`
Found dependency `leanInk`
`«doc-gen4»` locked `doc-gen` at `439303af06465824588a486f5f9c023ca69979f3`
Using `master` at `439303af06465824588a486f5f9c023ca69979f3`
Found dependency `doc-gen4`
Using `upgrade-lean` at `2fc57e0eecd031201f9315823daa1cf9cec8e2f3`
Found dependency `Unicode`
`«doc-gen4»` locked `main` at `3a74ad4a69a3720ad8bd5f50a3233fe393f3f38e`
Using `master` at `25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29`
Found dependency `mathlib`
Using `master` at `ecd37441047e490ff2ad339e16f45bb8b58591bd`
Found dependency `std`
Using `main` at `8dc73e59a2e682260bd4b92c0ddee14d36fc6518`
Found dependency `lake`
`«doc-gen4»` locked `master` at `2cc00e4e08473939842d823fd753dcac891ab709`
Using `master` at `6cfb4e3fd7ff700ace8c2cfdb85056d59f321920`
Found dependency `CMark`
`«doc-gen4»` locked `main` at `8c0f9c1b16ee8047813f43b1f92de471782114ff`
Using `master` at `8c0f9c1b16ee8047813f43b1f92de471782114ff`

Why is it just straight up ignoring the versions that doc-gen has locked? For Cli its even using a different branch:

`«doc-gen4»` locked `nightly` at `80b783a8905a4e8a29ced841abb64f710bc86f06`
Using `master` at `112b35fc348a4a18d2111ac2c6586163330b4941`

why?

[Mac]

@Henrik Böving lake#85 (comment) -- fixing this is part of the updates I am currently work on for v4.1.0.

[Henrik Böving]

Mhm mhm...well I guess in the mean time I can just delete the manifest.json in hte CI and regenerate it since mario promised std4 wont break :tm:

[Henrik Böving]

Hurray: docs4#Std.RBTree

[Henrik Böving]

@Mac https://github.com/leanprover/doc-gen4/blob/main/lakefile.lean can you fix the lakefile for leanprover/lean4:nightly-2023-04-11 please? :pleading_face:

[Mac Malone]

@Henrik Böving Could you give me some idea of what broke and why? I have not changed Lake recently, so I am out of the loop as to what needs fixing.

[Henrik Böving]

Oh. Well the lakefile.lean doesn't typecheck on the latest toolchain anymore.

error: ././../doc-gen4/lakefile.lean:74:11: error: unknown identifier 'Fact'
error: ././../doc-gen4/lakefile.lean:74:53: error: unknown identifier 'Fact.mk'
error: ././../doc-gen4/lakefile.lean:105:2: error: invalid field 'bindAsync', the environment does not contain 'Lake.CustomData.bindAsync'
  coreJob
has type
  CustomData (Package.name docGen4Pkg, `coreDocs)
error: ././../doc-gen4/lakefile.lean: package configuration has errors

[Henrik Böving]

So I was blindly assuming this was another case of, Mac has decided to redesign the API again :P

[Mac Malone]

@Henrik Böving Looking at the lean4-master, this is apparently @Gabriel Ebner's doing where he deleted the Fact class in this commit. Let see if we can rope him in to explain what how the new code works and how to it can be used to fix doc-gen4.

[Gabriel Ebner]

As you can see in the commit that Mac linked, all that happened is that Fact (pkg.name = n) was replaced by PackageName pkg n. So you need to write it like this now:

    have : PackageName docGen4Pkg _package.name := ⟨h⟩

[Henrik Böving]

What about bindAsync?

[Gabriel Ebner]

The lakefile builds just fine for me with that line. I only get the bindAsync error if I remove the have.