From 74558c622de91801e3e188bdf690eb9a665f965b Mon Sep 17 00:00:00 2001
From: grianneau <boris.djalal@gmail.com>
Date: Wed, 27 Jan 2021 09:43:38 +0100
Subject: 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
---
 ci/manifest              | 47 ---------------------------------------
 ci/manifest-opam         | 47 +++++++++++++++++++++++++++++++++++++++
 ci/manifest-sources-8.11 | 57 ++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 104 insertions(+), 47 deletions(-)
 delete mode 100644 ci/manifest
 create mode 100644 ci/manifest-opam
 create mode 100644 ci/manifest-sources-8.11

(limited to 'ci')

diff --git a/ci/manifest b/ci/manifest
deleted file mode 100644
index b002ce3..0000000
--- a/ci/manifest
+++ /dev/null
@@ -1,47 +0,0 @@
-# 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
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
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
-- 
cgit