nightly-2024-03-14

Stream: nightly-testing

[Kim Morrison]

Just noting that https://github.com/leanprover/lean4/pull/3667 is arriving in the next nightly, which enforces that "theorems are Props". I'm hoping this will not be too bad: we had this in community Lean 3.

[Jireh Loreaux]

I think it should be fine because we already have the defLemma linter.

[Kim Morrison]

Oh dear, release of nightly-2024-03-14 failed because of a recurrent problem in our CI in the fsanitize build. :-(

[Kevin Buzzard]

Is this related to https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean4.3Amaster/near/426709481 ?

[Kim Morrison]

No. The fsanitize build is a special build that is meant to detect memory leaks. It has been failing intermittently and in apparently unrelated places recently. We're still getting to the bottom of it ...

[Kevin Buzzard]

Is it related to https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean4.3Amaster/near/426738973 ? :-)

[Kevin Buzzard]

Not that it matters -- if someone is on the case I'll stop worrying for now :-)

[Kim Morrison]

I'm having trouble telling which message your linking to, @Kevin Buzzard. Perhaps a lean PR number is more useful?

[Kevin Buzzard]

I'm just saying "is the recurrent problem in CI fixed yet?"

[Kim Morrison]

Yes.