Troubleshooting github actions and blueprint compilation

Stream: new members

[Laura Monk]

Hello!
I have been setting up a new project (here) using this template. Unfortunately I have been having a lot of red dots in the action section, which mostly leave me very puzzled. I never really know what to do, whether there is something actually wrong or just a little change that needs to be made. So, I guess, my question is: how do I proceed when the actions do not work? I think the only thing I changed recently is the blueprint and it does not compile any more, which is a bit mysterious to me. But it is not the first time and I would like to have a smoother experience setting up the project.

[Kevin Buzzard]

Ooh -- I had the exact same problem in one of my repos. Here's a thread about it #general > Can't update BrownianMotion project @ 💬 .

[Kevin Buzzard]

@Pietro Monticone are you able to advise?

[Ruben Van de Velde]

Looks like --global-option was removed: https://github.com/pypa/pip/issues/11859

[Kevin Buzzard]

Right -- but this has already been fixed here https://github.com/leanprover-community/docgen-action/pull/11/files

[Ruben Van de Velde]

Ah, but @Laura Monk seems to have copied the blueprint workflow from somewhere rather than using that action

[Ruben Van de Velde]

I suspect that if you copy the file at https://github.com/ImperialCollegeLondon/FLT/blob/96f5ac1c6c21628f3a5ec931086ebbbadbb84a05/.github/workflows/blueprint.yml (replacing any occurrences of "FLT"), it will work again

[Laura Monk]

Thank you very much for looking into this! I'll try this on Monday and will let you know.

[Pietro Monticone]

Hi @Laura Monk, sorry for the delayed response. I'll open a PR fixing the issue soon.

[Pietro Monticone]

Done https://github.com/lauramonk/FriedmanStrongConv/pull/5

[Pietro Monticone]

PS: I’ll soon open a PR on LeanBlueprint to update the entire template and integrate all the new actions we have developed.

Once that is merged, I will update the LeanProject README accordingly, so that this issue is resolved for all new projects.

[Laura Monk]

Hi @Pietro Monticone, thank you so much for looking into this and the fixes! And, more generally, the template: it is helping tremendously with getting started in this new project, I am very excited.

[Laura Monk]

Ok, I merged the PRs but it looks quite unhappy now (many errors). Not sure if I was supposed to do something different?

[Pietro Monticone]

The PR solved the issue mentioned above, but not all the other issues I didn't know about :sweat_smile:.

[Laura Monk]

Makes sense! I'll try and chase the errors :)

[Laura Monk]

I guess a lot are due to me, but I am also getting a whole block of
Warning: Unknown package «doc-gen4», predicted module name: «docGen4». If this is the wrong module name and causes a cache miss, please open an issue on leanprover-community/docgen-action.

[Pietro Monticone]

There is a simple checkdecls error. It's telling you that some declarations (LocallyFiniteAt, degree, LocallyFinite, IsRegularOfDegree) are missing in your Lean codebase.

[Laura Monk]

Thanks, do you think that's it? I got concerned by the warnings at the beginning (Unknown package «doc-gen4», predicted module name: «docGen4" etc)

[Pietro Monticone]

The other one can be easily fixed by removing the unnecessary [[require]] field in your lakefile.toml as follows:

name = "FriedmanStrongConv"
defaultTargets = ["FriedmanStrongConv"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.23.0-rc2"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"

- [[require]]
- name = "«doc-gen4»"
- git = "https://github.com/leanprover/doc-gen4"
- rev = "main"

[[lean_lib]]
name = "FriedmanStrongConv"

[Pietro Monticone]

I can open a quick PR right now to fix the last one mentioned.

[Laura Monk]

I'll fix it now thank you!

[Pietro Monticone]

Ok, great. You're welcome.

[Laura Monk]

It's green :tada:

[Pietro Monticone]

Great! Happy to help.

[Laura Monk]

Hi, Unfortunately the CI broke again today here, not sure how (I had only changed a few references as it did). I tried to update, probably made a mess, tried to use the blueprint workflow from FLT as suggested above, but it is still red. Could I please ask for help?

[Pietro Monticone]

I’ll take a look at it later today.

[Laura Monk]

Thank you!

[Bryan Gin-ge Chen]

This looks like it's most likely related to some ongoing issues with github: #rss > GitHub Status - Incident History @ 💬

I suspect this will go away on its own after a few hours.

[Laura Monk]

Oh, thanks, I had a look there but it had not been posted yet. Fingers crossed!

[Laura Monk]

All good now thank you and sorry for the freak-out!