Use prebuilt what4-solvers binaries #1454
Conversation
atomb
force-pushed
the
at-prebuilt-solvers
branch
from
84adb11
to
af91e96
Compare
atomb
force-pushed
the
at-prebuilt-solvers
branch
2 times, most recently
from
a351955
to
11ef202
Compare
atomb
requested review from
brianhuffman,
kquick,
robdockins and
RyanGlScott
| wait | ||
| (cd $BIN && curl -o bins.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/$BIN_ZIP_FILE" && unzip -o bins.zip && rm bins.zip) | ||
| chmod +x $BIN/* | ||
| cp $BIN/yices_smt2$EXT $BIN/yices-smt2$EXT |
There was a problem hiding this comment.
What is the purpose of this line?
There was a problem hiding this comment.
Oh, I see now—this is changing from yices_smt2 (with an underscore) to yices-smt2 (with a hyphen). Is this something that should be done on what4-solvers' end, I wonder?
There was a problem hiding this comment.
Yeah, it ultimately should be done over there. But I'm waiting for a time when there are other changes that need to be made over there, too, because the build process takes a while.
| @@ -71,8 +69,7 @@ jobs: | |||
|
|
|||
| - uses: actions/checkout@v2 | |||
| - run: | | |||
| git submodule update --init | |||
| git -C deps/abcBridge submodule update --init | |||
There was a problem hiding this comment.
Now that we no longer invoke git -C deps/abcBridge submodule update --init, can we remove the abcBridge submodule?
There was a problem hiding this comment.
Oh, good point! I believe we can.
| CMD [ "/bin/bash" ] |
There was a problem hiding this comment.
Unnecessary whitespace change
| Z3_VERSION: "4.8.10" | ||
| CVC4_VERSION: "4.1.8" | ||
| YICES_VERSION: "2.6.2" | ||
| SOLVER_PKG_VERSION: "snapshot-20210917" |
There was a problem hiding this comment.
Are the comments above this line (about the solver versions needing to be specified in other locations) still relevant?
There was a problem hiding this comment.
For the moment, those comments are still relevant. Ultimately, I want the what4-solvers repo to contain Dockerfiles to produce base Docker images that all those ones can build on top of. That's not done yet, though.
| - shell: bash | ||
| working-directory: s2nTests | ||
| run: | | ||
| curl -o solvers-bin.zip -sL "https://github.com/GaloisInc/what4-solvers/releases/download/$SOLVER_PKG_VERSION/ubuntu-18.04-bin.zip" |
There was a problem hiding this comment.
Does ci.sh's install_system_deps() function do this for you?
There was a problem hiding this comment.
It unfortunately installs them in a different place. I'd like to refactor things so that's not true anymore, but for now I'm trying to make somewhat minimal changes.
|
I can't tell if this is related to the changes in this PR or not, but the two failing tests both seem to be infrastructure/setup failures of some kind. |
This reverts commit 391c778. Proofs don't actually work on Ubuntu 18.04, so we'll just need to get ABC binaries for 20.04.
They've been hanging
It's hanging, and I want to see whether all the other tests succeed.
atomb
force-pushed
the
at-prebuilt-solvers
branch
from
f004c4a
to
bd011b1
Compare
No description provided.