diff options
Diffstat (limited to 'dev')
66 files changed, 524 insertions, 443 deletions
diff --git a/dev/base_include b/dev/base_include index e76044f415..2f7183dd63 100644 --- a/dev/base_include +++ b/dev/base_include @@ -15,7 +15,6 @@ #directory "tactics";; #directory "printing";; #directory "grammar";; -#directory "intf";; #directory "stm";; #directory "vernac";; diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index dc33838f1e..c450e8157a 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 0000000000..b016fb3891 --- /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 ccf22cc866..f960ff0087 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 16c972e80c..7e606b5544 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 cbcf14ec24..3bba451ec6 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 8e0d2341d0..18f1a2f165 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 524a55a423..93e7bd99ab 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-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 48e01e9e93..5cee72cc73 100644..100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -19,13 +19,13 @@ : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}" ######################################################################## -# Unicoq + Metacoq +# Unicoq + Mtac2 ######################################################################## : "${unicoq_CI_BRANCH:=master}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" -: "${metacoq_CI_BRANCH:=master}" -: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}" +: "${mtac2_CI_BRANCH:=master-sync}" +: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}" ######################################################################## # Mathclasses + Corn @@ -142,7 +142,7 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=8.8+alpha}" +: "${Equations_CI_BRANCH:=master}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" ######################################################################## @@ -150,3 +150,9 @@ ######################################################################## : "${Elpi_CI_BRANCH:=coq-master}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}" + +######################################################################## +# fcsl-pcm +######################################################################## +: "${fcsl_pcm_CI_BRANCH:=master}" +: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index c90e516ae9..0082919679 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 558e8cbb8c..8ce5f2418f 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 d7a356930e..189734a0bc 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 6a0ce2aefa..fbdeff20c9 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 5d6bd6a368..5d57fce1c7 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 40eff03b78..d86d61ef6a 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 54cad5df4c..9298fc70af 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 8b725f6fec..ca759c7b39 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 c44e0a6552..9c58034be1 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 62854afac6..98735b4ec4 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-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh new file mode 100755 index 0000000000..fdc4c729b6 --- /dev/null +++ b/dev/ci/ci-fcsl-pcm.sh @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +fcsl_pcm_CI_DIR="${CI_BUILD_DIR}/fcsl-pcm" + +install_ssreflect + +git_checkout "${fcsl_pcm_CI_BRANCH}" "${fcsl_pcm_CI_GITURL}" "${fcsl_pcm_CI_DIR}" + +( cd "${fcsl_pcm_CI_DIR}" && make ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 5ca3ac47fc..845addb4cd 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 lite-display ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 292331b813..35c2284050 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 ec19bd9939..8599e4d50e 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 53eb55fc45..118d151500 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 8e6448e764..bd1d88993c 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 693135a4c9..6ded97984e 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 267e13359b..1af0f634c4 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -1,41 +1,34 @@ #!/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 -# Add or update the opam repo we need for dependency resolution -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_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout ${Iris_CI_BRANCH} ${Iris_URL_PARTS[0]} ${Iris_CI_DIR} ${Iris_URL_PARTS[1]} +git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" # 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_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} +git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" # 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 820ff89eec..5981aaaae7 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 db4a31e549..4fc06e8956 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 701403f2cf..8c6b910bbb 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 deleted file mode 100755 index c813b1fe99..0000000000 --- a/dev/ci/ci-metacoq.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -source ${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} - -( 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} - -( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh new file mode 100755 index 0000000000..1372acb8e5 --- /dev/null +++ b/dev/ci/ci-mtac2.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq +mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 + +# Setup UniCoq + +git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" + +( cd "${unicoq_CI_DIR}" && coq_makefile -f Make -o Makefile && make && make install ) + +# Setup MetaCoq + +git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}" + +( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 4f7e9517f4..58bbb7229f 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 25da01a822..e77a553047 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 8ecd8c441d..31387c8ddc 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 66b56add77..62a949f59a 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 5760fbafb0..3c0044bfe9 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 7716bcb59a..e9ba114148 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 c2e3670380..0000000000 --- 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/06454-ejgallego-evar+strict_to_constr.sh b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh new file mode 100644 index 0000000000..f4cb71cf19 --- /dev/null +++ b/dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "6454" ] || [ "$CI_BRANCH" = "evar+strict_to_constr" ]; then + + # ltac2_CI_BRANCH=econstr+more_fix + # ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=evar+strict_to_constr + Equations_CI_GITURL=https://github.com/ejgallego/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 78789a6fc5..0000000000 --- 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 9677b35253..0000000000 --- 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 4b681909d6..0000000000 --- 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 8a50fb1111..0000000000 --- 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 2451657d43..0000000000 --- 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 3a3ab44e03..0000000000 --- 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 d1d61fec2e..0000000000 --- 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 8afcbf78a3..0000000000 --- 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 df3e9cef28..0000000000 --- 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 a785290e7c..0000000000 --- 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 5dedca0ca5..0000000000 --- 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 333a9e84bd..0000000000 --- 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 0000000000..cf2af9ae95 --- /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/07136-evar-map-econstr.sh b/dev/ci/user-overlays/07136-evar-map-econstr.sh new file mode 100644 index 0000000000..06aa62726d --- /dev/null +++ b/dev/ci/user-overlays/07136-evar-map-econstr.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "7136" ] || [ "$CI_BRANCH" = "evar-map-econstr" ]; then + Equations_CI_BRANCH=8.9+alpha + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git + + Elpi_CI_BRANCH=coq-7136 + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh new file mode 100644 index 0000000000..7e554684e8 --- /dev/null +++ b/dev/ci/user-overlays/07152-ejgallego-api+vernac_expr_iso.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "7152" ] || [ "$CI_BRANCH" = "api+vernac_expr_iso" ]; 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=api+vernac_expr_iso + 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 9f0377ceea..a7474e3248 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/core.dbg b/dev/core.dbg index 57c136900d..edf67020ab 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -16,5 +16,4 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer intf.cma load_printer ltac_plugin.cmo diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 71fc396088..84ff94c66a 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 ``` -$ dev/tools/merge-pr XXXX +$ git checkout master +$ git pull +$ dev/tools/merge-pr.sh 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/doc/changes.md b/dev/doc/changes.md index ab78b0956f..2bad21bb20 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,23 @@ +## Changes between Coq 8.8 and Coq 8.9 + +### ML API + +Proof engine + + More functions have been changed to use `EConstr`, notably the + functions in `Evd`, and in particular `Evd.define`. + + Note that the core function `EConstr.to_constr` now _enforces_ by + default that the resulting term is ground, that is to say, free of + Evars. This is usually what you want, as open terms should be of + type `EConstr.t` to benefit from the invariants the `EConstr` API is + meant to guarantee. + + In case you'd like to violate this API invariant, you can use the + `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note + that setting this flag to false is deprecated so it is only meant to + be used as to help port pre-EConstr code. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e56..764d482957 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md index fd3cbd1bc3..14a1cc693c 100644 --- a/dev/doc/debugging.md +++ b/dev/doc/debugging.md @@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs 7. some hints: - To debug a failure/error/anomaly, add a breakpoint in - Vernac.vernac_com at the with clause of the "try ... interp com + `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com with ..." block, then go "back" a few steps to find where the failure/error/anomaly has been raised - Alternatively, for an error or an anomaly, add breakpoints in the middle diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f3e60edea8..8f1c165dd4 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -18,7 +18,7 @@ exec $OCAMLDEBUG \ -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ - -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ + -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index e4359f7038..5205350a61 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 2f6f1af541..00d04e6b3d 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -4,11 +4,20 @@ set -e set -o pipefail API=https://api.github.com/repos/coq/coq -OFFICIAL_REMOTE_URL="git@github.com:coq/coq" +OFFICIAL_REMOTE_GIT_URL="git@github.com:coq/coq" +OFFICIAL_REMOTE_HTTPS_URL="github.com/coq/coq" -# This script depends (at least) on git and jq. +# This script depends (at least) on git (>= 2.7) and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ +# Set SLOW_CONF to have the confirmation output wait for a newline +# E.g. call $ SLOW_CONF= dev/tools/merge-pr.sh /PR number/ +if [ -z ${SLOW_CONF+x} ]; then + QUICK_CONF="-n 1" +else + QUICK_CONF="" +fi + RED="\033[31m" RESET="\033[0m" GREEN="\033[32m" @@ -32,7 +41,7 @@ fi } ask_confirmation() { - read -p "Continue anyway? [y/N] " -n 1 -r + read -p "Continue anyway? [y/N] " $QUICK_CONF -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -61,10 +70,12 @@ fi # Fetching PR metadata -TITLE=$(curl -s "$API/pulls/$PR" | jq -r '.title') +PRDATA=$(curl -s "$API/pulls/$PR") + +TITLE=$(echo "$PRDATA" | jq -r '.title') info "title for PR $PR is ${BLUE}$TITLE" -BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label') +BASE_BRANCH=$(echo "$PRDATA" | jq -r '.base.label') info "PR $PR targets branch ${BLUE}$BASE_BRANCH" CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) @@ -77,11 +88,15 @@ if [ -z "$REMOTE" ]; then error "please run: git branch --set-upstream-to=THE_REMOTE/$CURRENT_LOCAL_BRANCH" 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 +REMOTE_URL=$(git remote get-url "$REMOTE" --all) +if [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}" ] && \ + [ "$REMOTE_URL" != "${OFFICIAL_REMOTE_GIT_URL}.git" ] && \ + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}" ] && \ + [ "$REMOTE_URL" != "https://${OFFICIAL_REMOTE_HTTPS_URL}.git" ] && \ + [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}" ]] && \ + [[ "$REMOTE_URL" != "https://"*"@${OFFICIAL_REMOTE_HTTPS_URL}.git" ]] ; then error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo" - error "that is ${BLUE}$OFFICIAL_REMOTE_URL" + error "that is ${BLUE}$OFFICIAL_REMOTE_GIT_URL" error "it points to ${BLUE}$REMOTE_URL${RESET} instead" ask_confirmation fi @@ -105,19 +120,39 @@ if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then ask_confirmation fi; +# Sanity check: the local branch is up-to-date with upstream + +LOCAL_BRANCH_COMMIT=$(git rev-parse HEAD) +UPSTREAM_COMMIT=$(git rev-parse @{u}) +if [ "$LOCAL_BRANCH_COMMIT" != "$UPSTREAM_COMMIT" ]; then + + # Is it just that the upstream branch is behind? + # It could just be that we merged other PRs and we didn't push yet + + if git merge-base --is-ancestor -- "$UPSTREAM_COMMIT" "$LOCAL_BRANCH_COMMIT"; then + warning "Your branch is ahead of ${REMOTE}." + warning "You should see this warning only if you've just merged another PR and did not push yet." + ask_confirmation + else + error "Local branch is not up-to-date with ${REMOTE}." + error "Pull before merging." + ask_confirmation + fi +fi + # Sanity check: CI failed -STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') +STATUS=$(curl -s "$API/commits/$COMMIT/status") -if [ "$STATUS" != "success" ]; then - error "CI unsuccessful on ${BLUE}$(curl -s "$API/commits/$COMMIT/status" | +if [ "$(echo "$STATUS" | jq -r '.state')" != "success" ]; then + error "CI unsuccessful on ${BLUE}$(echo "$STATUS" | jq -r -c '.statuses|map(select(.state != "success"))|map(.context)')" ask_confirmation fi; # Sanity check: has labels named "needs:" -NEEDS_LABELS=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') +NEEDS_LABELS=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("needs:"))) | map(.name)') if [ "$NEEDS_LABELS" != "[]" ]; then error "needs:something labels still present: ${BLUE}$NEEDS_LABELS" ask_confirmation @@ -125,7 +160,7 @@ fi # Sanity check: has milestone -MILESTONE=$(curl -s "$API/pulls/$PR" | jq -rc '.milestone.title') +MILESTONE=$(echo "$PRDATA" | jq -rc '.milestone.title') if [ "$MILESTONE" = "null" ]; then error "no milestone set, please set one" ask_confirmation @@ -133,7 +168,7 @@ fi # Sanity check: has kind -KIND=$(curl -s "$API/pulls/$PR" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)') +KIND=$(echo "$PRDATA" | jq -rc '.labels | map(select(.name | match("kind:"))) | map(.name)') if [ "$KIND" = "[]" ]; then error "no kind:something label set, please set one" ask_confirmation diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index a514b8866a..b56925c370 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -27,8 +27,8 @@ then # reset work tree and index # NB: untracked files which were not added are untouched - git apply --cached -R "$index" - git apply -R "$tree" + git apply --whitespace=nowarn --cached -R "$index" + git apply --whitespace=nowarn -R "$tree" # Fix index # For end of file newlines we must go through the worktree @@ -45,7 +45,7 @@ then # making git fail. Don't fail now: we fix the worktree first. if [ -s "$fixed_index" ] then - git apply -R "$fixed_index" + git apply --whitespace=nowarn -R "$fixed_index" fi # Fix worktree diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ba0c54407c..8d5b5bef4a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) let ppmetas metas = pp(Termops.pr_metaset metas) -let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd) -let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd) +let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd) +let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd) let pr_existentialset evars = prlist_with_sep spc pr_evar (Evar.Set.elements evars) let ppexistentialset evars = @@ -181,7 +181,7 @@ let ppproofview p = pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma) let ppopenconstr (x : Evd.open_constr) = - let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c) + let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c) (* spiwack: deactivated until a replacement is found let pppftreestate p = pp(print_pftreestate p) *) |