Lean: Adding a specialization file from PreSailM to SailM
#1084
Conversation
This file contains 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
Test Results 13 files ±0 29 suites ±0 0s ⏱️ ±0s For more details on these errors, see this check. Results for commit ed03e2e. ± Comparison against base commit fe85f30. ♻️ This comment has been updated with latest results. |
|
Seems to be causing the tests to fail with: |
|
Looks like the same issue with |
|
Should be fixed! |
|
I now see: ✔ [2/8] Built LeanRV64DLEAN.Sail.BitVec
✔ [3/8] Built LeanRV64DLEAN.Sail.Sail
✔ [4/8] Built LeanRV64DLEAN.Defs
✖ [5/8] Building LeanRV64DLEAN.RiscvExtras
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-02-05/bin/lean --tstack=400000 ././././LeanRV64DLEAN/RiscvExtras.lean -R ./././. -o ././.lake/build/lib/LeanRV64DLEAN/RiscvExtras.olean -i ././.lake/build/lib/LeanRV64DLEAN/RiscvExtras.ilean -c ././.lake/build/ir/LeanRV64DLEAN/RiscvExtras.c --json
error: ././././LeanRV64DLEAN/RiscvExtras.lean:64:32: function expected at
PreSailM
term has type
?m.461
error: ././././LeanRV64DLEAN/RiscvExtras.lean:65:30: function expected at
PreSailM
term has type
?m.503
error: ././././LeanRV64DLEAN/RiscvExtras.lean:68:35: function expected at
PreSailM
term has type
?m.544
error: ././././LeanRV64DLEAN/RiscvExtras.lean:70:34: function expected at
PreSailM
term has type
?m.609
error: ././././LeanRV64DLEAN/RiscvExtras.lean:72:34: function expected at
PreSailM
term has type
?m.648
error: ././././LeanRV64DLEAN/RiscvExtras.lean:74:37: function expected at
PreSailM
term has type
?m.687
error: Lean exited with code 1
✔ [6/8] Built LeanRV64DLEAN.Specialization
Some required builds logged failures:
- LeanRV64DLEAN.RiscvExtras
-Is there a https://github.com/riscv/sail-riscv/pulls PR that I am missing? |
|
We need the associated RISC-V model patch riscv/sail-riscv#763 |
Timmmm
pushed a commit
to riscv/sail-riscv
that referenced
this pull request
Feb 28, 2025
Adapt to the specialization patch [1], which hides the PreSailM monad in the PreSail namespace, and use the SailM monad instead. [1] rems-project/sail#1084
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.
This is preliminary work for changing the way loops and early returns are handled.
That change will help fix #1071