From 93d67b2ae95638766b4d4493402b9b198bcd3a33 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Tue, 28 Sep 2021 15:00:43 +0200
Subject: [PATCH] opam depext since no opam 2.1 yet on debian

---
 .gitlab-ci.yml       |  6 ++----
 Makefile             |  3 ---
 caisar.opam          |  2 +-
 caisar.opam.template |  2 +-
 tests/simple.t       | 22 +++++++++++++++++++++-
 5 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 667f7b7d..b2243fb7 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,13 +11,11 @@ tests:
   script:
   - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.11.1; fi
   - eval $(opam env)
-  - opam --version
-  - opam switch
   - sudo apt-get update
   - opam repository add remote https://opam.ocaml.org
-  - opam update
+  - opam depext --yes ocplib-endian base fmt alt-ergo.2.4.0
   - opam install . --deps-only --with-test --yes
-  - opam install --yes alt-ergo.2.4.0
+  - opam install alt-ergo.2.4.0 --yes
   - make
   - make test
   tags:
diff --git a/Makefile b/Makefile
index 56837ea4..b9f6d170 100644
--- a/Makefile
+++ b/Makefile
@@ -7,8 +7,5 @@ test:
 promote:
 	dune promote --root=.
 
-test:
-	dune runtest
-
 clean:
 	dune clean
diff --git a/caisar.opam b/caisar.opam
index 34af71c8..195dfada 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -36,5 +36,5 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 pin-depends: [
-  [ "why3" "git+https://gitlab.inria.fr/why3/why3.git#autodetection_from_file" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
 ]
diff --git a/caisar.opam.template b/caisar.opam.template
index 10174fed..fd083c6d 100644
--- a/caisar.opam.template
+++ b/caisar.opam.template
@@ -1,3 +1,3 @@
 pin-depends: [
-  [ "why3" "git+https://gitlab.inria.fr/why3/why3.git#autodetection_from_file" ]
+  [ "why3.1.4.0" "git+https://gitlab.inria.fr/why3/why3.git#4e3d0bc71f153fe5625a4a7c92d4dd6cd5e8cf75" ]
 ]
diff --git a/tests/simple.t b/tests/simple.t
index c8b5c220..45493a01 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -1160,28 +1160,48 @@ Test verify
   
   function x1 [@introduced] : t19
   
+  (* meta caisar_input function x1, 0 *)
+  
   function x2 [@introduced] : t19
   
+  (* meta caisar_input function x2, 1 *)
+  
   function x3 [@introduced] : t19
   
+  (* meta caisar_input function x3, 2 *)
+  
   function x4 [@introduced] : t19
   
+  (* meta caisar_input function x4, 3 *)
+  
   function x5 [@introduced] : t19
   
+  (* meta caisar_input function x5, 4 *)
+  
   axiom H [@introduced] : lt 0.0 x1
   
   axiom H1 [@introduced] : lt x1 0.5
   
   function y : t19
   
+  (* meta caisar_output function y, 0 *)
+  
   function y1 : t19
   
+  (* meta caisar_output function y1, 1 *)
+  
   function y2 : t19
   
+  (* meta caisar_output function y2, 2 *)
+  
   function y3 : t19
   
+  (* meta caisar_output function y3, 3 *)
+  
   function y4 : t19
   
-  goal G : lt 0.0 y4 /\ lt y4 0.5
+  (* meta caisar_output function y4, 4 *)
+  
+  goal G : lt 0.0 y /\ lt y 0.5
   
   end
-- 
GitLab