aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/MakeCoq_MinGW.bat8
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh87
-rwxr-xr-xdev/build/windows/patches_coq/ocaml-4.07.1.patch97
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-fiat-crypto.sh2
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile4
-rw-r--r--dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh23
-rw-r--r--dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh12
-rw-r--r--dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh9
-rw-r--r--dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh9
-rw-r--r--dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh6
-rw-r--r--dev/ci/user-overlays/10358-gares-elpi13.sh6
-rw-r--r--dev/doc/changes.md28
-rwxr-xr-xdev/lint-commits.sh31
-rw-r--r--dev/tools/coqdev.el6
-rwxr-xr-xdev/tools/update-compat.py32
-rw-r--r--dev/top_printers.ml4
17 files changed, 288 insertions, 78 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 7c8f73c7e4..78ca5e830a 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -331,7 +331,9 @@ IF "%CYGWIN_QUIET%" == "Y" (
)
IF "%GTK_FROM_SOURCES%"=="N" (
- SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-gtksourceview3.0
+ SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk3,mingw64-%ARCH%-libxml2
+ REM gtksourceview3 is always built from sources until the bug in DLLMain is fixed in cygwin
+ REM SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtksourceview3.0
)
REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
@@ -362,6 +364,9 @@ IF NOT "%APPVEYOR%" == "True" (
ECHO "========== INSTALL CYGWIN =========="
+REM If you need to add packages, see https://cygwin.com/packages/package_list.html for package names
+REM In the description of each package you also find the file list and maintainer there
+
IF "%RUNSETUP%"=="Y" (
%SETUP% ^
--proxy "%PROXY%" ^
@@ -376,6 +381,7 @@ IF "%RUNSETUP%"=="Y" (
-P pkg-config ^
-P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
-P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+ -P adwaita-icon-theme ^
-P libiconv-devel,libunistring-devel,libncurses-devel ^
-P gettext-devel,libgettextpo-devel ^
-P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 549f70e8fe..0699e2bd44 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -104,7 +104,8 @@ cd /build
mkdir -p "$SOURCE_LOCAL_CACHE_CFMT"
# sysroot prefix for the above /build/host/target combination
-PREFIX=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
+# This must be in MFMT (C:/.../) because the OCaml library path is based on it and OCaml is a MinGW application.
+PREFIXMINGW=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
# Install / Prefix folder for COQ
PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
@@ -113,10 +114,10 @@ PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
if [ "$INSTALLOCAML" == "Y" ]; then
PREFIXOCAML=$PREFIXCOQ
else
- PREFIXOCAML=$PREFIX
+ PREFIXOCAML=$PREFIXMINGW
fi
-mkdir -p "$PREFIX/bin"
+mkdir -p "$PREFIXMINGW/bin"
mkdir -p "$PREFIXCOQ/bin"
mkdir -p "$PREFIXOCAML/bin"
@@ -487,7 +488,7 @@ function build_post {
function build_conf_make_inst {
if build_prep "$1" "$2" "$3" ; then
$4
- logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" "${@:5}"
+ logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXMINGW" "${@:5}"
# shellcheck disable=SC2086
log1 make $MAKE_OPT
log2 make install
@@ -895,9 +896,9 @@ function make_libxml2 {
# Note: latest release version 2.9.2 fails during configuring lzma, so using 2.9.1
# Note: python binding requires <sys/select.h> which doesn't exist on cygwin
if build_prep https://git.gnome.org/browse/libxml2/snapshot libxml2-2.9.1 tar.xz ; then
- # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --disable-shared --without-python
+ # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXMINGW" --disable-shared --without-python
# shared library required by gtksourceview
- ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" --without-python
+ ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXMINGW" --without-python
# shellcheck disable=SC2086
log1 make $MAKE_OPT all
log2 make install
@@ -910,14 +911,13 @@ function make_libxml2 {
function make_gtk_sourceview3 {
# Cygwin packet dependencies: intltool
- # gtksourceview-2.11.2 requires GTK2
- # gtksourceview-2.91.9 requires GTK3
- # => We use gtksourceview-2.11.2 which seems to be the newest GTK2 based one
+ # Note: this is always built from sources cause of a bug in the cygwin delivery.
+ # Just dependencies are only built if we build from sources
if [ "$GTK_FROM_SOURCES" == "Y" ]; then
make_gtk3
make_libxml2
- build_conf_make_inst https://download.gnome.org/sources/gtksourceview/3.24 gtksourceview-3.24.9 tar.bz2 true
fi
+ build_conf_make_inst https://download.gnome.org/sources/gtksourceview/3.24 gtksourceview-3.24.11 tar.xz make_arch_pkg_config
}
##### FLEXDLL FLEXLINK #####
@@ -930,7 +930,7 @@ function make_gtk_sourceview3 {
# Install flexdll objects
function install_flexdll {
- cp flexdll.h "/usr/$TARGET_ARCH/sys-root/mingw/include"
+ cp flexdll.h "$PREFIXMINGW/include"
if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin"
cp flexdll*_mingw.o "$PREFIXOCAML/bin"
@@ -1202,7 +1202,7 @@ function make_lablgtk {
function copy_coq_dll {
if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
- cp "/usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1" "$PREFIXCOQ/bin/$1"
+ cp "$PREFIXMINGW/bin/$1" "$PREFIXCOQ/bin/$1"
fi
}
@@ -1282,27 +1282,58 @@ function copy_coq_objects {
}
# Copy required GTK config and support files
+# This must be called from inside the coq build folder!
function copy_coq_gtk {
- echo 'gtk-theme-name = "Default"' > "$PREFIX/etc/gtk-3.0/gtkrc"
- echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-3.0/gtkrc"
+
+ glib-compile-schemas $PREFIXMINGW/share/glib-2.0/schemas/
+ echo 'gtk-theme-name = "Default"' > "$PREFIXMINGW/etc/gtk-3.0/gtkrc"
if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
- install_glob "$PREFIX/etc/gtk-3.0" '*' "$PREFIXCOQ/gtk-3.0"
- install_glob "$PREFIX/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
- install_glob "$PREFIX/share/gtksourceview-3.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-3.0/styles"
- install_rec "$PREFIX/share/themes" '*' "$PREFIXCOQ/share/themes"
+ install_glob "$PREFIXMINGW/etc/gtk-3.0" '*' "$PREFIXCOQ/gtk-3.0"
+ install -D -T "$PREFIXMINGW/share/glib-2.0/schemas/gschemas.compiled" "$PREFIXCOQ/share/glib-2.0/schemas/gschemas.compiled"
+
+ install_glob "$PREFIXMINGW/share/gtksourceview-3.0/language-specs" '*' "$PREFIXCOQ/share/gtksourceview-3.0/language-specs"
+ install -D -T "ide/coq.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq.lang"
+ install -D -T "ide/coq-ssreflect.lang" "$PREFIXCOQ/share/gtksourceview-3.0/language-specs/coq-ssreflect.lang"
+
+ install_glob "$PREFIXMINGW/share/gtksourceview-3.0/styles" '*' "$PREFIXCOQ/share/gtksourceview-3.0/styles"
+ install -D -T "ide/coq_style.xml" "$PREFIXCOQ/share/gtksourceview-3.0/styles/coq_style.xml"
+
+ install_rec "$PREFIXMINGW/share/themes" '*' "$PREFIXCOQ/share/themes"
+
+ FOLDERS=""
+ # The sizes include all default sizes given in index.theme
+ # The types used haven been recorded with ProcMon in an installation with all icons present
+ for SIZE in 16x16 22x22 32x32 48x48; do
+ for TYPE in \
+ actions/bookmark actions/document devices/drive actions/format-text actions/go actions/list \
+ actions/media actions/pan actions/process actions/system actions/window \
+ mimetypes/text places/folder places/user status/dialog
+ do
+ CLASS=$(dirname $TYPE)
+ ICON=$(basename $TYPE)
+ if [[ ! "$FOLDERS" =~ "$SIZE/$CLASS" ]] ;then
+ FOLDERS="$FOLDERS$SIZE/$CLASS,"
+ fi
+ install_rec "/usr/share/icons/Adwaita/$SIZE/$CLASS" "$ICON*" "$PREFIXCOQ/share/icons/Adwaita/$SIZE/$CLASS"
+ done
+ done
+ echo Folders=$FOLDERS
+ install -D -T "/usr/share/icons/Adwaita/index.theme" "$PREFIXCOQ/share/icons/Adwaita/index.theme"
+ sed -i "s|^Directories=.*|Directories=$FOLDERS|" "$PREFIXCOQ/share/icons/Adwaita/index.theme"
+ gtk-update-icon-cache -f "$PREFIXCOQ/share/icons/Adwaita/"
# This below item look like a bug in make install
- if [ -d "$PREFIXCOQ/share/coq/" ] ; then
- COQSHARE="$PREFIXCOQ/share/coq/"
- else
- COQSHARE="$PREFIXCOQ/share/"
- fi
-
- mkdir -p "$PREFIXCOQ/ide"
- mv "$COQSHARE"*.png "$PREFIXCOQ/ide"
- rmdir "$PREFIXCOQ/share/coq" || true
+ # if [ -d "$PREFIXCOQ/share/coq/" ] ; then
+ # COQSHARE="$PREFIXCOQ/share/coq/"
+ # else
+ # COQSHARE="$PREFIXCOQ/share/"
+ # fi
+
+ # mkdir -p "$PREFIXCOQ/ide"
+ # mv "$COQSHARE"*.png "$PREFIXCOQ/ide"
+ # rmdir "$PREFIXCOQ/share/coq" || true
fi
}
@@ -1454,7 +1485,7 @@ function make_gcc {
--enable-languages=c --disable-nls \
--disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
# --disable-decimal-float seems to be required
- # --with-sysroot="$PREFIX" results in configure error that this is not an absolute path
+ # --with-sysroot="$PREFIXMINGW" results in configure error that this is not an absolute path
# shellcheck disable=SC2086
log1 make $MAKE_OPT
log2 make install
diff --git a/dev/build/windows/patches_coq/ocaml-4.07.1.patch b/dev/build/windows/patches_coq/ocaml-4.07.1.patch
new file mode 100755
index 0000000000..2d61b5b838
--- /dev/null
+++ b/dev/build/windows/patches_coq/ocaml-4.07.1.patch
@@ -0,0 +1,97 @@
+diff/patch file created on Tue, Jun 11, 2019 10:15:38 AM with:
+difftar-folder.sh tarballs/ocaml-4.07.1.tar.gz ocaml-4.07.1 1
+TARFILE= tarballs/ocaml-4.07.1.tar.gz
+FOLDER= ocaml-4.07.1/
+TARSTRIP= 1
+TARPREFIX= ocaml-4.07.1/
+ORIGFOLDER= ocaml-4.07.1.orig
+--- ocaml-4.07.1.orig/byterun/caml/osdeps.h 2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/caml/osdeps.h 2019-06-11 10:13:50.766997600 +0200
+@@ -98,6 +98,11 @@
+ */
+ extern char_os *caml_secure_getenv(char_os const *var);
+
++/* Modify or delete environment variable.
++ Returns 0 on success or an error code.
++*/
++extern int caml_putenv(char_os const *var, char_os const *value);
++
+ /* If [fd] refers to a terminal or console, return the number of rows
+ (lines) that it displays. Otherwise, or if the number of rows
+ cannot be determined, return -1. */
+--- ocaml-4.07.1.orig/byterun/debugger.c 2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/debugger.c 2019-06-11 10:14:02.706013700 +0200
+@@ -180,6 +180,7 @@
+ if (address == NULL) return;
+ if (dbg_addr != NULL) caml_stat_free(dbg_addr);
+ dbg_addr = address;
++ caml_putenv(_T("CAML_DEBUG_SOCKET"),_T(""));
+
+ #ifdef _WIN32
+ winsock_startup();
+--- ocaml-4.07.1.orig/byterun/unix.c 2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/unix.c 2019-06-11 10:14:11.252438800 +0200
+@@ -430,6 +430,19 @@
+ #endif
+ }
+
++int caml_putenv(char_os const *var, char_os const *value)
++{
++ char_os * s;
++ int ret;
++
++ s = caml_stat_strconcat_os(3, var, _T("="), value);
++ ret = putenv_os(s);
++ if (ret == -1) {
++ caml_stat_free(s);
++ }
++ return ret;
++}
++
+ int caml_num_rows_fd(int fd)
+ {
+ #ifdef TIOCGWINSZ
+--- ocaml-4.07.1.orig/byterun/win32.c 2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1/byterun/win32.c 2019-06-11 10:14:19.485640700 +0200
+@@ -727,6 +727,19 @@
+ return _wgetenv(var);
+ }
+
++int caml_putenv(char_os const *var, char_os const *value)
++{
++ char_os * s;
++ int ret;
++
++ s = caml_stat_strconcat_os(3, var, _T("="), value);
++ ret = putenv_os(s);
++ if (ret == -1) {
++ caml_stat_free(s);
++ }
++ return ret;
++}
++
+ /* caml_win32_getenv is used to implement Sys.getenv and Unix.getenv in such a
+ way that they get direct access to the Win32 environment rather than to the
+ copy that is cached by the C runtime system. The result of caml_win32_getenv
+--- ocaml-4.07.1.orig/config/Makefile.mingw 2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1//config/Makefile.mingw 2019-06-11 10:14:44.492969800 +0200
+@@ -89,7 +89,7 @@
+ NATDYNLINK=true
+ NATDYNLINKOPTS=
+ CMXS=cmxs
+-RUNTIMED=false
++RUNTIMED=true
+ ASM_CFI_SUPPORTED=false
+ WITH_FRAME_POINTERS=false
+ UNIX_OR_WIN32=win32
+--- ocaml-4.07.1.orig/config/Makefile.mingw64 2018-10-04 15:38:56.000000000 +0200
++++ ocaml-4.07.1//config/Makefile.mingw64 2019-06-11 10:14:53.664784900 +0200
+@@ -89,7 +89,7 @@
+ NATDYNLINK=true
+ NATDYNLINKOPTS=
+ CMXS=cmxs
+-RUNTIMED=false
++RUNTIMED=true
+ ASM_CFI_SUPPORTED=false
+ WITH_FRAME_POINTERS=false
+ UNIX_OR_WIN32=win32
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 95fceb773a..fa39b41565 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -215,7 +215,7 @@
########################################################################
# simple-io
########################################################################
-: "${simple_io_CI_REF:=dev}"
+: "${simple_io_CI_REF:=master}"
: "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}"
: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index bba17314f7..e8c8d22678 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -11,7 +11,7 @@ git_download fiat_crypto
# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241
fiat_crypto_CI_TARGETS1="c-files printlite lite"
-fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem"
+fiat_crypto_CI_TARGETS2="coq"
( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \
ulimit -s 32768 && \
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 8eebb3af64..818454dbbc 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-04-20-V1"
+# CACHEKEY: "bionic_coq-V2019-06-11-V1"
# ^^ Update when modifying this file.
FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
# `num` does not have a version number as the right version to install varies
# with the compiler version.
ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \
- CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8"
+ CI_OPAM="menhir.20181113 elpi.1.3.1 ocamlgraph.1.8.8"
# BASE switch; CI_OPAM contains Coq's CI dependencies.
ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5"
diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh
new file mode 100644
index 0000000000..242b177d71
--- /dev/null
+++ b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh
@@ -0,0 +1,23 @@
+if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then
+
+ fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726
+ fiat_parsers_CI_REF=master+change-for-coq-pr8726
+ fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat
+
+ elpi_CI_BRANCH=coq-master+fix-global-pr8726
+ elpi_CI_REF=coq-master+fix-global-pr8726
+ elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+ equations_CI_BRANCH=master+fix-global-pr8726
+ equations_CI_REF=master+fix-global-pr8726
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+ mtac2_CI_BRANCH=master+fix-global-pr8726
+ mtac2_CI_REF=master+fix-global-pr8726
+ mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+ paramcoq_CI_BRANCH=master+fix-global-pr8726
+ paramcoq_CI_REF=master+fix-global-pr8726
+ paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh
new file mode 100644
index 0000000000..e4cf74aa51
--- /dev/null
+++ b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9566" ] || [ "$CI_BRANCH" = "proof_global+move_termination_routine_out" ]; then
+
+ aac_tactics_CI_REF=proof_global+move_termination_routine_out
+ aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+ equations_CI_REF=proof_global+move_termination_routine_out
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ paramcoq_CI_REF=proof_global+move_termination_routine_out
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi
diff --git a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh
new file mode 100644
index 0000000000..c8cf85e73e
--- /dev/null
+++ b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10231" ] || [ "$CI_BRANCH" = "master+locating-warning-different-implicit-term-type" ]; then
+
+ equations_CI_REF=master+fix-manual-implicit-pr10231
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+ mtac2_CI_REF=master+fix-manual-implicit-pr10231
+ mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh
new file mode 100644
index 0000000000..c5f1510357
--- /dev/null
+++ b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then
+
+ mtac2_CI_REF=vernac-when-sideff
+ mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+ equations_CI_REF=vernac-when-sideff
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh
new file mode 100644
index 0000000000..2c3f490c03
--- /dev/null
+++ b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then
+
+ equations_CI_REF=rm-kernel-sideeff-role
+ equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/10358-gares-elpi13.sh b/dev/ci/user-overlays/10358-gares-elpi13.sh
new file mode 100644
index 0000000000..d2ba9b5ddf
--- /dev/null
+++ b/dev/ci/user-overlays/10358-gares-elpi13.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10358" ] || [ "$CI_BRANCH" = "elpi-13-coq" ]; then
+
+ elpi_CI_REF="elpi-13-coq"
+ elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 339ac2d9b7..51d90df89f 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -5,6 +5,21 @@
- Functions and types deprecated in 8.10 have been removed in Coq
8.11.
+- Type Decl_kinds.locality has been restructured, see commit
+ message. Main change to do generally is to change the flag "Global"
+ to "Global ImportDefaultBehavior".
+
+Proof state:
+
+ Proofs that are attached to a top-level constant (such as lemmas)
+ are represented by `Lemmas.t`, as they do contain additional
+ information related to the constant declaration.
+
+ Plugins that require access to the information about currently
+ opened lemmas can add one of the `![proof]` attributes to their
+ `mlg` entry, which will refine the type accordingly. See
+ documentation in `vernacentries` for more information.
+
## Changes between Coq 8.9 and Coq 8.10
### ML4 Pre Processing
@@ -59,6 +74,19 @@ Coqlib:
command then enables to locate the registered constant through its name. The
name resolution is dynamic.
+Proof state:
+
+- Handling of proof state has been fully functionalized, thus it is
+ not possible to call global functions such as `get_current_context ()`.
+
+ The main type for functions that need to handle proof state is
+ `Proof_global.t`.
+
+ Unfortunately, this change was not possible to do in a
+ backwards-compatible way, but in most case the api changes are
+ straightforward, with functions taking and returning an extra
+ argument.
+
Macros:
- The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
index 96c92e3162..539bb5f1f9 100755
--- a/dev/lint-commits.sh
+++ b/dev/lint-commits.sh
@@ -19,21 +19,40 @@ fi
BASE_COMMIT="$1"
HEAD_COMMIT="$2"
-bad=()
+bad_ws=()
+bad_compile=()
while IFS= read -r commit; do
echo Checking "$commit"
# git diff --check
# uses .gitattributes to know what to check
if ! git diff --check "${commit}^" "$commit";
- then
- bad+=("$commit")
+ then bad_ws+=("$commit")
+ fi
+
+ if ! make -f Makefile.dune check
+ then bad_compile+=("$commit")
fi
done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --)
-if [ "${#bad[@]}" != 0 ]
+# report errors
+
+CODE=0
+
+if [ "${#bad_ws[@]}" != 0 ]
then
>&2 echo "Whitespace errors!"
- >&2 echo "In commits ${bad[*]}"
+ >&2 echo "In commits ${bad_ws[*]}"
>&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
- exit 1
+ >&2 echo
+ CODE=1
fi
+
+if [ "${#bad_compile[@]}" != 0 ]
+then
+ >&2 echo "Compilation errors!"
+ >&2 echo "In commits ${bad_compile[*]}"
+ >&2 echo
+ CODE=1
+fi
+
+exit $CODE
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index b89ae67a82..5f9f326750 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -78,11 +78,7 @@ Specifically `camldebug-command-name' and `ocamldebug-command-name'."
Note that this function is executed before _Coqproject is read if it exists."
(let ((dir (coqdev-default-directory)))
(when dir
- (unless coq-prog-args
- (setq coq-prog-args
- `("-coqlib" ,dir
- "-topfile" ,buffer-file-name)))
- (setq-local coq-prog-name (concat dir "bin/coqtop")))))
+ (setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude")))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)
(defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg"
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index ff9b32fe78..0338cd42c7 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -73,8 +73,6 @@ FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
-BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
-BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v')
TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
@@ -401,34 +399,6 @@ dev/tools/update-compat.py --assert-unchanged %s || exit $?
''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip()
update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args)
-def update_bug_4789(new_versions, **args):
- # we always update this compat notation to oldest
- # currently-supported compat version, which should never be the
- # current version
- with open(BUG_4798_PATH, 'r') as f: contents = f.read()
- new_contents = BUG_HEADER + r"""Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "%s").
-Check match 2 with 0 => 0 | S n => n end. (* fails *)
-""" % new_versions[0]
- update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
-
-def update_bug_9166(new_versions, **args):
- # we always update this compat notation to oldest
- # currently-supported compat version, which should never be the
- # current version
- with open(BUG_9166_PATH, 'r') as f: contents = f.read()
- new_contents = BUG_HEADER + r"""Set Warnings "+deprecated".
-
-Notation bar := option (compat "%s").
-
-Definition foo (x: nat) : nat :=
- match x with
- | 0 => 0
- | S bar => bar
- end.
-""" % new_versions[0]
- update_if_changed(contents, new_contents, BUG_9166_PATH, **args)
-
def update_compat_notations_in(old_versions, new_versions, contents):
for v in old_versions:
if v not in new_versions:
@@ -508,7 +478,5 @@ if __name__ == '__main__':
update_test_suite(new_versions, **args)
update_test_suite_run(**args)
update_doc_index(new_versions, **args)
- update_bug_4789(new_versions, **args)
- update_bug_9166(new_versions, **args)
update_compat_notations(known_versions, new_versions, **args)
display_git_grep(known_versions, new_versions)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4ce87faaa1..87b4d31054 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -533,7 +533,7 @@ let _ =
let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
- let cmd_class _ = VtQuery,VtNow in
+ let cmd_class _ = VtQuery in
let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
vernac_extend ~command:"PrintConstr" [cmd]
@@ -542,7 +542,7 @@ let _ =
let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
- let cmd_class _ = VtQuery,VtNow in
+ let cmd_class _ = VtQuery in
let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
vernac_extend ~command:"PrintPureConstr" [cmd]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 03:19:52 +0000