diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-07-25 14:51:18 +0100 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-07-25 14:55:54 +0100 |
| commit | bd697d0c54ca047ef93755898f9fa0d919e25f1c (patch) | |
| tree | dabc23669e56194087440119c35cbf5e94205da9 /prover_snapshots/coq/build | |
| parent | 7e6ffe27372f6d740e3f96ec94a3dc05047b5500 (diff) | |
| download | sail-riscv-bd697d0c54ca047ef93755898f9fa0d919e25f1c.zip sail-riscv-bd697d0c54ca047ef93755898f9fa0d919e25f1c.tar.gz sail-riscv-bd697d0c54ca047ef93755898f9fa0d919e25f1c.tar.bz2 | |
Add snapshots of theorem prover definitions
Diffstat (limited to 'prover_snapshots/coq/build')
| -rwxr-xr-x | prover_snapshots/coq/build | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/prover_snapshots/coq/build b/prover_snapshots/coq/build new file mode 100755 index 0000000..c35c3b3 --- /dev/null +++ b/prover_snapshots/coq/build @@ -0,0 +1,23 @@ +#!/bin/bash + +if [ ! -d RV64 ]; then + echo Run build from the coq directory + exit 1 +fi + +if [ ! -d ../bbv ]; then + echo 'Check out a copy of https://github.com/mit-plv/bbv in the parent directory and build it.' + exit 1 +fi + +set -ex +cd lib/sail +make +cd ../../RV32 +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_extras.v +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_types.v +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv.v +cd ../RV64 +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_extras.v +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_types.v +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv.v |