Installing with docker yields error: `cannot open scripts/ci/install-mathsat-linux.sh: No such file`
Closed this issue · 3 comments
After running the command: sudo docker build . -t horus
I got this:
=> ERROR [ 6/14] RUN sh scripts/ci/install-mathsat-linux.sh && sh scripts/ci/install-cvc5-linux.sh && 0.3s
[ 6/14] RUN sh scripts/ci/install-mathsat-linux.sh && sh scripts/ci/install-cvc5-linux.sh && if [ $(arch) = "aarch64" ]; then sh scripts/ci/install-z3-from-source.sh; else sh scripts/ci/install-z3-linux-amd64.sh; fi && rm -rf scripts/:
#10 0.243 sh: 0: cannot open scripts/ci/install-mathsat-linux.sh: No such file
executor failed running [/bin/sh -c sh scripts/ci/install-mathsat-linux.sh && sh scripts/ci/install-cvc5-linux.sh && if [ $(arch) = "aarch64" ]; then sh scripts/ci/install-z3-from-source.sh; else sh scripts/ci/install-z3-linux-amd64.sh; fi && rm -rf scripts/]: exit code: 2
Hi! Thanks so much for trying out Horus!
Yup, looks like you found a small issue in our Dockerfile. 😱 We used to have an install script for MathSAT, but we got rid of it. I'll make a PR for that and let you know when it's merged! 😄
Okay, try it on this branch: langfield/remove-mathsat-scripts-from-dockerfile
On the off-chance that you run into more issues, I'll fix them with more commits on the same branch, and merge it when you're satisfied it's working well!
Now it worked. Thanks!