diff options
Diffstat (limited to 'prover_snapshots/coq/build')
| -rwxr-xr-x | prover_snapshots/coq/build | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/prover_snapshots/coq/build b/prover_snapshots/coq/build new file mode 100755 index 0000000..f8a1c2f --- /dev/null +++ b/prover_snapshots/coq/build @@ -0,0 +1,27 @@ +#!/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 +cd ../duopod +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_extras.v +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_duopod_types.v +coqc -R ../../bbv/theories bbv -R ../lib/sail Sail riscv_duopod.v |