blob: b002ce31285e2ea63800fc7fffc95da0f9717d31 (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
# To be run on https://builds.sr.ht
# Testing the opam package with the veriT and CVC4 provers
image: debian/sid
packages:
- screen
- opam
- atool
- autoconf
- bison
- flex
sources:
- https://github.com/smtcoq/smtcoq.git
tasks:
- opam: |
opam init --no-setup
opam switch create ocaml-base-compiler.4.09.0
- smtcoq: |
eval $(opam env)
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam install camlp5 conf-findutils conf-m4 ocamlfind num coq coq-smtcoq
- cvc4: |
wget http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.6-x86_64-linux-opt
chmod ugo+x cvc4-1.6-x86_64-linux-opt
- verit: |
wget https://www.lri.fr/~keller/Documents-recherche/Smtcoq/veriT9f48a98.tar.gz
aunpack veriT9f48a98.tar.gz
cd veriT9f48a98
autoconf
./configure
make
- bin: |
mkdir bin
cd bin
ln -s ~/cvc4-1.6-x86_64-linux-opt cvc4
ln -s ~/veriT9f48a98/veriT veriT
- unit: |
eval $(opam env)
export PATH=~/bin:$PATH
export LFSCSIGS="/home/build/smtcoq/src/lfsc/tests/signatures/"
export DONTSHOWVERIT="yes"
cd smtcoq/unit-tests
sed -i "s/..\/src/~\/.opam\/ocaml-base-compiler.4.09.0\/lib\/coq\/user-contrib\/SMTCoq/g" Makefile
make verit
make lfsc
|
