From 649cc52200303abe4559d4c501c8aca06eed7591 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 12 Jun 2017 12:07:34 -0400
Subject: [travis overlay] Partially Revert 013c0232953f1f58

I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed---
 dev/ci/ci-basic-overlay.sh | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7a9df93c45..03cf0a9d14 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -97,14 +97,14 @@
 ########################################################################
 # bedrock_src
 ########################################################################
-: ${bedrock_src_CI_BRANCH:=trunk__API}
-: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${bedrock_src_CI_BRANCH:=master}
+: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # bedrock_facade
 ########################################################################
-: ${bedrock_facade_CI_BRANCH:=trunk__API}
-: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${bedrock_facade_CI_BRANCH:=master}
+: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
 
 ########################################################################
 # formal-topology
-- 
cgit v1.2.3


From e36d139f6cb73d1e5021a77d38925b2879efda62 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 13 Jun 2017 17:24:43 +0200
Subject: Revert "[travis] temporary UniMath overlay"

This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43.

Not necessary anymore since UniMath/UniMath#715 has been merged.
---
 dev/ci/ci-basic-overlay.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 3adc319355..d7714274e7 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -13,8 +13,8 @@
 ########################################################################
 # UniMath
 ########################################################################
-: ${UniMath_CI_BRANCH:=coq_makefile2-fix}
-: ${UniMath_CI_GITURL:=https://github.com/maximedenes/UniMath.git}
+: ${UniMath_CI_BRANCH:=master}
+: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}
 
 ########################################################################
 # Unicoq + Metacoq
-- 
cgit v1.2.3


From c70a21a1c522639138dbcfac53fb2ed96d731d98 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:05:04 +0200
Subject: [travis] fix CoLoR by inserting some Require Import FunInd

---
 dev/ci/ci-color.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 57f569858b..a0a4e0749d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -18,4 +18,18 @@ sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${C
 sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
 sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
 
+# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
+sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
+sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
+sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
+sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
+sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
+sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
+sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
+sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
+
 ( cd ${Color_CI_DIR} && make -j ${NJOBS} )
-- 
cgit v1.2.3


From bba2186f781695db9d0987758119fde061499fbc Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 12:44:01 +0200
Subject: [travis] fix Software Foundation (one added Require Extraction)

---
 dev/ci/ci-sf.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 7d23ccad97..23ef41d2dd 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
 wget ${sf_CI_TARURL}
 tar xvfz sf.tgz
 
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
 ( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
 
 
-- 
cgit v1.2.3


From 2470182ac4bded5c433c8f6bc77eb7b96576dc8d Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 14:48:22 +0200
Subject: [travis] overlays for CompCert and VST (an extra Require Export
 FunInd)

---
 dev/ci/ci-user-overlay.sh | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 200d431bcb..62c245b4fe 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -47,3 +47,10 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums"
     Corn_CI_BRANCH=external-bignums
     Corn_CI_GITURL=https://github.com/letouzey/corn.git
 fi
+
+if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
+    CompCert_CI_BRANCH=less_init_plugins
+    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
+    VST_CI_BRANCH=less_init_plugins
+    VST_CI_GITURL=https://github.com/letouzey/VST.git
+fi
-- 
cgit v1.2.3


From bb6dbba6a76f83c7cbac7a1f8d6eaa14da2d3d40 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 13 Jun 2017 15:47:56 +0200
Subject: [travis] overlay for fiat-crypto (a Require Import FunInd)

---
 dev/ci/ci-user-overlay.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 62c245b4fe..2ecd40416f 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -53,4 +53,6 @@ if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins"
     CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
     VST_CI_BRANCH=less_init_plugins
     VST_CI_GITURL=https://github.com/letouzey/VST.git
+    fiat_crypto_CI_BRANCH=less_init_plugins
+    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
 fi
-- 
cgit v1.2.3


From f4cec75fe74ff3f66f401efab357cae79124d984 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 14 Jun 2017 10:32:17 +0200
Subject: Temporary overlays because fewer plugins are loaded at startup.

---
 dev/ci/ci-basic-overlay.sh | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 54db58c01f..b582921ecb 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -73,14 +73,14 @@
 ########################################################################
 # CompCert
 ########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: ${CompCert_CI_BRANCH:=less_init_plugins}
+: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
 
 ########################################################################
 # VST
 ########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: ${VST_CI_BRANCH:=less_init_plugins}
+: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git}
 
 ########################################################################
 # fiat_parsers
@@ -91,8 +91,8 @@
 ########################################################################
 # fiat_crypto
 ########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
+: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
+: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
 ########################################################################
 # bedrock_src
-- 
cgit v1.2.3


From c5dabed1c1f33005fe942882ea0fcf008d52784a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jun 2017 11:45:45 +0200
Subject: Remove bedrock from test suite.

Bedrock relies on the 8.4 compat flag that we are removing, and we heard
from MIT that they did not plan to port bedrock to more recent versions
of Coq.
---
 dev/ci/ci-basic-overlay.sh  | 12 ------------
 dev/ci/ci-bedrock-facade.sh | 10 ----------
 dev/ci/ci-bedrock-src.sh    | 10 ----------
 dev/ci/ci-user-overlay.sh   |  4 ----
 4 files changed, 36 deletions(-)
 delete mode 100755 dev/ci/ci-bedrock-facade.sh
 delete mode 100755 dev/ci/ci-bedrock-src.sh

(limited to 'dev/ci')

diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7f66dfb3b0..0099e815f4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -94,18 +94,6 @@
 : ${fiat_crypto_CI_BRANCH:=less_init_plugins}
 : ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
-########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
 ########################################################################
 # formal-topology
 ########################################################################
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 95cfa3073f..0000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index 532611d4b3..0000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 2ecd40416f..b242ce3bd9 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -33,10 +33,6 @@ fi
 echo "DEBUG: ci-user-overlay.sh 0"
 if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
     echo "DEBUG: ci-user-overlay.sh 1"
-    bedrock_src_CI_BRANCH=trunk__API
-    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    bedrock_facade_CI_BRANCH=trunk__API
-    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
     fiat_parsers_CI_BRANCH=trunk__API
     fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
 fi
-- 
cgit v1.2.3


From d06af26e6cd93c6bb819b38573603a5e1121ed68 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 13 Jun 2017 18:24:45 +0200
Subject: Each user overlay goes into its own file.

This will avoid stupid merge conflicts in the future.
---
 dev/ci/ci-common.sh                                |  4 +-
 dev/ci/ci-user-overlay.sh                          | 58 ----------------------
 .../user-overlays/00669-maximedenes-ssr-merge.sh   |  4 ++
 dev/ci/user-overlays/README.md                     | 14 ++++++
 4 files changed, 21 insertions(+), 59 deletions(-)
 delete mode 100644 dev/ci/ci-user-overlay.sh
 create mode 100644 dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
 create mode 100644 dev/ci/user-overlays/README.md

(limited to 'dev/ci')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f1e1515d41..5435e95885 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -18,7 +18,9 @@ ls "$COQBIN"
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
 
-source ${ci_dir}/ci-user-overlay.sh
+for overlay in ${ci_dir}/user-overlays/*.sh; do
+  source ${overlay}
+done
 source ${ci_dir}/ci-basic-overlay.sh
 
 mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
deleted file mode 100644
index 2ecd40416f..0000000000
--- a/dev/ci/ci-user-overlay.sh
+++ /dev/null
@@ -1,58 +0,0 @@
-#!/usr/bin/env bash
-
-# Add user overlays here. You can use some logic to detect if you are
-# in your travis branch and conditionally enable the overlay.
-
-# Some useful Travis variables:
-# (https://docs.travis-ci.com/user/environment-variables/#Default-Environment-Variables)
-#
-# - TRAVIS_BRANCH: For builds not triggered by a pull request this is
-#   the name of the branch currently being built; whereas for builds
-#   triggered by a pull request this is the name of the branch
-#   targeted by the pull request (in many cases this will be master).
-#
-# - TRAVIS_COMMIT: The commit that the current build is testing.
-#
-# - TRAVIS_PULL_REQUEST: The pull request number if the current job is
-#   a pull request, “false” if it’s not a pull request.
-#
-# - TRAVIS_PULL_REQUEST_BRANCH: If the current job is a pull request,
-#   the name of the branch from which the PR originated. "" if the
-#   current job is a push build.
-
-echo $TRAVIS_PULL_REQUEST_BRANCH
-echo $TRAVIS_PULL_REQUEST
-echo $TRAVIS_BRANCH
-echo $TRAVIS_COMMIT
-
-if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
-    mathcomp_CI_BRANCH=ssr-merge
-    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
-fi
-
-echo "DEBUG: ci-user-overlay.sh 0"
-if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
-    echo "DEBUG: ci-user-overlay.sh 1"
-    bedrock_src_CI_BRANCH=trunk__API
-    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    bedrock_facade_CI_BRANCH=trunk__API
-    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    fiat_parsers_CI_BRANCH=trunk__API
-    fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then
-    math_classes_CI_BRANCH=external-bignums
-    math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git
-    Corn_CI_BRANCH=external-bignums
-    Corn_CI_GITURL=https://github.com/letouzey/corn.git
-fi
-
-if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
-    CompCert_CI_BRANCH=less_init_plugins
-    CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
-    VST_CI_BRANCH=less_init_plugins
-    VST_CI_GITURL=https://github.com/letouzey/VST.git
-    fiat_crypto_CI_BRANCH=less_init_plugins
-    fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
-fi
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
new file mode 100644
index 0000000000..af4a96f4ae
--- /dev/null
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -0,0 +1,4 @@
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
new file mode 100644
index 0000000000..9146d3d521
--- /dev/null
+++ b/dev/ci/user-overlays/README.md
@@ -0,0 +1,14 @@
+# Add overlays for your pull requests in this directory
+
+An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh).
+
+The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`.
+
+Example: `00669-maximedenes-ssr-merge.sh` containing
+
+```
+if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+    mathcomp_CI_BRANCH=ssr-merge
+    mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+fi
+```
-- 
cgit v1.2.3