Zulip Chat Archive
Stream: general
Topic: leanchecker toolchain CI failure
Mauricio Collares (Nov 17 2023 at 11:21):
Staging CI has been complaining that leanchecker's toolchain (v4.3.0-rc1) is not installed:
- https://github.com/leanprover-community/mathlib4/actions/runs/6900921426/job/18774853373
- https://github.com/leanprover-community/mathlib4/actions/runs/6901043935/job/18775176917
- https://github.com/leanprover-community/mathlib4/actions/runs/6902430659/job/18779131388
This can be fixed with a leanchecker bump, but why does elan refuse to install the older version? So far this has only happened on hoskinson9, and there have been successful runs on hoskinson3 and hoskinson6. @maintainers
Scott Morrison (Nov 17 2023 at 12:19):
Oops, my fault.
It's late here, but #8471 is my short-term fix. I've set it to auto-merge, but if anyone is available to shepherd it along that would be great.
Scott Morrison (Nov 17 2023 at 12:19):
Branches that are already on v4.3.0-rc2 will need to merge the master after this lands.
Mauricio Collares (Nov 17 2023 at 12:31):
It is trying to run leanchecker/build/bin/leanchecker, but the build dir is now inside .lake
Mauricio Collares (Nov 17 2023 at 12:40):
Thanks Scott! Sorry for not pushing the .lake fix, I was at a talk
Last updated: Dec 20 2023 at 11:08 UTC