diff options
118 files changed, 1115 insertions, 1039 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 213b87735..1a3c99369 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -38,13 +38,11 @@ Whitespace discipline (do not indent using tabs, no trailing spaces, text files Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. -- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22%20) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. +- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. - [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments. -- [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicates the PR needs testing. This is often used when testing beyond what the test suite can handle is required. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing. +- [needs: benchmarking](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22) and [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing. -The release manager uses the following filter to know which PRs seem ready for merge. If you are waiting for a PR to be merged, make sure it appears in this list: - -- [Pull requests ready for merge](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Apr%20is%3Aopen%20-label%3A%22needs%3A%20discussion%22%20-label%3A%22needs%3A%20testing%22%20-label%3A%22needs%3A%20fixing%22%20-label%3A%22needs%3A%20progress%22%20-label%3A%22needs%3A%20rebase%22%20-label%3A%22needs%3A%20review%22%20-label%3A%22needs%3A%20help%22%20-label%3A%22needs%3A%20independent%20fix%22%20-label%3A%22needs%3A%20feedback%22%20-label%3A%22help%20wanted%22%20-review%3Achanges_requested%20-status%3Apending%20base%3Amaster%20sort%3Aupdated-asc%20-label%3A%22needs%3A%20squashing%22%20) +To learn more about the merging process, you can read the [merging documentation for Coq maintainers](/dev/doc/MERGING.md). ## Documentation @@ -52,7 +50,7 @@ Currently the process for contributing to the documentation is the same as for c Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a [GitHub issue search](https://github.com/coq/coq/issues?q=is%3Aopen+is%3Aissue+label%3A%22kind%3A+documentation%22). Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code. -The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/refman`](/doc/refman). These are written in LaTeX and compiled to HTML with [HeVeA](http://hevea.inria.fr/). +The sources for the [Coq reference manual](https://coq.inria.fr/distrib/current/refman/) are at [`doc/sphinx`](/doc/sphinx). These are written in reStructuredText and compiled to HTML and PDF with [Sphinx](http://www.sphinx-doc.org/). You may also contribute to the informal documentation available in [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ). Both of these are editable by anyone with a GitHub account. diff --git a/Makefile.doc b/Makefile.doc index ecc68979e..fc791ce1c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,13 +60,11 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Universes.v.tex \ - Misc.v.tex) + Universes.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ - RefMan-uti.tex \ - AsyncProofs.tex) \ + RefMan-uti.tex) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index dc33838f1..c450e8157 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -10,19 +10,19 @@ VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml) APP=bin/CoqIDE_${VERSION}.app # Create a .app file with CoqIDE, without signing it -make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP +make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP" # Add Coq to the .app file -make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop +make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop # Create the dmg bundle -mkdir -p $DMGDIR -ln -sf /Applications $DMGDIR/Applications -cp -r $APP $DMGDIR +mkdir -p "$DMGDIR" +ln -sf /Applications "$DMGDIR/Applications" +cp -r "$APP" "$DMGDIR" mkdir -p _build # Temporary countermeasure to hdiutil error 5341 # head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg +hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg" diff --git a/dev/build/windows/MakeCoq_88git_installer.bat b/dev/build/windows/MakeCoq_88git_installer.bat new file mode 100755 index 000000000..b016fb389 --- /dev/null +++ b/dev/build/windows/MakeCoq_88git_installer.bat @@ -0,0 +1,27 @@ +@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== BUILD COQ ==========
+
+call MakeCoq_SetRootPath
+
+call MakeCoq_MinGW.bat ^
+ -arch=64 ^
+ -installer=Y ^
+ -coqver=git-v8.8 ^
+ -destcyg=%ROOTPATH%\cygwin_coq64_88_inst ^
+ -destcoq=%ROOTPATH%\coq64_88_inst ^
+ -addon=bignums
+
+IF %ERRORLEVEL% NEQ 0 (
+ ECHO MakeCoq_88git_installer.bat failed with error code %ERRORLEVEL%
+ EXIT /b %ERRORLEVEL%
+)
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index ccf22cc86..f960ff008 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -34,7 +34,7 @@ REM see -ocaml in ReadMe.txt SET INSTALLOCAML=N REM see -make in ReadMe.txt -SET INSTALLMAKE=Y +SET INSTALLMAKE=N REM see -destcyg in ReadMe.txt SET DESTCYG=C:\bin\cygwin_coq @@ -267,7 +267,6 @@ IF "%INSTALLMODE%" == "mingwincygwin" ( IF "%MAKEINSTALLER%" == "Y" ( SET INSTALLMODE=relocatable SET INSTALLOCAML=Y - SET INSTALLMAKE=Y ) REM ========== CONFIRM PARAMETERS ========== diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh index 16c972e80..7e606b554 100644 --- a/dev/build/windows/configure_profile.sh +++ b/dev/build/windows/configure_profile.sh @@ -14,30 +14,30 @@ rcfile=~/.bash_profile donefile=~/.bash_profile.upated +# to learn about `exec >> $file`, see https://www.tldp.org/LDP/abs/html/x17974.html +exec >> $rcfile + if [ ! -f $donefile ] ; then - echo >> $rcfile - - if [ "$1" != "" -a "$1" != " " ]; then - echo export http_proxy="http://$1" >> $rcfile - echo export https_proxy="http://$1" >> $rcfile - echo export ftp_proxy="http://$1" >> $rcfile + if [ "$1" != "" ] && [ "$1" != " " ]; then + echo export http_proxy="http://$1" + echo export https_proxy="http://$1" + echo export ftp_proxy="http://$1" fi - - mkdir -p $RESULT_INSTALLDIR_CFMT/bin + + mkdir -p "$RESULT_INSTALLDIR_CFMT/bin" # A tightly controlled path helps to avoid issues # Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path! # Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH # See cat /proc/mounts - echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile + echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" # find and xargs complain if the environment is larger than (I think) 8k. # ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit - echo unset ORIGINAL_PATH >> $rcfile - + echo unset ORIGINAL_PATH # Other installations of OCaml will mess up things - echo unset OCAMLLIB >> $rcfile + echo unset OCAMLLIB touch $donefile fi diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh index cbcf14ec2..3bba451ec 100644 --- a/dev/build/windows/difftar-folder.sh +++ b/dev/build/windows/difftar-folder.sh @@ -42,7 +42,7 @@ fi if [ "$strip" -gt 0 ] ; then # Get the path/name of the first file from teh 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)/ + prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/ else prefix= fi @@ -60,13 +60,13 @@ mkdir -p "$empty" # Print information (this is ignored by patch) -echo diff/patch file created on $(date) with: -echo difftar-folder.sh $@ -echo TARFILE= $tarfile -echo FOLDER= $folder -echo TARSTRIP= $strip -echo TARPREFIX= $prefix -echo ORIGFOLDER= $orig +echo diff/patch file created on "$(date)" with: +echo difftar-folder.sh "$@" +echo TARFILE= "$tarfile" +echo FOLDER= "$folder" +echo TARSTRIP= "$strip" +echo TARPREFIX= "$prefix" +echo ORIGFOLDER= "$orig" # Make sure tar uses english output (for Mod time differs) export LC_ALL=C @@ -76,14 +76,14 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim # Substitute ': Mod time differs' with nothing file=${file/: Mod time differs/} # Check if file exists - if [ -f "$folder/$file" ] ; then + if [ -f "$folder/$file" ] ; then # Extract original file tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file" # Compute diff - diff -u "$orig/$file" "$folder/$file" + diff -u "$orig/$file" "$folder/$file" fi done if [ -d "$new" ] ; then - diff -u -r --unidirectional-new-file $empty $new + diff -u -r --unidirectional-new-file "$empty" "$new" fi diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8e0d2341d..18f1a2f16 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -67,7 +67,7 @@ RMDIR_BEFORE_BUILD=1 ###################### ARCHITECTURES ##################### # The OS on which the build of the tool/lib runs -BUILD=`gcc -dumpmachine` +BUILD=$(gcc -dumpmachine) # The OS on which the tool runs # "`find /bin -name "*mingw32-gcc.exe"`" -dumpmachine @@ -132,34 +132,38 @@ CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//\//%2f} # Copy files cp "$CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini" $TARBALLS cp /etc/setup/installed.db $TARBALLS - + ###################### LOGGING ##################### # The folder which receives log files mkdir -p buildlogs -LOGS=`pwd`/buildlogs +LOGS=$(pwd)/buildlogs # The current log target (first part of the log file name) LOGTARGET=other +# Log command output - take log target name from command name (like log1 make => log target is "<module>-make") log1() { - "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err + "$@" > "$LOGS/$LOGTARGET-$1.log" 2> "$LOGS/$LOGTARGET-$1.err" } +# Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install") log2() { - "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err + "$@" > "$LOGS/$LOGTARGET-$1-$2.log" 2> "$LOGS/$LOGTARGET-$1-$2.err" } +# Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure") log_1_3() { - "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err + "$@" > "$LOGS/$LOGTARGET-$1-$3.log" 2> "$LOGS/$LOGTARGET-$1-$3.err" } +# Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar") logn() { LOGTARGETEX=$1 shift - "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err + "$@" > "$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2> "$LOGS/$LOGTARGET-$LOGTARGETEX.err" } - + ###################### 'UNFIX' SED ##################### # In Cygwin SED used to do CR-LF to LF conversion, but since sed 4.4-1 this was changed @@ -183,7 +187,7 @@ logn() { # - create build folder # - extract source archive # - patch source file if patch exists -# +# # Parameters # $1 file server name including protocol prefix # $2 file name (without extension) @@ -206,68 +210,68 @@ function get_expand_source_tar { else name=$2 fi - + if [ "$#" -ge 6 ] ; then folder=$6 else folder=$name fi - + # Set logging target logtargetold=$LOGTARGET LOGTARGET=$name - + # Get the source archive either from the source cache or online - if [ ! -f $TARBALLS/$name.$3 ] ; then + if [ ! -f "$TARBALLS/$name.$3" ] ; then if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" ] ; then - cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS + cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" "$TARBALLS" else - wget $1/$2.$3 - if file -i $2.$3 | grep text/html; then - echo Download failed: $1/$2.$3 + wget "$1/$2.$3" + if file -i "$2.$3" | grep text/html; then + echo Download failed: "$1/$2.$3" echo The file wget downloaded is an html file: - cat $2.$3 + cat "$2.$3" exit 1 fi if [ ! "$2.$3" == "$name.$3" ] ; then - mv $2.$3 $name.$3 + mv "$2.$3" "$name.$3" fi - mv $name.$3 $TARBALLS + mv "$name.$3" "$TARBALLS" # Save the source archive in the source cache if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then - cp $TARBALLS/$name.$3 "$SOURCE_LOCAL_CACHE_CFMT" + cp "$TARBALLS/$name.$3" "$SOURCE_LOCAL_CACHE_CFMT" fi fi fi - + # Remove build directory (clean build) if [ $RMDIR_BEFORE_BUILD -eq 1 ] ; then - rm -f -r $folder + rm -f -r "$folder" fi - + # Create build directory and cd - mkdir -p $folder - cd $folder - + mkdir -p "$folder" + cd "$folder" + # Extract source archive if [ "$3" == "zip" ] ; then - log1 unzip $TARBALLS/$name.$3 + log1 unzip "$TARBALLS/$name.$3" if [ "$strip" == "1" ] ; then # Ok, this is dirty, but it works and it fails if there are name clashes - mv */* . + mv -- */* . else echo "Unzip strip count not supported" return 1 fi else - logn untar tar xvaf $TARBALLS/$name.$3 --strip $strip + logn untar tar xvaf "$TARBALLS/$name.$3" --strip $strip fi - + # Patch if patch file exists - if [ -f $PATCHES/$name.patch ] ; then - log1 patch -p1 -i $PATCHES/$name.patch + if [ -f "$PATCHES/$name.patch" ] ; then + log1 patch -p1 -i "$PATCHES/$name.patch" fi - + # Go back to base folder cd .. @@ -283,7 +287,7 @@ function get_expand_source_tar { # - cd to build folder and extract source archive # - create bin_special subfolder and add it to $PATH # - remember things for build_post -# +# # Parameters # $1 file server name including protocol prefix # $2 file name (without extension) @@ -305,27 +309,27 @@ function build_prep { else name=$2 fi - + # Check if build is already done - if [ ! -f flagfiles/$name.finished ] ; then + if [ ! -f "flagfiles/$name.finished" ] ; then BUILD_PACKAGE_NAME=$name BUILD_OLDPATH=$PATH - BUILD_OLDPWD=`pwd` + BUILD_OLDPWD=$(pwd) LOGTARGET=$name - touch flagfiles/$name.started - - get_expand_source_tar $1 $2 $3 $strip $name - - cd $name - + touch "flagfiles/$name.started" + + get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" + + cd "$name" + # Create a folder and add it to path, where we can put special binaries # The path is restored in build_post mkdir bin_special - PATH=`pwd`/bin_special:$PATH - + PATH=$(pwd)/bin_special:$PATH + return 0 - else + else return 1 fi } @@ -337,9 +341,9 @@ function build_prep { # ------------------------------------------------------------------------------ function build_post { - if [ ! -f flagfiles/$BUILD_PACKAGE_NAME.finished ]; then - cd $BUILD_OLDPWD - touch flagfiles/$BUILD_PACKAGE_NAME.finished + if [ ! -f "flagfiles/$BUILD_PACKAGE_NAME.finished" ]; then + cd "$BUILD_OLDPWD" + touch "flagfiles/$BUILD_PACKAGE_NAME.finished" PATH=$BUILD_OLDPATH LOGTARGET=other fi @@ -362,9 +366,10 @@ function build_post { # ------------------------------------------------------------------------------ function build_conf_make_inst { - if build_prep $1 $2 $3 ; then + 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="$PREFIX" "${@:5}" + # shellcheck disable=SC2086 log1 make $MAKE_OPT log2 make install log2 make clean @@ -383,6 +388,7 @@ function build_conf_make_inst { function install_glob { # Check if any files matching the pattern exist if [ "$(echo $1)" != "$1" ] ; then + # shellcheck disable=SC2086 install -D -t $2 $1 fi } @@ -398,7 +404,7 @@ function install_glob { # ------------------------------------------------------------------------------ function install_rec { - ( cd $1 && find -type f -name "$2" -exec install -D -T $1/{} $3/{} \; ) + ( cd "$1" && find . -type f -name "$2" -exec install -D -T "$1"/{} "$3"/{} \; ) } # ------------------------------------------------------------------------------ @@ -411,7 +417,7 @@ function install_rec { function list_files { if [ ! -e "/build/filelists/$1" ] ; then - ( cd "$PREFIXCOQ" && find -type f | sort > /build/filelists/$1 ) + ( cd "$PREFIXCOQ" && find . -type f | sort > /build/filelists/"$1" ) fi } @@ -439,7 +445,7 @@ function diff_files { # ------------------------------------------------------------------------------ function filter_files { - egrep "$3" "/build/filelists/$2" > "/build/filelists/$1" + grep -E "$3" "/build/filelists/$2" > "/build/filelists/$1" } # ------------------------------------------------------------------------------ @@ -453,7 +459,7 @@ function files_to_nsis { # Split the path in the file list into path and filename and create SetOutPath and File instructions # Note: File /oname cannot be used, because it does not create the paths as SetOutPath does # Note: I didn't check if the redundant SetOutPath instructions have a bad impact on installer size or install time - cat "/build/filelists/$1" | tr '/' '\\' | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh" + tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh" } @@ -501,7 +507,7 @@ function make_fontconfig { make_freetype make_expat # CONFIGURE PARAMETERS - # build/install fails without --disable-docs + # build/install fails without --disable-docs build_conf_make_inst http://www.freedesktop.org/software/fontconfig/release fontconfig-2.11.94 tar.gz true --disable-docs } @@ -532,7 +538,7 @@ function make_ncurses { # # CONFIGURE PARAMETERS # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW) - # additional changes + # additional changes # ADD --with-pkg-config # ADD --enable-pc-files # ADD --without-manpages @@ -604,7 +610,7 @@ function make_gdk-pixbuf { # CONFIGURE PARAMETERS # --with-included-loaders=yes statically links the image file format handlers # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory" - build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes + build_conf_make_inst http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32 gdk-pixbuf-2.32.1 tar.xz true --with-included-loaders=yes } ##### CAIRO ##### @@ -657,8 +663,8 @@ function make_gtk3 { build_conf_make_inst http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16 gtk+-3.16.7 tar.xz true # make all incl. tests and examples runs through fine - # make install fails with issue with - # + # make install fails with issue with + # # make[5]: Entering directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo' # test -n "" || ../../gtk/gtk-update-icon-cache --ignore-theme-index --force "/usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor" # gtk-update-icon-cache.exe: Failed to open file /usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor/.icon-theme.cache : No such file or directory @@ -676,7 +682,8 @@ function make_libxml2 { 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 # 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="$PREFIX" --without-python + # shellcheck disable=SC2086 log1 make $MAKE_OPT all log2 make install log2 make clean @@ -708,12 +715,12 @@ function make_gtk_sourceview2 { # Install flexdll objects function install_flexdll { - cp flexdll.h /usr/$TARGET_ARCH/sys-root/mingw/include + cp flexdll.h "/usr/$TARGET_ARCH/sys-root/mingw/include" if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then - cp flexdll*_mingw.o /usr/$TARGET_ARCH/bin + cp flexdll*_mingw.o "/usr/$TARGET_ARCH/bin" cp flexdll*_mingw.o "$PREFIXOCAML/bin" elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then - cp flexdll*_mingw64.o /usr/$TARGET_ARCH/bin + cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin" cp flexdll*_mingw64.o "$PREFIXOCAML/bin" else echo "Unknown target architecture" @@ -724,8 +731,8 @@ function install_flexdll { # Install flexlink function install_flexlink { - cp flexlink.exe /usr/$TARGET_ARCH/bin - + cp flexlink.exe "/usr/$TARGET_ARCH/bin" + cp flexlink.exe "$PREFIXOCAML/bin" } @@ -745,8 +752,10 @@ function get_flex_dll_link_bin { function make_flex_dll_link { if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then + # shellcheck disable=SC2086 log1 make $MAKE_OPT build_mingw flexlink.exe elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then + # shellcheck disable=SC2086 log1 make $MAKE_OPT build_mingw64 flexlink.exe else echo "Unknown target architecture" @@ -769,11 +778,11 @@ function make_ln { if [ ! -f flagfiles/myln.finished ] ; then touch flagfiles/myln.started mkdir -p myln - cd myln + ( cd myln cp $PATCHES/ln.c . - $TARGET_ARCH-gcc -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c + "$TARGET_ARCH-gcc" -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c install -D ln.exe "$PREFIXCOQ/bin/ln.exe" - cd .. + ) touch flagfiles/myln.finished fi } @@ -799,14 +808,14 @@ function make_ocaml { # Prefix is fixed in make file - replace it with the real one # TODO: this might not work if PREFIX contains spaces sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile - + # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path: # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4 # So we put an explicit path in there sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile - + # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT # I verified that 4.02.3 still doesn't support parallel build log2 make world -f Makefile.nt @@ -815,12 +824,12 @@ function make_ocaml { log2 make opt.opt -f Makefile.nt log2 make install -f Makefile.nt # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development - + # Move license files and other into into special folder if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then mkdir -p "$PREFIXOCAML/license_readme/ocaml" # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources. - rm -f *.txt + rm -f ./*.txt cp LICENSE "$PREFIXOCAML/license_readme/ocaml/License.txt" cp INSTALL "$PREFIXOCAML/license_readme/ocaml/Install.txt" cp README "$PREFIXOCAML/license_readme/ocaml/ReadMe.txt" @@ -909,9 +918,10 @@ function make_camlp5 { make_ocaml make_findlib if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then - logn configure ./configure + logn configure ./configure # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile + # shellcheck disable=SC2086 log1 make world.opt $MAKE_OPT log2 make install # For some reason gramlib.a is not copied, but it is required by Coq @@ -939,15 +949,15 @@ function make_lablgtk { make_gtk_sourceview2 if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe - cp /bin/$TARGET_ARCH-pkg-config.exe bin_special/pkg-config.exe - logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXOCAML" - + cp "/bin/$TARGET_ARCH-pkg-config.exe" bin_special/pkg-config.exe + logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML" + # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT - + # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip logn make-world-pre make world || true - $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll - + "$TARGET_ARCH-strip.exe" --strip-unneeded src/dlllablgtk2.dll + log2 make world log2 make install log2 make clean @@ -978,7 +988,7 @@ function make_stdint { function copy_coq_dll { if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then - cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 "$PREFIXCOQ/bin/$1" + cp "/usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1" "$PREFIXCOQ/bin/$1" fi } @@ -994,7 +1004,7 @@ function copy_coq_dlls { # Do this recursively until there are no further missing DLLs (File close + reopen) # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script. # Do the same for coqc and ocamlc (usually doesn't result in additional files) - + copy_coq_dll LIBATK-1.0-0.DLL copy_coq_dll LIBCAIRO-2.DLL copy_coq_dll LIBEXPAT-1.DLL @@ -1018,7 +1028,7 @@ function copy_coq_dlls { copy_coq_dll LIBXML2-2.DLL copy_coq_dll ZLIB1.DLL - # Depends on if GTK is built from sources + # Depends on if GTK is built from sources if [ "$GTK_FROM_SOURCES" == "Y" ]; then copy_coq_dll libiconv-2.dll else @@ -1036,21 +1046,21 @@ function copy_coq_dlls { i686) copy_coq_dll LIBGCC_S_SJLJ-1.DLL ;; *) false ;; esac - + # Win pthread version change copy_coq_dll LIBWINPTHREAD-1.DLL } function copy_coq_objects { # copy objects only from folders which exist in the target lib directory - find . -type d | while read FOLDER ; do + find . -type d | while read -r FOLDER ; do if [ -e "$PREFIXCOQ/lib/$FOLDER" ] ; then - install_glob $FOLDER/'*.cmxa' "$PREFIXCOQ/lib/$FOLDER" - install_glob $FOLDER/'*.cmi' "$PREFIXCOQ/lib/$FOLDER" - install_glob $FOLDER/'*.cma' "$PREFIXCOQ/lib/$FOLDER" - install_glob $FOLDER/'*.cmo' "$PREFIXCOQ/lib/$FOLDER" - install_glob $FOLDER/'*.a' "$PREFIXCOQ/lib/$FOLDER" - install_glob $FOLDER/'*.o' "$PREFIXCOQ/lib/$FOLDER" + install_glob "$FOLDER"/'*.cmxa' "$PREFIXCOQ/lib/$FOLDER" + install_glob "$FOLDER"/'*.cmi' "$PREFIXCOQ/lib/$FOLDER" + install_glob "$FOLDER"/'*.cma' "$PREFIXCOQ/lib/$FOLDER" + install_glob "$FOLDER"/'*.cmo' "$PREFIXCOQ/lib/$FOLDER" + install_glob "$FOLDER"/'*.a' "$PREFIXCOQ/lib/$FOLDER" + install_glob "$FOLDER"/'*.o' "$PREFIXCOQ/lib/$FOLDER" fi done } @@ -1066,7 +1076,7 @@ function copq_coq_gtk { install_glob "$PREFIX/share/gtksourceview-2.0/language-specs/"'*' "$PREFIXCOQ/share/gtksourceview-2.0/language-specs" install_glob "$PREFIX/share/gtksourceview-2.0/styles/"'*' "$PREFIXCOQ/share/gtksourceview-2.0/styles" install_rec "$PREFIX/share/themes/" '*' "$PREFIXCOQ/share/themes" - + # This below item look like a bug in make install if [ -d "$PREFIXCOQ/share/coq/" ] ; then COQSHARE="$PREFIXCOQ/share/coq/" @@ -1111,11 +1121,11 @@ function make_coq { case $COQ_VERSION in # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip # e.g. git-trunk => download from https://github.com/coq/coq/archive/trunk.zip - git-*) + git-*) COQ_BUILD_PATH=/build/coq-${COQ_VERSION} - build_prep https://github.com/coq/coq/archive ${COQ_VERSION##git-} zip 1 coq-${COQ_VERSION} + build_prep https://github.com/coq/coq/archive "${COQ_VERSION##git-}" zip 1 "coq-${COQ_VERSION}" ;; - + # e.g. /cygdrive/d/coqgit /*) # Todo: --exclude-vcs-ignores doesn't work because tools/coqdoc/coqdoc.sty is excluded => fix .gitignore @@ -1124,11 +1134,11 @@ function make_coq { tar -zcf $TARBALLS/coq-local.tar.gz --exclude-vcs -C "${COQ_VERSION%/*}" "${COQ_VERSION##*/}" build_prep NEVER-DOWNLOADED coq-local tar.gz ;; - + # e.g. 8.6 => https://coq.inria.fr/distrib/8.6/files/coq-8.6.tar.gz *) COQ_BUILD_PATH=/build/coq-$COQ_VERSION - build_prep https://coq.inria.fr/distrib/V$COQ_VERSION/files coq-$COQ_VERSION tar.gz + build_prep "https://coq.inria.fr/distrib/V$COQ_VERSION/files" "coq-$COQ_VERSION" tar.gz ;; esac then @@ -1142,16 +1152,17 @@ function make_coq { fi # The windows resource compiler binary name is hard coded - sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build + sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true # 8.4x doesn't support parallel make if [[ $COQ_VERSION == 8.4* ]] ; then log1 make else + # shellcheck disable=SC2086 make $MAKE_OPT fi - + if [ "$INSTALLMODE" == "relocatable" ]; then ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" fi @@ -1161,7 +1172,7 @@ function make_coq { if [ "$INSTALLOCAML" == "Y" ]; then copy_coq_objects fi - + copq_coq_gtk copy_coq_license @@ -1169,7 +1180,7 @@ function make_coq { # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)" # make clean - + build_post fi } @@ -1180,7 +1191,7 @@ function make_mingw_make { if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then # The config.h.win32 file is fine - don't edit it # We need to copy the mingw gcc here as "gcc" - then the batch file will use it - cp /usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe ./gcc.exe + cp "/usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe" ./gcc.exe # By some magic cygwin bash can run batch files logn build ./build_w32.bat gcc # Copy make to Coq folder @@ -1193,7 +1204,8 @@ function make_mingw_make { function make_binutils { if build_prep http://ftp.gnu.org/gnu/binutils binutils-2.27 tar.gz ; then - logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXCOQ" --program-prefix=$TARGET- + logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ" --program-prefix="$TARGET-" + # shellcheck disable=SC2086 log1 make $MAKE_OPT log2 make install # log2 make clean @@ -1219,12 +1231,13 @@ function make_gcc { mkdir -p "$PREFIXCOQ/mingw/include" # See https://gcc.gnu.org/install/configure.html - logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET \ - --prefix="$PREFIXCOQ" --program-prefix=$TARGET- --disable-win32-registry --with-sysroot="$PREFIXCOQ" \ + logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" \ + --prefix="$PREFIXCOQ" --program-prefix="$TARGET-" --disable-win32-registry --with-sysroot="$PREFIXCOQ" \ --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 + # shellcheck disable=SC2086 log1 make $MAKE_OPT log2 make install # log2 make clean @@ -1252,21 +1265,22 @@ function get_cygwin_mingw_sources { # Take the 2nd field of the last line => ${SOURCE} = x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz # Remove that path part => ${SOURCEFILE} = mingw64-x86_64-gcc-5.4.0-2-src.tar.xz - grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//' | while read ARCHIVE ; do + grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//' | while read -r ARCHIVE ; do local ARCHIVEESC=${ARCHIVE//+/\\+} - local SOURCE=`egrep -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2` + local SOURCE + SOURCE=$(grep -E -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2) local SOURCEFILE=${SOURCE##*/} # Get the source file (either from the source cache or online) - if [ ! -f $TARBALLS/$SOURCEFILE ] ; then + if [ ! -f "$TARBALLS/$SOURCEFILE" ] ; then if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" ] ; then cp "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" $TARBALLS else wget "$CYGWIN_REPOSITORY/$SOURCE" - mv $SOURCEFILE $TARBALLS + mv "$SOURCEFILE" "$TARBALLS" # Save the source archive in the source cache if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then - cp $TARBALLS/$SOURCEFILE "$SOURCE_LOCAL_CACHE_CFMT" + cp "$TARBALLS/$SOURCEFILE" "$SOURCE_LOCAL_CACHE_CFMT" fi fi fi @@ -1281,26 +1295,25 @@ function get_cygwin_mingw_sources { function make_coq_installer { make_coq - make_mingw_make get_cygwin_mingw_sources # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build: # ocaml: ocaml + menhir + camlp5 + findlib # ocaml_coq: as above + coq # ocaml_coq_addons: as above + lib/user-contrib/* - + # Create coq file list as ocaml_coq / ocaml diff_files coq ocaml_coq ocaml - + # Filter out object files - filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$' - + filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$' + # Filter out plugin object files filter_files coq_objects_plugins coq_objects '/lib/plugins/.*\.(cmxa|cmi|cma|cmo|a|o)$' - + # Coq objects objects required for plugin development = coq objects except those for pre installed plugins diff_files coq_plugindev coq_objects coq_objects_plugins - + # Addons (TODO: including objects that could go to the plugindev thing, but # then one would have to make that package depend on this one, so not # implemented yet) @@ -1308,45 +1321,46 @@ function make_coq_installer { # Coq files, except objects needed only for plugin development diff_files coq_base coq coq_plugindev - + # Convert section files to NSIS format files_to_nsis coq_base files_to_nsis coq_addons files_to_nsis coq_plugindev files_to_nsis ocaml - + # Get and extract NSIS Binaries if build_prep http://downloads.sourceforge.net/project/nsis/NSIS%202/2.51 nsis-2.51 zip ; then - NSIS=`pwd`/makensis.exe + NSIS=$(pwd)/makensis.exe chmod u+x "$NSIS" # Change to Coq folder - cd $COQ_BUILD_PATH + cd "$COQ_BUILD_PATH" # Copy patched nsi file cp ../patches/coq_new.nsi dev/nsis cp ../patches/StrRep.nsh dev/nsis cp ../patches/ReplaceInFile.nsh dev/nsis - VERSION=`grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r'` + VERSION=$(grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r') cd dev/nsis - logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi - + logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi + build_post fi } ###################### ADDONS ##################### + function make_addon_bignums { - if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1; then + if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local - logn make make all - logn make-install make install + log1 make all + log2 make install build_post fi } function make_addons { for addon in $COQ_ADDONS; do - make_addon_$addon + "make_addon_$addon" done } @@ -1374,4 +1388,3 @@ list_files ocaml_coq_addons if [ "$MAKEINSTALLER" == "Y" ] ; then make_coq_installer fi - diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 524a55a42..93e7bd99a 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -4,6 +4,6 @@ wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/o tar -xf opam64.tar.xz bash opam64/install.sh opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c -eval $(opam config env) +eval "$(opam config env)" opam install -y ocamlfind camlp5 -cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate +cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index c90e516ae..008291967 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -6,11 +6,11 @@ ci_dir="$(dirname "$0")" # Let's avoid to source ci-common twice in this case if [ -z "${CI_BUILD_DIR}" ]; then - source ${ci_dir}/ci-common.sh + . "${ci_dir}/ci-common.sh" fi -bignums_CI_DIR=${CI_BUILD_DIR}/Bignums +bignums_CI_DIR="${CI_BUILD_DIR}/Bignums" -git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR} +git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}" -( cd ${bignums_CI_DIR} && make && make install) +( cd "${bignums_CI_DIR}" && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 558e8cbb8..8ce5f2418 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" CoLoR_CI_DIR=${CI_BUILD_DIR}/color # Compile CoLoR -git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} -( cd ${CoLoR_CI_DIR} && make ) +git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}" +( cd "${CoLoR_CI_DIR}" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index d7a356930..189734a0b 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -20,7 +20,8 @@ else export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" else # assume local - export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" + export CI_BRANCH fi export COQBIN="$PWD/bin" fi @@ -35,10 +36,10 @@ ls "$COQBIN" CI_BUILD_DIR="$PWD/_build_ci" # shellcheck source=ci-basic-overlay.sh -source "${ci_dir}/ci-basic-overlay.sh" +. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null - source "${overlay}" + . "${overlay}" done mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" @@ -68,7 +69,7 @@ git_checkout() checkout_mathcomp() { - git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}" } make() diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 6a0ce2aef..fbdeff20c 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,11 +1,11 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert +CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" opam install -j "$NJOBS" -y menhir -git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} +git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" -( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh index 5d6bd6a36..5d57fce1c 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph +coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph" -git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} +git_checkout "${coq_dpdgraph_CI_BRANCH}" "${coq_dpdgraph_CI_GITURL}" "${coq_dpdgraph_CI_DIR}" -( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make && make test-suite ) +( cd "${coq_dpdgraph_CI_DIR}" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 40eff03b7..d86d61ef6 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot +Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot" install_ssreflect -git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR} +git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}" -( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 54cad5df4..9298fc70a 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Corn_CI_DIR=${CI_BUILD_DIR}/corn +Corn_CI_DIR="${CI_BUILD_DIR}/corn" -git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR} +git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}" -( cd ${Corn_CI_DIR} && make && make install ) +( cd "${Corn_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh index 8b725f6fe..ca759c7b3 100755 --- a/dev/ci/ci-cpdt.sh +++ b/dev/ci/ci-cpdt.sh @@ -1,10 +1,9 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" wget http://adam.chlipala.net/cpdt/cpdt.tgz tar xvfz cpdt.tgz ( cd cpdt && make clean && make ) - diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index c44e0a655..9c58034be 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Elpi_CI_DIR=${CI_BUILD_DIR}/elpi +Elpi_CI_DIR="${CI_BUILD_DIR}/elpi" -git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR} +git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}" -( cd ${Elpi_CI_DIR} && make && make install ) +( cd "${Elpi_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 62854afac..98735b4ec 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Equations_CI_DIR=${CI_BUILD_DIR}/Equations +Equations_CI_DIR="${CI_BUILD_DIR}/Equations" -git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR} +git_checkout "${Equations_CI_BRANCH}" "${Equations_CI_GITURL}" "${Equations_CI_DIR}" -( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install) +( cd "${Equations_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 5ca3ac47f..6c8dce5bd 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,11 +1,11 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto +fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" -git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR} -( cd ${fiat_crypto_CI_DIR} && git submodule update --init --recursive ) +git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" +( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) -( cd ${fiat_crypto_CI_DIR} && make lite ) +( cd "${fiat_crypto_CI_DIR}" && make lite ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 292331b81..35c228405 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat +fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat" -git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR} +git_checkout "${fiat_parsers_CI_BRANCH}" "${fiat_parsers_CI_GITURL}" "${fiat_parsers_CI_DIR}" -( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core ) +( cd "${fiat_parsers_CI_DIR}" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index ec19bd993..8599e4d50 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -Flocq_CI_DIR=${CI_BUILD_DIR}/flocq +Flocq_CI_DIR="${CI_BUILD_DIR}/flocq" -git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR} +git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}" -( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) +( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 53eb55fc4..118d15150 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology +formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology" -git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR} +git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}" -( cd ${formal_topology_CI_DIR} && make ) +( cd "${formal_topology_CI_DIR}" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 8e6448e76..bd1d88993 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq +GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" -git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR} +git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" -( cd ${GeoCoq_CI_DIR} && \ +( cd "${GeoCoq_CI_DIR}" && \ ./configure-ci.sh && \ make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c..6ded97984 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT +HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT -git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} +git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) +( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 267e13359..b019fa059 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -1,11 +1,11 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp -Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq -lambdaRust_CI_DIR=${CI_BUILD_DIR}/lambdaRust +stdpp_CI_DIR="${CI_BUILD_DIR}/coq-stdpp" +Iris_CI_DIR="${CI_BUILD_DIR}/iris-coq" +lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust" install_ssreflect @@ -13,29 +13,29 @@ install_ssreflect opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev # Setup lambdaRust first -git_checkout ${lambdaRust_CI_BRANCH} ${lambdaRust_CI_GITURL} ${lambdaRust_CI_DIR} +git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" # Extract required version of Iris -Iris_VERSION=$(cat ${lambdaRust_CI_DIR}/opam | fgrep coq-iris | egrep 'dev\.([0-9.-]+)' -o) -Iris_URL=$(opam show coq-iris.$Iris_VERSION -f upstream-url) -read -a Iris_URL_PARTS <<< $(echo $Iris_URL | tr '#' ' ') +Iris_VERSION=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o) +Iris_URL=$(opam show "coq-iris.$Iris_VERSION" -f upstream-url) +read -r -a Iris_URL_PARTS <<< "$(echo "$Iris_URL" | tr '#' ' ')" # Setup Iris -git_checkout ${Iris_CI_BRANCH} ${Iris_URL_PARTS[0]} ${Iris_CI_DIR} ${Iris_URL_PARTS[1]} +git_checkout "${Iris_CI_BRANCH}" "${Iris_URL_PARTS[0]}" "${Iris_CI_DIR}" "${Iris_URL_PARTS[1]}" # Extract required version of std++ -stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o) -stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url) -read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ') +stdpp_VERSION=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o) +stdpp_URL=$(opam show "coq-stdpp.$stdpp_VERSION" -f upstream-url) +read -r -a stdpp_URL_PARTS <<< "$(echo "$stdpp_URL" | tr '#' ' ')" # Setup std++ -git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} +git_checkout "${stdpp_CI_BRANCH}" "${stdpp_URL_PARTS[0]}" "${stdpp_CI_DIR}" "${stdpp_URL_PARTS[1]}" # Build std++ -( cd ${stdpp_CI_DIR} && make && make install ) +( cd "${stdpp_CI_DIR}" && make && make install ) # Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris -( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install ) +( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install ) # Build lambdaRust -( cd ${lambdaRust_CI_DIR} && make && make install ) +( cd "${lambdaRust_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 820ff89ee..5981aaaae 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 +ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2" -git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} +git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}" -( cd ${ltac2_CI_DIR} && make && make tests && make install ) +( cd "${ltac2_CI_DIR}" && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index db4a31e54..4fc06e895 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes +math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" -git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR} +git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" -( cd ${math_classes_CI_DIR} && make && make install ) +( cd "${math_classes_CI_DIR}" && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 701403f2c..8c6b910bb 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -2,14 +2,14 @@ # $0 is not the safest way, but... ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp +mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" -checkout_mathcomp ${mathcomp_CI_DIR} +checkout_mathcomp "${mathcomp_CI_DIR}" # odd_order takes too much time for travis. -( cd ${mathcomp_CI_DIR}/mathcomp && \ +( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/PFsection/d' Make && \ sed -i.bak '/stripped_odd_order_theorem/d' Make && \ make Makefile.coq && make -f Makefile.coq all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index c813b1fe9..a66dc1e76 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -1,19 +1,19 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq # Setup UniCoq -git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR} +git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" -( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && make install ) +( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install ) # Setup MetaCoq -git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR} +git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}" -( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make ) +( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 4f7e9517f..58bbb7229 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} -wget -qO- ${sf_lf_CI_TARURL} | tar xvz -wget -qO- ${sf_plf_CI_TARURL} | tar xvz -wget -qO- ${sf_vfa_CI_TARURL} | tar xvz +mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" || exit 1 +wget -qO- "${sf_lf_CI_TARURL}" | tar xvz +wget -qO- "${sf_plf_CI_TARURL}" | tar xvz +wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh index 25da01a82..e77a55304 100755 --- a/dev/ci/ci-template.sh +++ b/dev/ci/ci-template.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" Template_CI_BRANCH=master Template_CI_GITURL=https://github.com/Template/Template -Template_CI_DIR=${CI_BUILD_DIR}/Template +Template_CI_DIR="${CI_BUILD_DIR}/Template" -git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR} +git_checkout "${Template_CI_BRANCH}" "${Template_CI_GITURL}" "${Template_CI_DIR}" -( cd ${Template_CI_DIR} && make ) +( cd "${Template_CI_DIR}" && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 8ecd8c441..31387c8dd 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -1,10 +1,10 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -tlc_CI_DIR=${CI_BUILD_DIR}/tlc +tlc_CI_DIR="${CI_BUILD_DIR}/tlc" -git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR} +git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}" -( cd ${tlc_CI_DIR} && make ) +( cd "${tlc_CI_DIR}" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 66b56add7..62a949f59 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,13 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath +UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" -git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR} +git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" -( cd ${UniMath_CI_DIR} && \ +( cd "${UniMath_CI_DIR}" && \ sed -i.bak '/Folds/d' Makefile && \ sed -i.bak '/HomologicalAlgebra/d' Makefile && \ make BUILD_COQ=no ) - diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 5760fbafb..3c0044bfe 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -1,13 +1,13 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" -source ${ci_dir}/ci-common.sh +. "${ci_dir}/ci-common.sh" -VST_CI_DIR=${CI_BUILD_DIR}/VST +VST_CI_DIR="${CI_BUILD_DIR}/VST" # opam install -j ${NJOBS} -y menhir -git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR} +git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" # Targets are: msl veric floyd progs , we remove progs to save time # Patch to avoid the upper version limit -( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd ) +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd ) diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh index 7716bcb59..e9ba11414 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,3 +1,5 @@ +#!/bin/sh + if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh deleted file mode 100644 index c2e367038..000000000 --- a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then - Equations_CI_BRANCH=rm-local-polymorphic-flag - Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh deleted file mode 100644 index 78789a6fc..000000000 --- a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then - HoTT_CI_BRANCH=check-poly-effects - HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git -fi diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh deleted file mode 100644 index 9677b3525..000000000 --- a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then - Equations_CI_BRANCH=API-removal - Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git - coq_dpdgraph_CI_BRANCH=API-removal - coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git - ltac2_CI_BRANCH=API-removal - ltac2_CI_GITURL=https://github.com/gares/ltac2.git -fi diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh deleted file mode 100644 index 4b681909d..000000000 --- a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh +++ /dev/null @@ -1,7 +0,0 @@ - if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then - ltac2_CI_BRANCH=econstr+more_fix - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=econstr+more_fix - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh deleted file mode 100644 index 8a50fb111..000000000 --- a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then - Equations_CI_BRANCH=fix-6535 - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh deleted file mode 100644 index 2451657d4..000000000 --- a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then - ltac2_CI_BRANCH=fix-for/6676 - ltac2_CI_GITURL=https://github.com/gares/ltac2.git - Equations_CI_BRANCH=fix-for/6676 - Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git -fi diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh deleted file mode 100644 index 3a3ab44e0..000000000 --- a/dev/ci/user-overlays/06686-ccnv-no-proj.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then - Equations_CI_BRANCH=ccnv-fixes - Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh deleted file mode 100644 index d1d61fec2..000000000 --- a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh +++ /dev/null @@ -1,13 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then - ltac2_CI_BRANCH=located+vernac - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+vernac - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - fiat_parsers_CI_BRANCH=located+vernac - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - - Elpi_CI_BRANCH=located+vernac - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh deleted file mode 100644 index 8afcbf78a..000000000 --- a/dev/ci/user-overlays/06775-univ-cumul-weak.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then - Elpi_CI_BRANCH=coq-master - Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh deleted file mode 100644 index df3e9cef2..000000000 --- a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh +++ /dev/null @@ -1,14 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then - - ltac2_CI_BRANCH=located+vernac_2 - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+vernac_2 - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - # fiat_parsers_CI_BRANCH=located+vernac - # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - - Elpi_CI_BRANCH=located+vernac_2 - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git -fi diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh deleted file mode 100644 index a785290e7..000000000 --- a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then - - ltac2_CI_BRANCH=located+libnames - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Equations_CI_BRANCH=located+libnames - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - Elpi_CI_BRANCH=located+libnames - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - - coq_dpdgraph_CI_BRANCH=located+libnames - coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git - -fi diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh deleted file mode 100644 index 5dedca0ca..000000000 --- a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then - - Equations_CI_BRANCH=ssr+correct_packing - Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_BRANCH=ssr+correct_packing - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - Elpi_CI_BRANCH=ssr+correct_packing - Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git - -fi diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh deleted file mode 100644 index 333a9e84b..000000000 --- a/dev/ci/user-overlays/06923-ppedrot-export-options.sh +++ /dev/null @@ -1,7 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then - ltac2_CI_BRANCH=export-options - ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 - - Equations_CI_BRANCH=export-options - Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations -fi diff --git a/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh new file mode 100644 index 000000000..cf2af9ae9 --- /dev/null +++ b/dev/ci/user-overlays/06960-ejgallego-ltac+tacdepr.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "6960" ] || [ "$CI_BRANCH" = "ltac+tacdepr" ]; then + + # Equations_CI_BRANCH=ssr+correct_packing + # Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_BRANCH=ltac+tacdepr + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + # Elpi_CI_BRANCH=ssr+correct_packing + # Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9f0377cee..a7474e324 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,6 +7,8 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub Example: `00669-maximedenes-ssr-merge.sh` containing ``` +#!/bin/sh + if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then mathcomp_CI_BRANCH=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 71fc39608..3a2df6a81 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -1,6 +1,7 @@ # Merging changes in Coq -This document describes how patches (submitted as Pull Requests) should be +This document describes how patches (submitted as pull requests +on the `master` branch) should be merged into the main repository (https://github.com/coq/coq). ## Code owners @@ -65,14 +66,57 @@ In some rare cases (e.g. the conflicts are in the CHANGES file), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push to `master` directly. Don't use the GitHub interface to fix these conflicts. -The command to be used is: +To merge the PR proceed in the following way ``` +$ git checkout master +$ git pull $ dev/tools/merge-pr XXXX +$ git push upstream ``` -where `XXXX` is the number of the PR to be merged. This operation should be followed by a push. +where `XXXX` is the number of the PR to be merged and `upstream` is the name +of your remote pointing to `git@github.com:coq/coq.git`. +Note that you are only supposed to merge PRs into `master`. PRs should rarely +target the stable branch, but when it is the case they are the responsibility +of the release manager. + +This script conducts various checks before proceeding to merge. Don't bypass them +without a good reason to, and in that case, write a comment in the PR thread to +explain the reason. Maintainers MUST NOT merge their own patches. DON'T USE the GitHub interface for merging, since it will prevent the automated backport script from operating properly, generates bad commit messages, and a messy history when there are conflicts. + +### What to do if the PR has overlays + +If the PR breaks compatibility of some developments in CI, then the author must +have prepared overlays for these developments (see [`dev/ci/README.md`](/dev/ci/README.md)) +and the PR must absolutely update the `CHANGES` file. + +There are two cases to consider: + +- If the patch is backward compatible (best scenario), then you should get + upstream maintainers to integrate it before merging the PR. +- If the patch is not backward compatible (which is often the case when + patching plugins after an update to the Coq API), then you can proceed to + merge the PR and then notify upstream they can merge the patch. This is a + less preferable scenario because it is probably going to create + spurious CI failures for unrelated PRs. + +### Merge script dependencies + +The merge script passes option `-S` to `git merge` to ensure merge commits +are signed. Consequently, it depends on the GnuPG command utility being +installed and a GPG key being available. Here is a short tutorial to +creating your own GPG key: +<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/> + +The script depends on a few other utilities. If you are a Nix user, the +simplest way of getting them is to run `nix-shell` first. + +**Note for homebrew (MacOS) users:** it has been reported that installing GnuPG +is not out of the box. Installing explicitly "pinentry-mac" seems important for +typing of passphrase to work correctly (see also this +[Stack Overflow Q-and-A](https://stackoverflow.com/questions/39494631/gpg-failed-to-sign-the-data-fatal-failed-to-write-commit-object-git-2-10-0)). diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index e4359f703..5205350a6 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -27,9 +27,9 @@ BRANCH=backport-pr-${PRNUM} RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../') MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/') -if git checkout -b ${BRANCH}; then +if git checkout -b "${BRANCH}"; then - if ! git cherry-pick -x ${RANGE}; then + if ! git cherry-pick -x "${RANGE}"; then echo "Please fix the conflicts, then exit." bash while ! git cherry-pick --continue; do @@ -50,7 +50,7 @@ else fi -if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then +if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then echo read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r echo @@ -63,8 +63,8 @@ if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi -git merge -S --no-ff ${BRANCH} -m "${MESSAGE}" -git branch -d ${BRANCH} +git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}" +git branch -d "${BRANCH}" # To-Do: # - Support for backporting a PR before it is merged diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index ecfdfab94..20612eeb8 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -80,8 +80,8 @@ if [ -z "$REMOTE" ]; then exit 1 fi REMOTE_URL=$(git remote get-url "$REMOTE" --push) -if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \ - "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then +if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \ + [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" error "that is ${BLUE}$OFFICIAL_REMOTE_URL" error "it points to ${BLUE}$REMOTE_URL${RESET} instead" diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex deleted file mode 100644 index 8f9d876cb..000000000 --- a/doc/refman/AsyncProofs.tex +++ /dev/null @@ -1,221 +0,0 @@ -\achapter{Asynchronous and Parallel Proof Processing\label{Asyncprocessing}} -%HEVEA\cutname{async-proofs.html} -\aauthor{Enrico Tassi} - -\label{pralitp} -\index{Asynchronous and Parallel Proof Processing!presentation} - -This chapter explains how proofs can be asynchronously processed by Coq. -This feature improves the reactivity of the system when used in interactive -mode via CoqIDE. In addition, it allows Coq to take advantage of -parallel hardware when used as a batch compiler by decoupling the checking -of statements and definitions from the construction and checking of proofs -objects. - -This feature is designed to help dealing with huge libraries of theorems -characterized by long proofs. In the current state, it may not be beneficial -on small sets of short files. - -This feature has some technical limitations that may make it unsuitable for -some use cases. - -For example, in interactive mode, some errors coming from the kernel of Coq -are signaled late. The type of errors belonging to this category -are universe inconsistencies. - -At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. - -Finally, asynchronous processing is disabled when running CoqIDE in Windows. The -current implementation of the feature is not stable on Windows. It can be -enabled, as described below at \ref{interactivecaveats}, though doing so is not -recommended. - -\section{Proof annotations} - -To process a proof asynchronously Coq needs to know the precise statement -of the theorem without looking at the proof. This requires some annotations -if the theorem is proved inside a \texttt{Section} (see Section~\ref{Section}). - -When a section ends, Coq looks at the proof object to decide which -section variables are actually used and hence have to be quantified in the -statement of the theorem. To avoid making the construction of proofs -mandatory when ending a section, one can start each proof with the -\texttt{Proof using} command (Section~\ref{ProofUsing}) that declares which -section variables the theorem uses. - -The presence of \texttt{Proof using} is needed to process proofs -asynchronously in interactive mode. - -It is not strictly mandatory in batch mode if it is not the first time -the file is compiled and if the file itself did not change. When the -proof does not begin with \texttt{Proof using}, the system records in an -auxiliary file, produced along with the \texttt{.vo} file, the list of -section variables used. - -\subsubsection{Automatic suggestion of proof annotations} - -The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a -\texttt{Qed} command is processed, a correct proof annotation. It is up -to the user to modify the proof script accordingly. - -\section{Proof blocks and error resilience} - -Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq -is able to completely check a document containing errors instead of bailing -out at the first failure. - -Two kind of errors are supported: errors occurring in vernacular commands and -errors occurring in proofs. - -To properly recover from a failing tactic, Coq needs to recognize the structure of -the proof in order to confine the error to a sub proof. Proof block detection -is performed by looking at the syntax of the proof script (i.e. also looking at indentation). -Coq comes with four kind of proof blocks, and an ML API to add new ones. - -\begin{description} -\item[curly] blocks are delimited by \texttt{\{} and \texttt{\}}, see \ref{Proof-handling} -\item[par] blocks are atomic, i.e. just one tactic introduced by the \texttt{par:} goal selector -\item[indent] blocks end with a tactic indented less than the previous one -\item[bullet] blocks are delimited by two equal bullet signs at the same indentation level -\end{description} - -\subsection{Caveats} - -When a vernacular command fails the subsequent error messages may be bogus, i.e. caused by -the first error. Error resiliency for vernacular commands can be switched off passing -\texttt{-async-proofs-command-error-resilience off} to CoqIDE. - -An incorrect proof block detection can result into an incorrect error recovery and -hence in bogus errors. Proof block detection cannot be precise for bullets or -any other non well parenthesized proof structure. Error resiliency can be -turned off or selectively activated for any set of block kind passing to -CoqIDE one of the following options: -\texttt{-async-proofs-tactic-error-resilience off}, -\texttt{-async-proofs-tactic-error-resilience all}, -\texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. -Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. - -\section{Interactive mode} - -At the time of writing the only user interface supporting asynchronous proof -processing is CoqIDE. - -When CoqIDE is started, two Coq processes are created. The master one follows -the user, giving feedback as soon as possible by skipping proofs, which are -delegated to the worker process. The worker process, whose state can be seen -by clicking on the button in the lower right corner of the main CoqIDE window, -asynchronously processes the proofs. If a proof contains an error, it is -reported in red in the label of the very same button, that can also be used to -see the list of errors and jump to the corresponding line. - -If a proof is processed asynchronously the corresponding \texttt{Qed} command -is colored using a lighter color that usual. This signals that -the proof has been delegated to a worker process (or will be processed -lazily if the \texttt{-async-proofs lazy} option is used). Once finished, the -worker process will provide the proof object, but this will not be -automatically checked by the kernel of the main process. To force -the kernel to check all the proof objects, one has to click the button -with the gears. Only then are all the universe constraints checked. - -\subsubsection{Caveats} -\label{interactivecaveats} - -The number of worker processes can be increased by passing CoqIDE the -\texttt{-async-proofs-j $n$} flag. Note that the memory consumption -increases too, since each worker requires the same amount of memory as -the master process. Also note that increasing the number of workers may -reduce the reactivity of the master process to user commands. - -To disable this feature, one can pass the \texttt{-async-proofs off} flag to -CoqIDE. Conversely, on Windows, where the feature is disabled by default, -pass the \texttt{-async-proofs on} flag to enable it. - -Proofs that are known to take little time to process are not delegated to a -worker process. The threshold can be configure with \texttt{-async-proofs-delegation-threshold}. Default is 0.03 seconds. - -\section{Batch mode} - -When Coq is used as a batch compiler by running \texttt{coqc} or -\texttt{coqtop -compile}, it produces a \texttt{.vo} file for each -\texttt{.v} file. A \texttt{.vo} file contains, among other things, -theorems statements and proofs. Hence to produce a \texttt{.vo} Coq need -to process all the proofs of the \texttt{.v} file. - -The asynchronous processing of proofs can decouple the generation of a -compiled file (like the \texttt{.vo} one) that can be loaded by -\texttt{Require} from the generation and checking of the proof objects. -The \texttt{-quick} flag can be passed to \texttt{coqc} or -\texttt{coqtop} to produce, quickly, \texttt{.vio} files. Alternatively, -when using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the -\texttt{quick} target can be used to compile all files using the -\texttt{-quick} flag. - -A \texttt{.vio} file can be loaded using \texttt{Require} exactly as a -\texttt{.vo} file but proofs will not be available (the \texttt{Print} -command produces an error). Moreover, some universe constraints might be -missing, so universes inconsistencies might go unnoticed. A -\texttt{.vio} file does not contain proof objects, but proof tasks, -i.e. what a worker process can transform into a proof object. - -Compiling a set of files with the \texttt{-quick} flag allows one to work, -interactively, on any file without waiting for all the proofs to be checked. - -When working interactively, one can fully check all the \texttt{.v} files by -running \texttt{coqc} as usual. - -Alternatively one can turn each \texttt{.vio} into the corresponding -\texttt{.vo}. All \texttt{.vio} files can be processed in parallel, -hence this alternative might be faster. The command \texttt{coqtop - -schedule-vio2vo 2 a b c} can be used to obtain a good scheduling for 2 -workers to produce \texttt{a.vo}, \texttt{b.vo}, and \texttt{c.vo}. When -using a \texttt{Makefile} produced by \texttt{coq\_makefile}, the -\texttt{vio2vo} target can be used for that purpose. Variable \texttt{J} -should be set to the number of workers, e.g. \texttt{make vio2vo J=2}. -The only caveat is that, while the \texttt{.vo} files obtained from -\texttt{.vio} files are complete (they contain all proof terms and -universe constraints), the satisfiability of all universe constraints has -not been checked globally (they are checked to be consistent for every -single proof). Constraints will be checked when these \texttt{.vo} files -are (recursively) loaded with \texttt{Require}. - -There is an extra, possibly even faster, alternative: just check the -proof tasks stored in \texttt{.vio} files without producing the -\texttt{.vo} files. This is possibly faster because all the proof tasks -are independent, hence one can further partition the job to be done -between workers. The \texttt{coqtop -schedule-vio-checking 6 a b c} -command can be used to obtain a good scheduling for 6 workers to check -all the proof tasks of \texttt{a.vio}, \texttt{b.vio}, and -\texttt{c.vio}. Auxiliary files are used to predict how long a proof task -will take, assuming it will take the same amount of time it took last -time. When using a \texttt{Makefile} produced by \texttt{coq\_makefile}, -the \texttt{checkproofs} target can be used to check all \texttt{.vio} -files. Variable \texttt{J} should be set to the number of workers, -e.g. \texttt{make checkproofs J=6}. As when converting \texttt{.vio} -files to \texttt{.vo} files, universe constraints are not checked to be -globally consistent. Hence this compilation mode is only useful for quick -regression testing and on developments not making heavy use of the $Type$ -hierarchy. - -\section{Limiting the number of parallel workers} -\label{coqworkmgr} - -Many Coq processes may run on the same computer, and each of them may start -many additional worker processes. -The \texttt{coqworkmgr} utility lets one limit the number of workers, globally. - -The utility accepts the \texttt{-j} argument to specify the maximum number of -workers (defaults to 2). \texttt{coqworkmgr} automatically starts in the -background and prints an environment variable assignment like -\texttt{COQWORKMGR\_SOCKET=localhost:45634}. The user must set this variable in -all the shells from which Coq processes will be started. If one uses just -one terminal running the bash shell, then \texttt{export `coqworkmgr -j 4`} will -do the job. - -After that, all Coq processes, e.g. \texttt{coqide} and \texttt{coqc}, -will honor the limit, globally. - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Misc.tex b/doc/refman/Misc.tex deleted file mode 100644 index ab00fbfe3..000000000 --- a/doc/refman/Misc.tex +++ /dev/null @@ -1,63 +0,0 @@ -\achapter{\protect{Miscellaneous extensions}} -%HEVEA\cutname{miscellaneous.html} - -\asection{Program derivation} - -Coq comes with an extension called {\tt Derive}, which supports -program derivation. Typically in the style of Bird and Meertens or -derivations of program refinements. To use the {\tt Derive} extension -it must first be required with {\tt Require Coq.Derive.Derive}. When -the extension is loaded, it provides the following command. - -\subsection[\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$] - {\tt Derive \ident$_1$ SuchThat \term{} As \ident$_2$\comindex{Derive}} - -The name $\ident_1$ can appear in \term. This command opens a new -proof presenting the user with a goal for \term{} in which the name -$\ident_1$ is bound to a existential variables {\tt ?x} (formally, -there are other goals standing for the existential variables but they -are shelved, as described in Section~\ref{shelve}). - -When the proof ends two constants are defined: -\begin{itemize} -\item The first one is name $\ident_1$ and is defined as the proof of - the shelved goal (which is also the value of {\tt ?x}). It is -always transparent. -\item The second one is name $\ident_2$. It has type {\tt \term}, and - its body is the proof of the initially visible goal. It is opaque if - the proof ends with {\tt Qed}, and transparent if the proof ends - with {\tt Defined}. -\end{itemize} - -\Example -\begin{coq_example*} -Require Coq.derive.Derive. -Require Import Coq.Numbers.Natural.Peano.NPeano. - -Section P. - -Variables (n m k:nat). - -\end{coq_example*} -\begin{coq_example} -Derive p SuchThat ((k*n)+(k*m) = p) As h. -Proof. -rewrite <- Nat.mul_add_distr_l. -subst p. -reflexivity. -\end{coq_example} -\begin{coq_example*} -Qed. - -End P. - -\end{coq_example*} -\begin{coq_example} -Print p. -Check h. -\end{coq_example} - -Any property can be used as \term, not only an equation. In -particular, it could be an order relation specifying some form of -program refinement or a non-executable property from which deriving a -program is convenient. diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index cfb3c625b..e51116007 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,9 +117,7 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes -\include{Misc.v} %BEGIN LATEX \RefManCutCommand{ENDADDENDUM=\thepage} %END LATEX diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst new file mode 100644 index 000000000..b0343a8f0 --- /dev/null +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -0,0 +1,67 @@ +.. include:: ../replaces.rst + +.. _miscellaneousextensions: + +Miscellaneous extensions +======================= + +:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html +:Converted by: Paul Steckler + +.. contents:: + :local: + :depth: 1 +---- + +Program derivation +----------------- + +|Coq| comes with an extension called ``Derive``, which supports program +derivation. Typically in the style of Bird and Meertens or derivations +of program refinements. To use the Derive extension it must first be +required with ``Require Coq.Derive.Derive``. When the extension is loaded, +it provides the following command: + +.. cmd:: Derive @ident SuchThat @term As @ident + +The first `ident` can appear in `term`. This command opens a new proof +presenting the user with a goal for term in which the name `ident` is +bound to an existential variable `?x` (formally, there are other goals +standing for the existential variables but they are shelved, as +described in Section :ref:`TODO-8.17.4`). + +When the proof ends two constants are defined: + ++ The first one is named using the first `ident` and is defined as the proof of the + shelved goal (which is also the value of `?x`). It is always + transparent. ++ The second one is named using the second `ident`. It has type `term`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with ``Qed``, and transparent if the proof ends with ``Defined``. + +.. example:: + .. coqtop:: all + + Require Coq.derive.Derive. + Require Import Coq.Numbers.Natural.Peano.NPeano. + + Section P. + + Variables (n m k:nat). + + Derive p SuchThat ((k*n)+(k*m) = p) As h. + Proof. + rewrite <- Nat.mul_add_distr_l. + subst p. + reflexivity. + Qed. + + End P. + + Print p. + Check h. + +Any property can be used as `term`, not only an equation. In particular, +it could be an order relation specifying some form of program +refinement or a non-executable property from which deriving a program +is convenient. diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst new file mode 100644 index 000000000..8c1b9d152 --- /dev/null +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -0,0 +1,229 @@ +.. include:: ../replaces.rst + +.. _asynchronousandparallelproofprocessing: + +Asynchronous and Parallel Proof Processing +========================================== + +:Author: Enrico Tassi + +This chapter explains how proofs can be asynchronously processed by +|Coq|. This feature improves the reactivity of the system when used in +interactive mode via |CoqIDE|. In addition, it allows |Coq| to take +advantage of parallel hardware when used as a batch compiler by +decoupling the checking of statements and definitions from the +construction and checking of proofs objects. + +This feature is designed to help dealing with huge libraries of +theorems characterized by long proofs. In the current state, it may +not be beneficial on small sets of short files. + +This feature has some technical limitations that may make it +unsuitable for some use cases. + +For example, in interactive mode, some errors coming from the kernel +of |Coq| are signaled late. The type of errors belonging to this +category are universe inconsistencies. + +At the time of writing, only opaque proofs (ending with ``Qed`` or +``Admitted``) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running |CoqIDE| in +Windows. The current implementation of the feature is not stable on +Windows. It can be enabled, as described below at :ref:`interactive-mode`, +though doing so is not recommended. + +Proof annotations +---------------------- + +To process a proof asynchronously |Coq| needs to know the precise +statement of the theorem without looking at the proof. This requires +some annotations if the theorem is proved inside a Section (see +Section :ref:`TODO-2.4`). + +When a section ends, |Coq| looks at the proof object to decide which +section variables are actually used and hence have to be quantified in +the statement of the theorem. To avoid making the construction of +proofs mandatory when ending a section, one can start each proof with +the ``Proof using`` command (Section :ref:`TODO-7.1.5`) that declares which section +variables the theorem uses. + +The presence of ``Proof`` using is needed to process proofs asynchronously +in interactive mode. + +It is not strictly mandatory in batch mode if it is not the first time +the file is compiled and if the file itself did not change. When the +proof does not begin with Proof using, the system records in an +auxiliary file, produced along with the `.vo` file, the list of section +variables used. + +Automatic suggestion of proof annotations +````````````````````````````````````````` + +The command ``Set Suggest Proof Using`` makes |Coq| suggest, when a ``Qed`` +command is processed, a correct proof annotation. It is up to the user +to modify the proof script accordingly. + + +Proof blocks and error resilience +-------------------------------------- + +|Coq| 8.6 introduced a mechanism for error resiliency: in interactive +mode |Coq| is able to completely check a document containing errors +instead of bailing out at the first failure. + +Two kind of errors are supported: errors occurring in vernacular +commands and errors occurring in proofs. + +To properly recover from a failing tactic, |Coq| needs to recognize the +structure of the proof in order to confine the error to a sub proof. +Proof block detection is performed by looking at the syntax of the +proof script (i.e. also looking at indentation). |Coq| comes with four +kind of proof blocks, and an ML API to add new ones. + +:curly: blocks are delimited by { and }, see Chapter :ref:`proofhandling` +:par: blocks are atomic, i.e. just one tactic introduced by the `par:` + goal selector +:indent: blocks end with a tactic indented less than the previous one +:bullet: blocks are delimited by two equal bullet signs at the same + indentation level + +Caveats +```````` + +When a vernacular command fails the subsequent error messages may be +bogus, i.e. caused by the first error. Error resiliency for vernacular +commands can be switched off by passing ``-async-proofs-command-error-resilience off`` +to |CoqIDE|. + +An incorrect proof block detection can result into an incorrect error +recovery and hence in bogus errors. Proof block detection cannot be +precise for bullets or any other non well parenthesized proof +structure. Error resiliency can be turned off or selectively activated +for any set of block kind passing to |CoqIDE| one of the following +options: + +- ``-async-proofs-tactic-error-resilience off`` +- ``-async-proofs-tactic-error-resilience all`` +- ``-async-proofs-tactic-error-resilience`` :n:`{*, blocktype}` + +Valid proof block types are: “curly”, “par”, “indent”, and “bullet”. + +.. _interactive-mode: + +Interactive mode +--------------------- + +At the time of writing the only user interface supporting asynchronous +proof processing is |CoqIDE|. + +When |CoqIDE| is started, two |Coq| processes are created. The master one +follows the user, giving feedback as soon as possible by skipping +proofs, which are delegated to the worker process. The worker process, +whose state can be seen by clicking on the button in the lower right +corner of the main |CoqIDE| window, asynchronously processes the proofs. +If a proof contains an error, it is reported in red in the label of +the very same button, that can also be used to see the list of errors +and jump to the corresponding line. + +If a proof is processed asynchronously the corresponding Qed command +is colored using a lighter color that usual. This signals that the +proof has been delegated to a worker process (or will be processed +lazily if the ``-async-proofs lazy`` option is used). Once finished, the +worker process will provide the proof object, but this will not be +automatically checked by the kernel of the main process. To force the +kernel to check all the proof objects, one has to click the button +with the gears. Only then are all the universe constraints checked. + +Caveats +``````` + +The number of worker processes can be increased by passing |CoqIDE| +the ``-async-proofs-j n`` flag. Note that the memory consumption increases too, +since each worker requires the same amount of memory as the master +process. Also note that increasing the number of workers may reduce +the reactivity of the master process to user commands. + +To disable this feature, one can pass the ``-async-proofs off`` flag to +|CoqIDE|. Conversely, on Windows, where the feature is disabled by +default, pass the ``-async-proofs on`` flag to enable it. + +Proofs that are known to take little time to process are not delegated +to a worker process. The threshold can be configure with +``-async-proofs-delegation-threshold``. Default is 0.03 seconds. + +Batch mode +--------------- + +When |Coq| is used as a batch compiler by running `coqc` or `coqtop` +-compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, +among other things, theorems statements and proofs. Hence to produce a +.vo |Coq| need to process all the proofs of the `.v` file. + +The asynchronous processing of proofs can decouple the generation of a +compiled file (like the `.vo` one) that can be loaded by ``Require`` from the +generation and checking of the proof objects. The ``-quick`` flag can be +passed to `coqc` or `coqtop` to produce, quickly, `.vio` files. +Alternatively, when using a Makefile produced by `coq_makefile`, +the ``quick`` target can be used to compile all files using the ``-quick`` flag. + +A `.vio` file can be loaded using ``Require`` exactly as a `.vo` file but +proofs will not be available (the Print command produces an error). +Moreover, some universe constraints might be missing, so universes +inconsistencies might go unnoticed. A `.vio` file does not contain proof +objects, but proof tasks, i.e. what a worker process can transform +into a proof object. + +Compiling a set of files with the ``-quick`` flag allows one to work, +interactively, on any file without waiting for all the proofs to be +checked. + +When working interactively, one can fully check all the `.v` files by +running `coqc` as usual. + +Alternatively one can turn each `.vio` into the corresponding `.vo`. All +.vio files can be processed in parallel, hence this alternative might +be faster. The command ``coqtop -schedule-vio2vo 2 a b c`` can be used to +obtain a good scheduling for two workers to produce `a.vo`, `b.vo`, and +`c.vo`. When using a Makefile produced by `coq_makefile`, the ``vio2vo`` target +can be used for that purpose. Variable `J` should be set to the number +of workers, e.g. ``make vio2vo J=2``. The only caveat is that, while the +.vo files obtained from `.vio` files are complete (they contain all proof +terms and universe constraints), the satisfiability of all universe +constraints has not been checked globally (they are checked to be +consistent for every single proof). Constraints will be checked when +these `.vo` files are (recursively) loaded with ``Require``. + +There is an extra, possibly even faster, alternative: just check the +proof tasks stored in `.vio` files without producing the `.vo` files. This +is possibly faster because all the proof tasks are independent, hence +one can further partition the job to be done between workers. The +``coqtop -schedule-vio-checking 6 a b c`` command can be used to obtain a +good scheduling for 6 workers to check all the proof tasks of `a.vio`, +`b.vio`, and `c.vio`. Auxiliary files are used to predict how long a proof +task will take, assuming it will take the same amount of time it took +last time. When using a Makefile produced by coq_makefile, the +``checkproofs`` target can be used to check all `.vio` files. Variable `J` +should be set to the number of workers, e.g. ``make checkproofs J=6``. As +when converting `.vio` files to `.vo` files, universe constraints are not +checked to be globally consistent. Hence this compilation mode is only +useful for quick regression testing and on developments not making +heavy use of the `Type` hierarchy. + +Limiting the number of parallel workers +-------------------------------------------- + +Many |Coq| processes may run on the same computer, and each of them may +start many additional worker processes. The `coqworkmgr` utility lets +one limit the number of workers, globally. + +The utility accepts the ``-j`` argument to specify the maximum number of +workers (defaults to 2). `coqworkmgr` automatically starts in the +background and prints an environment variable assignment +like ``COQWORKMGR_SOCKET=localhost:45634``. The user must set this variable +in all the shells from which |Coq| processes will be started. If one +uses just one terminal running the bash shell, then +``export ‘coqworkmgr -j 4‘`` will do the job. + +After that, all |Coq| processes, e.g. `coqide` and `coqc`, will honor the +limit, globally. diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index a60f32645..fac0d0a4f 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -376,7 +376,7 @@ contributed by Jean Goubault was integrated in the basic theories. Pierre Courtieu developed a command and a tactic to reason on the inductive structure of recursively defined functions. -Jacek Chrzszcz designed and implemented the module system of |Coq| whose +Jacek Chrząszcz designed and implemented the module system of |Coq| whose foundations are in Judicaël Courant’s PhD thesis. The development was coordinated by C. Paulin. @@ -478,7 +478,7 @@ Marché and Bruno Barras. Claude Marché coordinated the edition of the Reference Manual for |Coq| V8.0. -Pierre Letouzey and Jacek Chrzszcz respectively maintained the +Pierre Letouzey and Jacek Chrząszcz respectively maintained the extraction tool and module system of |Coq|. Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and other diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 75e955136..db03693ff 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -54,6 +54,8 @@ Table of contents addendum/ring addendum/nsatz addendum/generalized-rewriting + addendum/parallel-proof-processing + addendum/miscellaneous-extensions .. toctree:: :caption: Reference diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index da34e3b55..2af73c28e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1635,7 +1635,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). .. tacv:: elim @term using @term .. tacv:: elim @term using @term with @bindings_list - Allows the user to give explicitly an elimination predicate :n:`@term` that + Allows the user to give explicitly an induction principle :n:`@term` that is not the standard one for the underlying inductive type of :n:`@term`. The :n:`@bindings_list` clause allows instantiating premises of the type of :n:`@term`. diff --git a/ide/MacOS/relatify_with-respect-to_.sh b/ide/MacOS/relatify_with-respect-to_.sh deleted file mode 100755 index a24af9395..000000000 --- a/ide/MacOS/relatify_with-respect-to_.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh - -set -e - -for i in "$3/"*.dylib -do install_name_tool -change "$2"/$(basename $i) @executable_path/../Resources/lib/$(basename $i) "$1" -done -case "$1" in - *.dylib) - install_name_tool -id @executable_path/../Resources/lib/$(basename $1) $1 - for i in "$3"/*.dylib - do install_name_tool -change "$2/"$(basename $1) @executable_path/../Resources/lib/$(basename $1) $i - done;; - *) -esac diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 48ddd9496..bb5fd5294 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -589,11 +589,17 @@ let explicitize inctx impl (cf,f) args = let expl () = match ip with | Some i -> - if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then - raise Expl + (* Careful: It is possible to have declared implicits ending + before the principal argument *) + let is_impl = + try is_status_implicit (List.nth impl (i-1)) + with Failure _ -> false + in + if is_impl + then raise Expl else let (args1,args2) = List.chop i args in - let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in + let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in let args1 = exprec 1 (args1,impl1) in let args2 = exprec (i+1) (args2,impl2) in let ip = Some (List.length args1) in diff --git a/interp/impargs.ml b/interp/impargs.ml index 9ad62c0de..b424f73de 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -139,7 +139,7 @@ let argument_less = function | Hyp _, Conclusion -> true | Conclusion, _ -> false -let update pos rig (na,st) = +let update pos rig st = let e = if rig then match st with @@ -163,7 +163,7 @@ let update pos rig (na,st) = | Some (DepFlex fpos as x) -> if argument_less (pos,fpos) then DepFlex pos else x | Some Manual -> assert false - in na, Some e + in Some e (* modified is_rigid_reference with a truncated env *) let is_flexible_reference env sigma bound depth f = @@ -214,6 +214,8 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc +(* compute the list of implicit arguments *) + let rec is_rigid_head sigma t = match kind sigma t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true @@ -226,7 +228,14 @@ let rec is_rigid_head sigma t = match kind sigma t with | Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _ | Prod _ | Meta _ | Cast _ -> assert false -(* calcule la liste des arguments implicites *) +let is_rigid env sigma t = + let open Context.Rel.Declaration in + let t = whd_all env sigma t in + match kind sigma t with + | Prod (na,a,b) -> + let (_,t) = splay_prod (push_rel (LocalAssum (na,a)) env) sigma b in + is_rigid_head sigma t + | _ -> true let find_displayed_name_in all avoid na (env, b) = let envnames_b = (env, b) in @@ -234,43 +243,54 @@ let find_displayed_name_in all avoid na (env, b) = if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b else compute_displayed_name_in Evd.empty flag avoid na b -let compute_implicits_gen strict strongly_strict revpat contextual all env sigma (t : EConstr.t) = - let rigid = ref true in +let compute_implicits_names_gen all env sigma t = + let open Context.Rel.Declaration in + let rec aux env avoid names t = + let t = whd_all env sigma t in + match kind sigma t with + | Prod (na,a,b) -> + let na',avoid' = find_displayed_name_in all avoid na (names,b) in + aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b + | _ -> List.rev names + in aux env Id.Set.empty [] t + +let compute_implicits_names = compute_implicits_names_gen true + +let compute_implicits_explanation_gen strict strongly_strict revpat contextual env sigma t = let open Context.Rel.Declaration in - let rec aux env avoid n names (t : EConstr.t) = + let rec aux env n t = let t = whd_all env sigma t in match kind sigma t with - | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in all avoid na (names,b) in - add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) - (aux (push_rel (LocalAssum (na',a)) env) avoid' (n+1) (na'::names) b) - | _ -> - rigid := is_rigid_head sigma t; - let names = List.rev names in - let v = Array.map (fun na -> na,None) (Array.of_list names) in - if contextual then - add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v - else v + | Prod (na,a,b) -> + add_free_rels_until strict strongly_strict revpat n env sigma a (Hyp (n+1)) + (aux (push_rel (LocalAssum (na,a)) env) (n+1) b) + | _ -> + let v = Array.make n None in + if contextual then + add_free_rels_until strict strongly_strict revpat n env sigma t Conclusion v + else v in match kind sigma (whd_all env sigma t) with - | Prod (na,a,b) -> - let na',avoid = find_displayed_name_in all Id.Set.empty na ([],b) in - let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in - !rigid, Array.to_list v - | _ -> true, [] + | Prod (na,a,b) -> + let v = aux (push_rel (LocalAssum (na,a)) env) 1 b in + Array.to_list v + | _ -> [] -let compute_implicits_flags env sigma f all t = - compute_implicits_gen +let compute_implicits_explanation_flags env sigma f t = + compute_implicits_explanation_gen (f.strict || f.strongly_strict) f.strongly_strict - f.reversible_pattern f.contextual all env sigma t + f.reversible_pattern f.contextual env sigma t -let compute_auto_implicits env sigma flags enriching t = - if enriching then compute_implicits_flags env sigma flags true t - else compute_implicits_gen false false false true true env sigma t +let compute_implicits_flags env sigma f all t = + List.combine + (compute_implicits_names_gen all env sigma t) + (compute_implicits_explanation_flags env sigma f t) -let compute_implicits_names env sigma t = - let _, impls = compute_implicits_gen false false false false true env sigma t in - List.map fst impls +let compute_auto_implicits env sigma flags enriching t = + List.combine + (compute_implicits_names env sigma t) + (if enriching then compute_implicits_explanation_flags env sigma flags t + else compute_implicits_explanation_gen false false false true env sigma t) (* Extra information about implicit arguments *) @@ -329,13 +349,16 @@ let rec prepare_implicits f = function Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps' | _::imps -> None :: prepare_implicits f imps -let set_implicit id imp insmax = - (id,(match imp with None -> Manual | Some imp -> imp),insmax) - -let rec assoc_by_pos k = function - (ExplByPos (k', x), b) :: tl when Int.equal k k' -> (x,b), tl - | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl - | [] -> raise Not_found +(* +If found, returns Some (x,(b,fi,fo)) and l with the entry removed, +otherwise returns None and l unchanged. + *) +let assoc_by_pos k l = + let rec aux = function + (ExplByPos (k', x), b) :: tl when Int.equal k k' -> Some (x,b), tl + | hd :: tl -> let (x, tl) = aux tl in x, hd :: tl + | [] -> raise Not_found + in try aux l with Not_found -> None, l let check_correct_manual_implicits autoimps l = List.iter (function @@ -352,70 +375,65 @@ let check_correct_manual_implicits autoimps l = (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name.")) l -let set_manual_implicits env flags enriching autoimps l = - let try_forced k l = - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - if fo then - let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in - l', Some (id,Manual,(b,fi)) - else l, None - with Not_found -> l, None - in +(* Take a list l of explicitations, and map them to positions. *) +let flatten_explicitations l autoimps = + let rec aux k l = function + | (Name id,_)::imps -> + let value, l' = + try + let eq = explicitation_eq in + let flags = List.assoc_f eq (ExplByName id) l in + Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l + with Not_found -> assoc_by_pos k l + in value :: aux (k+1) l' imps + | (Anonymous,_)::imps -> + let value, l' = assoc_by_pos k l + in value :: aux (k+1) l' imps + | [] when List.is_empty l -> [] + | [] -> + check_correct_manual_implicits autoimps l; + [] + in aux 1 l autoimps + +let set_manual_implicits flags enriching autoimps l = if not (List.distinct l) then user_err Pp.(str "Some parameters are referred more than once."); (* Compare with automatic implicits to recover printing data and names *) - let rec merge k l = function - | (Name id,imp)::imps -> - let l',imp,m = - try - let eq = explicitation_eq in - let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in - List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) - with Not_found -> - try - let (id, (b, fi, fo)), l' = assoc_by_pos k l in - l', (Some Manual), (Some (b,fi)) - with Not_found -> - let m = match enriching, imp with - | true, Some _ -> Some (flags.maximal, true) - | _ -> None - in - l, imp, m - in - let imps' = merge (k+1) l' imps in - let m = Option.map (fun (b,f) -> - (* match imp with Some Manual -> (b,f) *) - (* | _ -> *)set_maximality imps' b, f) m in - Option.map (set_implicit id imp) m :: imps' - | (Anonymous,imp)::imps -> - let l', forced = try_forced k l in - forced :: merge (k+1) l' imps - | [] when begin match l with [] -> true | _ -> false end -> [] - | [] -> - check_correct_manual_implicits autoimps l; - [] - in - merge 1 l autoimps - -let compute_semi_auto_implicits env sigma f manual t = - match manual with - | [] -> - if not f.auto then [DefaultImpArgs, []] - else let _,l = compute_implicits_flags env sigma f false t in - [DefaultImpArgs, prepare_implicits f l] - | _ -> - let _,autoimpls = compute_auto_implicits env sigma f f.auto t in - [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] + let rec merge k autoimps explimps = match autoimps, explimps with + | autoimp::autoimps, explimp::explimps -> + let imps' = merge (k+1) autoimps explimps in + begin match autoimp, explimp with + | (Name id,_), Some (_, (b, fi, _)) -> + Some (id, Manual, (set_maximality imps' b, fi)) + | (Name id,Some exp), None when enriching -> + Some (id, exp, (set_maximality imps' flags.maximal, true)) + | (Name _,_), None -> None + | (Anonymous,_), Some (Some id, (b, fi, true)) -> + Some (id,Manual,(b,fi)) + | (Anonymous,_), Some (None, (b, fi, true)) -> + let id = Id.of_string ("arg_" ^ string_of_int k) in + Some (id,Manual,(b,fi)) + | (Anonymous,_), Some (_, (_, _, false)) -> None + | (Anonymous,_), None -> None + end :: imps' + | [], [] -> [] + (* flatten_explicitations returns a list of the same length as autoimps *) + | _ -> assert false + in merge 1 autoimps (flatten_explicitations l autoimps) + +let compute_semi_auto_implicits env sigma f t = + if not f.auto then [DefaultImpArgs, []] + else let l = compute_implicits_flags env sigma f false t in + [DefaultImpArgs, prepare_implicits f l] (*s Constants. *) -let compute_constant_implicits flags manual cst = +let compute_constant_implicits flags cst = let env = Global.env () in let sigma = Evd.from_env env in let cb = Environ.lookup_constant cst env in let ty = of_constr cb.const_type in - let impls = compute_semi_auto_implicits env sigma flags manual ty in + let impls = compute_semi_auto_implicits env sigma flags ty in impls (*s Inductives and constructors. Their implicit arguments are stored @@ -423,7 +441,7 @@ let compute_constant_implicits flags manual cst = $i$ are the implicit arguments of the inductive and $v$ the array of implicit arguments of the constructors. *) -let compute_mib_implicits flags manual kn = +let compute_mib_implicits flags kn = let env = Global.env () in let sigma = Evd.from_env env in let mib = Environ.lookup_mind kn env in @@ -439,34 +457,34 @@ let compute_mib_implicits flags manual kn = let imps_one_inductive i mip = let ind = (kn,i) in let ar, _ = Global.type_of_global_in_context env (IndRef ind) in - ((IndRef ind,compute_semi_auto_implicits env sigma flags manual (of_constr ar)), + ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)), Array.mapi (fun j c -> - (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags manual c)) + (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c)) (Array.map of_constr mip.mind_nf_lc)) in Array.mapi imps_one_inductive mib.mind_packets -let compute_all_mib_implicits flags manual kn = - let imps = compute_mib_implicits flags manual kn in +let compute_all_mib_implicits flags kn = + let imps = compute_mib_implicits flags kn in List.flatten (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) -let compute_var_implicits flags manual id = +let compute_var_implicits flags id = let env = Global.env () in let sigma = Evd.from_env env in - compute_semi_auto_implicits env sigma flags manual (NamedDecl.get_type (lookup_named id env)) + compute_semi_auto_implicits env sigma flags (NamedDecl.get_type (lookup_named id env)) (* Implicits of a global reference. *) -let compute_global_implicits flags manual = function - | VarRef id -> compute_var_implicits flags manual id - | ConstRef kn -> compute_constant_implicits flags manual kn +let compute_global_implicits flags = function + | VarRef id -> compute_var_implicits flags id + | ConstRef kn -> compute_constant_implicits flags kn | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits flags manual kn).(i) in imps + let ((_,imps),_) = (compute_mib_implicits flags kn).(i) in imps | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits flags manual kn).(i) in snd cimps.(j-1) + let (_,cimps) = (compute_mib_implicits flags kn).(i) in snd cimps.(j-1) (* Merge a manual explicitation with an implicit_status list *) @@ -573,34 +591,34 @@ let rebuild_implicits (req,l) = | ImplLocal -> assert false | ImplConstant (con,flags) -> let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags [] con in + let newimpls = compute_constant_implicits flags con in req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> - let newimpls = compute_all_mib_implicits flags [] kn in + let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = - match olds, news with - | (_, oldimpls) :: old, (gr, newimpls) :: tl -> - (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl - | [], [] -> [] - | _, _ -> assert false + match olds, news with + | (_, oldimpls) :: old, (gr, newimpls) :: tl -> + (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl + | [], [] -> [] + | _, _ -> assert false in req, aux l newimpls | ImplInteractive (ref,flags,o) -> (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_global_implicits flags [] ref in - [ref,List.map2 merge_impls oldimpls newimpls] + let oldimpls = snd (List.hd l) in + let newimpls = compute_global_implicits flags ref in + [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in - if flags.auto then - let newimpls = List.hd (compute_global_implicits flags [] ref) in - let p = List.length (snd newimpls) - userimplsize in - let newimpls = on_snd (List.firstn p) newimpls in - [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] - else - [ref,oldimpls] + let oldimpls = snd (List.hd l) in + if flags.auto then + let newimpls = List.hd (compute_global_implicits flags ref) in + let p = List.length (snd newimpls) - userimplsize in + let newimpls = on_snd (List.firstn p) newimpls in + [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] + else + [ref,oldimpls] let classify_implicits (req,_ as obj) = match req with | ImplLocal -> Dispose @@ -622,7 +640,7 @@ let inImplicits : implicits_obj -> obj = let is_local local ref = local || isVarRef ref && is_in_section ref let declare_implicits_gen req flags ref = - let imps = compute_global_implicits flags [] ref in + let imps = compute_global_implicits flags ref in add_anonymous_leaf (inImplicits (req,[ref,imps])) let declare_implicits local ref = @@ -643,7 +661,7 @@ let declare_mib_implicits kn = let flags = !implicit_args in let imps = Array.map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) - (compute_mib_implicits flags [] kn) in + (compute_mib_implicits flags kn) in add_anonymous_leaf (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps)) @@ -653,8 +671,8 @@ type manual_explicitation = Constrexpr.explicitation * (bool * bool * bool) type manual_implicits = manual_explicitation list let compute_implicits_with_manual env sigma typ enriching l = - let _,autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in - set_manual_implicits env !implicit_args enriching autoimpls l + let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in + set_manual_implicits !implicit_args enriching autoimpls l let check_inclusion l = (* Check strict inclusion *) @@ -679,26 +697,26 @@ let declare_manual_implicits local ref ?enriching l = let env = Global.env () in let sigma = Evd.from_env env in let t, _ = Global.type_of_global_in_context env ref in + let t = of_constr t in let enriching = Option.default flags.auto enriching in - let isrigid,autoimpls = compute_auto_implicits env sigma flags enriching (of_constr t) in + let autoimpls = compute_auto_implicits env sigma flags enriching t in let l' = match l with | [] -> assert false | [l] -> - [DefaultImpArgs, set_manual_implicits env flags enriching autoimpls l] + [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] | _ -> - check_rigidity isrigid; - let l = List.map (fun imps -> (imps,List.length imps)) l in - let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in - check_inclusion l; - let nargs = List.length autoimpls in - List.map (fun (imps,n) -> - (LessArgsThan (nargs-n), - set_manual_implicits env flags enriching autoimpls imps)) l in + check_rigidity (is_rigid env sigma t); + let l = List.map (fun imps -> (imps,List.length imps)) l in + let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in + check_inclusion l; + let nargs = List.length autoimpls in + List.map (fun (imps,n) -> + (LessArgsThan (nargs-n), + set_manual_implicits flags enriching autoimpls imps)) l in let req = if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) - in - add_anonymous_leaf (inImplicits (req,[ref,l'])) + in add_anonymous_leaf (inImplicits (req,[ref,l'])) let maybe_declare_manual_implicits local ref ?enriching l = match l with diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a1a3be70f..58df9abc4 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -245,6 +245,12 @@ let implicit_application env ?(allow_partial=true) f ty = CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid in c, avoid +let warn_ignoring_implicit_status = + CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" + (fun na -> + strbrk "Ignoring implicit status of product binder " ++ + Name.print na ++ strbrk " and following binders") + let implicits_of_glob_constr ?(with_products=true) l = let add_impl i na bk l = match bk with | Implicit -> @@ -260,20 +266,18 @@ let implicits_of_glob_constr ?(with_products=true) l = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match DAst.get c with - | GProd (na, bk, t, b) -> - if with_products then abs na bk b - else - let () = match bk with - | Implicit -> - Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - Name.print na ++ strbrk " and following binders") - | _ -> () - in [] - | GLambda (na, bk, t, b) -> abs na bk b - | GLetIn (na, b, t, c) -> aux i b - | GRec (fix_kind, nas, args, tys, bds) -> - let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) - | _ -> [] + match DAst.get c with + | GProd (na, bk, t, b) -> + if with_products then abs na bk b + else + let () = match bk with + | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | _ -> () + in [] + | GLambda (na, bk, t, b) -> abs na bk b + | GLetIn (na, b, t, c) -> aux i b + | GRec (fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + | _ -> [] in aux 1 l diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 9eb6f62cc..72db3b31c 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -142,19 +142,6 @@ type multi = | RepeatStar | RepeatPlus -type 'a core_destruction_arg = - | ElimOnConstr of 'a - | ElimOnIdent of lident - | ElimOnAnonHyp of int - -type 'a destruction_arg = - clear_flag * 'a core_destruction_arg - -type inversion_kind = - | SimpleInversion - | FullInversion - | FullInversionClear - type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) univdecl_extensible_instance : bool; (* Can new universes be added *) diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 0e84a07aa..06f969f19 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -297,13 +297,9 @@ type inline = type module_ast_inl = module_ast * inline type module_binder = bool option * lident list * module_ast_inl -(** Cumulativity can be set globally, locally or unset locally and it - can not enabled at all. *) -type cumulative_inductive_parsing_flag = - | GlobalCumulativity - | GlobalNonCumulativity - | LocalCumulativity - | LocalNonCumulativity +(** [Some b] if locally enabled/disabled according to [b], [None] if + we should use the global flag. *) +type vernac_cumulative = VernacCumulative | VernacNonCumulative (** {6 The type of vernacular expressions} *) @@ -338,7 +334,7 @@ type nonrec vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list @@ -501,14 +497,13 @@ type vernac_type = | VtProofMode of string (* Queries are commands assumed to be "pure", that is to say, they don't modify the interpretation state. *) - | VtQuery of vernac_part_of_script * Feedback.route_id + | VtQuery (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list -and vernac_part_of_script = bool and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index a11a0dc00..91cc64523 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -19,6 +19,8 @@ open Util (*********************) (* Explicit lifts and basic operations *) +(* Invariant to preserve in this module: no lift contains two consecutive + [ELSHFT] nor two consecutive [ELLFT]. *) type lift = | ELID | ELSHFT of lift * int (* ELSHFT(l,n) == lift of n, then apply lift l *) @@ -28,15 +30,15 @@ type lift = let el_id = ELID (* compose a relocation of magnitude n *) -let rec el_shft_rec n = function - | ELSHFT(el,k) -> el_shft_rec (k+n) el +let el_shft_rec n = function + | ELSHFT(el,k) -> ELSHFT(el,k+n) | el -> ELSHFT(el,n) let el_shft n el = if Int.equal n 0 then el else el_shft_rec n el (* cross n binders *) -let rec el_liftn_rec n = function +let el_liftn_rec n = function | ELID -> ELID - | ELLFT(k,el) -> el_liftn_rec (n+k) el + | ELLFT(k,el) -> ELLFT(n+k, el) | el -> ELLFT(n, el) let el_liftn n el = if Int.equal n 0 then el else el_liftn_rec n el diff --git a/kernel/esubst.mli b/kernel/esubst.mli index b82d6fdf0..a674c425a 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -56,7 +56,11 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs (** {6 Compact representation } *) (** Compact representation of explicit relocations - [ELSHFT(l,n)] == lift of [n], then apply [lift l]. - - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *) + - [ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. + + Invariant ensured by the private flag: no lift contains two consecutive + [ELSHFT] nor two consecutive [ELLFT]. +*) type lift = private | ELID | ELSHFT of lift * int diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 8b445985b..593dcbf58 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -161,20 +161,10 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) (* Gallina inductive declarations *) - | cum = cumulativity_token; priv = private_token; f = finite_token; + | cum = OPT cumulativity_token; priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - let cum = - match cum with - Some true -> LocalCumulativity - | Some false -> LocalNonCumulativity - | None -> - if Flags.is_polymorphic_inductive_cumulativity () then - GlobalCumulativity - else - GlobalNonCumulativity - in VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (NoDischarge, recs) @@ -257,7 +247,8 @@ GEXTEND Gram | IDENT "Class" -> (Class true,BiFinite) ] ] ; cumulativity_token: - [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] + [ [ IDENT "Cumulative" -> VernacCumulative + | IDENT "NonCumulative" -> VernacNonCumulative ] ] ; private_token: [ [ IDENT "Private" -> true | -> false ] ] diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 49f7aae43..319b410df 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1512,7 +1512,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1527,7 +1527,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2743a8a2f..ae84eaa93 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -969,7 +969,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic = Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); - Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); + Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid)); (fun g -> let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 6637de745..434feba95 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -25,7 +25,7 @@ val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eva val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry -val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry +val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5951f2b11..aea00c240 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -84,7 +84,7 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t +val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 5347eda7d..59473a5e5 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -23,7 +23,7 @@ val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_typ val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type val wit_destruction_arg : - (constr_expr with_bindings Tacexpr.destruction_arg, - glob_constr_and_expr with_bindings Tacexpr.destruction_arg, - delayed_open_constr_with_bindings Tacexpr.destruction_arg) genarg_type + (constr_expr with_bindings Tactics.destruction_arg, + glob_constr_and_expr with_bindings Tactics.destruction_arg, + delayed_open_constr_with_bindings Tactics.destruction_arg) genarg_type diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 8b0c44041..3baa475ab 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector = | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,7 +73,7 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * + 'dconstr with_bindings Tactics.destruction_arg * (intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -265,7 +269,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 8b0c44041..3baa475ab 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -40,25 +40,29 @@ type goal_selector = Vernacexpr.goal_selector = | SelectList of (int * int) list | SelectId of Id.t | SelectAll +[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] -type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = +type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = | ElimOnConstr of 'a | ElimOnIdent of lident | ElimOnAnonHyp of int +[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] type 'a destruction_arg = - clear_flag * 'a core_destruction_arg + clear_flag * 'a Tactics.core_destruction_arg +[@@ocaml.deprecated "Use Tactics.destruction_arg"] -type inversion_kind = Misctypes.inversion_kind = +type inversion_kind = Inv.inversion_kind = | SimpleInversion | FullInversion | FullInversionClear +[@@ocaml.deprecated "Use Tactics.inversion_kind"] type ('c,'d,'id) inversion_strength = | NonDepInversion of - inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option | DepInversion of - inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option + Inv.inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option | InversionUsing of 'c * 'id list type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b @@ -69,7 +73,7 @@ type 'id message_token = | MsgIdent of 'id type ('dconstr,'id) induction_clause = - 'dconstr with_bindings destruction_arg * + 'dconstr with_bindings Tactics.destruction_arg * (intro_pattern_naming_expr CAst.t option (* eqn:... *) * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *) * 'id clause_expr option (* in ... *) @@ -265,7 +269,7 @@ and 'a gen_tactic_expr = ('p,'a gen_tactic_expr) match_rule list | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located - | TacSelect of goal_selector * 'a gen_tactic_expr + | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr (* For ML extensions *) | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located (* For syntax extensions *) diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 42566575c..7897cb170 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -133,6 +133,12 @@ let intro_clear ids future_ipats = isCLR_PUSHL clear_ids end +let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl -> + let ctx = Goal.hyps gl in + List.iter (Ssrcommon.check_hyp_exists ctx) hyps; + tclUNIT () +end + (** [=> []] *****************************************************************) let tac_case t = Goal.enter begin fun _ -> @@ -229,7 +235,9 @@ let rec ipat_tac1 future_ipats ipat : unit tactic = | IPatNoop -> tclUNIT () | IPatSimpl Nop -> tclUNIT () - | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats + | IPatClear ids -> + tacCHECK_HYPS_EXIST ids <*> + intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats | IPatSimpl (Simpl n) -> V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n)) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 0d82a9f09..5f3967440 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -585,21 +585,10 @@ let pr_ssripat _ _ _ = pr_ipat let pr_ssripats _ _ _ = pr_ipats let pr_ssriorpat _ _ _ = pr_iorpat -(* -let intern_ipat ist ipat = - let rec check_pat = function - | IPatClear clr -> ignore (List.map (intern_hyp ist) clr) - | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat - | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat - | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat - | _ -> () in - check_pat ipat; ipat -*) - let intern_ipat ist = map_ipat (fun id -> id) - (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *) + (intern_hyp ist) (glob_ast_closure_term ist) let intern_ipats ist = List.map (intern_ipat ist) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index bbf0e2b60..7eb8396ac 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -767,8 +767,9 @@ open Decl_kinds if p then let cm = match cum with - | GlobalCumulativity | LocalCumulativity -> "Cumulative" - | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + | Some VernacCumulative -> "Cumulative" + | Some VernacNonCumulative -> "NonCumulative" + | None -> "" in cm ^ " " ^ kind else kind diff --git a/stm/stm.ml b/stm/stm.ml index a0305efee..ba0a2017a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2782,16 +2782,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) | VtMeta, _ -> let id, w = Backtrack.undo_vernac_classifier expr in process_back_meta_command ~newtip ~head id x w + (* Query *) - | VtQuery (false,route), VtNow -> - let query_sid = VCS.cur_tip () in - (try - let st = Vernacstate.freeze_interp_state `No in - ignore(stm_vernac_interp ~route query_sid st x) - with e -> - let e = CErrors.push e in - Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok - | VtQuery (true, route), w -> + | VtQuery, w -> let id = VCS.new_node ~id:newtip () in let queue = if !cur_opt.async_proofs_full then `QueryQueue (ref false) @@ -2803,9 +2796,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | VtQuery (false,_), VtLater -> - anomaly(str"classifier: VtQuery + VtLater must imply part_of_script.") - (* Proof *) | VtStartProof (mode, guarantee, names), w -> let id = VCS.new_node ~id:newtip () in @@ -3048,8 +3038,9 @@ let query ~doc ~at ~route s = let { CAst.loc; v=ast } = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; + let st = State.get_cached at in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in - ignore(process_transaction aast (VtQuery (false,route), VtNow)) + ignore(stm_vernac_interp ~route at st aast) done; with | End_of_input -> () diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index eecee40df..c08cc6e36 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -16,8 +16,6 @@ open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] -let string_of_in_script b = if b then " (inside script)" else "" - let string_of_parallel = function | `Yes (solve,abs) -> "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" @@ -34,7 +32,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route + | VtQuery -> "Query" | VtMeta -> "Meta " let string_of_vernac_when = function @@ -70,7 +68,7 @@ let classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater + | VernacCheckMayEval _ -> VtQuery, VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -205,7 +203,7 @@ let classify_vernac e = static_control_classifier ~poly e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier ~poly e with - | ( VtQuery _ | VtProofStep _ | VtSideff _ + | ( VtQuery | VtProofStep _ | VtSideff _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, @@ -214,6 +212,6 @@ let classify_vernac e = in static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e -let classify_as_query = VtQuery (true,Feedback.default_route), VtLater +let classify_as_query = VtQuery, VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater diff --git a/tactics/equality.mli b/tactics/equality.mli index c0be917a0..ccf454c3e 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -80,20 +80,20 @@ val discrConcl : unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic (* Below, if flag is [None], it takes the value from the dynamic value of the option *) val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : inj_flags option -> intro_patterns option -> evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic val injConcl : inj_flags option -> unit Proofview.tactic val simpleInjClause : inj_flags option -> evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic -val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic +val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) diff --git a/tactics/inv.ml b/tactics/inv.ml index 067fc8941..d76c9a697 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -64,6 +64,11 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + let compute_eqn env sigma n i ai = (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) diff --git a/tactics/inv.mli b/tactics/inv.mli index c63d57af5..9d4ffdd7b 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -15,6 +15,11 @@ open Tactypes type inversion_status = Dep of constr option | NoDep +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + val inv_clause : inversion_kind -> or_and_intro_pattern option -> Id.t list -> quantified_hypothesis -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0d9f3d821..d0ec3358a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1159,6 +1159,13 @@ let tactic_infer_flags with_evar = { Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 079baa3ef..7809dbf48 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -95,6 +95,14 @@ val try_intros_until : (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg + val onInductionArg : (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> constr with_bindings destruction_arg -> unit Proofview.tactic diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index dc5a500db..88237815b 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -9,7 +9,15 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual + +# to learn about <(cmd) see https://www.gnu.org/software/bash/manual/html_node/Process-Substitution.html +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual + sort -u > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index dc5a500db..5811dd17e 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -9,7 +9,13 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual + sort -u > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/findlib-package/run.sh b/test-suite/coq-makefile/findlib-package/run.sh index 5b24df639..5cab400cc 100755 --- a/test-suite/coq-makefile/findlib-package/run.sh +++ b/test-suite/coq-makefile/findlib-package/run.sh @@ -7,7 +7,8 @@ export OCAMLPATH=$OCAMLPATH:$PWD/findlib if which cygpath 2>/dev/null; then # the only way I found to pass OCAMLPATH on win is to have it contain # only one entry - export OCAMLPATH=`cygpath -w $PWD/findlib` + OCAMLPATH=$(cygpath -w "$PWD"/findlib) + export OCAMLPATH fi make -C findlib/foo clean coq_makefile -f _CoqProject -o Makefile diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 03df9cf05..bbd2fc460 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -8,7 +8,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 03df9cf05..bbd2fc460 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -8,7 +8,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index d3bb53106..45bf1481d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -11,7 +11,12 @@ make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 89bafe9ad..8f9ab9a71 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,17 +1,17 @@ #!/usr/bin/env bash -NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true -if [[ `which ocamlopt` && $NATIVECOMP ]]; then +NATIVECOMP=$(grep "let no_native_compiler = false" ../../../config/coq_config.ml)||true +if [[ $(which ocamlopt) && $NATIVECOMP ]]; then . ../template/init.sh - + coq_makefile -f _CoqProject -o Makefile cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index 5433d9e92..1e2bd979b 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -9,7 +9,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index 5433d9e92..1e2bd979b 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -9,7 +9,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index 5433d9e92..1e2bd979b 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -9,7 +9,7 @@ make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib` && find .) | sort > actual +(cd "$(find tmp -name user-contrib)" && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/quick2vo/run.sh b/test-suite/coq-makefile/quick2vo/run.sh index 9e681223b..dda51dd2e 100755 --- a/test-suite/coq-makefile/quick2vo/run.sh +++ b/test-suite/coq-makefile/quick2vo/run.sh @@ -1,11 +1,11 @@ #!/usr/bin/env bash -a=`uname` +a=$(uname) . ../template/init.sh coq_makefile -f _CoqProject -o Makefile # vio2vo is broken on Windows (#6720) -if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then make quick2vo J=2 test -f theories/test.vo make validate diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index e19d168cf..2e066d30d 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -1,10 +1,11 @@ +#!/bin/sh . ../template/path-init.sh rm -rf _test mkdir _test find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';' -cd _test +cd _test || exit 1 mkdir -p src mkdir -p theories/sub diff --git a/test-suite/coq-makefile/template/path-init.sh b/test-suite/coq-makefile/template/path-init.sh index dd19ab2b1..c79b56652 100755 --- a/test-suite/coq-makefile/template/path-init.sh +++ b/test-suite/coq-makefile/template/path-init.sh @@ -1,3 +1,4 @@ +#!/bin/sh set -e set -o pipefail diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh index a918cceb6..9f3b648aa 100755 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/run.sh @@ -4,7 +4,8 @@ set -x set -e cd "$(dirname "${BASH_SOURCE[0]}")" -export COQLIB="$(cd ../../../.. && pwd)" +COQLIB="$(cd ../../../.. && pwd)" +export COQLIB -./001-correct-diff-sorting-order/run.sh || exit $? -./002-single-file-sorting/run.sh || exit $? +./001-correct-diff-sorting-order/run.sh +./002-single-file-sorting/run.sh diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 43c83e412..11a04d5c2 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -58,16 +58,14 @@ TO_SED_IN_PER_LINE=( -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs ) -for ext in "" .desired; do - for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed - done -done for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do - echo "cat $file" - cat "$file" - echo - diff -u $file.desired.processed $file.processed || exit $? + for ext in "" .desired; do + grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed + done + echo "cat $file" + cat "$file" + echo + diff -u $file.desired.processed $file.processed || exit $? done cd ../per-file-before @@ -92,13 +90,12 @@ echo "cat A.v.timing.diff" cat A.v.timing.diff echo +file=A.v.timing.diff + for ext in "" .desired; do - for file in A.v.timing.diff; do - cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed - done -done -for file in A.v.timing.diff; do - diff -u $file.desired.processed $file.processed || exit $? + sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed" done +diff -u "$file.desired.processed" "$file.processed" || exit $? + exit 0 diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index 5354f794f..fc95d84b9 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -11,7 +11,12 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index 5354f794f..fc95d84b9 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -11,7 +11,12 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual +( + while IFS= read -r -d '' d + do + pushd "$d" >/dev/null && find . && popd >/dev/null + done < <(find tmp -name user-contrib -print0) +) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/vio2vo/run.sh b/test-suite/coq-makefile/vio2vo/run.sh index 85656da41..e555d62f3 100755 --- a/test-suite/coq-makefile/vio2vo/run.sh +++ b/test-suite/coq-makefile/vio2vo/run.sh @@ -1,12 +1,12 @@ #!/usr/bin/env bash -a=`uname` +a=$(uname) . ../template/init.sh coq_makefile -f _CoqProject -o Makefile make quick # vio2vo is broken on Windows (#6720) -if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then make vio2vo J=2 test -f theories/test.vo make validate diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index e07612b84..a15a8fbee 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -1,3 +1,4 @@ +#!/bin/sh rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 299f49469..6bb2ba2da 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -1,17 +1,18 @@ +#!/bin/sh # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R # See bugs 2242, 2337, 2339 rm -f misc/deps/lib/*.vo misc/deps/client/*.vo -tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` -$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput -diff -u --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1 +tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX) +$coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > "$tmpoutput" +diff -u --strip-trailing-cr misc/deps/deps.out "$tmpoutput" 2>&1 R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 $coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 S=$? -if [ $R = 0 -a $S = 0 ]; then +if [ $R = 0 ] && [ $S = 0 ]; then printf "coqdep and coqtop agree\n" exit 0 else diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh index 13e264c09..acb45b229 100755 --- a/test-suite/misc/deps-utf8.sh +++ b/test-suite/misc/deps-utf8.sh @@ -1,15 +1,16 @@ +#!/bin/sh # Check reading directories matching non pure ascii idents # See bug #5715 (utf-8 working on macos X and linux) # Windows is still not compliant -a=`uname` -if [ "$a" = "Darwin" -o "$a" = "Linux" ]; then +a=$(uname) +if [ "$a" = "Darwin" ] || [ "$a" = "Linux" ]; then rm -f misc/deps/théorèmes/*.v -tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` +tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX) $coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v R=$? $coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v S=$? -if [ $R = 0 -a $S = 0 ]; then +if [ $R = 0 ] && [ $S = 0 ]; then exit 0 else exit 1 diff --git a/test-suite/misc/exitstatus.sh b/test-suite/misc/exitstatus.sh index cea1de862..a327f4248 100755 --- a/test-suite/misc/exitstatus.sh +++ b/test-suite/misc/exitstatus.sh @@ -1,7 +1,8 @@ +#!/bin/sh $coqtop -load-vernac-source misc/exitstatus/illtyped.v N=$? $coqc misc/exitstatus/illtyped.v P=$? -printf "On ill-typed input, coqtop returned $N.\n" -printf "On ill-typed input, coqc returned $P.\n" -if [ $N = 1 -a $P = 1 ]; then exit 0; else exit 1; fi +printf "On ill-typed input, coqtop returned %s.\n" "$N" +printf "On ill-typed input, coqc returned %s.\n" "$P" +if [ $N = 1 ] && [ $P = 1 ]; then exit 0; else exit 1; fi diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index 28e7dc362..ef3f056d8 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,3 +1,2 @@ -printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | egrep "Error|Unbound" -if [ $? = 0 ]; then exit 1; else exit 0; fi - +#!/bin/sh +if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh index d87a86035..ef61ca624 100755 --- a/test-suite/misc/universes.sh +++ b/test-suite/misc/universes.sh @@ -1,8 +1,9 @@ +#!/bin/sh # Sort universes for the whole standard library EXPECTED_UNIVERSES=4 # Prop is not counted $coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1 $coqc -R misc/universes Universes misc/universes/universes 2>&1 mv universes.txt misc/universes -N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l` -printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES +N=$(awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l) +printf "Found %s/%s universes\n" "$N" "$EXPECTED_UNIVERSES" if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out new file mode 100644 index 000000000..e9c28faf1 --- /dev/null +++ b/test-suite/output/Projections.out @@ -0,0 +1,2 @@ +fun S : store => S.(store_funcs) + : store -> host_func diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v new file mode 100644 index 000000000..098a518dc --- /dev/null +++ b/test-suite/output/Projections.v @@ -0,0 +1,11 @@ + +Set Printing Projections. + +Class HostFunction := host_func : Type. + +Section store. + Context `{HostFunction}. + Record store := { store_funcs : host_func }. +End store. + +Check (fun (S:@store nat) => S.(store_funcs)). diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out new file mode 100644 index 000000000..151595406 --- /dev/null +++ b/test-suite/output/ssr_clear.out @@ -0,0 +1,3 @@ +The command has indeed failed with message: +Ltac call to "move (ssrmovearg) (ssrclauses)" failed. +No assumption is named NO_SUCH_NAME diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v new file mode 100644 index 000000000..573ec47e0 --- /dev/null +++ b/test-suite/output/ssr_clear.v @@ -0,0 +1,6 @@ +Require Import ssreflect. + +Example foo : True -> True. +Proof. +Fail move=> {NO_SUCH_NAME}. +Abort. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a08cfa9f4..0dabed6b7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -315,16 +315,24 @@ let check_vio_tasks opts = (* vio files *) let schedule_vio opts = - (* We must add update the loadpath here as the scheduling process - happens outside of the STM *) - let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; - if opts.vio_checking then Vio_checking.schedule_vio_checking opts.vio_files_j opts.vio_files else Vio_checking.schedule_vio_compilation opts.vio_files_j opts.vio_files +let do_vio opts = + (* We must initialize the loadpath here as the vio scheduling + process happens outside of the STM *) + if opts.vio_files <> [] || opts.vio_tasks <> [] then + let iload_path = build_load_path opts in + List.iter Mltop.add_coq_path iload_path; + + (* Vio compile pass *) + if opts.vio_files <> [] then schedule_vio opts; + (* Vio task pass *) + if opts.vio_tasks <> [] then check_vio_tasks opts + + (******************************************************************************) (* Color Options *) (******************************************************************************) @@ -483,10 +491,9 @@ let init_toplevel arglist = end else begin try compile_files opts; - (* Vio compile pass *) - if opts.vio_files <> [] then schedule_vio opts; - (* Vio task pass *) - check_vio_tasks opts; + (* Careful this will modify the load-path and state so after + this point some stuff may not be safe anymore. *) + do_vio opts; (* Allow the user to output an arbitrary state *) outputstate opts; None, opts diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0e8ca2289..b44c7cccb 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -534,17 +534,14 @@ let vernac_assumption ~atts discharge kind l nl = if not status then Feedback.feedback Feedback.AddedAxiom let should_treat_as_cumulative cum poly = - if poly then - match cum with - | GlobalCumulativity | LocalCumulativity -> true - | GlobalNonCumulativity | LocalNonCumulativity -> false - else - match cum with - | GlobalCumulativity | GlobalNonCumulativity -> false - | LocalCumulativity -> - user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") - | LocalNonCumulativity -> - user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + match cum with + | Some VernacCumulative -> + if poly then true + else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | Some VernacNonCumulative -> + if poly then false + else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") + | None -> poly && Flags.is_polymorphic_inductive_cumulativity () let vernac_record cum k poly finite struc binders sort nameopt cfs = let is_cumulative = should_treat_as_cumulative cum poly in @@ -565,7 +562,6 @@ let vernac_record cum k poly finite struc binders sort nameopt cfs = indicates whether the type is inductive, co-inductive or neither. *) let vernac_inductive ~atts cum lo finite indl = - let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -602,6 +598,7 @@ let vernac_inductive ~atts cum lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in + let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite let vernac_fixpoint ~atts discharge l = |