Zulip Chat Archive

Stream: mathlib4

Topic: MathlibTest.TransImports

Kim Morrison (Feb 06 2025 at 00:35):

@Damiano Testa, sorry to have so many requests, but could you take a look at MathlibTest.TransImports are change it so it is not testing details of Lean internals? I just had to change this on nightly-testing, and I would like to avoid this issue breaking a lean-pr-testing-NNNN branch, which would potentially be annoying.

Damiano Testa (Feb 06 2025 at 06:36):

Sorry about that! #21492.

Last updated: May 02 2025 at 03:31 UTC