From b50bd0f9fd2fedb7dd14edd39baabf2fc3be8e3b Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 3 May 2019 10:06:29 +0000
Subject: Add overlays for CompCert, VST, and coquelicot

---
 dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh b/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
new file mode 100644
index 0000000000..88f5f73e5f
--- /dev/null
+++ b/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9854" ] || [ "$CI_BRANCH" = "field_simplify_int" ]; then
+
+    compcert_CI_REF=field_simplify_int
+    compcert_CI_GITURL=https://github.com/vbgl/CompCert
+
+    coquelicot_CI_REF=field_simplify_int
+    coquelicot_CI_GITURL=https://gitlab.com/vbgl/coquelicot
+
+    vst_CI_REF=field_simplify_int
+    vst_CI_GITURL=https://github.com/vbgl/VST
+
+fi
-- 
cgit v1.2.3


From 782312a65310dc717d830b3e8e5a7ba54b4cfb6e Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 3 May 2019 12:00:34 +0000
Subject: [nix-ci] Add coquelicot, improve flocq

---
 dev/ci/nix/coquelicot.nix | 9 +++++++++
 dev/ci/nix/default.nix    | 1 +
 dev/ci/nix/flocq.nix      | 1 +
 3 files changed, 11 insertions(+)
 create mode 100644 dev/ci/nix/coquelicot.nix

(limited to 'dev')

diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix
new file mode 100644
index 0000000000..d379bfa73d
--- /dev/null
+++ b/dev/ci/nix/coquelicot.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ssreflect }:
+
+{
+  buildInputs = [ autoconf automake ];
+  coqBuildInputs = [ ssreflect ];
+  configure = "./autogen.sh && ./configure";
+  make = "./remake";
+  clean = "./remake clean";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 17070e66ee..a9cc91170f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -72,6 +72,7 @@ let projects = {
   CoLoR = callPackage ./CoLoR.nix {};
   CompCert = callPackage ./CompCert.nix {};
   coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+  coquelicot = callPackage ./coquelicot.nix {};
   Corn = callPackage ./Corn.nix {};
   cross_crypto = callPackage ./cross_crypto.nix {};
   Elpi = callPackage ./Elpi.nix {};
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
index e153043557..71028ec2dc 100644
--- a/dev/ci/nix/flocq.nix
+++ b/dev/ci/nix/flocq.nix
@@ -4,4 +4,5 @@
   buildInputs = [ autoconf automake ];
   configure = "./autogen.sh && ./configure";
   make = "./remake";
+  clean = "./remake clean";
 }
-- 
cgit v1.2.3


From 5d426eecb6c7f2e956cde98780aef349fdc75af0 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 7 May 2019 14:17:50 +0000
Subject: Remove overlays for CompCert and VST

---
 dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh b/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
index 88f5f73e5f..720adbc979 100644
--- a/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
+++ b/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
@@ -1,12 +1,6 @@
 if [ "$CI_PULL_REQUEST" = "9854" ] || [ "$CI_BRANCH" = "field_simplify_int" ]; then
 
-    compcert_CI_REF=field_simplify_int
-    compcert_CI_GITURL=https://github.com/vbgl/CompCert
-
     coquelicot_CI_REF=field_simplify_int
     coquelicot_CI_GITURL=https://gitlab.com/vbgl/coquelicot
 
-    vst_CI_REF=field_simplify_int
-    vst_CI_GITURL=https://github.com/vbgl/VST
-
 fi
-- 
cgit v1.2.3


From 281e6657c7fe5033a13c7a2fd2b6cc6f51cb6911 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Thu, 9 May 2019 10:44:15 +0200
Subject: Switched Coquelicot CI URLs from INRIA gforge to INRIA gitlab

---
 dev/ci/ci-basic-overlay.sh                            | 3 ++-
 dev/ci/ci-coquelicot.sh                               | 1 -
 dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh | 6 ------
 3 files changed, 2 insertions(+), 8 deletions(-)
 delete mode 100644 dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh

(limited to 'dev')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4f5988c59c..d39b92467d 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -105,7 +105,8 @@
 # Coquelicot
 ########################################################################
 : "${coquelicot_CI_REF:=master}"
-: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
 
 ########################################################################
 # CompCert
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 33627fd8ef..6cb8dad604 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
 
 install_ssreflect
 
-FORCE_GIT=1
 git_download coquelicot
 
 ( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh b/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
deleted file mode 100644
index 720adbc979..0000000000
--- a/dev/ci/user-overlays/09854-vbgl-field_simplify_int.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9854" ] || [ "$CI_BRANCH" = "field_simplify_int" ]; then
-
-    coquelicot_CI_REF=field_simplify_int
-    coquelicot_CI_GITURL=https://gitlab.com/vbgl/coquelicot
-
-fi
-- 
cgit v1.2.3