aboutsummaryrefslogtreecommitdiff
path: root/test-suite/vos/run.sh
blob: 2496fc8602b5a9a71aac72ef0528925c06eb29e6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
#!/bin/bash
set -e
set -o pipefail
export PATH="$COQBIN:$PATH"

# Clean
rm -f *.vo *.vos *.vok *.glob *.aux Makefile

# Test building all vos, then all vok
coq_makefile -R . TEST -o Makefile *.v
make vos
make vok

# Cleanup
make clean

# Test using compilation in custom order
set -x #echo on
coqc A.v
coqc -vos B.v
coqc -vos C.v
coqc -vok B.v
coqc -vok C.v