aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/makecoq_mingw.sh4
-rw-r--r--dev/ci/appveyor.bat2
-rw-r--r--dev/ci/ci-common.sh11
-rw-r--r--dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh2
-rw-r--r--dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh9
-rw-r--r--dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh4
-rw-r--r--dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh4
-rw-r--r--dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh4
-rw-r--r--dev/ci/user-overlays/06217-coqdep-at-once.sh3
-rw-r--r--dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh4
-rw-r--r--dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh4
-rw-r--r--dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh4
-rw-r--r--dev/ci/user-overlays/README.md4
-rw-r--r--dev/doc/changes.md7
-rw-r--r--dev/doc/xml-protocol.md6
15 files changed, 30 insertions, 42 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index f12cbe0a78..c467678215 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1087,7 +1087,7 @@ function copy_coq_license {
install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true
install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true
install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true
- install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt"
+ install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true
install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt"
install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt"
install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt"
@@ -1174,7 +1174,7 @@ function make_mingw_make {
if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then
# The config.h.win32 file is fine - don't edit it
# We need to copy the mingw gcc here as "gcc" - then the batch file will use it
- cp /usr/bin/${ARCH}-w64-mingw32-gcc-5.4.0.exe ./gcc.exe
+ cp /usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe ./gcc.exe
# By some magic cygwin bash can run batch files
logn build ./build_w32.bat gcc
# Copy make to Coq folder
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
index e2fbf1f6d1..72ee89962c 100644
--- a/dev/ci/appveyor.bat
+++ b/dev/ci/appveyor.bat
@@ -37,5 +37,5 @@ if %USEOPAM% == true (
GOTO :EOF
:ErrorExit
- ECHO ERROR MakeCoq_MinGW.bat failed
+ ECHO ERROR %0 failed
EXIT /b 1
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 23131c94c6..58c90ff11d 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -5,8 +5,17 @@ set -xe
if [ -n "${GITLAB_CI}" ];
then
export COQBIN=`pwd`/_install_ci/bin
- export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
+ export CI_BRANCH="$CI_COMMIT_REF_NAME"
else
+ if [ -n "${TRAVIS}" ];
+ then
+ export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
+ export CI_BRANCH="$TRAVIS_BRANCH"
+ elif [ -n "${CIRCLECI}" ];
+ then
+ export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
+ export CI_BRANCH="$CIRCLE_BRANCH"
+ fi
export COQBIN=`pwd`/bin
fi
export PATH="$COQBIN:$PATH"
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index af4a96f4ae..7716bcb59a 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,4 +1,4 @@
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_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/01033-SkySkimmer-restrict-harder.sh b/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
deleted file mode 100644
index 5c4dd1324f..0000000000
--- a/dev/ci/user-overlays/01033-SkySkimmer-restrict-harder.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "1033" ] || [ "$TRAVIS_BRANCH" = "restrict-harder" ]; then
- formal_topology_CI_BRANCH=ci
- formal_topology_CI_GITURL=https://github.com/SkySkimmer/topology.git
-
- HoTT_CI_BRANCH=coq-pr-1033
- HoTT_CI_GITURL=https://github.com/SkySkimmer/HoTT.git
-
- Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
deleted file mode 100644
index cdca8e525a..0000000000
--- a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then
- ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer
- ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh
deleted file mode 100644
index 6741cf26fb..0000000000
--- a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then
- ltac2_CI_BRANCH=master
- ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2
-fi
diff --git a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh b/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
deleted file mode 100644
index c9f1272bed..0000000000
--- a/dev/ci/user-overlays/06197-ejgallego-plugins+remove_locality_hack.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6197" ] || [ "$TRAVIS_BRANCH" = "plugins+remove_locality_hack" ]; then
- ltac2_CI_BRANCH=localityfixyou
- ltac2_CI_GITURL=https://github.com/ejgallego/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06217-coqdep-at-once.sh b/dev/ci/user-overlays/06217-coqdep-at-once.sh
deleted file mode 100644
index 68e1901f7f..0000000000
--- a/dev/ci/user-overlays/06217-coqdep-at-once.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6217" ] || [ "$TRAVIS_BRANCH" = "coqdep-at-once" ]; then
- UniMath_CI_GITURL=https://github.com/SkySkimmer/UniMath.git
-fi
diff --git a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh b/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh
deleted file mode 100644
index 7e9b5febdd..0000000000
--- a/dev/ci/user-overlays/06324-SkySkimmer-abstract-vs-restrict.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6324" ] || [ "$TRAVIS_BRANCH" = "fix-6323-restrict+abstract" ]; then
- Equations_CI_BRANCH=fix-coq-6324
- Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh b/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh
deleted file mode 100644
index c0dcf79e1d..0000000000
--- a/dev/ci/user-overlays/06392-ejgallego-econstr+fix_class.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6392" ] || [ "$TRAVIS_BRANCH" = "econstr+fix_class" ]; then
- Equations_CI_BRANCH=econstr+fix_class
- Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh b/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
deleted file mode 100644
index 8aea7dee3a..0000000000
--- a/dev/ci/user-overlays/06413-ejgallego-interp+less_impstyle_p2.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6413" ] || [ "$TRAVIS_BRANCH" = "interp+less_impstyle_p2" ]; then
- Equations_CI_BRANCH=interp+less_impstyle_p2
- Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 9146d3d521..9f0377ceea 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub
Example: `00669-maximedenes-ssr-merge.sh` containing
```
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
mathcomp_CI_BRANCH=ssr-merge
mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
fi
```
+
+(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh))
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 01aa6b599b..f6fbb69424 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -68,6 +68,13 @@ Declaration of printers for arguments used only in vernac command
happen. An alternative is to register the corresponding argument as
a value, using "Geninterp.register_val0 wit None".
+### XML IDE Protocol
+
+- Before 8.8, `Query` only executed the first command present in the
+ `query` string; starting with 8.8, the caller may include several
+ statements. This is useful for instance for temporarily setting an
+ option and then executing a command.
+
## Changes between Coq 8.6 and Coq 8.7
### Ocaml
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 18f6288f6f..b35571e9ca 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -330,6 +330,12 @@ the STM API, `force` triggers a `Join`.
<string>${message}</string>
</value>
```
+
+Before 8.8, `Query` only executed the first command present in the
+`query` string; starting with 8.8, the caller may include several
+statements. This is useful for instance for temporarily setting an
+option and then executing a command.
+
-------------------------------
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:21:36 +0000