aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/build/windows/makecoq_mingw.sh2
-rw-r--r--dev/ci/README.md6
-rw-r--r--dev/ci/ci-common.sh4
-rwxr-xr-xdev/ci/ci-hott.sh2
-rw-r--r--dev/ci/user-overlays/07859-printers.sh6
-rw-r--r--dev/ci/user-overlays/07908-proj-mind.sh6
-rw-r--r--dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh6
-rw-r--r--dev/ci/user-overlays/08063-jasongross-string-eqb.sh6
-rw-r--r--dev/ocamldebug-coq.run2
-rw-r--r--dev/tools/coqdev.el2
-rw-r--r--dev/vm_printers.ml2
11 files changed, 30 insertions, 14 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index da5ac2b15c..aee4dd74d8 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -793,7 +793,7 @@ function make_ln {
function make_ocaml {
get_flex_dll_link_bin
- if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then
+ if build_prep https://github.com/ocaml/ocaml/archive/4.07.0 ocaml-4.07.0 tar.gz 1 ; then
# See README.win32.adoc
cp config/m-nt.h byterun/caml/m.h
cp config/s-nt.h byterun/caml/s.h
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 45176581cd..43d680af61 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -75,9 +75,6 @@ We are currently running tests on the following platforms:
camlp5, and with warnings as errors; it runs the test-suite and tests the
compilation of several external developments.
-- Circle CI runs tests that are redundant with GitLab CI and may be removed
- eventually.
-
- Travis CI is used to test the compilation of Coq and run the test-suite on
macOS. It also runs a linter that checks whitespace discipline. A
[pre-commit hook](../tools/pre-commit) is automatically installed by
@@ -165,8 +162,7 @@ automatically built and uploaded to your GitLab registry, and is
loaded by subsequent jobs.
**IMPORTANT**: When updating Coq's CI docker image, you must modify
-the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml),
-[`.circleci/config.yml`](../../.circleci/config.yml),
+the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml)
and [`Dockerfile`](docker/bionic_coq/Dockerfile)
The Docker building job reuses the uploaded image if it is available,
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index a68cd0933e..9259a6e0c8 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -20,10 +20,6 @@ else
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"
else # assume local
CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
export CI_BRANCH
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 6ded97984e..184b90a50b 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
-( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make )
+( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate )
diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh
new file mode 100644
index 0000000000..27f588e214
--- /dev/null
+++ b/dev/ci/user-overlays/07859-printers.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then
+ Equations_CI_BRANCH=fix-printers
+ Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07908-proj-mind.sh b/dev/ci/user-overlays/07908-proj-mind.sh
new file mode 100644
index 0000000000..293eeb5a5a
--- /dev/null
+++ b/dev/ci/user-overlays/07908-proj-mind.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7908" ] || [ "$CI_BRANCH" = "proj-mind" ]; then
+ Equations_CI_BRANCH=fix-proj-mind
+ Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
new file mode 100644
index 0000000000..56c0dc3433
--- /dev/null
+++ b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then
+ Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field
+ Equations_CI_GITURL=https://github.com/bollu/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
new file mode 100644
index 0000000000..99a11b9fbf
--- /dev/null
+++ b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then
+ quickchick_CI_BRANCH=fix-for-pr-8063
+ quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick
+fi
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 2bec09de2b..bccd3fefb4 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -33,7 +33,7 @@ if [ -z "$GUESS_CHECKER" ]; then
-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
-I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \
-I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
- -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
+ -I $COQTOP/plugins/firstorder \
-I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \
-I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \
-I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 70a9756e51..ec72f96509 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -33,7 +33,7 @@
(defun coqdev-default-directory ()
"Return the Coq repository containing `default-directory'."
- (let ((dir (locate-dominating-file default-directory "META.coq")))
+ (let ((dir (locate-dominating-file default-directory "META.coq.in")))
(when dir (expand-file-name dir))))
(defun coqdev-setup-compile-command ()
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index c8385da618..98190b05b5 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -17,7 +17,7 @@ let ppripos (ri,pos) =
| Reloc_getglobal kn ->
print_string ("getglob "^(Constant.to_string kn)^"\n")
| Reloc_proj_name p ->
- print_string ("proj "^(Constant.to_string p)^"\n")
+ print_string ("proj "^(Projection.Repr.to_string p)^"\n")
);
print_flush ()
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 12:39:58 +0000