From b0a6838ebe51760a6020145a0051137f6a4fcef0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 May 2019 11:31:15 +0200
Subject: Add overlays.

---
 dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
new file mode 100644
index 0000000000..0e1449f36c
--- /dev/null
+++ b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then
+
+    unicoq_CI_REF=whd-for-evar-conv-no-stack
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
-- 
cgit v1.2.3


From 928bced545407a2043fe2acaa5b31b1aa07988d5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:43:55 +0200
Subject: Remove ppedrot/ltac2 from CI after integration in main repo

---
 dev/ci/ci-basic-overlay.sh | 7 -------
 dev/ci/ci-ltac2.sh         | 8 --------
 2 files changed, 15 deletions(-)
 delete mode 100755 dev/ci/ci-ltac2.sh

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4f5988c59c..f97e781832 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -80,13 +80,6 @@
 : "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}"
 : "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}"
 
-########################################################################
-# Ltac2
-########################################################################
-: "${ltac2_CI_REF:=master}"
-: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}"
-: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}"
-
 ########################################################################
 # GeoCoq
 ########################################################################
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
deleted file mode 100755
index 4df22bf249..0000000000
--- a/dev/ci/ci-ltac2.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-git_download ltac2
-
-( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install )
-- 
cgit v1.2.3


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/ci')

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/ci')

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/ci')

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 df8e45d9bd3908278254e769839ddc98d5057ee5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 8 May 2019 20:35:58 +0200
Subject: Clean-up: remove dead appveyor.sh file.

---
 dev/ci/appveyor.sh | 17 -----------------
 1 file changed, 17 deletions(-)
 delete mode 100644 dev/ci/appveyor.sh

(limited to 'dev/ci')

diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
deleted file mode 100644
index f26e0904bc..0000000000
--- a/dev/ci/appveyor.sh
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/bash
-
-set -e -x
-
-APPVEYOR_OPAM_VARIANT=ocaml-variants.4.07.1+mingw64c
-NJOBS=2
-
-wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
-tar -xf opam64.tar.xz
-bash opam64/install.sh
-
-opam init default -j $NJOBS -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $APPVEYOR_OPAM_VARIANT --disable-sandboxing
-eval "$(opam env)"
-opam install -j $NJOBS -y num ocamlfind ounit
-
-# Full regular Coq Build
-cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make -j $NJOBS && make byte -j $NJOBS && make -j $NJOBS -C test-suite all INTERACTIVE= # && make validate
-- 
cgit v1.2.3


From 053e64206aa70c6a12c75b59e8267eeaba00d1ce Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 8 May 2019 20:40:19 +0200
Subject: Remove ltac2 add-on from Windows installer now that it is in the main
 Coq package.

---
 dev/ci/gitlab.bat | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/ci')

diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index cc1931d13d..6c4ccfc14d 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -41,7 +41,6 @@ IF "%WINDOWS%" == "enabled_all_addons" (
   SET EXTRA_ADDONS=^
     -addon=bignums ^
     -addon=equations ^
-    -addon=ltac2 ^
     -addon=mtac2 ^
     -addon=mathcomp ^
     -addon=menhir ^
-- 
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/ci')

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


From 1b4c0a1e52286d4957f6c79c8ff14868a6f3e838 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 May 2019 22:10:57 +0200
Subject: Add overlays for coq/coq#10052.

---
 dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
new file mode 100644
index 0000000000..9f9cc19e83
--- /dev/null
+++ b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then
+
+    relation_algebra_CI_REF=cleanup-logic-convert-hyp
+    relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra
+
+fi
-- 
cgit v1.2.3


From ba62d040b8ff53ce66c2dbaa83a44b0037cb620f Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 7 May 2019 10:14:07 +0000
Subject: Add overlay for elpi

---
 dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+    elpi_CI_REF=canonical-disable-hint
+    elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
-- 
cgit v1.2.3


From 96f31931743c950f006682a398c501c30e96fda0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 13 May 2019 11:40:03 +0200
Subject: Add overlay for Unicoq

---
 dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
new file mode 100644
index 0000000000..bc8aa33565
--- /dev/null
+++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then
+
+    unicoq_CI_REF=detype-anonymous
+    unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+fi
-- 
cgit v1.2.3


From ce083774403b70d58c71c5a6ba104c337613add4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 12 Nov 2018 23:37:47 +0100
Subject: Adding overlay for Equations.

---
 .../08893-herbelin-master+moving-evars-of-term-on-econstr.sh       | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
new file mode 100644
index 0000000000..dc39ea5ef0
--- /dev/null
+++ b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then
+
+    equations_CI_BRANCH=master+fix-evars_of_term-pr8893
+    equations_CI_REF=master+fix-evars_of_term-pr8893
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
-- 
cgit v1.2.3


From 06b60655b98580baab98f35f6c89716e2381934c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 14 May 2019 14:17:57 +0200
Subject: Overlay for value-returning run_tactic

---
 dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
new file mode 100644
index 0000000000..4032b1c6b5
--- /dev/null
+++ b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then
+
+    paramcoq_CI_REF=run_tactic_gen
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+fi
-- 
cgit v1.2.3


From 02d547e3bc531c9a0bec8d47436c204e3bc15ddc Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 15 May 2019 09:20:37 +0000
Subject: [Nix-CI] Bignums no longer depends on camlp5

---
 dev/ci/nix/bignums.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/ci')

diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix
index 1d931c858e..d813ddd8d7 100644
--- a/dev/ci/nix/bignums.nix
+++ b/dev/ci/nix/bignums.nix
@@ -1,5 +1,5 @@
 { ocamlPackages }:
 
 {
-  buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ];
+  buildInputs = [ ocamlPackages.ocaml ];
 }
-- 
cgit v1.2.3


From 3faa91524befcd3c163ec34684986fde3aa37462 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 15 May 2019 12:14:24 +0000
Subject: [Nix-ci] Update Unicoq patch

---
 dev/ci/nix/unicoq/unicoq-num.patch | 31 -------------------------------
 1 file changed, 31 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/nix/unicoq/unicoq-num.patch b/dev/ci/nix/unicoq/unicoq-num.patch
index 6d96d94dfc..6d2f6470b1 100644
--- a/dev/ci/nix/unicoq/unicoq-num.patch
+++ b/dev/ci/nix/unicoq/unicoq-num.patch
@@ -4,19 +4,6 @@ Date:   Thu Nov 29 08:59:22 2018 +0000
 
     Make explicit dependency to num
 
-diff --git a/Make b/Make
-index 550dc6a..8aa1309 100644
---- a/Make
-+++ b/Make
-@@ -9,7 +9,7 @@ src/logger.ml
- src/munify.mli
- src/munify.ml
- src/unitactics.mlg
--src/unicoq.mllib
-+src/unicoq.mlpack
- theories/Unicoq.v
- test-suite/munifytest.v
- test-suite/microtests.v
 diff --git a/Makefile.local b/Makefile.local
 new file mode 100644
 index 0000000..88be365
@@ -24,21 +11,3 @@ index 0000000..88be365
 +++ b/Makefile.local
 @@ -0,0 +1 @@
 +CAMLPKGS += -package num
-diff --git a/src/unicoq.mllib b/src/unicoq.mllib
-deleted file mode 100644
-index 2b84e2d..0000000
---- a/src/unicoq.mllib
-+++ /dev/null
-@@ -1,3 +0,0 @@
--Logger
--Munify
--Unitactics
-diff --git a/src/unicoq.mlpack b/src/unicoq.mlpack
-new file mode 100644
-index 0000000..2b84e2d
---- /dev/null
-+++ b/src/unicoq.mlpack
-@@ -0,0 +1,3 @@
-+Logger
-+Munify
-+Unitactics
-- 
cgit v1.2.3


From f6751f5e8aae4f37d302f700d2f5f2e9fba73a1e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 14 May 2019 14:28:43 +0200
Subject: Overlay for definition-not-visible overhaul

---
 .../10157-SkySkimmer-def-not-visible-generic-warning.sh             | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh

(limited to 'dev/ci')

diff --git a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh
new file mode 100644
index 0000000000..fcbeb32a58
--- /dev/null
+++ b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10188" ] || [ "$CI_BRANCH" = "def-not-visible-remove-warning" ]; then
+
+    elpi_CI_REF=def-not-visible-generic-warning
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
-- 
cgit v1.2.3