diff options
author | grianneau <boris.djalal@gmail.com> | 2021-01-27 09:43:38 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-27 09:43:38 +0100 |
commit | 74558c622de91801e3e188bdf690eb9a665f965b (patch) | |
tree | 05e6b90604b8bd7c7e00debe034237e5db975169 /ci/manifest-opam | |
parent | 09117dcb494ed47828ee658b9c72ad83c880a438 (diff) | |
download | smtcoq-74558c622de91801e3e188bdf690eb9a665f965b.tar.gz smtcoq-74558c622de91801e3e188bdf690eb9a665f965b.zip |
Add ci manifest to compile from the sources
* compiling SMTCoq from sources from branch 8.11
* manifest using debian/stable to make it work with OCaml 8.09.1
Diffstat (limited to 'ci/manifest-opam')
-rw-r--r-- | ci/manifest-opam | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/ci/manifest-opam b/ci/manifest-opam new file mode 100644 index 0000000..b002ce3 --- /dev/null +++ b/ci/manifest-opam @@ -0,0 +1,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 |