leanproject upgrade delay?

Stream: general

[Adam Topaz]

I wanted to use some fresh new mathlib features in a (branch of) lean-liquid, so, as one usually does, I used leanproject upgrade-mathlib and expected to be able to use these new features. However it looks like this command did not pull the latest commit from the master branch of mathlib. Is this expected?

I also tried making a new project with leanproject new test and the same thing happens -- mathlib is not completely current.

I'm mostly wondering whether this is expected behavior and things should be updated after some time, or if there are some other issues.

Some additional info: leanproject pulls the following mathlib commit:
394719f58c3bdb39ef811d8ec76fc120a631975d
but manually using git pull origin master in the _target/deps/mathlib folder gives a more recent commit:
a5b7de0a178fc31eb6a12b2e62c68a0ea8e63a89 (as expected)

[Bryan Gin-ge Chen]

Ah, I see the issue.

[Bryan Gin-ge Chen]

GitHub deactivates scheduled GitHub actions workflows if a repo hasn't been active in more than 2 months. So I went to https://github.com/leanprover-community/azure-scripts/actions and re-enabled them.

[Adam Topaz]

Ah!

[Bryan Gin-ge Chen]

I manually re-ran the "Update lean-3.. branch" job just now, so it should be fixed.

[Bryan Gin-ge Chen]

This has happened before; we should probably see if we can set up some kind of advance notification for the maintainers.

[Adam Topaz]

Or we could set up another Cron job there to make a commit to that repo with a comment or something every month :wink:

[Adam Topaz]

Or is GitHub clever enough to see through such a trick?

[Bryan Gin-ge Chen]

No idea! Could be worth trying.

[Julian Berman]

That indeed does work.

[Julian Berman]

At least until GitHub changes the condition in the obvious way where the 60 day limit requires a non-action to commit to the repo. But for now yeah folks do that (they have a second action that keeps the first action alive).