diff options
Diffstat (limited to 'dev')
89 files changed, 1520 insertions, 560 deletions
diff --git a/dev/base_include b/dev/base_include index e76044f415..fc38305cca 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";; @@ -190,7 +189,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;; +let parse_vernac = Pcoq.parse_string Pvernac.Vernac_.vernac_control;; let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of @@ -205,7 +204,9 @@ let e s = implicit syntax *) let constr_of_string s = - Constrintern.interp_constr (Global.env()) Evd.empty (parse_constr s);; + let env = Global.env () in + let sigma = Evd.from_env env in + Constrintern.interp_constr env sigma (parse_constr s);; (* get the body of a constant *) @@ -232,7 +233,7 @@ let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; -let go () = Coqloop.loop ~state:Option.(get !Coqloop.drop_last_doc) +let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc)) let _ = print_string 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..ecc45735f1 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 + "$@" > >(tee "$LOGS/$LOGTARGET-$1.log" | sed -e "s/^/$LOGTARGET-$1.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1.err" | sed -e "s/^/$LOGTARGET-$1.err: /" 1>&2) } +# 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 + "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2.log" | sed -e "s/^/$LOGTARGET-$1-$2.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2.err" | sed -e "s/^/$LOGTARGET-$1-$2.err: /" 1>&2) } +# 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 + "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3.log" | sed -e "s/^/$LOGTARGET-$1-$3.log: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3.err" | sed -e "s/^/$LOGTARGET-$1-$3.err: /" 1>&2) } +# 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 + "$@" > >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.log" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.log: /") 2> >(tee "$LOGS/$LOGTARGET-$LOGTARGETEX.err" | sed -e "s/^/$LOGTARGET-$LOGTARGETEX.err: /" 1>&2) } - + ###################### '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" @@ -838,7 +847,7 @@ function make_ocaml { function make_ocaml_tools { make_findlib - make_menhir + # make_menhir make_camlp5 } @@ -847,7 +856,7 @@ function make_ocaml_tools { function make_ocaml_libs { make_findlib make_lablgtk - make_stdint + # make_stdint } ##### FINDLIB Ocaml library manager ##### @@ -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,16 +949,31 @@ 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 - + + # lablgtk binary needs to be stripped - otherwise flexdll goes wild + # Fix version 1: explicit strip after failed build - this randomly fails in CI + # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html + # logn make-world-pre make world || true + # $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll + + # Fix version 2: Strip by passing linker argument rather than explicit call to strip + # See https://github.com/alainfrisch/flexdll/issues/6 + # Argument to ocamlmklib: -ldopt "-link -Wl,-s" + # -ldopt is the okamlmklib linker prefix option + # -link is the flexlink linker prefix option + # -Wl, is the gcc (linker driver) linker prefix option + # -s is the gnu linker option for stripping symbols + # These changes are included in dev/build/windows/patches_coq/lablgtk-2.18.3.patch + log2 make world + + # lablgtk does not escape FINDLIBDIR path, which can contain backslashes + sed -i "s|^FINDLIBDIR=.*|FINDLIBDIR=$PREFIXOCAML/libocaml/site-lib|" config.make + log2 make install log2 make clean build_post @@ -978,7 +1003,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 +1019,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 +1043,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 +1061,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 +1091,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 +1136,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 +1149,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 +1167,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 +1187,7 @@ function make_coq { if [ "$INSTALLOCAML" == "Y" ]; then copy_coq_objects fi - + copq_coq_gtk copy_coq_license @@ -1169,7 +1195,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 +1206,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 +1219,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 +1246,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 +1280,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 +1310,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 +1336,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 +1403,3 @@ list_files ocaml_coq_addons if [ "$MAKEINSTALLER" == "Y" ] ; then make_coq_installer fi - diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch index 0691c1fc8f..23c303135d 100644 --- a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch +++ b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch @@ -1,6 +1,12 @@ -diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure ---- lablgtk-2.18.3/configure 2014-10-29 08:51:05.000000000 +0100 -+++ lablgtk-2.18.3.patched/configure 2015-10-29 08:58:08.543985500 +0100 +diff/patch file created on Wed, Apr 25, 2018 11:08:05 AM with: +difftar-folder.sh ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz lablgtk-2.18.3 1 +TARFILE= ../coq-msoegtrop/dev/build/windows/source_cache/lablgtk-2.18.3.tar.gz +FOLDER= lablgtk-2.18.3 +TARSTRIP= 1 +TARPREFIX= lablgtk-2.18.3/ +ORIGFOLDER= lablgtk-2.18.3.orig +--- lablgtk-2.18.3.orig/configure 2014-10-29 08:51:05.000000000 +0100 ++++ lablgtk-2.18.3/configure 2018-04-25 10:58:54.454501600 +0200 @@ -2667,7 +2667,7 @@ fi @@ -10,10 +16,8 @@ diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5 $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;} OCAMLFIND=no - -diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli ---- lablgtk-2.18.3/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3.patched/src/glib.mli 2016-01-25 09:50:59.884715200 +0100 +--- lablgtk-2.18.3.orig/src/glib.mli 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/glib.mli 2018-04-25 10:58:54.493555500 +0200 @@ -75,6 +75,7 @@ type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI] type id @@ -22,10 +26,8 @@ diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli val add_watch : cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id val remove : id -> unit - -diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml ---- lablgtk-2.18.3/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3.patched/src/glib.ml 2016-01-25 09:50:59.891715900 +0100 +--- lablgtk-2.18.3.orig/src/glib.ml 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/glib.ml 2018-04-25 10:58:54.479543500 +0200 @@ -72,6 +72,8 @@ type id external channel_of_descr : Unix.file_descr -> channel @@ -35,10 +37,22 @@ diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml external remove : id -> unit = "ml_g_source_remove" external add_watch : cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id - -diff -u -r lablgtk-2.18.3/src/ml_glib.c lablgtk-2.18.3.patched/src/ml_glib.c ---- lablgtk-2.18.3/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 -+++ lablgtk-2.18.3.patched/src/ml_glib.c 2016-01-25 09:50:59.898716600 +0100 +--- lablgtk-2.18.3.orig/src/Makefile 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/Makefile 2018-04-25 10:58:54.506522500 +0200 +@@ -461,9 +461,9 @@ + do rm -f "$(BINDIR)"/$$f; done + + lablgtk.cma liblablgtk2$(XA): $(COBJS) $(MLOBJS) +- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) ++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) + lablgtk.cmxa: $(COBJS) $(MLOBJS:.cmo=.cmx) +- $(LIBRARIAN) -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) ++ $(LIBRARIAN) -ldopt "-link -Wl,-s" -o lablgtk -oc lablgtk2 $^ $(GTKLIBS) + lablgtk.cmxs: DYNLINKLIBS=$(GTK_LIBS) + + lablgtkgl.cma liblablgtkgl2$(XA): $(GLCOBJS) $(GLMLOBJS) +--- lablgtk-2.18.3.orig/src/ml_glib.c 2014-10-29 08:51:06.000000000 +0100 ++++ lablgtk-2.18.3/src/ml_glib.c 2018-04-25 10:58:54.539535600 +0200 @@ -25,6 +25,8 @@ #include <string.h> #include <locale.h> diff --git a/dev/checker.dbg b/dev/checker.dbg new file mode 100644 index 0000000000..b2323b6175 --- /dev/null +++ b/dev/checker.dbg @@ -0,0 +1,6 @@ +load_printer threads.cma +load_printer str.cma +load_printer clib.cma +load_printer dynlink.cma +load_printer lib.cma +load_printer check.cma diff --git a/dev/checker_db b/dev/checker_db new file mode 100644 index 0000000000..327e636c57 --- /dev/null +++ b/dev/checker_db @@ -0,0 +1,39 @@ +source checker.dbg + +load_printer checker_printers.cmo + +install_printer Checker_printers.pP + +install_printer Checker_printers.ppfuture + +install_printer Checker_printers.ppid +install_printer Checker_printers.pplab +install_printer Checker_printers.ppmbid +install_printer Checker_printers.ppdir +install_printer Checker_printers.ppmp +install_printer Checker_printers.ppcon +install_printer Checker_printers.ppproj +install_printer Checker_printers.ppkn +install_printer Checker_printers.ppmind +install_printer Checker_printers.ppind + +install_printer Checker_printers.ppbigint + +install_printer Checker_printers.ppintset +install_printer Checker_printers.ppidset + +install_printer Checker_printers.ppidmapgen + +install_printer Checker_printers.ppididmap + +install_printer Checker_printers.ppuni +install_printer Checker_printers.ppuni_level +install_printer Checker_printers.ppuniverse_set +install_printer Checker_printers.ppuniverse_instance +install_printer Checker_printers.ppauniverse_context +install_printer Checker_printers.ppuniverse_context +install_printer Checker_printers.ppconstraints +install_printer Checker_printers.ppuniverse_context_future +install_printer Checker_printers.ppuniverses + +install_printer Checker_printers.pploc diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml new file mode 100644 index 0000000000..40ae1a7b05 --- /dev/null +++ b/dev/checker_printers.ml @@ -0,0 +1,73 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open Names +open Univ + +let pp x = Pp.pp_with Format.std_formatter x + +(** Future printer *) + +let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) + +(* name printers *) +let ppid id = pp (Id.print id) +let pplab l = pp (Label.print l) +let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) +let ppdir dir = pp (DirPath.print dir) +let ppmp mp = pp(str (ModPath.debug_to_string mp)) +let ppcon con = pp(Constant.debug_print con) +let ppproj con = pp(Constant.debug_print (Projection.constant con)) +let ppkn kn = pp(str (KerName.to_string kn)) +let ppmind kn = pp(MutInd.debug_print kn) +let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) + +(* term printers *) +let ppbigint n = pp (str (Bigint.to_string n));; + +let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" +let ppintset l = pp (prset int (Int.Set.elements l)) +let ppidset l = pp (prset Id.print (Id.Set.elements l)) + +let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" + +let pridmap pr l = + let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in + prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) +let ppidmap pr l = pp (pridmap pr l) + +let pridmapgen l = + let dom = Id.Set.elements (Id.Map.domain l) in + if dom = [] then str "[]" else + str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]" +let ppidmapgen l = pp (pridmapgen l) + +let prididmap = pridmap (fun _ -> Id.print) +let ppididmap = ppidmap (fun _ -> Id.print) + +let pP s = pp (hov 0 s) + +(* proof printers *) +let ppuni u = pp(Universe.pr u) +let ppuni_level u = pp (Level.pr u) + +let ppuniverse_set l = pp (LSet.pr l) +let ppuniverse_instance l = pp (Instance.pr l) +let ppauniverse_context l = pp (AUContext.pr Level.pr l) +let ppuniverse_context l = pp (pr_universe_context Level.pr l) +let ppconstraints c = pp (pr_constraints Level.pr c) +let ppuniverse_context_future c = + let ctx = Future.force c in + ppuniverse_context ctx +let ppuniverses u = pp (Univ.pr_universes u) + +let pploc x = let (l,r) = Loc.unloc x in + print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli new file mode 100644 index 0000000000..2f9500c5c3 --- /dev/null +++ b/dev/checker_printers.mli @@ -0,0 +1,54 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Printers for the ocaml toplevel. *) + +val pp : Pp.t -> unit +val pP : Pp.t -> unit (* with surrounding box *) + +val ppfuture : 'a Future.computation -> unit + +val ppid : Names.Id.t -> unit +val pplab : Names.Label.t -> unit +val ppmbid : Names.MBId.t -> unit +val ppdir : Names.DirPath.t -> unit +val ppmp : Names.ModPath.t -> unit +val ppcon : Names.Constant.t -> unit +val ppproj : Names.Projection.t -> unit +val ppkn : Names.KerName.t -> unit +val ppmind : Names.MutInd.t -> unit +val ppind : Names.inductive -> unit + +val ppbigint : Bigint.bigint -> unit + +val ppintset : Int.Set.t -> unit +val ppidset : Names.Id.Set.t -> unit + +val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t +val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit + +val pridmapgen : 'a Names.Id.Map.t -> Pp.t +val ppidmapgen : 'a Names.Id.Map.t -> unit + +val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t +val ppididmap : Names.Id.t Names.Id.Map.t -> unit + +(* Universes *) +val ppuni : Univ.Universe.t -> unit +val ppuni_level : Univ.Level.t -> unit (* raw *) +val ppuniverse_set : Univ.LSet.t -> unit +val ppuniverse_instance : Univ.Instance.t -> unit +val ppauniverse_context : Univ.AUContext.t -> unit +val ppuniverse_context : Univ.UContext.t -> unit +val ppconstraints : Univ.Constraint.t -> unit +val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit +val ppuniverses : Univ.universes -> unit + +val pploc : Loc.t -> unit diff --git a/dev/ci/README.md b/dev/ci/README.md index bb13587e94..697a160ca9 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -36,9 +36,8 @@ On the condition that: - You do not push, to the branches that we test, commits that haven't been first tested to compile with the corresponding branch(es) of Coq. -- Your development compiles in less than 35 minutes with just two threads. - If this is not the case, consider adding a "lite" target that compiles just - part of it. +- You maintain a reasonable build time for your development, or you provide + a "lite" target that we can use. In case you forget to comply with these last three conditions, we would reach out to you and give you a 30-day grace period during which your development @@ -54,9 +53,10 @@ Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at set the corresponding variables in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding target to [`Makefile.ci`](/Makefile.ci); add new jobs to -[`.travis.yml`](/.travis.yml) and [`.gitlab-ci.yml`](/.gitlab-ci.yml) so that -this new target is run. **Do not hesitate to submit an incomplete pull request -if you need help to finish it.** +[`.gitlab-ci.yml`](/.gitlab-ci.yml), +[`.circleci/config.yml`](/.circleci/config.yml) and +[`.travis.yml`](/.travis.yml) so that this new target is run. **Do not +hesitate to submit an incomplete pull request if you need help to finish it.** You may also be interested in having your development tested in our performance benchmark. Currently this is done by providing an OPAM package @@ -71,62 +71,110 @@ When you submit a pull request (PR) on Coq GitHub repository, this will automatically launch a battery of CI tests. The PR will not be integrated unless these tests pass. -Currently, we have two CI platforms: +We are currently running tests on the following platforms: -- Travis is the main CI platform. It tests the compilation of Coq, of the +- GitLab CI is the main CI platform. It tests the compilation of Coq, of the documentation, and of CoqIDE on Linux with several versions of OCaml / camlp5, and with warnings as errors; it runs the test-suite and tests the - compilation of several external developments. It also tests the compilation - of Coq on OS X. + compilation of several external developments. + +- Circle CI runs tests that are redundant with GitLab CI and may be removed + eventually. + +- Travis CI is used to test the compilation of Coq and run the test-suite on + macOS. It also runs a linter that checks whitespace discipline. A + [pre-commit hook](/dev/tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline without pain. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. -You can anticipate the results of these tests prior to submitting your PR -by having them run of your fork of Coq, on GitHub or GitLab. This can be -especially helpful given that our Travis platform is often overloaded and -therefore there can be a significant delay before these tests are actually -run on your PR. To take advantage of this, simply create a Travis account -and link it to your GitHub account, or activate the pipelines on your GitLab -fork. +You can anticipate the results of most of these tests prior to submitting your +PR by running GitLab CI on your private branches. To do so follow these steps: -You can also run one CI target locally (using `make ci-somedev`). +1. Log into GitLab CI (the easiest way is to sign in with your GitHub account). +2. Click on "New Project". +3. Choose "CI / CD for external repository" then click on "GitHub". +4. Find your fork of the Coq repository and click on "Connect". +5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project). +6. You are encouraged to go to the CI / CD general settings and increase the + timeout from 1h to 2h for better reliability. -Whenever your PR breaks tested developments, you should either adapt it -so that it doesn't, or provide a branch fixing these developments (or at -least work with the author of the development / other Coq developers to -prepare these fixes). Then, add an overlay in -[`dev/ci/user-overlays`](/dev/ci/user-overlays) (see the README there) -in a separate commit in your PR. +Now everytime you push (including force-push unless you changed the default +GitLab setting) to your fork on GitHub, it will be synchronized on GitLab and +CI will be run. You will receive an e-mail with a report of the failures if +there are some. -The process to merge your PR is then to submit PRs to the external -development repositories, merge the latter first (if the fixes are -backward-compatible), drop the overlay commit and merge the PR on Coq then. +You can also run one CI target locally (using `make ci-somedev`). See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. - -Travis specific information ---------------------------- - -Travis rebuilds all of Coq's executables and stdlib for each job. Coq -is built with `./configure -local`, then used for the job's test. - - -GitLab specific information ---------------------------- - -GitLab is set up to use the "build artifact" feature to avoid -rebuilding Coq. In one job, Coq is built with `./configure -prefix -install` and `make install` is run, then the `install` directory +### Breaking changes + +When your PR breaks an external project we test in our CI, you must prepare a +patch (or ask someone to prepare a patch) to fix the project: + +1. Fork the external project, create a new branch, push a commit adapting + the project to your changes. +2. Test your pull request with your adapted version of the external project by + adding an overlay file to your pull request (cf. + [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)). +3. Fixes to external libraries (pure Coq projects) *must* be backward + compatible (i.e. they should also work with the development version of Coq, + and the latest stable version). This will allow you to open a PR on the + external project repository to have your changes merged *before* your PR on + Coq can be integrated. + + On the other hand, patches to plugins (projects linking to the Coq ML API) + can very rarely be made backward compatible and plugins we test will + generally have a dedicated branch per Coq version. + You can still open a pull request but the merging will be requested by the + developer who merges the PR on Coq. There are plans to improve this, cf. + [#6724](https://github.com/coq/coq/issues/6724). + +Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file. + +Advanced GitLab CI information +------------------------------ + +GitLab CI is set up to use the "build artifact" feature to avoid +rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci` +and `make install` is run, then the `_install_ci` directory persists to and is used by the next jobs. Artifacts can also be downloaded from the GitLab repository. Currently, available artifacts are: - the Coq executables and stdlib, in three copies varying in - architecture and Ocaml version used to build Coq. -- the Coq documentation, in two different copies varying in the OCaml - version used to build Coq + architecture and OCaml version used to build Coq. +- the Coq documentation, built only in the `build:base` job. When submitting + a documentation PR, this can help reviewers checking the rendered result. As an exception to the above, jobs testing that compilation triggers -no Ocaml warnings build Coq in parallel with other tests. +no OCaml warnings build Coq in parallel with other tests. + +### GitLab and Windows + +If your repository has access to runners tagged `windows`, setting the +secret variable `WINDOWS` to `enabled` will add jobs building Windows +versions of Coq (32bit and 64bit). + +The Windows jobs are enabled on Coq's repository, where pipelines for +pull requests run. + +### GitLab and Docker + +System and opam packages are installed in a Docker image. The image is +automatically built and uploaded to your GitLab registry, and is +loaded by subsequent jobs. + +**IMPORTANT**: When updating Coq's CI docker image, you must modify +the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`, +and `Dockerfile`. + +The Docker building job reuses the uploaded image if it is available, +but if you wish to save more time you can skip the job by setting +`SKIP_DOCKER` to `true`. + +This means you will need to change its value when the Docker image +needs to be updated. You can do so for a single pipeline by starting +it through the web interface. diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index 524a55a423..c72705c7f7 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) -opam install -y ocamlfind camlp5 -cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate +eval "$(opam config env)" +opam install -y ocamlfind camlp5 ounit +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..87d837b387 100644..100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -11,6 +11,8 @@ ######################################################################## : "${mathcomp_CI_BRANCH:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" +: "${oddorder_CI_BRANCH:=master}" +: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}" ######################################################################## # UniMath @@ -19,13 +21,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 @@ -91,6 +93,12 @@ : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}" ######################################################################## +# cross-crypto +######################################################################## +: "${cross_crypto_CI_BRANCH:=master}" +: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto.git}" + +######################################################################## # fiat_parsers ######################################################################## : "${fiat_parsers_CI_BRANCH:=master}" @@ -142,7 +150,7 @@ ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=8.8+alpha}" +: "${Equations_CI_BRANCH:=master}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" ######################################################################## @@ -150,3 +158,27 @@ ######################################################################## : "${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}" + +######################################################################## +# pidetop +######################################################################## +: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" + +######################################################################## +# ext-lib +######################################################################## +: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}" + +######################################################################## +# quickchick +######################################################################## +: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.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..5b5cbd11ae 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -8,8 +8,13 @@ export NJOBS if [ -n "${GITLAB_CI}" ]; then + export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH" export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]] + then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + fi else if [ -n "${TRAVIS}" ]; then @@ -20,8 +25,10 @@ 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 OCAMLPATH="$PWD:$OCAMLPATH" export COQBIN="$PWD/bin" fi export PATH="$COQBIN:$PATH" @@ -35,10 +42,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" @@ -66,11 +73,6 @@ git_checkout() echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } -checkout_mathcomp() -{ - git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} -} - make() { # +x: add x only if defined @@ -88,7 +90,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp "${mathcomp_CI_DIR}" + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 6a0ce2aefa..8d490591b6 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -1,11 +1,10 @@ #!/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-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh new file mode 100755 index 0000000000..a0d3aa6551 --- /dev/null +++ b/dev/ci/ci-cross-crypto.sh @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto" + +git_checkout "${cross_crypto_CI_BRANCH}" "${cross_crypto_CI_GITURL}" "${cross_crypto_CI_DIR}" +( cd "${cross_crypto_CI_DIR}" && git submodule update --init --recursive ) + +( cd "${cross_crypto_CI_DIR}" && 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-ext-lib.sh b/dev/ci/ci-ext-lib.sh new file mode 100755 index 0000000000..cf212c2fb5 --- /dev/null +++ b/dev/ci/ci-ext-lib.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}" ]; +then + . "${ci_dir}/ci-common.sh" +fi + +ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib" + +git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}" + +( cd "${ext_lib_CI_DIR}" && make && 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..48a1366aba 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -1,11 +1,14 @@ #!/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} && make lite ) +( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) + +fiat_crypto_CI_TARGETS1="printlite lite lite-display" +fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem nonautogenerated-specific nonautogenerated-specific-display" +( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS1} && make -j 1 ${fiat_crypto_CI_TARGETS2} ) 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..920272bcfb 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -1,12 +1,10 @@ #!/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} && \ - ./configure-ci.sh && \ - make ) +( cd "${GeoCoq_CI_DIR}" && ./configure.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..6a064b2971 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}" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 701403f2cf..20328baf2a 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -2,14 +2,13 @@ # $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" +oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" -checkout_mathcomp ${mathcomp_CI_DIR} +git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" +git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" -# odd_order takes too much time for travis. -( 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 ) +( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) +( cd "${oddorder_CI_DIR}/" && make ) 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-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 0000000000..32cba0808e --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" + +git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" + +# Travis / Gitlab have different filesystem layout due to use of +# `-local`. We need to improve this divergence but if we use Dune this +# "local" oddity goes away automatically so not bothering... +if [ -d "$COQBIN/../lib/coq" ]; then + COQLIB="$COQBIN/../lib/coq/" +else + COQLIB="$COQBIN/../" +fi + +( cd "${pidetop_CI_DIR}" && jbuilder build @install ) + +echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh new file mode 100755 index 0000000000..fc39e2685d --- /dev/null +++ b/dev/ci/ci-quickchick.sh @@ -0,0 +1,18 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" + +# This script could be included inside other ones +# Let's avoid to source ci-common twice in this case +if [ -z "${CI_BUILD_DIR}" ]; +then + . "${ci_dir}/ci-common.sh" +fi + +quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick" + +install_ssreflect + +git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" + +( cd "${quickchick_CI_DIR}" && make && make install) 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..aa20fe1ff0 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -1,14 +1,10 @@ #!/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} - -( cd ${UniMath_CI_DIR} && \ - sed -i.bak '/Folds/d' Makefile && \ - sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make BUILD_COQ=no ) +git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" +( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 5760fbafb0..7a097eaab4 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -1,13 +1,10 @@ #!/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 ) diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md new file mode 100644 index 0000000000..919e2a735f --- /dev/null +++ b/dev/ci/docker/README.md @@ -0,0 +1,36 @@ +## Overall Docker Setup for Coq's CI. + +This directory provides Docker images to be used by Coq's CI. The +images do support Docker autobuild on `hub.docker.com` and Gitlab's +private registry. + +Gitlab CI will build and tag a Docker by default for every job if the +`SKIP_DOCKER` variable is not set to `false`. In Coq's CI, this +variable is usually set to `false` indeed to avoid booting a useless +job. + +## Manual Building + +You can also manually build and push any image: + +- Build the image `docker build -t base:$VERSION .` + +To upload/push to your hub: + +- Create a https://hub.docker.com account. +- Login into your space `docker login --username=$USER` +- Push the image: + + `docker tag base:$VERSION $USER/base:$VERSION` + + `docker push $USER/base:$VERSION` + +## Debugging / Misc + +To open a shell inside an image do `docker run -ti --entrypoint /bin/bash <imageID>` + +Each `RUN` command creates an "layer", thus a Docker build is +incremental and it always help to put things updated more often at the +end. + +## Possible Improvements: + +- Use ARG for customizing versions, centralize variable setup; diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile new file mode 100644 index 0000000000..a1178ee2a0 --- /dev/null +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -0,0 +1,49 @@ +# CACHEKEY: "bionic_coq-V2018-05-07-V2" +# ^^ Update when modifying this file. + +FROM ubuntu:bionic +LABEL maintainer="e@x80.org" + +ENV DEBIAN_FRONTEND="noninteractive" + +RUN apt-get update -qq && apt-get install -y -qq m4 wget time gcc-multilib opam \ + libgtk2.0-dev libgtksourceview2.0-dev \ + texlive-latex-extra texlive-fonts-recommended hevea \ + python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex python3-pip + +RUN pip3 install antlr4-python3-runtime + +# Basic OPAM setup +ENV NJOBS="2" \ + OPAMROOT=/root/.opamcache \ + OPAMROOTISOK="true" + +# Base opam is the set of base packages required by Coq +ENV COMPILER="4.02.3" \ + BASE_OPAM="num ocamlfind jbuilder ounit" + +RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update + +# Setup of the base switch; CI_OPAM contains Coq's CI dependencies. +ENV CAMLP5_VER="6.14" \ + COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" \ + CI_OPAM="menhir elpi ocamlgraph" + +RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM + +# base+32bit switch +RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER + +# BE switch +ENV COMPILER_BE="4.06.1" \ + CAMLP5_VER_BE="7.05" \ + COQIDE_OPAM_BE="lablgtk.2.18.6 conf-gtksourceview.2" + +RUN opam switch -y -j $NJOBS $COMPILER_BE && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE + +# BE+flambda switch +RUN opam switch -y -j $NJOBS "${COMPILER_BE}+flambda" && eval $(opam config env) && \ + opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_BE $COQIDE_OPAM_BE $CI_OPAM diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat new file mode 100644 index 0000000000..70278e6d09 --- /dev/null +++ b/dev/ci/gitlab.bat @@ -0,0 +1,50 @@ +@ECHO OFF + +REM This script builds and signs the Windows packages on Gitlab + +if %ARCH% == 32 ( + SET ARCHLONG=i686 + SET CYGROOT=C:\cygwin + SET SETUP=setup-x86.exe +) + +if %ARCH% == 64 ( + SET ARCHLONG=x86_64 + SET CYGROOT=C:\cygwin64 + SET SETUP=setup-x86_64.exe +) + +powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/%SETUP%', '%SETUP%')" +SET CYGCACHE=%CYGROOT%\var\cache\setup +SET CI_PROJECT_DIR_MFMT=%CI_PROJECT_DIR:\=/% +SET CI_PROJECT_DIR_CFMT=%CI_PROJECT_DIR_MFMT:C:/=/cygdrive/c/% +SET DESTCOQ=C:\coq%ARCH%_inst +SET COQREGTESTING=Y +SET PATH=%PATH%;C:\Program Files\7-Zip\;C:\Program Files\Microsoft SDKs\Windows\v7.1\Bin + +if exist %CYGROOT%\build\ rd /s /q %CYGROOT%\build +if exist %DESTCOQ%\ rd /s /q %DESTCOQ% + +call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ + -arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^ + -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -addon=bignums -make=N ^ + -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit + +copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit +7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit + +REM DO NOT echo the signing command below, as this would leak secrets in the logs +IF DEFINED WIN_CERTIFICATE_PATH ( + IF DEFINED WIN_CERTIFICATE_PASSWORD ( + ECHO Signing package + @signtool sign /f %WIN_CERTIFICATE_PATH% /p %WIN_CERTIFICATE_PASSWORD% dev\nsis\*.exe + signtool verify /pa dev\nsis\*.exe + ) +) + +GOTO :EOF + +:ErrorExit + ECHO ERROR %0 failed + EXIT /b 1 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/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh new file mode 100644 index 0000000000..b22ab36302 --- /dev/null +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || \ + [ "$CI_PULL_REQUEST" = "7543" ] || [ "$CI_BRANCH" = "ide+split" ] ; then + + pidetop_CI_BRANCH=stm+top + pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.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/07196-ejgallego-tactics+push_fix_naming_out.sh b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh new file mode 100644 index 0000000000..ea9cd8ee07 --- /dev/null +++ b/dev/ci/user-overlays/07196-ejgallego-tactics+push_fix_naming_out.sh @@ -0,0 +1,21 @@ +if [ "$CI_PULL_REQUEST" = "7196" ] || [ "$CI_BRANCH" = "tactics+push_fix_naming_out" ] || [ "$CI_BRANCH" = "pr-7196" ]; then + + # Needed overlays: https://gitlab.com/coq/coq/pipelines/21244550 + # + # equations + # ltac2 + + # The below developments should instead use a backwards compatible fix. + # + # color + # iris-lambda-rust + # math-classes + # formal-topology + + ltac2_CI_BRANCH=tactics+push_fix_naming_out + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=tactics+push_fix_naming_out + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh new file mode 100644 index 0000000000..517088a247 --- /dev/null +++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then + + ltac2_CI_BRANCH=fast-constr-match-no-context + ltac2_CI_GITURL=https://github.com/ppedrot/ltac2 + +fi diff --git a/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh new file mode 100644 index 0000000000..115f29f1ee --- /dev/null +++ b/dev/ci/user-overlays/07558-ejgallego-vernac+move_parser.sh @@ -0,0 +1,14 @@ +if [ "$CI_PULL_REQUEST" = "7558" ] || [ "$CI_BRANCH" = "vernac+move_parser" ]; then + + _OVERLAY_BRANCH=vernac+move_parser + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + ltac2_CI_BRANCH="$_OVERLAY_BRANCH" + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 9f0377ceea..aec2dfe0a6 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -1,12 +1,27 @@ # Add overlays for your pull requests in this directory -An overlay is a file containing very simple logic to test whether we are currently building a specific pull request or git branch (useful so that overlays work on your own fork) and which changes some of the variables whose default can be found in [`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh). +When your pull request breaks an external project we test in our CI and you +have prepared a branch with the fix, you can add an "overlay" to your pull +request to test it with the adapted version of the external project. -The name of your overlay file should be of the form `five_digit_PR_number-GitHub_handle-branch_name.sh`. +An overlay is a file which defines where to look for the patched version so that +testing is possible. It redefines some variables from +[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh): +give the name of your branch using a `_CI_BRANCH` variable and the location of +your fork using a `_CI_GITURL` variable. + +Moreover, the file contains very simple logic to test the pull request number +or branch name and apply it only in this case. + +The name of your overlay file should start with a five-digit pull request +number, followed by a dash, anything (for instance your GitHub nickname +and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). Example: `00669-maximedenes-ssr-merge.sh` containing ``` +#!/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..972ba701e4 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -2,8 +2,8 @@ source camlp5.dbg load_printer threads.cma load_printer str.cma load_printer clib.cma -load_printer lib.cma load_printer dynlink.cma +load_printer lib.cma load_printer kernel.cma load_printer library.cma load_printer engine.cma @@ -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 3a2df6a81f..65457b63af 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -1,8 +1,8 @@ # Merging changes in Coq -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). +This document describes how patches, submitted as pull requests (PRs) on the +`master` branch, should be merged into the main repository +(https://github.com/coq/coq). ## Code owners @@ -10,8 +10,8 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the system, two owners. One is the principal maintainer of the component, the other is the secondary maintainer. -When a pull request is submitted, GitHub will automatically ask the principal -maintainer for a review. If the pull request touches several parts, all the +When a PR is submitted, GitHub will automatically ask the principal +maintainer for a review. If the PR touches several parts, all the corresponding principal maintainers will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. @@ -43,10 +43,31 @@ A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. (*) In case a component is touched in a trivial way (adding/removing one file in -a `Makefile`, etc), or by applying a systematic process (global renaming, -deprecationg propagation, etc) that has been reviewed globally, the assignee can +a `Makefile`, etc), or by applying a systematic refactoring process (global +renaming for instance) that has been reviewed globally, the assignee can say in a comment they think a review is not required and proceed with the merge. +### Breaking changes + +If the PR breaks compatibility of some external projects in CI, then fixes to +those external projects should have been prepared (cf. the relevant sub-section +in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested +with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md). + +Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file. + +If overlays are missing, ask the author to prepare them and label the PR with +the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. + +When fixes are ready, there are two cases to consider: + +- For patches that are backward compatible (best scenario), you should get the + external project maintainers to integrate them before merging the PR. +- For patches that are not backward compatible (which is often the case when + patching plugins after an update to the Coq API), you can proceed to merge + the PR and then notify the external project maintainers they can merge the + patch. + ## Merging Once all reviewers approved the PR, the assignee is expected to check that CI @@ -70,7 +91,7 @@ To merge the PR proceed in the following way ``` $ git checkout master $ git pull -$ dev/tools/merge-pr XXXX +$ dev/tools/merge-pr.sh XXXX $ git push upstream ``` where `XXXX` is the number of the PR to be merged and `upstream` is the name @@ -89,29 +110,12 @@ 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/> +installed and a GPG key being available. Here is a short documentation on +how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/. 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. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index ab78b0956f..4838dd734a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,70 @@ +## Changes between Coq 8.8 and Coq 8.9 + +### ML API + +Misctypes + +- Syntax for universe sorts and kinds has been moved from `Misctypes` + to `Glob_term`, as these are turned into kernel terms by + `Pretyping`. + +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. + +- A few type alias have been deprecated, in all cases the message + should indicate what the canonical form is. An important change is + the move of `Globnames.global_reference` to `Names.GlobRef.t`. + +ML Libraries used by Coq + +- Introduction of a "Smart" module for collecting "smart*" functions, e.g. + Array.Smart.map. +- Uniformization of some names, e.g. Array.Smart.fold_left_map instead + of Array.smartfoldmap. + +Printer.ml API + +- The mechanism in Printer that allowed dynamically overriding pr_subgoals, + pr_subgoal and pr_goal was removed to simplify the code. It was + earlierly used by PCoq. + +Source code organization + +- We have eliminated / fused some redundant modules and relocated a + few interfaces files. The `intf` folder is gone, and now for example + `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and + so on. Changes should be compatible, but in a few cases stricter + layering requirements may mean that functions have moved. In all + cases adapting is a matter of changing the module name. + +Vernacular commands + +- The implementation of vernacular commands has been refactored so it + is self-contained now, including the parsing and extension + mechanisms. This involves a couple of non-backward compatible + changes due to layering issues, where some functions have been moved + from `Pcoq` to `Pvernac` and from `Vernacexpr` to modules in + `tactics/`. In all cases adapting is a matter of changing the module + name. + +### Unit testing + + The test suite now allows writing unit tests against OCaml code in the Coq + code base. Those unit tests create a dependency on the OUnit test framework. + ## Changes between Coq 8.7 and Coq 8.8 ### Bug tracker @@ -74,6 +141,11 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +Types Alias deprecation and type relocation. + +- A few type alias have been deprecated, in all cases the message + should indicate what the canonical form is. + ### STM API The STM API has seen a general overhaul. The main change is the 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/doc/release-process.md b/dev/doc/release-process.md new file mode 100644 index 0000000000..1821a181f1 --- /dev/null +++ b/dev/doc/release-process.md @@ -0,0 +1,100 @@ +# Release process # + +## As soon as the previous version branched off master ## + +- [ ] Create a new issue to track the release process where you can copy-paste + the present checklist. +- [ ] Change the version name to the next major version and the magic numbers + (see [#7008](https://github.com/coq/coq/pull/7008/files)). +- [ ] Put the corresponding alpha tag using `git tag -s`. + The `VX.X+alpha` tag marks the first commit to be in `master` and not in the + branch of the previous version. +- [ ] Create the `X.X+beta1` milestone if it did not already exist. +- [ ] Decide the release calendar with the team (freeze date, beta date, final + release date) and put this information in the milestone (using the + description and due date fields). + +## About one month before the beta ## + +- [ ] Create the `X.X.0` milestone and set its due date. +- [ ] Send an announcement of the upcoming freeze on Coqdev and ask people to + remove from the beta milestone what they already know won't be ready on time + (possibly postponing to the `X.X.0` milestone for minor bug fixes, + infrastructure and documentation updates). +- [ ] Determine which issues should / must be fixed before the beta, add them + to the beta milestone, possibly with a + ["priority: blocker"](https://github.com/coq/coq/labels/priority%3A%20blocker) + label. Make sure that all these issues are assigned (and that the assignee + provides an ETA). +- [ ] Ping the development coordinator (**@mattam82**) to get him started on + the update to the Credits chapter of the reference manual. + See also [#7058](https://github.com/coq/coq/issues/7058). + The command to get the list of contributors for this version is + `git shortlog -s -n VX.X+alpha..master | cut -f2 | sort -k 2` + (the ordering is approximative as it will misplace people with middle names). + +## On the date of the feature freeze ## + +- [ ] Create the new version branch `vX.X` and + [protect it](https://github.com/coq/coq/settings/branches) + (activate the "Protect this branch", "Require pull request reviews before + merging" and "Restrict who can push to this branch" guards). +- [ ] Remove all remaining unmerged feature PRs from the beta milestone. +- [ ] Start a new project to track PR backporting. The proposed model is to + have a "X.X-only PRs" column for the rare PRs on the stable branch, a + "Request X.X inclusion" column for the PRs that were merged in `master` that + are to be considered for backporting, a "Waiting for CI" column to put the + PRs in the process of being backported, and "Shipped in ..." columns to put + what was backported. (The release manager is the person responsible for + merging PRs that target the version branch and backporting appropriate PRs + that are merged into `master`). + A message to **@coqbot** in the milestone description tells it to + automatically add merged PRs to the "Request X.X inclusion" column. +- [ ] Delay non-blocking issues to the appropriate milestone and ensure + blocking issues are solved. If required to solve some blocking issues, + it is possible to revert some feature PRs in the version branch only. + +## Before the beta release date ## + +- [ ] Ensure the Credits chapter has been updated. +- [ ] Ensure an empty `CompatXX.v` file has been created. +- [ ] Ensure that an appropriate version of the plugins we will distribute with + Coq has been tagged. +- [ ] Have some people test the recently auto-generated Windows and MacOS + packages. +- [ ] Change the version name from alpha to beta1 (see + [#7009](https://github.com/coq/coq/pull/7009/files)). + We generally do not update the magic numbers at this point. +- [ ] Put the `VX.X+beta1` tag using `git tag -s`. + +### These steps are the same for all releases (beta, final, patch-level) ### + +- [ ] Send an e-mail on Coqdev announcing that the tag has been put so that + package managers can start preparing package updates. +- [ ] Draft a release on GitHub. +- [ ] Get **@maximedenes** to sign the Windows and MacOS packages and + upload them on GitHub. +- [ ] Prepare a page of news on the website with the link to the GitHub release + (see [coq/www#63](https://github.com/coq/www/pull/63)). +- [ ] Upload the new version of the reference manual to the website. + *TODO: setup some continuous deployment for this.* +- [ ] Merge the website update, publish the release + and send annoucement e-mails. +- [ ] Ping **@Zimmi48** to publish a new version on Zenodo. + *TODO: automate this.* +- [ ] Close the milestone + +## At the final release time ## + +- [ ] Change the version name to X.X.0 and the magic numbers (see + [#7271](https://github.com/coq/coq/pull/7271/files)). +- [ ] Put the `VX.X.0` tag. + +Repeat the generic process documented above for all releases. + +- [ ] Switch the default version of the reference manual on the website. + +## At the patch-level release time ## + +We generally do not update the magic numbers at this point (see +[`2881a18`](https://github.com/coq/coq/commit/2881a18)). diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index f3e60edea8..2bec09de2b 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -14,11 +14,19 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH -exec $OCAMLDEBUG \ +GUESS_CHECKER= +for arg in "$@"; do + if [ "${arg##*/}" = coqchk.byte ]; then + GUESS_CHECKER=1 + fi +done + +if [ -z "$GUESS_CHECKER" ]; then + 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 \ @@ -35,3 +43,11 @@ exec $OCAMLDEBUG \ -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ -I $COQTOP/ide \ "$@" +else + exec $OCAMLDEBUG \ + -I $CAMLP5LIB -I +threads \ + -I $COQTOP \ + -I $COQTOP/config -I $COQTOP/clib \ + -I $COQTOP/lib -I $COQTOP/checker \ + "$@" +fi 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/check-owners-pr.sh b/dev/tools/check-owners-pr.sh new file mode 100755 index 0000000000..d2910279b5 --- /dev/null +++ b/dev/tools/check-owners-pr.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env sh + +usage() { + { echo "usage: $0 PR [ARGS]..." + echo "A wrapper around check-owners.sh to check owners for a PR." + echo "Assumes upstream is the canonical Coq repository." + echo "Assumes the PR is against master." + echo + echo " PR: PR number" + echo " ARGS: passed through to check-owners.sh" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi;; + "") + usage + exit 1;; +esac + +PR="$1" +shift + +# this puts both refs in the FETCH_HEAD file but git rev-parse will use the first +git fetch upstream "+refs/pull/$PR/head" master + +head=$(git rev-parse FETCH_HEAD) +base=$(git merge-base upstream/master "$head") + +git diff --name-only -z "$base" "$head" | xargs -0 dev/tools/check-owners.sh "$@" diff --git a/dev/tools/check-owners.sh b/dev/tools/check-owners.sh new file mode 100755 index 0000000000..1a97508abb --- /dev/null +++ b/dev/tools/check-owners.sh @@ -0,0 +1,138 @@ +#!/usr/bin/env bash + +# Determine CODEOWNERS of the files given in argument +# For a given commit range: +# git diff --name-only -z COMMIT1 COMMIT2 | xargs -0 dev/tools/check-owners.sh [opts] + +# NB: gitignore files will be messed up if you interrupt the script. +# You should be able to just move the .gitignore.bak files back manually. + +usage() { + { echo "usage: $0 [--show-patterns] [--owner OWNER] [FILE]..." + echo " --show-patterns: instead of printing file names print the matching patterns (more compact)" + echo " --owner: show only files/patterns owned by OWNER (use Nobody to see only non-owned files)" + } >&2 +} + +case "$1" in + "--help"|"-h") + usage + if [ $# = 1 ]; then exit 0; else exit 1; fi +esac + +if ! [ -e .github/CODEOWNERS ]; then + >&2 echo "No CODEOWNERS set up or calling from wrong directory." + exit 1 +fi + +files=() +show_patterns=false + +target_owner="" + +while [[ "$#" -gt 0 ]]; do + case "$1" in + "--show-patterns") + show_patterns=true + shift;; + "--owner") + if [[ "$#" = 1 ]]; then + >&2 echo "Missing argument to --owner" + usage + exit 1 + elif [[ "$target_owner" != "" ]]; then + >&2 echo "Only one --owner allowed" + usage + exit 1 + fi + target_owner="$2" + shift 2;; + *) + files+=("$@") + break;; + esac +done + +# CODEOWNERS uses .gitignore patterns so we want to use git to parse it +# The only available tool for that is git check-ignore +# However it provides no way to use alternate .gitignore files +# so we rename them temporarily + +find . -name .gitignore -print0 | while IFS= read -r -d '' f; do + if [ -e "$f.bak" ]; then + >&2 echo "$f.bak exists!" + exit 1 + else + mv "$f" "$f.bak" + fi +done + +# CODEOWNERS is not quite .gitignore patterns: +# after the pattern is the owner (space separated) +# git would interpret that as a big pattern containing spaces +# so we create a valid .gitignore by removing all but the first field + +while read -r pat _; do + printf '%s\n' "$pat" >> .gitignore +done < .github/CODEOWNERS + +# associative array [file => owner] +declare -A owners + +for f in "${files[@]}"; do + data=$(git check-ignore --verbose --no-index "./$f") + code=$? + + if [[ "$code" = 1 ]] || ! [[ "$data" =~ .gitignore:.* ]] ; then + # no match, or match from non tracked gitignore (eg global gitignore) + if [ "$target_owner" != "" ] && [ "$target_owner" != Nobody ] ; then + owner="" + else + owner="Nobody" + pat="$f" # no patterns for unowned files + fi + else + # data looks like [.gitignore:$line:$pattern $file] + # extract the line to look it up in CODEOWNERS + data=${data#'.gitignore:'} + line=${data%%:*} + + # NB: supports multiple owners + # Does not support secondary owners declared in comment + read -r pat fowners < <(sed "${line}q;d" .github/CODEOWNERS) + + owner="" + if [ "$target_owner" != "" ]; then + for o in $fowners; do # do not quote: multiple owners possible + if [ "$o" = "$target_owner" ]; then + owner="$o" + fi + done + else + owner="$fowners" + fi + fi + + if [ "$owner" != "" ]; then + if $show_patterns; then + owners[$pat]="$owner" + else + owners[$f]="$owner" + fi + fi +done + +for f in "${!owners[@]}"; do + printf '%s: %s\n' "$f" "${owners[$f]}" +done | sort -k 2 -k 1 # group by owner + +# restore gitignore files +rm .gitignore +find . -name .gitignore.bak -print0 | while IFS= read -r -d '' f; do + base=${f%.bak} + if [ -e "$base" ]; then + >&2 echo "$base exists!" + else + mv "$f" "$base" + fi +done diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 62fdaec802..70a9756e51 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -23,7 +23,7 @@ ;; If you load this file from a git repository, checking out an old ;; commit will make it disappear and cause errors for your Emacs -;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; startup. To ignore those errors use (require 'coqdev nil t). If you ;; check out a malicious commit Emacs startup would allow it to run ;; arbitrary code, to avoid this you can copy coqdev.el to any ;; location and adjust the load path accordingly (of course if you run @@ -103,5 +103,48 @@ Note that this function is executed before _Coqproject is read if it exists." 2 (3 . 4) (5 . 6))) (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) +(defvar bug-reference-bug-regexp) +(defvar bug-reference-url-format) +(defun coqdev-setup-bug-reference-mode () + "Setup `bug-reference-bug-regexp' and `bug-reference-url-format' for Coq. + +This does not enable `bug-reference-mode'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local bug-reference-bug-regexp "#\\(?2:[0-9]+\\)") + (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) + +(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end) + "Add LEFT and RIGHT around the BEG..END. +Leave the point after RIGHT. BEG and END default to the bounds +of the current region. Leave point OFFSET characters after the +left quote (if OFFSET is nil, leave the point after the right +quote)." + (unless beg + (if (region-active-p) + (setq beg (region-beginning) end (region-end)) + (setq beg (point) end nil))) + (save-excursion + (goto-char (or end beg)) + (insert right)) + (save-excursion + (goto-char beg) + (insert left)) + (if (and end (not offset)) ;; Second test handles the ::`` case + (goto-char (+ end (length left) (length right))) + (goto-char (+ beg (or offset (length left)))))) + +(defun coqdev-sphinx-rst-coq-action () + "Insert a Sphinx role template or quote the current region." + (interactive) + (pcase (read-char "Command [gntm:`]?") + (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`")) + (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`")) + (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`")) + (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`")) + (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1)) + (?` (coqdev-sphinx-quote-coq-refman-region "``" "``")))) + (provide 'coqdev) ;;; coqdev ends here diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index ecfdfab948..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 @@ -79,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 @@ -107,6 +120,26 @@ 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") diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index a514b8866a..ad2f2f93e7 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -14,9 +14,9 @@ then # We fix whitespace in the index and in the working tree # separately to preserve non-added changes. - index=$(mktemp "git-fix-ws-index.XXXXX") - fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXX") - tree=$(mktemp "git-fix-ws-tree.XXXXX") + index=$(mktemp "git-fix-ws-index.XXXXXX") + fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXXX") + tree=$(mktemp "git-fix-ws-tree.XXXXXX") 1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'." 1>&2 echo "If an error destroys your changes you can recover using them." 1>&2 echo "(The files are cleaned up on success.)" @@ -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..10a7a4158b 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) *) @@ -203,17 +203,17 @@ let pproof p = pp(Proof.pr_proof p) let ppuni u = pp(Universe.pr u) let ppuni_level u = pp (Level.pr u) -let prlev = Universes.pr_with_global_universes +let prlev = UnivNames.pr_with_global_universes let ppuniverse_set l = pp (LSet.pr prlev l) let ppuniverse_instance l = pp (Instance.pr prlev l) let ppuniverse_context l = pp (pr_universe_context prlev l) let ppuniverse_context_set l = pp (pr_universe_context_set prlev l) let ppuniverse_subst l = pp (Univ.pr_universe_subst l) -let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) +let ppuniverse_opt_subst l = pp (UnivSubst.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Termops.pr_evar_universe_context l) let ppconstraints c = pp (pr_constraints Level.pr c) -let ppuniverseconstraints c = pp (Universes.Constraints.pr c) +let ppuniverseconstraints c = pp (UnivProblem.Set.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx @@ -221,7 +221,9 @@ let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c) let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = - pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) + let env = Global.env () in + let sigma = Evd.from_env env in + pp (pr_named_context env sigma (named_context_of_val e)) let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ @@ -230,7 +232,7 @@ let ppenv e = pp let ppenvwithcst e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ - str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") + str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).env_globals.env_constants (mt ()) ++ str "}") let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index dad6dcc1c0..63d7d58053 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit val ppclosedglobconstridmap : Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit -val ppglobal : Globnames.global_reference -> unit +val ppglobal : Names.GlobRef.t -> unit val ppconst : Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit @@ -139,11 +139,11 @@ val ppuniverse_instance : Univ.Instance.t -> unit val ppuniverse_context : Univ.UContext.t -> unit val ppuniverse_context_set : Univ.ContextSet.t -> unit val ppuniverse_subst : Univ.universe_subst -> unit -val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit +val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit val ppuniverse_level_subst : Univ.universe_level_subst -> unit val ppevar_universe_context : UState.t -> unit val ppconstraints : Univ.Constraint.t -> unit -val ppuniverseconstraints : Universes.Constraints.t -> unit +val ppuniverseconstraints : UnivProblem.Set.t -> unit val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit val ppcumulativity_info : Univ.CumulativityInfo.t -> unit val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 2ddf927d9b..16917586f5 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -1,5 +1,6 @@ open Format open Term +open Constr open Names open Cbytecodes open Cemitcodes |