CI on Archive/

Stream: mathlib4

[David Renshaw]

after mathlib4#11507, some files in Archive don't build. Isn't CI supposed to catch that?

[David Renshaw]

(PR incoming to fix the Archive/ files...)

[David Renshaw]

mathlib4#11535

[Sébastien Gouëzel]

As you can see on https://github.com/leanprover-community/mathlib4/actions/runs/8350648107/job/22857519289, the build failed on Archive, but it was still marked as successful. There is indeed something fishy with our CI.

[Sébastien Gouëzel]

Also, the build archive step packs everything (including mathlib) and tries to upload it again...

[Sébastien Gouëzel]

and so does the build counterexample step.

[Damiano Testa]

I wonder if we should make the two steps

bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive -KCI | tee stdout.log"
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples -KCI | tee stdout.log"

in analogy with the master build step.

[Yaël Dillies]

@Mario Carneiro, the CI failure on Archive would have been caught had shake run on it. Is there a specific reason we are not running shake on Archive?

[Damiano Testa]

#11540 fails on the archive build failure and should work otherwise.

[Damiano Testa]

Now that the fix PR has been merged, I merged master in #11540, to make sure that now it passes its own CI.

[Damiano Testa]

Linting now, with successful previous steps.

This does not address the issue with re-uploading the cache, but maybe that can come later? There have been many changes to how CI works in the last week and I prefer to make atomic fixes...

[Damiano Testa]

Surprisingly, the lean4checker step failed!

Cloning into 'lean4checker'...
fatal: unable to access 'https://github.com/leanprover/lean4checker/': gnutls_handshake() failed: Error in the pull function.
Error: Process completed with exit code 128.

Rerunning the jobs.

[Patrick Massot]

gnutls_handshake() failed does not sound like a kernel type-checking issue…

[Damiano Testa]

Yes, I think that this is a transient error: it was the lean4checker step in CI, but not really the lean4checker talking.

[Damiano Testa]

I was simply showing surprise since I normally consider the lean4checker step as "the likeliest to pass".

[Damiano Testa]

The second run was successful!

[Thomas Murrills]

Hmm, I also got

error: > git clone https://github.com/leanprover-community/import-graph.git ./.lake/packages/importGraph
error: stderr:
Cloning into './.lake/packages/importGraph'...
fatal: unable to access 'https://github.com/leanprover-community/import-graph.git/': GnuTLS recv error (-54): Error in the pull function.
error: external command `git` exited with code 128

on a random PR (in a different spot, "build cache", not lean4checker), which seems at least superficially related.

[Thomas Murrills]

I wonder if this is a trend/something worth handling generically somehow...

[Thomas Murrills]

(Re-running the job makes it work, as expected.)

[Damiano Testa]

I believe that #11540 might be a fix for CI: it failed when Archive was broken and it works now that Archive is no longer broken.

[Mario Carneiro]

@Yaël Dillies said:

Mario Carneiro, the CI failure on Archive would have been caught had shake run on it. Is there a specific reason we are not running shake on Archive?

It would require either some changes to shake or some duplicated work to run it three times on Mathlib, Archive, Counterexamples

[Mario Carneiro]

because it will only suggest changes for files from the same project as the specified root file (as defined by the first component of the module name)

[Johan Commelin]

But shaking Archive and Counterexamples isnt very important, right? Those files are rarely imported elsewhere, so it also doesnt matter too much what their own imports are

[Mario Carneiro]

s/rarely/never/

[Mario Carneiro]

except possibly Counterexamples importing other Counterexamples? Not sure if that happens

[Yaël Dillies]

Johan Commelin said:

But shaking Archive and Counterexamples isnt very important, right? Those files are rarely imported elsewhere, so it also doesnt matter too much what their own imports are

The issue here is that there was a file A imported in a file B, which itself was imported in an archive file C, with C needing the content of both A and B. shake suggested removing the import A -> B, but because it is blind to the archive it didn't suggest adding the import A -> C.

[Yaël Dillies]

Mario Carneiro said:

it will only suggest changes for files from the same project as the specified root file (as defined by the first component of the module name)

Yes so this seems like a fundamental limitation which prevents shake from doing the right in the situation I just described

[Mario Carneiro]

Yaël Dillies said:

Johan Commelin said:

But shaking Archive and Counterexamples isnt very important, right? Those files are rarely imported elsewhere, so it also doesnt matter too much what their own imports are

The issue here is that there was a file A imported in a file B, which itself was imported in an archive file C, with C needing the content of both A and B. shake suggested removing the import A -> B, but because it is blind to the archive it didn't suggest adding the import A -> C.

I think this kind of cross-project analysis should be considered out of scope for shake. Because you can say the same thing about missing changes to the SphereEversion project or what have you

[Mario Carneiro]

Yaël Dillies said:

Mario Carneiro said:

it will only suggest changes for files from the same project as the specified root file (as defined by the first component of the module name)

Yes so this seems like a fundamental limitation which prevents shake from doing the right in the situation I just described

It's not a fundamental limitation, it's a basic filter performed at the beginning. The way shake works, it always computes information about every module imported from the specified root modules, it just suppresses errors originating e.g. in unshaken files in Lean

[Eric Wieser]

Damiano Testa said:

I wonder if we should make the two steps

bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Archive -KCI | tee stdout.log"
bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build Counterexamples -KCI | tee stdout.log"

in analogy with the master build step.

#11612 makes this change

[Damiano Testa]

There is also #11540 that does that change.