unable to bump

Stream: FLT

[Kevin Buzzard]

so FLT#273 is still held up on "uncaught exception: parser 'subscript' was not found", i.e. blocked on lean4#6325 . It's just beginning to get a bit frustrating that we can't bump mathlib, but I still have plenty of other FLT-related things to think about. Is there any way around this issue or do I just have to wait? The bump branch builds fine on my machine.

[Yaël Dillies]

One solution would be to temporarily remove the checkdecls call in CI

[Pietro Monticone]

Yes, and it might be helpful to open a task issue as a reminder to uncomment this once lean4#6325 is merged.

[Pietro Monticone]

@Kevin Buzzard To make sure the checkdecls and most of the other CI steps will pass you can still locally run the run_before_push.sh here.

[Kevin Buzzard]

So I get

buzzard@buster:~/lean-projects/FLT$ leanblueprint checkdecls
uncaught exception: parser 'subscript' was not found
Command 'lake exe checkdecls blueprint/lean_decls' returned non-zero exit status 1.
buzzard@buster:~/lean-projects/FLT$

and

buzzard@buster:~/lean-projects/FLT$ ./scripts/run_before_push.sh
Checking if you are in the correct directory...
[snip]
✅ Web version of the blueprint generated successfully.
Checking if Lean declarations in the blueprint match the codebase...
uncaught exception: parser 'subscript' was not found
❌ Error: Some declarations in the blueprint do not match Lean declarations in the codebase.
Press any key to exit...

But you're suggesting that it's OK to push anyway, and presumably I get a red x on the repo, but you're saying that this is not the end of the world?

[Yaël Dillies]

If you remove the checkdecls step from CI, then you won't get the :cross_mark: on the repo

[Kevin Buzzard]

Perhaps it's about time I learnt something about CI for my own project.

[Pietro Monticone]

Just comment out from lines 118 to 120 included here https://github.com/ImperialCollegeLondon/FLT/blob/main/.github/workflows/blueprint.yml

[Pietro Monticone]

In the bump PR https://github.com/ImperialCollegeLondon/FLT/pull/273

[Kevin Buzzard]

I had independently come to the conclusion that this might be the thing to do (and also that to comment out a line I use #), but what I don't understand is why is the file blueprint.yml being parsed when I make a PR?

[Ruben Van de Velde]

It defines what jobs github runs when you make a pr

[Ruben Van de Velde]

In particular, line 3-26 define when things happen, and 15-25 say "when you make a pr"

[Kevin Buzzard]

What is telling github "look at the file blueprint.yml"? Or is it looking at all the files in .github all of the time? (just to be clear, I'm not completely computer-illiterate, but I've never looked in a .github directrory before)

[Shreyas Srinivas]

Briefly, github looks for all yml files inside that folder for tasks

[Shreyas Srinivas]

Some programs actively tell computers to "do something". Sometimes there are already "do something" programs like github which read a "roadmap" that you put in specific sorts of files in specific places. Here Github is the "do something" program. It is checking .github for all the "roadmaps" and doing stuff that they say.

[Kevin Buzzard]

OK, so hopefully I disabled checkdecls in FLT#273 and I opened the issue FLT#287 to track this.