lint and build

Stream: mathlib4

[Sébastien Gouëzel]

In the current staging workflow for bors (https://github.com/leanprover-community/mathlib4/actions/runs/12071366218/job/33662964049), the build has failed right away because an import is not good, with the message

✖ [?/?] Computing build jobs
error: no such file or directory (error code: 2)
  file: ././././Mathlib/CategoryTheory/Sites/InducedTopology.lean
Some required builds logged failures:
- Computing build jobs
error: build failed

In particular, the cache step has not uploaded anything. But now the lint step is building all of mathlib, and all this will be wasted because no file will be uploaded to the cache.

I don't know anything about CI, so I have no idea if this can/should be fixed, but I wanted to point this out in case someone knows better.

[Johan Commelin]

Thanks! I'm sure we can try to handle such a case better. For now I would just cancel the linting step, I think.

[Johan Commelin]

Ooh, it is already done, it seems.

[Sébastien Gouëzel]

Yeah, it just finished.

[Damiano Testa]

It should be possible to make the linting only happen if lake build --no-build is successful. I would have to check whether that lake option is working as intended now, though (and I won't be able to do this soon, either).

[Damiano Testa]

If someone can confirm whether no-build works, then simply changing the linting step to if lake build --no-build; then [whatever it is now]; else exit 1; fi may do the trick.

[Yaël Dillies]

I find it very useful for linting to happen even the build failed, because it replays all the files that had an error. This makes them much easier to find, as compared to the build mathlib step which is a sea of the form

✔ [5666/5675] Built Mathlib.NumberTheory.EulerProduct.DirichletLSeries
✔ [5667/5675] Built Mathlib.NumberTheory.Harmonic.ZetaAsymp
✔ [5668/5675] Built Mathlib.NumberTheory.LSeries.ZMod
✔ [5669/5675] Built Mathlib.Analysis.CStarAlgebra.Module.Defs
✔ [5670/5675] Built Mathlib.NumberTheory.FLT.Three

[Yaël Dillies]

... but I agree that my reliance on this is probably a hack. Would be great if we could just replay the build of the broken files in a separate CI step

[Sébastien Gouëzel]

Replaying the files in the lint step looks definitely good to me. What is weird here is that the lint step builds more than the build step.

[Sébastien Gouëzel]

i.e., lake exe runLinter Mathlib (the lint step command) fails later than the build step command lake build --wfail -KCI.

[Yaël Dillies]

Oh I see. Yes for sure one shouldn't outbuild the build

[Damiano Testa]

In this case, it seems that there was a non-existing import that prevented the actual build step from running, but the failure settings of the lint step are different, so it still build the rest of mathlib anyway. Is this correct?

[Damiano Testa]

I still think that if no-build works, then it is the way to go: it reports the issues, but does not go ahead to build anything new.