blob: b93f959b5adf1d869dd6678a54b6a57e3a016a30 (
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
48
49
50
51
52
53
54
55
56
57
|
# To be run on https://builds.sr.ht
# Testing the opam package with the veriT and CVC4 provers
image: debian/stable
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.1
- coq: |
eval $(opam env)
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam update
opam install -y -j2 camlp5 conf-findutils conf-m4 ocamlfind num coq.8.11.2
- smtcoq: |
eval $(opam env)
cd smtcoq
git checkout coq-8.11
cd src
./configure.sh
make
make install
cd ../..
- 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.1\/lib\/coq\/user-contrib\/SMTCoq/g" Makefile
make verit
make lfsc
|
