blob: a4afcd958ee2b2cf9b0e2d8b1630e7515a878b8e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
#!/bin/bash
if [ ! -d cheri-mips ]; 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/coq
make
cd ../../cheri-mips
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail mips_extras.v
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail mips_types.v
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail mips.v
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail cheri_types.v
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail cheri.v
cd ../riscv
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail riscv_extras.v
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail riscv_types.v
coqc -R ../../bbv/theories bbv -R ../lib/coq Sail riscv.v
|
