#!/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