Closed matthiastz closed 4 years ago
Hi, Have you installed all the dependencies? It would be easier to run it on docker. See https://github.com/uwdb/Cosette/blob/master/Dockerfile
Hi stechu, thanks for the reply.
I followed your instruction and used the repos Dockerfile. This is what I did:
sudo docker image build .
sudo docker tag <image_name> cosette:1 # give repo and tag name for locally build docker image
sudo docker run -it -p 3434:8080 --name <image_name> cosette:1 # i guess the port directive is not really needed here
The main docker file "just" seems to install HoTT and Coq, is this correct?
This is what my system looks like after docker run
:
➜ Cosette git:(master) ✗ sudo docker run -it -p 3434:8080 --name a03760f720a7 cosette:1
root@21d66c7773bd:/# ls
HoTT bin boot coq-8.5pl1 coq-8.5pl1.tar.gz dev etc home lib lib64 media mnt opt proc root run sbin srv sys tmp usr var
root@21d66c7773bd:/#
I am not sure how to proceed further to use the Cosette solver locally. My goal is to run my own defined querys with Cosette either via .cos input files or even better with a frontend similar to https://demo.cosette.cs.washington.edu/. Could you please provide some more information on what steps I need to take to run the Cosette solver locally with Docker? Would be really appreciated, thanks.
Even did run sh init_docker.sh
because i thought it is somehow related to the main docker file you mentioned, but that also does not seem to help much. Do I need to run FrontendDockerFile
?
Update:
I can somehow run Cosette locally now by doing the following:
return json_res
)
Hi, i tried using Cosette via checking out the source code and ran different python commands to first test the Cosette functionality.
E.g. the following is not working for me:
python solver_test.py
yields inI did setup
temp.cos
with the following content:and did run
python manual_test.py
, which results inERROR
the third test also does not work: