PR fail: Error: Process completed with exit code 1.

Stream: mathlib4

[Ralf Stephan]

Why is #14049 failing? I don't understand the log:

Run lake exe mk_all
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
✔ [1/8] Fetched proofwidgets:optRelease
✔ [2/8] Built Mathlib.Util.GetAllModules
✔ [3/8] Built Mathlib.Util.GetAllModules:c.o
✔ [4/8] Built Cli.Basic
✔ [5/8] Built mk_all
✔ [6/8] Built mk_all:c.o
✔ [7/8] Built Cli.Basic:c.o
✔ [8/8] Built mk_all
Updating 'Archive.lean'
Error: Process completed with exit code 1.

[Damiano Testa]

It is saying that there is an unexpected file in Archive.lean. Did you add or remove a file from there?

[Damiano Testa]

(Unexpected simply means that the file is not accounted for by the Archive.lean file, nothing else.)

[Damiano Testa]

Ah, should have clicked the link! So, when you add a file, try running lake exe mk_all (maybe with also the flag --git if you have files that are not part of the PR in Mathlib) to update the "import all" files. You will see that locally you should get the same output: Updating 'Archive.lean'. This is telling you that the script modified that file, since it should have found the new Archive/... file and added it. Now commit the new Archive.lean file and push!

[Damiano Testa]

(In case you care about these things, the reason CI fails is that the exit code of lake exe mk_all if the number of "import all" files that it had to modify. Thus, CI can only pass if there are no modifications to these files, compared to what the PR pushes.)

[Rida Hamadani]

I think a better error message for this would be nice

[Damiano Testa]

This step of CI has always been confusing: when it said "Check that all files are imported" there were also lots of questions about it. I am really not sure how to formulate unambiguously what this is flagging.

[Damiano Testa]

(Part of the reason is probably also that maintaining these "import all" files is not something that should be done so much, but that is another discussion.)

[Ruben Van de Velde]

Can it show the git diff output?

[Yaël Dillies]

What I find really confusing is that it stops CI entirely rather than letting it build mathlib (and giving me cache :pray:)

[Ruben Van de Velde]

Yeah, I mentioned that somewhere as well

[Damiano Testa]

I think that Michael has a PR adding a --check flag to mk_all and wants to use that in CI: maybe that would be a good place to suggest an improvement?

[Yaël Dillies]

In fact, since the mk_all step is a guaranteed easy fix, can't we put it after the build step?

[Yaël Dillies]

of course the better solution is to have a non-linear CI but it seems github is making that very hard...

[Damiano Testa]

I wonder whether we should have mk_all run

• before the build, but without the error being caught, so that CI builds all the files;
• and then again after the build, this time failing on errors...

[Ruben Van de Velde]

Yeah, it definitely needs to run before the build

[Michael Rothgang]

Damiano Testa said:

I think that Michael has a PR adding a --check flag to mk_all and wants to use that in CI: maybe that would be a good place to suggest an improvement?

It's #13617. @Ralf Stephan After that PR, the error message would become
The file 'Mathlib.lean' is out of date: run `lake exe mk_all` to update it.
Would this have been more understandable to you? Is there a different wording which would have been even better?

[Michael Rothgang]

Yaël Dillies said:

In fact, since the mk_all step is a guaranteed easy fix, can't we put it after the build step?

It depends on what your PR does. If your PR is merely adding a new file, having CI run and succeed is also confusing - since it's not testing the new code. If you refactor ten files and forgot to add a new leaf file, getting cache is obviously nicer.

[Michael Rothgang]

Damiano Testa said:

I wonder whether we should have mk_all run

• before the build, but without the error being caught, so that CI builds all the files;
• and then again after the build, this time failing on errors...

I like this idea! It seems like it would give the best of both worlds :-)

[Damiano Testa]

It's #13617. @**Ralf Stephan** After that PR, the error message would become
```The file 'Mathlib.lean' is out of date: run `lake exe mk_all` to update it.```
Would this have been more understandable to you? Is there a different wording which would have been even better?

I feel like we are closing in on the issue: the automation is telling what humans should be doing...

[Yaël Dillies]

Michael Rothgang said:

It depends on what your PR does. If your PR is merely adding a new file, having CI run and succeed is also confusing - since it's not testing the new code.

I think you misunderstood me. Schematically, I'm saying CI should run lake build; lake exe mk_all, not lake exe mk_all; lake build. Note that we can configure lake build to build all files in the Mathlib directory, not just the ones imported in the Mathlib file.

[Kim Morrison]

This would be a huge change to how lake build works, and contrary to how we currently want people to use lake build by default, so I would discourage Mathlib from doing this.

[Yaël Dillies]

Hmm... okay. Then maybe Damiano's lake exe mk_all (catching errors); lake build; lake exe mk_all is the way to go

[Damiano Testa]

I am testing this out in #14077.

[Damiano Testa]

I cannot seem to get past the "check the cache" stage on that PR.

[Damiano Testa]

The first lake exe mk_all notices the error, but the error is caught, lake build builds the extra file as well, the file appears to be uploaded, but lake exe cache get seems to not find it.

[Ruben Van de Velde]

Alternative: #14078

[Damiano Testa]

I like your version! I do not have a strong opinion on which following steps to perform anyway (e.g. Archive and Counterexamples). An argument in favour of adding them would be that if you added a file to Archive you would get nothing from this PR run, other than the same information that we had before the change.

[Damiano Testa]

Ruben, out of curiosity, I checked whether the "check the cache" step worked with your workflow as well, but it fails there too: #14079.

[Ralf Stephan]

Michael Rothgang said:

It's #13617. Ralf Stephan After that PR, the error message would become
The file 'Mathlib.lean' is out of date: run `lake exe mk_all` to update it.
Would this have been more understandable to you? Is there a different wording which would have been even better?

Yes, completely sufficient, thanks.

[Michael Rothgang]

I guess there's a third option, quite similar to what Yael proposed: just reorder the "lake build" and "mk_all" steps. No modification of lake build, which avoids the issue Kim pointed out, right?

In terms of user experience, that doesn't seem to have big downsides:

• if a branch just adds a leaf file, building the rest of mathlib is just hitting the cache. If a new file is imported in the relevant file, it will still get built -> good.
• if there is substantial rebuilding to be done, this can happen already, as Yael points out.
• CI still errors if an import-only file is out of date

[Michael Rothgang]

This feels slightly easier than the other CI changes - but I don't have strong preferences either way.

[Yaël Dillies]

I would still like to know: What would it take to have non-linear CI?

[Damiano Testa]

My view is that I would hope that the lake build step in CI is "what it should be" and "what it should be", in my opinion, is "a build of all the files in Mathlib. The fact that the new files in the PR have or have not been explicitly added to Mathlib.lean should not really matter. Moreover, would the final linting check be possibly different if the file is imported or not? That is also valuable information.

[Ruben Van de Velde]

I'm not sure I agree - if I add a leaf file and forget to add it to Mathlib.lean, I still want to see the errors on github

[Yaël Dillies]

Well, what about we (literally, not schematically) replace the lake build step by lake exe mk_all; lake build? Then we will build all the files, regardless of whether they have been added to Mathlib.lean

[Kim Morrison]

Yaël Dillies said:

I would still like to know: What would it take to have non-linear CI?

I think it's pretty straightforward. You can copy artifacts between build jobs (and indeed there are some github actions that make this relatively painless), and so all jobs that require build artifacts would have to have explicit steps to copy these artifacts (I guess they could just run cache get at every step, but I'd prefer to avoid this significant increase in hitting the cache).

[Damiano Testa]

Yaël, isn't what you say what both PRs linked above (Ruben's and mine) propose?