Put a foo.bpl file in proofs directory. Then run
docker-compose run boogie proofs/foo.bpl
Put a foo.bpl file in proofs directory. Then run
docker-compose run boogie proofs/foo.bpl
| version: "3.7" | |
| services: | |
| boogie: | |
| build: . | |
| hostname: boogie | |
| container_name: boogie | |
| volumes: | |
| - type: bind | |
| source: ./proofs | |
| target: /root/proofs | |
| working_dir: /root |
| FROM mono | |
| WORKDIR /root | |
| RUN apt-get update && apt-get install -y z3 unzip | |
| RUN curl -LO https://github.com/boogie-org/boogie/archive/master.zip | |
| RUN unzip master.zip | |
| WORKDIR boogie-master | |
| RUN curl -LO https://nuget.org/nuget.exe | |
| RUN mono ./nuget.exe restore Source/Boogie.sln || mozroots --import --sync | |
| RUN xbuild Source/Boogie.sln | |
| RUN ln -s /usr/bin/z3 Binaries/z3.exe | |
| RUN ln -s $PWD/Binaries/boogie /usr/bin/boogie | |
| ENTRYPOINT ["boogie"] |