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 | |
| 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')
| -rw-r--r-- | ci/manifest-opam (renamed from ci/manifest) | 0 | ||||
| -rw-r--r-- | ci/manifest-sources-8.11 | 57 |
2 files changed, 57 insertions, 0 deletions
diff --git a/ci/manifest b/ci/manifest-opam index b002ce3..b002ce3 100644 --- a/ci/manifest +++ b/ci/manifest-opam diff --git a/ci/manifest-sources-8.11 b/ci/manifest-sources-8.11 new file mode 100644 index 0000000..b93f959 --- /dev/null +++ b/ci/manifest-sources-8.11 @@ -0,0 +1,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 |