lake silence

Stream: lean4

[Patrick Massot]

I couldn’t find a GitHub issue specifically about that, but let me check here: is there already an issue about the fact that lake always starts by printing nothing for at least 15 seconds when updating? Does anyone understand what it does? Could we get a message about it at the very beginning?

[Patrick Massot]

I suspect it tries to print stuff but this is somehow blocked and printed all at once when it’s done.

[Jon Eugster]

I've experienced that too, and I get this especially in a project which imports mathlib: it feels like the message

info: mathlib: cloning https://github.com/leanprover-community/mathlib4

is only displayed after it's done cloning instead of beforehand. (but didn't investigate further)

It sounds like the following conversation is related: #lean4 > lake new ... math gives `Invalid lake configuration`

[Patrick Massot]

Jon Eugster said:

it feels like the message

info: mathlib: cloning https://github.com/leanprover-community/mathlib4

is only displayed after it's done cloning instead of beforehand. (but didn't investigate further)

I agree this is what it feels like.

[Kim Morrison]

@Mac Malone? I've experienced this too, and agree it is very disconcerting.

[Kim Morrison]

@Mac Malone, is there an open issue for this? I still can't find one.

[Mac Malone]

@Kim Morrison Its seems to be rebirth of lean4#5615, apparently some failure not caught by the original tests. A new issue would be welcome.

[Kim Morrison]

@Mac Malone, I've reopened lean4#5615 -- it seems last week Kevin reported the same issue.