Update the SAW integration #78
Merged
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
1. Update the SAW download to use the latest release instead of an ancient nightly that's no longer available. 2. Skip the downloads of both SAW and Cryptol if IN_SAW_CI is set to "yes". These are motivated by the use of this tree in the SAW CI tests, which has been blowing up, first because we tried to delete the ancient nightlies, then because the website reorg broke the downloads. However, at least point (1) seems to be of general value.
(instead of a long-gone snapshot from saw.galois.com) Needed to unbreak this repository's own CI.
sauclovian-g
force-pushed
the
update-saw-download
branch
from
3f1ea27 to
418129e
Compare
RyanGlScott
approved these changes
Jan 28, 2025
There was a problem hiding this comment.
I don't have much context for the specifics of these proofs, so it's hard for me to tell if it would be straightforward to repair the parts of the proofs that have bitrotted or not. That being said, memory_safety.saw (the only parts of these proofs that SAW's CI runs) now works, which is an encouraging first step. I propose that we file issues about the other proofs that aren't currently working and then merge this.
kquick
reviewed
Jan 28, 2025
scripts/install.sh
Outdated
| @@ -46,17 +49,21 @@ then | |||
| cp deps/yices/*/bin/yices-smt2 bin/yices-smt2 | |||
| fi | |||
|
|
|||
| # fetch ABC | |||
| # fetch what4_solvers for ABC | |||
| fi | ||
|
|
||
| # fetch SAW | ||
| if [ ! -f bin/saw ] | ||
| if [ ! -f bin/saw ] && [ ${IN_SAW_CI:-no} != yes ] |
There was a problem hiding this comment.
See my recommendation in the other PR about the env var name CI_TEST_LEVEL.
There was a problem hiding this comment.
(and see there for why I didn't here)
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.
Allows fixing up the problems currently seen in the SAW CI. (GaloisInc/saw-script#2166)