automatically updating project

Stream: lean4

[Jon Eugster]

I have a script which periodically updates a lean project using lake update -R && lake build.

Now I just had a failure where lake update -R just went into an infinite loop without recovery. Deleting .lake/ solved the issue, but I'd prefer not to call rm -rf .lake/ just preemptively on every update.

• Is there a recommendation for a more stable updating procedure? Would lake clean -R && lake update && lake build make a difference?
• Are there any recommendation on how to debug this next time to provide a useful bug report? My hunch is that some download got corrupted (no space left or bad connection) and then lake could not recover next time it tried.

[Sebastian Ullrich]

A stacktrace would be very helpful for that

[Mac Malone]

Jon Eugster said:

Now I just had a failure where lake update -R just went into an infinite loop without recovery.

That seems like a serious bug that should never happen! I think the goal should just be to fix it. More information would be very helpful!

[Jon Eugster]

It's probably not that useful, but @Mac Malone here are the things I could read from the system logs:

Logs and stuff

The first error message started on Dec 2, which is exactly after mathlibs bump to v4.4.1-rc1:

Dec  2 12:00:01 adam lean4web: Starting build.
Dec  2 12:00:04 adam lean4web: error: ./.lake/packages/mathlib/lakefile.lean:6:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
Dec  2 12:00:04 adam lean4web: error: ./.lake/packages/mathlib/lakefile.lean: package configuration has errors
Dec  2 12:00:04 adam lean4web: Finished in 0:3 min.

I guess this is a bit surprising, but I think I can explain that: lake update -R ran on v4.3.0, mathlib's post-update hook would change the toolchain to v4.4.0-rc1, but to do so, mathlib's v4.4.0-rc1-lakefile would first need to be parsed in v4.3.0, which it couldn't. Am I reading this right? Guess I just need to add this well-known workaround back to the script:

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain

Then these error message continued until Dec 5, where it started to just produce processes that kept running infinitely.

Dec  5 18:00:01 adam lean4web: Starting build.
Dec  6 00:00:01 adam lean4web: Starting build.
Dec  6 06:00:01 adam lean4web: Starting build.
...

The corresponding mathlib PR and the 4 PRs before that seem to be just ordinary PR's.

Unfortunately, I already restarted the server, so there are no stacktraces I could access anymore. But before restarting I saw this, indicating that they indeed didn't stop:

stuck cronjobs from the last few days

adam@adam:~/lean4web$ pstree -aplcT -C age `pidof cron`
cron,975 -f -P
  ├─cron,2468858 -f -P
  │       ├─logger,2468861 -t lean4web
  │       └─npm run build_s,2468860
  │           └─sh,2468876 -c server/build.sh
  │               └─bash,2468877 server/build.sh
  │                   └─bash,2468881 server/build.sh
  │                       └─lake,2468883 update -R
  ├─cron,2570418 -f -P
  │       ├─logger,2570421 -t lean4web
  │       └─npm run build_s,2570420
  │           └─sh,2570437 -c server/build.sh
  │               └─bash,2570438 server/build.sh
  │                   └─bash,2570442 server/build.sh
  │                       └─lake,2570444 update -R
  ├─cron,2658795 -f -P
  │       ├─logger,2658798 -t lean4web
  │       └─npm run build_s,2658797
  │           └─sh,2658813 -c server/build.sh
  │               └─bash,2658814 server/build.sh
  │                   └─bash,2658818 server/build.sh
  │                       └─lake,2658820 update -R
  ├─cron,2735206 -f -P
  │       ├─logger,2735209 -t lean4web
  │       └─npm run build_s,2735208
  │           └─sh,2735224 -c server/build.sh
  │               └─bash,2735225 server/build.sh
  │                   └─bash,2735229 server/build.sh
  │                       └─lake,2735231 update -R
  ├─cron,2852274 -f -P
  │       ├─logger,2852277 -t lean4web
  │       └─npm run build_s,2852276
  │           └─sh,2852299 -c server/build.sh
  │               └─bash,2852300 server/build.sh
  │                   └─bash,2852304 server/build.sh
  │                       └─lake,2852306 update -R
  ├─cron,2963787 -f -P
  │       ├─logger,2963790 -t lean4web
  │       └─npm run build_s,2963789
  │           └─sh,2963805 -c server/build.sh
  │               └─bash,2963806 server/build.sh
  │                   └─bash,2963810 server/build.sh
  │                       └─lake,2963812 update -R
  ├─cron,3039969 -f -P
  │       ├─logger,3039972 -t lean4web
  │       └─npm run build_s,3039971
  │           └─sh,3039988 -c server/build.sh
  │               └─bash,3039989 server/build.sh
  │                   └─bash,3039993 server/build.sh
  │                       └─lake,3039995 update -R
  └─cron,3139496 -f -P
          ├─logger,3139499 -t lean4web
          └─npm run build_s,3139498
              └─sh,3139515 -c server/build.sh
                  └─bash,3139516 server/build.sh
                      └─bash,3139520 server/build.sh
                          └─lake,3139522 update -R

[Utensil Song]

This is caused by lean4#2858, which has detailed explanations in the PR. The workaround is suggested here.

[Jon Eugster]

Thanks for digging that out. The fix you linked to is essentially the same I mention with curl, both just copy the relevant toolchain in manually.

I guess the take-away here is that mathlib's update-hook doesn't quiet work if you need it to be reliable.

The more interesting part about this log was the second half, but I'm sad I don't have enough information on that one to get anywhere

[Utensil Song]

The technical reason for why the post_update hook didn't work, is:

1. the old lake runs lake update
2. it got a new Mathlib, containing its new lakefile, using a new lake feature, like leanOption in your case
3. the old lake can't process the new lakefile, so it failed with the error you see, before ever getting to process and execute the post_update defined in Mathlib's new lakefile

This is explained here.

[Mario Carneiro]

The second bug is that when lake update fails in (3) during elaboration, it leaves a olean.trace file which is empty, which is not valid json and so if you run lake update with new lake it will still complain unless you pass -R

[Utensil Song]

Very subtle indeed

[Jon Eugster]

And do you also know how this lead then to the process lake update -R just hanging up and not terminating for days, and also not complaining? That was the original question. All the things you describe are just part of how did we get lake in a bad state to start from.

[Mario Carneiro]

nope

[Utensil Song]

Do you have other lake processes on the same server? Possibly triggered by other users. Could it be lake waiting on another lake process on the same directory? I observed this before, but I'm not sure if such behavior is still there.

[Jon Eugster]

maybe it could be that one process crashed (maybe for outside reasons) without removing the lockfile and then in future all processes just waited, that's not a bad idea at all!

[Utensil Song]

The first bug is known to complain and exit. The second bug also exits immediately too (I've made .lake/lakefile.olean.trace empty):

% lake update
error: compiled configuration is invalid; run with `-R` to reconfigure

lake -R will recreate the .lake/lakefile.olean.trace whether it's empty or incomplete.

Also, I can't observe lake blocking on each other now.