How to test making a core change with mathlib?

Stream: nightly-testing

[Michael Rothgang]

Hi! I have a basic question which I'm sure is documented somewhere, but I cannot find that documentation. Points to RTFM are very welcome; I'd read the manual if I could find one! I'd like to test the change in lean#12007 (tweaking some pretty-printing --- i.e., should not cause any additional build failures anywhere :fingers_crossed:).

• My first attempt was simply making a PR to the main core branch. That didn't generate a mathlib toolchain. Would there have been a label to apply to the core PR, to automatically generate a mathlib toolchain for me?
• Reading the sticky comment, I rebased my PR on the nightly-with-mathlib branch... still no luck.
• In a final attempt, I forked the nightly-testing repository, checked out the nightly-testing branched and switched the lean toolchain to the one from my PR: #33991. Running lake build locally yields failures in batteries, i.e. unrelated to my PR.

What am I doing wrong/what should I be doing instead?

[Johan Commelin]

https://leanprover-community.github.io/contribute/tags_and_branches.html says

For any PR that potentially affects Std or Mathlib, you should base your PR off the HEAD of the nightly-with-mathlib branch. In that case, a lean-pr-testing-NNNN Mathlib branch is created, described in detail below, and results from this branch are reported via comments in the PR discussion.

Clearly this information is out of date. I think that entire page needs a thorough rewrite.

It seems to me that the branch should have been created in the mathlib4-nightly-testing repo, but that hasn't happened.

[Johan Commelin]

Isn't the issue that there are still other CI steps failing on your PR to core?

[Michael Rothgang]

https://github.com/leanprover/lean4/blob/master/doc/dev/index.md has the same information (condensed) - so should probably also be rewritten.

[Michael Rothgang]

Johan Commelin said:

Isn't the issue that there are still other CI steps failing on your PR to core?

Fair... while I am rather surprised, let me try to investigate. First stumbling block is more outdated documentation: the snippet

# in the Lean rootdir
elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

fails with an error "not a directory: build/release/stage0". What's the correct incantation?

[Johan Commelin]

I'm sorry, but I don't know the answer. Hopefully someone from the FRO can chime in.

[Kim Morrison]

Johan Commelin said:

Clearly this information is out of date.

Sorry, what is out of date here? (Std should become Batteries.)

[Kim Morrison]

Michael Rothgang said:

fails with an error "not a directory: build/release/stage0". What's the correct incantation?

I think this is correct, but if you haven't done a build on the command line yet that stage0/ subdirectory won't exist yet.

[Kim Morrison]

Oh, I see

• All PRs to Mathlib should be made from branches of the Mathlib repository itself.
  • This is required for Mathlib's .olean caching mechanism.
  • Please ask on the zulip chat for "write" permission to Mathlib. Please write a sentence about your background and plans.

is outdated. I guess we need to explain how to ask for write access on the mathlib4-nightly-testing fork.

[Kim Morrison]

Kim Morrison said:

(Std should become Batteries.)

https://github.com/leanprover-community/leanprover-community.github.io/pull/776

[Kim Morrison]

Further revisions in https://github.com/leanprover-community/leanprover-community.github.io/pull/777, but this still needs careful review.

[Kim Morrison]

Looks pretty good to me.