diff options
Diffstat (limited to 'dev')
72 files changed, 416 insertions, 429 deletions
diff --git a/dev/base_include b/dev/base_include index b214959bad..f764eaf4f5 100644 --- a/dev/base_include +++ b/dev/base_include @@ -185,7 +185,7 @@ open Declareops;; let constbody_of_string s = let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in - Option.get (Global.body_of_constant_body b);; + Option.get (Global.body_of_constant_body Library.indirect_accessor b);; (* Get the current goal *) (* diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index c3f3a97ff5..78ca5e830a 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -285,9 +285,9 @@ SET RESULT_INSTALLDIR_WFMT=%DESTCOQ% SET TARGET_ARCH=%ARCH%-w64-mingw32
SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
-REM Convert pathes to various formats
+REM Convert paths to various formats
REM WFMT = windows format (C:\..) Used in this batch file.
-REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM CFMT = cygwin format (\cygdrive\c\..) Used for Cygwin PATH variable, which is : separated, so C: doesn't work.
REM MFMT = MinGW format (C:/...) Used for the build, because \\ requires escaping. Mingw can handle \ and /.
SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
@@ -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 ^
@@ -429,13 +435,13 @@ ECHO ========== BATCH FUNCTIONS ========== REM 01234567890123456789012345678901234567890123456789012345678901234567890123456789
ECHO -arch ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
ECHO -mode ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
- ECHO ^<absoloute = install coq in -destcoq absulute path^>
+ ECHO ^<absolute = install coq in -destcoq absolute path^>
ECHO ^<relocatable = install relocatable coq in -destcoq path^>
ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
ECHO -ocaml ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
ECHO -make ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
ECHO -destcyg ^<path to cygwin destination folder^>
- ECHO -destcoq ^<path to coq destination folder (mode=absoloute/relocatable)^>
+ ECHO -destcoq ^<path to coq destination folder (mode=absolute/relocatable)^>
ECHO -setup ^<cygwin setup program name^> (auto adjusted to -arch)
ECHO -proxy ^<internet proxy^>
ECHO -cygrepo ^<cygwin download repository^>
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index a392115ea4..052014824f 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -43,7 +43,7 @@ paths like "C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys DLL. The missing piece is a posix shell running on plain Windows (without msys or -Cygwin DLL) and not beeing a binary from obscure sources. I am working on it ... +Cygwin DLL) and not being a binary from obscure sources. I am working on it ... Since compiling gcc and binutils takes a while and it is not of much use without a shell, the building of these components is currently disabled. OCaml is built @@ -131,7 +131,7 @@ mingwinCygwin: Install coq in the default Cygwin mingw sysroot folder. Todo: The coq share folder should be configured to e.g. /share/coq. As is, coqc scans the complete share folder, which slows it down 5x for short files. -absoloute: Install coq in the absolute path given with -destcoq. +absolute: Install coq in the absolute path given with -destcoq. The resulting Coq will not be relocatable. That is the root folder must not be renamed/moved. @@ -274,11 +274,11 @@ Default value: N ===== -cygquiet ===== -Control if the Cygwin setup runs quitely or interactive. +Control if the Cygwin setup runs quietly or interactive. Possible values: -Y: Install Cygwin quitely without user interaction. +Y: Install Cygwin quietly without user interaction. N: Install Cygwin interactively (allows to select additional packages). @@ -299,7 +299,7 @@ The version of Coq to download and compile. Possible values: 8.4pl6, 8.5pl2, 8.5pl3, 8.6 (download from https://coq.inria.fr/distrib/V$COQ_VERSION/files/coq-<version>.tar.gz) Others versions might work, but are untested. - 8.4 is only tested in mode=absoloute + 8.4 is only tested in mode=absolute git-v8.6, git-trunk (download from https://github.com/coq/coq/archive/<version without git->.zip) @@ -344,12 +344,12 @@ selecting more packages) ==================== TODO ==================== - Check for spaces in destination paths -- Check for = signs in all paths (DOS commands don't work with pathes with = in it, possibly even when quoted) +- Check for = signs in all paths (DOS commands don't work with paths with = in it, possibly even when quoted) - Installer doesn't remove OCAMLLIB environment variables (it is in the script, but doesn't seem to work) - CoqIDE doesn't find theme files - Finish / test mingw_in_Cygwin mode (coqide doesn't start, coqc slow cause of scanning complete share folder) -- Possibly create/login as specific user to bash (not sure if it makes sense - nead to create additional bash login link then) -- maybe move share/doc/menhir somehwere else (reduces coqc startup time) +- Possibly create/login as specific user to bash (not sure if it makes sense - need to create additional bash login link then) +- maybe move share/doc/menhir somewhere else (reduces coqc startup time) - Use original installed file list for removing files in uninstaller ==================== Issues with relocation ==================== diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh index 3bba451ec6..543ca972cd 100644 --- a/dev/build/windows/difftar-folder.sh +++ b/dev/build/windows/difftar-folder.sh @@ -40,7 +40,7 @@ fi # Get path prefix if --strip is used if [ "$strip" -gt 0 ] ; then - # Get the path/name of the first file from teh tar and extract the first $strip path components + # Get the path/name of the first file from the tar and extract the first $strip path components # This assumes that the first file in the tar file has at least $strip many path components prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/ else diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d737632638..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 @@ -765,7 +766,7 @@ function make_ncurses { # gettext make/make install work anyway # # CONFIGURE PARAMETERS - # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW) + # --enable-term-driver --enable-sp-funcs is required for mingw (see README.MinGW) # additional changes # ADD --with-pkg-config # ADD --enable-pc-files @@ -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 } @@ -1281,28 +1281,59 @@ function copy_coq_objects { done } -# Copy required GTK config and suport files +# 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/build/windows/patches_coq/pkg-config.c b/dev/build/windows/patches_coq/pkg-config.c index e4fdcd4d7d..c4c7ec2bff 100755 --- a/dev/build/windows/patches_coq/pkg-config.c +++ b/dev/build/windows/patches_coq/pkg-config.c @@ -1,5 +1,5 @@ // MinGW personality wrapper for pkgconf -// This is an excutable replacement for the shell scripts /bin/ARCH-pkg-config +// This is an executable replacement for the shell scripts /bin/ARCH-pkg-config // Compile with e.g. // gcc pkg-config.c -DARCH=x86_64-w64-mingw32 -o pkg-config.exe // gcc pkg-config.c -DARCH=i686-w64-mingw32 -o pkg-config.exe diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 98ea594366..408d36df7f 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -31,7 +31,7 @@ PR by running GitLab CI on your private branches. To do so follow these steps: 6. You are encouraged to go to the CI / CD general settings and increase the timeout from 1h to 2h for better reliability. -Now everytime you push (including force-push unless you changed the default +Now every time you push (including force-push unless you changed the default GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and CI will be run. You will receive an e-mail with a report of the failures if there are some. 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/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 95f143bb95..d99e140bce 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -8,14 +8,14 @@ install_ssreflect # Setup lambdaRust first git_download lambdaRust -# Extract required version of Iris -Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) +Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris git_download Iris # Extract required version of std++ -stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp 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/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh deleted file mode 100644 index 2b4c1489ad..0000000000 --- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh +++ /dev/null @@ -1,13 +0,0 @@ -_OVERLAY_BRANCH=ho-matching-occ-sel - -if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - unicoq_CI_REF="PR7819-overlay" - - mtac2_CI_REF="PR7819-overlay" - mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 - - equations_CI_GITURL=https://github.com/mattam82/Coq-Equations - equations_CI_REF="PR7819-overlay" - -fi 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/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh deleted file mode 100644 index 67f6f8610a..0000000000 --- a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then - - ltac2_CI_REF=master-parsing-decimal - ltac2_CI_GITURL=https://github.com/proux01/ltac2 - - quickchick_CI_REF=master-parsing-decimal - quickchick_CI_GITURL=https://github.com/proux01/QuickChick - - Corn_CI_REF=master-parsing-decimal - Corn_CI_GITURL=https://github.com/proux01/corn - - HoTT_CI_REF=master-parsing-decimal - HoTT_CI_GITURL=https://github.com/proux01/HoTT - - stdlib2_CI_REF=master-parsing-decimal - stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 - -fi diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh deleted file mode 100644 index 81e18226ed..0000000000 --- a/dev/ci/user-overlays/08817-sprop.sh +++ /dev/null @@ -1,34 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then - aac_tactics_CI_REF=sprop - aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics - - coq_dpdgraph_CI_REF=sprop - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - - coqhammer_CI_REF=sprop - coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer - - elpi_CI_REF=sprop - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=sprop - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - ltac2_CI_REF=sprop - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - unicoq_CI_REF=sprop - unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq - - mtac2_CI_REF=sprop - mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 - - paramcoq_CI_REF=sprop - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - quickchick_CI_REF=sprop - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - - relation_algebra_CI_REF=sprop - relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra -fi diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh deleted file mode 100644 index c04621114f..0000000000 --- a/dev/ci/user-overlays/08829-proj-syntax-check.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then - lambdaRust_CI_REF=proj-syntax-check - lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust - lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive -fi 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 deleted file mode 100644 index dc39ea5ef0..0000000000 --- a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh +++ /dev/null @@ -1,7 +0,0 @@ -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 diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh deleted file mode 100644 index 12be1b676a..0000000000 --- a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then - - HoTT_CI_REF=rm-hardwired-hint-db - HoTT_CI_GITURL=https://github.com/vbgl/HoTT - - ltac2_CI_REF=rm-hardwired-hint-db - ltac2_CI_GITURL=https://github.com/vbgl/ltac2 - - UniMath_CI_REF=rm-hardwired-hint-db - UniMath_CI_GITURL=https://github.com/vbgl/UniMath - -fi diff --git a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh deleted file mode 100644 index c09d1b8929..0000000000 --- a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh +++ /dev/null @@ -1,30 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9129" ] || [ "$CI_BRANCH" = "proof+no_global_partial" ]; then - - aac_tactics_CI_REF=proof+no_global_partial - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - # coqhammer_CI_REF=proof+no_global_partial - # coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - - elpi_CI_REF=proof+no_global_partial - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=proof+no_global_partial - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_REF=proof+no_global_partial - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - # unicoq_CI_REF=proof+no_global_partial - # unicoq_CI_GITURL=https://github.com/ejgallego/unicoq - - mtac2_CI_REF=proof+no_global_partial - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+no_global_partial - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=proof+no_global_partial - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh deleted file mode 100644 index 1e1d36d54a..0000000000 --- a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then - - elpi_CI_REF=recarg-cleanup - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - quickchick_CI_REF=recarg-cleanup - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh deleted file mode 100644 index 23eb24c304..0000000000 --- a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then - - ltac2_CI_REF=proofview+proof_info - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - fiat_parsers_CI_REF=proofview+proof_info - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - -fi diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh deleted file mode 100644 index 1110157069..0000000000 --- a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then - - equations_CI_REF=set-implicits - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - mtac2_CI_REF=set-implicits - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh deleted file mode 100644 index cca85a2f68..0000000000 --- a/dev/ci/user-overlays/09439-sep-variance.sh +++ /dev/null @@ -1,14 +0,0 @@ - -if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then - elpi_CI_REF=sep-variance - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=sep-variance - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - mtac2_CI_REF=sep-variance - mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 - - paramcoq_CI_REF=sep-variance - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq -fi diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh deleted file mode 100644 index 1af8b5430d..0000000000 --- a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then - - quickchick_CI_REF=context-constructor - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - - equations_CI_REF=context-constructor - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -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/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh deleted file mode 100644 index 27ce9aca16..0000000000 --- a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then - - equations_CI_REF=hooks_unify - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=hooks_unify - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=hooks_unify - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh deleted file mode 100644 index 18a295cdbb..0000000000 --- a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then - - equations_CI_REF=more-delta-in-termination-checking - equations_CI_GITURL=https://github.com/gares/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh deleted file mode 100644 index ccb3498764..0000000000 --- a/dev/ci/user-overlays/09678-printed-by-env.sh +++ /dev/null @@ -1,14 +0,0 @@ - -if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then - elpi_CI_REF=printed-by-env - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - equations_CI_REF=printed-by-env - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - - ltac2_CI_REF=printed-by-env - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - quickchick_CI_REF=printed-by-env - quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick -fi diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh deleted file mode 100644 index b17454fc4c..0000000000 --- a/dev/ci/user-overlays/09733-gares-quotations.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then - - ltac2_CI_REF=quotations - ltac2_CI_GITURL=https://github.com/gares/ltac2 - -fi diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh deleted file mode 100644 index 4b49011de3..0000000000 --- a/dev/ci/user-overlays/09815-token-type.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then - ltac2_CI_REF=token-type - ltac2_CI_GITURL=https://github.com/proux01/ltac2 -fi diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh deleted file mode 100644 index bb14a8c204..0000000000 --- a/dev/ci/user-overlays/09870-vbgl-recordops.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then - - elpi_CI_REF=pr-9870 - elpi_CI_GITURL=https://github.com/vbgl/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh deleted file mode 100644 index 01d3068591..0000000000 --- a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh +++ /dev/null @@ -1,21 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then - - elpi_CI_REF=pretyping-rm-global - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - coqhammer_CI_REF=pretyping-rm-global - coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer - - equations_CI_REF=pretyping-rm-global - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - - ltac2_CI_REF=pretyping-rm-global - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - paramcoq_CI_REF=pretyping-rm-global - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - - mtac2_CI_REF=pretyping-rm-global - mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh deleted file mode 100644 index 9a6e25d893..0000000000 --- a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then - - elpi_CI_REF=overlay-elpi1.2-coq-master - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi 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 deleted file mode 100644 index 9f9cc19e83..0000000000 --- a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh +++ /dev/null @@ -1,6 +0,0 @@ -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 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 deleted file mode 100644 index 0e1449f36c..0000000000 --- a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh +++ /dev/null @@ -1,6 +0,0 @@ -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 diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh deleted file mode 100644 index 2015935dd9..0000000000 --- a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh +++ /dev/null @@ -1,6 +0,0 @@ -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 diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh deleted file mode 100644 index 4032b1c6b5..0000000000 --- a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh +++ /dev/null @@ -1,6 +0,0 @@ -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 diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh deleted file mode 100644 index bc8aa33565..0000000000 --- a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then - - unicoq_CI_REF=detype-anonymous - unicoq_CI_GITURL=https://github.com/maximedenes/unicoq - -fi diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh new file mode 100644 index 0000000000..c584438b21 --- /dev/null +++ b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then + + quickchick_CI_REF=instance-no-bang + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + +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/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh new file mode 100644 index 0000000000..735b2ebbc3 --- /dev/null +++ b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "10362" ] || [ "$CI_BRANCH" = "delay-poly-opaque" ]; then + + paramcoq_CI_REF=delay-poly-opaque + paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq + + elpi_CI_REF=delay-poly-opaque + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + coqhammer_CI_REF=delay-poly-opaque + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + + coq_dpdgraph_CI_REF=delay-poly-opaque + coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 7fb73e447d..4c2f264a74 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -21,14 +21,14 @@ The name of your overlay file should start with a five-digit pull request number, followed by a dash, anything (for instance your GitHub nickname and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). -Example: `00669-maximedenes-ssr-merge.sh` containing +Example: `10185-SkySkimmer-instance-no-bang.sh` containing ``` -#!/bin/sh +if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then + + quickchick_CI_REF=instance-no-bang + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_REF=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index c9eceb1270..66f5a96802 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -92,7 +92,7 @@ When fixes are ready, there are two cases to consider: Once all reviewers approved the PR, the assignee is expected to check that CI completed without relevant failures, and that the PR comes with appropriate documentation and test cases. If not, they should leave a comment on the PR and -put the approriate label. Otherwise, they are expected to merge the PR using the +put the appropriate label. Otherwise, they are expected to merge the PR using the [merge script](../tools/merge-pr.sh). When CI has a few failures which look spurious, restarting the corresponding diff --git a/dev/doc/archive/naming-conventions.tex b/dev/doc/archive/naming-conventions.tex index 0b0811d81b..8b0b14efb8 100644 --- a/dev/doc/archive/naming-conventions.tex +++ b/dev/doc/archive/naming-conventions.tex @@ -570,11 +570,11 @@ Example: \formula{eq\_true\_neg: \~{} eq\_true b <-> eq\_true (negb b)}. Zero on domain {\D} & D0 & (notation \verb=0=)\\ One on domain {\D} & D1 (if explicitly defined) & (notation \verb=1=)\\ Successor on domain {\D} & Dsucc\\ -Predessor on domain {\D} & Dpred\\ -Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existng libraries that already use \texttt{plus} and \texttt{mult}} +Predecessor on domain {\D} & Dpred\\ +Addition on domain {\D} & Dadd/Dplus\footnote{Coq historically uses \texttt{plus} and \texttt{mult} for addition and multiplication which are inconsistent notations, the recommendation is to use \texttt{add} and \texttt{mul} except in existing libraries that already use \texttt{plus} and \texttt{mult}} & (infix notation \verb=+= [50,L])\\ Multiplication on domain {\D} & Dmul/Dmult\footnotemark[\value{footnote}] & (infix notation \verb=*= [40,L]))\\ -Soustraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ +Subtraction on domain {\D} & Dminus & (infix notation \verb=-= [50,L])\\ Opposite on domain {\D} & Dopp (if any) & (prefix notation \verb=-= [35,R]))\\ Inverse on domain {\D} & Dinv (if any) & (prefix notation \verb=/= [35,R]))\\ Power on domain {\D} & Dpower & (infix notation \verb=^= [30,R])\\ diff --git a/dev/doc/archive/versions-history.tex b/dev/doc/archive/versions-history.tex index 25dabad497..46516dd4e4 100644 --- a/dev/doc/archive/versions-history.tex +++ b/dev/doc/archive/versions-history.tex @@ -372,7 +372,7 @@ Coq V8.4pl5& released 22 October 2014 & \\ Coq V8.4pl6& released 9 April 2015 & \\ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ -&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{asynchronous evaluation} [8-8-2013]\\ && \feature{new proof engine deployed} [2-11-2013]\\ && \feature{universe polymorphism} [6-5-2014]\\ && \feature{primitive projections} [6-5-2014]\\ diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index b0a2b04121..6bbf83aa7e 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -9,13 +9,13 @@ HISTORY: * March 2010 (Pierre Letouzey). Revised build system. In particular, no more stage1,2,3 : - - Stage3 was removed some time ago when coqdep was splitted into + - Stage3 was removed some time ago when coqdep was split into coqdep_boot and full coqdep. - Stage1,2 were replaced by brutal inclusion of all .d at the start of Makefile.build, without trying to guess what could be done at what time. Some initial inclusions hence _fail_, but "make" tries again later and succeed. - - Btw, .ml4 are explicitely turned into .ml files, which stay after build. + - Btw, .ml4 are explicitly turned into .ml files, which stay after build. By default, they are in binary ast format, see READABLE_ML4 option. * February 2014 (Pierre Letouzey). @@ -87,8 +87,8 @@ Cons: clear-text generated .ml. -Makefiles hierachy ------------------- +Makefiles hierarchy +------------------- The Makefile is separated in several files : @@ -101,7 +101,7 @@ The Makefile is separated in several files : FIND_SKIP_DIRS ---------------- +-------------- The recommended style of using FIND_SKIP_DIRS is for example diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 49251d61a1..372e40a0b7 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -108,14 +108,14 @@ automatically. You can use `ocamldebug` with Dune; after a build, do: ``` -dune exec dev/dune-dbg +dune exec dev/dune-dbg /path/to/foo.v (ocd) source dune_db ``` or ``` -dune exec dev/dune-dbg checker +dune exec dev/dune-dbg checker Foo (ocd) source dune_db ``` @@ -124,6 +124,8 @@ refined, so you need to build enough of Coq once to use this target [it will then correctly compute the deps and rebuild if you call the script again] This will be fixed in the future. +For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. + ## Dropping from coqtop: After doing `make -f Makefile.dune voboot`, the following commands should work: diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 8cefe699cc..a14781a058 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -18,8 +18,8 @@ See http://www.gnu.org/software/make/manual/make.htmlPrerequisite-Types * Annotation before commands: +/-/@ a command starting by - is always successful (errors are ignored) -a command starting by + is runned even if option -n is given to make -a command starting by @ is not echoed before being runned +a command starting by + is run even if option -n is given to make +a command starting by @ is not echoed before being run * Custom functions @@ -36,7 +36,7 @@ If the file given to -include doesn't exist, make tries to build it, and even retries again if necessary, but doesn't care if this build finally fails. We used to rely on this "feature", but this should not be the case anymore. We kept "-include" instead of "include" for -avoiding warnings about initially non-existant files. +avoiding warnings about initially non-existent files. Changes (for old-timers) ------------------------ diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7221c3de56..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 @@ -1278,7 +1306,7 @@ next_global_ident_away true -> next_ident_away_in_goal next_global_ident_away false -> next_global_ident_away ``` -### Cleaning in commmand.ml +### Cleaning in command.ml Functions about starting/ending a lemma are in lemmas.ml Functions about inductive schemes are in indschemes.ml @@ -1593,7 +1621,7 @@ Other kinds of objects: #### Writing subst_thing functions -The subst_thing shoud not copy the thing if it hasn't actually +The subst_thing should not copy the thing if it hasn't actually changed. There are some cool emacs macros in dev/objects.el to help writing subst functions this way quickly and without errors. Also there are *_smartmap functions in Util. diff --git a/dev/doc/econstr.md b/dev/doc/econstr.md index bb17e8fb62..16abf3f519 100644 --- a/dev/doc/econstr.md +++ b/dev/doc/econstr.md @@ -25,7 +25,7 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter Essentially, each time it sees an evar which happens to be defined in the provided evar-map, it replaces it with the corresponding body and carries on. -Due to universe unification occuring at the tactic level, the same goes for +Due to universe unification occurring at the tactic level, the same goes for universe instances and sorts. See the `ESort` and `EInstance` modules in `EConstr`. diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 774552237a..a2c8d2f5ac 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -121,7 +121,7 @@ a limited set of derivation rules), it is recommended to generate proofs as much as possible by refining in ML tactics when it is possible and easy enough. Indeed, this prevents dependence on fragile constructions such as unification. -Obviously, it does not forbid the use of tacticals to mimick what one would do +Obviously, it does not forbid the use of tacticals to mimic what one would do in Ltac. Each Ltac primitive has a corresponding ML counterpart with simple semantics. A list of such tacticals can be found in the `Tacticals` module. Most of them are a porting of the tacticals from the old engine to the new one, so diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 189d6f9fa5..452160ea5a 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -113,7 +113,7 @@ - [ ] Upload the new version of the reference manual to the website. *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release - and send annoucement e-mails. + and send announcement e-mails. - [ ] Ping **@Zimmi48** to publish a new version on Zenodo. *TODO: automate this.* - [ ] Close the milestone diff --git a/dev/doc/universes.md b/dev/doc/universes.md index c276603ed2..026c3830a2 100644 --- a/dev/doc/universes.md +++ b/dev/doc/universes.md @@ -163,9 +163,9 @@ only, it's just a matter of using `Evd.fresh_global` / The universe graph ------------------ -To accomodate universe polymorphic definitions, the graph structure in +To accommodate universe polymorphic definitions, the graph structure in kernel/univ.ml was modified. The new API forces every universe to be -declared before it is mentionned in any constraint. This forces to +declared before it is mentioned in any constraint. This forces to declare every universe to be >= Set or > Set. Every universe variable introduced during elaboration is >= Set. Every _global_ universe is now declared explicitly > Set, _after_ typechecking the definition. In diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index 48671c03b6..e23d1234f7 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -437,7 +437,7 @@ Searches for objects that satisfy a list of constraints. If `${positiveConstrain * Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. * SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string. * In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure. -* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*. +* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is omitted*. ------------------------------- @@ -3,7 +3,7 @@ (public_name coq.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) - (modules :standard) + (modules top_printers) (optional) (libraries coq.toplevel coq.plugins.ltac)) @@ -11,7 +11,7 @@ (targets dune-dbg) (deps dune-dbg.in ../checker/coqchk.bc - ../topbin/coqtop_byte_bin.bc + ../topbin/coqc_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 80ad0500e0..bd0a837938 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,11 +3,14 @@ # Run in a proper install dune env. case $1 in checker) + shift exe=_build/default/checker/coqchk.bc ;; *) - exe=_build/default/topbin/coqtop_byte_bin.bc + exe=_build/default/topbin/coqc_bin.bc ;; esac -ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe +emacs="${INSIDE_EMACS:+-emacs}" + +ocamldebug $emacs $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe "$@" diff --git a/dev/header.c b/dev/header.c index 663c43b3d6..6201cb3b73 100644 --- a/dev/header.c +++ b/dev/header.c @@ -1,6 +1,6 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ /* <O___,, * (see CREDITS file for the list of authors) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ diff --git a/dev/header.ml b/dev/header.ml index 7c3ee60040..87553dcb56 100644 --- a/dev/header.ml +++ b/dev/header.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/dev/header.py b/dev/header.py index f81c8aa6a2..86114503d4 100644 --- a/dev/header.py +++ b/dev/header.py @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index d8043558eb..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 "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." - exit 1 + >&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." + >&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/nsis/coq.nsi b/dev/nsis/coq.nsi index f48013cf2e..b4c5d3d528 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -6,7 +6,7 @@ ;SetCompress off SetCompressor lzma -; Comment out after debuging. +; Comment out after debugging. ; The VERSION should be passed as an argument at compile time using : ; diff --git a/dev/tools/change-header b/dev/tools/change-header index 687c02f4f1..59c6f43958 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -13,22 +13,19 @@ newheader=$2 if [ ! -f $oldheader ]; then echo Cannot read file $oldheader; exit 1; fi if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi -n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"` -nsucc=`expr $n + 1` - -linea='(* -*- coding:utf-8 -*- *)' -lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' +n=$(wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g") +nsucc=$(expr $n + 1) modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do - headline=`head -n 1 $i` - if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then - # Has emacs header +for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do + headline=$(head -n 1 $i) + if $(echo $headline | grep "(\* -\*- .* \*)" > /dev/null) || $(echo $headline | grep "^#\!" > /dev/null); then + # Has header head -n +$nsucc $i | tail -n $n > $i.head.tmp$$ hasheadline=1 - nnext=`expr $nsucc + 1` + nnext=$(expr $nsucc + 1) else head -n +$n $i > $i.head.tmp$$ hasheadline=0 @@ -44,9 +41,9 @@ for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o cat $newheader >> $i.tmp$$ tail -n +$nnext $i >> $i.tmp$$ mv $i.tmp$$ $i - modified=`expr $modified + 1` + modified=$(expr $modified + 1) else - kept=`expr $kept + 1` + kept=$(expr $kept + 1) fi rm $i.head.tmp$$ done diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index c6687b9731..5f9f326750 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -78,13 +78,38 @@ 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" + "Command run by `coqdev-ocamldebug'") + +(defun coqdev-ocamldebug () + "Runs a command in an ocamldebug buffer." + (interactive) + (let* ((dir (read-directory-name "Run from directory: " + (coqdev-default-directory))) + (name "ocamldebug-coq") + (buffer-name (concat "*" name "*"))) + (pop-to-buffer buffer-name) + (unless (comint-check-proc buffer-name) + (setq default-directory dir) + (setq coqdev-ocamldebug-command + (read-from-minibuffer "Command to run: " + coqdev-ocamldebug-command)) + (let* ((cmdlist (tuareg--split-args coqdev-ocamldebug-command)) + (cmdlist (mapcar #'substitute-in-file-name cmdlist))) + (apply #'make-comint name + (car cmdlist) + nil + (cdr cmdlist)) + (set-process-filter (get-buffer-process (current-buffer)) + #'ocamldebug-filter) + (set-process-sentinel (get-buffer-process (current-buffer)) + #'ocamldebug-sentinel) + (ocamldebug-mode))) + (ocamldebug-set-buffer))) + ;; This Elisp snippet adds a regexp parser for the format of Anomaly ;; backtraces (coqc -bt ...), to the error parser of the Compilation ;; mode (C-c C-c: "Compile command: ..."). File locations in traces 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 2859b56cbe..8343853af5 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -532,8 +532,8 @@ let _ = let open Vernacextend in 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 ~st = in_current_context econstr_display c; st in - let cmd_class _ = VtQuery,VtNow in + let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) 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] @@ -541,8 +541,8 @@ let _ = let open Vernacextend in 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 ~st = in_current_context print_pure_econstr c; st in - let cmd_class _ = VtQuery,VtNow in + let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) 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] diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 2aa1808322..5a2144f996 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex index ae4b569b36..84894b6f7c 100644 --- a/dev/v8-syntax/memo-v8.tex +++ b/dev/v8-syntax/memo-v8.tex @@ -55,7 +55,7 @@ _ are allowed after the first character. Quoted strings are used typically to give a filename (which may not be a regular identifier). As before they are written between double quotes ("). Unlike for V7, there is no escape character: characters -are written normaly but the double quote which is doubled. +are written normally but the double quote which is doubled. \section{Main changes in terms w.r.t. V7} @@ -252,7 +252,7 @@ became \TERM{context}. Syntax is unified with subterm matching. \subsection{Occurrences} -To avoid ambiguity between a numeric literal and the optionnal +To avoid ambiguity between a numeric literal and the optional occurrence numbers of this term, the occurrence numbers are put after the term itself. This applies to tactic \TERM{pattern} and also \TERM{unfold} diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index dd3908c25f..601d52ddda 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -1167,7 +1167,6 @@ $$ \nlsep \TERM{Show}~\OPT{\NT{num}} \nlsep \TERM{Show}~\TERM{Implicit}~\TERM{Arguments}~\OPT{\NT{num}} \nlsep \TERM{Show}~\TERM{Node} -\nlsep \TERM{Show}~\TERM{Script} \nlsep \TERM{Show}~\TERM{Existentials} \nlsep \TERM{Show}~\TERM{Tree} \nlsep \TERM{Show}~\TERM{Conjecture} |