Zulip Chat Archive

Stream: general

Topic: oleans broken in CI

Scott Morrison (May 22 2022 at 23:15):

I tried to review #14304, but the oleans seem to be broken: leanpkg build recompiles a bunch of stuff about dfinsupp that isn't touched by the PR.

Eric Wieser (May 22 2022 at 23:21):

This happens a lot when CI fails (because then lean build runs only once) but I haven't seen it before when it succeeds (when lean build runs twice)

Eric Wieser (May 22 2022 at 23:21):

I guess we need to add a third lean build now to CI?

Eric Wieser (May 22 2022 at 23:22):

(You can fix this type of issue with git commit --allow-empty -m "rebuild please" && git push)

Scott Morrison (May 23 2022 at 00:01):

Haha, I just merge master and push. :-) I should try your version.

Mauricio Collares (May 23 2022 at 00:01):

Eric Wieser (May 23 2022 at 00:05):

Scott Morrison said:

Haha, I just merge master and push. :-) I should try your version.

That can be a lot slower

Last updated: Dec 20 2023 at 11:08 UTC