add rust nightly for hax, allow lean to fail - wip #1
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
F-WRunTime
reviewed
Jan 8, 2026
|
|
||
| ## Why it currently fails in CI: | ||
|
|
||
| - Installing hax from crates.io (cargo install cargo-hax --version 0.3.5) on the pinned nightly fails due to mismatches with rustc internals (e.g., missing/renamed types like CanonicalTyVarKind, DynKind, AssocItemContainer). |
Member
There was a problem hiding this comment.
Does this then not work locally? If it is working locally, How is the local setup different than CI?
|
|
||
| ## What kind of help we need from DevOps: | ||
|
|
||
| - Help pin and install a consistent hax toolchain in CI. Most likely we need to install hax from the same git revision as our local working checkout (not the crates.io 0.3.5 package), e.g. cargo install --git ... --rev <HAX_REV> cargo-hax and the companion binaries, using the pinned nightly nightly-2025-11-08. |
Member
There was a problem hiding this comment.
Yeah can we document this.
My suggestion is following our convention of defining
dependencies that are not submodules within a folder at the root deps/<depName>
Within the file is ideally a stable git-tag if not available for the dependent then referencing a git-sha.
We'll then build up CI references around that for stability / consistency / documented in revision history
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
changes to fix CI: add rust nightly for hax, allow lean to fail - wip