doc-gen4 problems on v4.22.0-rc1

Stream: nightly-testing

[Kim Morrison]

@Henrik Böving, might you be able to look at https://github.com/leanprover/doc-gen4/pull/302?

[Henrik Böving]

I fixed all but one error which I've asked Kyle about

[Kim Morrison]

I think the remaining error is actually a question for @Marc Huisinga, as the change occurs in lean#8511.

[Kim Morrison]

Ah, but @Marc Huisinga is on a tropical island.

[Henrik Böving]

Well he is not going to answer for the forseeable future :D

[Kim Morrison]

My guess is that we just call

  let (sigStx, infos) ← withTheReader Core.Context ({ · with currNamespace := n.getPrefix }) <|
    PrettyPrinter.delabCore t (delab := PrettyPrinter.Delaborator.delabConstWithSignature)

at least, it type checks. :-)

[Kim Morrison]

Are our tests in CI robust enough that this is worth a try?

[Henrik Böving]

I wouldn't expect something to fail if this prints out whatever, we probably have to visually inspect the doc-gen output to see if it did the right thing :tm:

[Kim Morrison]

Is there any doc-gen output that we can inspect merely by running CI?

[Henrik Böving]

I usually just run lake build DocGen4:docs and look at it locally

[Kim Morrison]

Well that was not what I was hoping to see:

info: stderr:
ld64.lld: error: undefined symbol: lean_inc_ref_cold

[Henrik Böving]

Did you lake clean in between?

[Henrik Böving]

that fixed this for me

[Kim Morrison]

Yeah, my voodoo fix is not right, lots of

PANIC at Lean.PrettyPrinter.Delaborator.delabConst Lean.PrettyPrinter.Delaborator.Builtins:95:35: unreachable code has been reached
backtrace:

[Henrik Böving]

:D

[Henrik Böving]

so we wait for our local pretty printing magician

[Kim Morrison]

@Henrik Böving, still there? I have another candidate fix (backport the code from before #8511!). doc-gen4 builds, how do I view anything after lake build DocGen4:docs?

[Henrik Böving]

you go to .lake/build/doc and run something like python3 -m http.server

[Kim Morrison]

Okay, superficially seems okay, at least, there are signatures. :-)

[Henrik Böving]

Great, I would personally still prefer for Kyle to sign off on that stuff or are we under pressure here?

[Kim Morrison]

No, it's fine to wait until tomorrow, as I'm going to fall asleep before I could get the Mathlib bump PR merged anyway.

[Kim Morrison]

@Kyle Miller, when you're coming to this, you'll see my "let's restore the pre lean#8511 code" in https://github.com/leanprover/doc-gen4/pull/302. Feel free to remove that commit and replace it with whatever is sensible. :-)

[Kyle Miller]

@Kim Morrison @Henrik Böving Updated the PR. I tested it locally, but it probably would be good to spot check the output once more.

[Henrik Böving]

will do, thanks!

[Henrik Böving]

Yeah it looks fine to me :thumbs_up:

[Kim Morrison]

'd