Help -- CI broken

Stream: FLT

[Kevin Buzzard]

Currently we have an error "Error: Failed to CreateArtifact: Received non-retryable error: Failed request: (409) Conflict: an artifact with this name already exists on the workflow run" in the second "upload docs and blueprint artifact" thingy (why are there two)?

Screenshot-from-2024-08-04-11-05-00.png

Anyone know what's going on?

[Yaël Dillies]

You have a duplicated CI step. Do you see what I mean or should I open a PR?

[Kevin Buzzard]

Please feel free to open a PR, I don't even know where CI is stored

[Yaël Dillies]

CI is stored in the .github folder. Here are the relevant lines: https://github.com/ImperialCollegeLondon/FLT/blame/main/.github/workflows/push.yml#L103-L111

[Yaël Dillies]

flt#117 https://github.com/ImperialCollegeLondon/FLT/pull/117

[Yaël Dillies]

Whoops, wrong linkifier. Maybe someone here can fix it?

[Kevin Buzzard]

Ok I now know where the CI instructions are stored -- thanks! The step isn't duplicated, one says path: docs/ and the other says path: docs/_site. Why did you choose to delete the one you chose?

[Yaël Dillies]

Only one of them is used. I kept the docs/_site one since it's the one that my projects use and they work :shrug:

[Ruben Van de Velde]

Linkifier is FLT#117

[Damiano Testa]

The docs/_site means that the action is going to clone the repo to docs/_site. I wonder whether having chosen this path will affect the later step that does mv docs/docs .lake/build/doc. If CI fails, then maybe this one should change to mv docs/_stye/docs .lake/build/doc.

[Damiano Testa]

Anyway, working on CI is really like driving a car blindfolded: the implications of each step are really mysterious.

[Kevin Buzzard]

So the workflow is "push something and see if it works" rather than "test to see if it works and then push"?

[Damiano Testa]

Testing locally is always a good idea, but CI has a different set of rules, so not everything that works locally works in CI as is.

[Damiano Testa]

Usually, if you can make every step report some message it is very useful for debugging.

[Damiano Testa]

In this case, it worked, so everything is good!

[Damiano Testa]

But, for instance, when you ask to download your repo, unless you explicitly mention that you want to download all the repo, it just does a shallow clone, which means that you only get the current branch and no history.

[Damiano Testa]

So, maybe a better description is: if you know how to replicate exactly the steps that you run locally, then you are good! But knowing that is very hard, at least for me.

[Kevin Buzzard]

How do you test locally? I'm on Ubuntu

[Damiano Testa]

You run the commands one at a time and see whether they have the required effects. Some are "actions" so you should know what those are supposed to do.

[Damiano Testa]

For instance,

jobs:
  style_lint:
    name: Lint style
    runs-on: ubuntu-latest
    steps:
      - name: Check for long lines
        if: always()
        run: |
          ! (find FLT -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')

      - name: Don't 'import Mathlib', use precise imports
        if: always()
        run: |
          ! (find FLT -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')

[Damiano Testa]

is instructing the remote machine to run on ubuntu-latest the following steps:

! (find FLT -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
! (find FLT -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')

[Damiano Testa]

the rest is intended mostly as a comment to both you and the computer to try to make sense of what is going on.

[Damiano Testa]

So, likely, the first command is going to test for long lines (and you can see that there is grep .{101} somewhere in there and the second one is checking something about imports (and you can see that it is looking for lines that match exactly import Mathlib).

[Damiano Testa]

However, the next step is

  build_project:
    runs-on: ubuntu-latest
    name: Build project
    steps:
      - name: Checkout project
        uses: actions/checkout@v4
        with:
          fetch-depth: 0

and this is an "action" (actions/checkout@v4): this is a bundled set of commands that in this case is downloading the whole repository (so this you cannot really test locally).

[Damiano Testa]

The main takeaway is that every command that you issue has lots of "implicit" assumptions that depend on exactly what system you are using, in which timezone the command is run, what sorting convention you have for strings, and so on.

[Damiano Testa]

So, basically, you are writing commands on your computer that are supposed to work on a generic other computer.

[Damiano Testa]

That is why, sorting order, timezones, case-sensitivity, special characters in files are all quite problematic for CI and I think that every one of them has caused a CI failure at some point in mathlib in the last month or so.

[Patrick Massot]

Short version: setting up CI is a nightmare.

[Yakov Pechersky]

nektos/act is a nice way to model GitHub runners and workflows locally

[Kevin Buzzard]

(deleted -- hopefully solved)

[Kim Morrison]

CI is broken again

[Ruben Van de Velde]

Kim Morrison said:

CI is broken again

FLT#124

[Kevin Buzzard]

Thanks. I'm travelling and I don't seem to have a way of detecting this. Is there a way of getting a notification when I just blindly push to master (as I do a lot) and then CI breaks? Come October when I'm taking all of this very seriously I'm hoping to do better.

[Rémy Degenne]

That's not exactly what you are asking, but one thing you can do is protect your main/master branch (in Settings/Branches) by setting "Require a pull request before merging". Then as the owner of the repo you can still push to master, but you'll see a big warning in your terminal that you are overruling the branch protection.
It won't tell you when you broke master, but it will remind you that you should not push to master and should instead work on a branch and open a PR.

[Ruben Van de Velde]

I think this can work:
Screenshot-from-2024-09-09-13-46-15.png
at https://github.com/settings/notifications

But then you need to filter out the ones about FLT in your email client

[Kim Morrison]

@Kevin Buzzard, I think you better get used to not pushing to master. :-) This is what CI is for. If you push to master directly without waiting for a CI, every time you break it you prevent everyone else from working on the project.

[Kim Morrison]

(And if you're really going to get FLT "done", you're not going to have time to push to anything except the blueprint. :-)

[Yaël Dillies]

My two cents: I push to master on LeanAPAP and PFR, but I always run lake exe mk_all; lake build beforehand

[Kevin Buzzard]

OK I'll switch to always PRing. Thanks! I have no idea what I'm doing but am keen to learn.

[Kevin Buzzard]

OK I give up. CI is broken and I just spent about an hour trying to fix it. @Pietro Monticone your PR here deleted a bunch of stuff from lake-manifest.json -- was this intentional? I've tried to put it back; this may or may not be what's causing the CI issues.

[Pietro Monticone]

This should fix it https://github.com/ImperialCollegeLondon/FLT/pull/129.

I run the usual:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake -Kenv=dev update
lake exe cache get

But that didn't update doc-gen4 and dependencies. Now I have run:

lake -R -Kenv=dev update «doc-gen4»

and it updated correctly.

[Kevin Buzzard]

It didn't just not update doc-gen4, it deleted it from the manifest! Presumably this is the same phenomenon as this ?

[Pietro Monticone]

I tend to believe so too.

[Pietro Monticone]

I have just tested it locally, and the documentation builds without issues.

[Kevin Buzzard]

Yeah things are looking promising on github too :-) Thanks!