diff options
Diffstat (limited to 'dev')
54 files changed, 777 insertions, 411 deletions
diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 5af0fcff3a..61cf6bc4cc 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -247,7 +247,7 @@ IF "%~0" == "-addon" ( IF NOT "%~0" == "" ( ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW ECHO !!! Illegal parameter %~0 - ECHO Usage: + ECHO Usage: ECHO MakeCoq_MinGW CALL :PrintPars GOTO :EOF @@ -267,7 +267,6 @@ IF "%INSTALLMODE%" == "mingwincygwin" ( IF "%MAKEINSTALLER%" == "Y" ( SET INSTALLMODE=relocatable - SET INSTALLOCAML=Y ) REM ========== CONFIRM PARAMETERS ========== @@ -275,7 +274,7 @@ REM ========== CONFIRM PARAMETERS ========== CALL :PrintPars REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block IF "%COQREGTESTING%"=="Y" (GOTO DontAsk) - SET /p ANSWER=Is this correct? y/n + SET /p ANSWER="Is this correct? y/n " IF NOT "%ANSWER%"=="y" (GOTO :EOF) :DontAsk @@ -315,12 +314,13 @@ ECHO RESULT INSTALL DIR (MINGW) = %RESULT_INSTALLDIR_MFMT% ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT% REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset -SET MAKE_OPT=-j %MAKE_THREADS% +SET MAKE_OPT=-j %MAKE_THREADS% REM ========== DERIVED CYGWIN SETUP OPTIONS ========== -REM WARNING: Add a space after the = otherwise the variable will be unset -SET CYGWIN_OPT= +REM One can't set a variable to empty in DOS, but you can set it to a space this way. +REM The quotes are just there to make the space visible and to protect from "remove trailing spaces". +SET "CYGWIN_OPT= " IF "%CYGWIN_FROM_CACHE%" == "Y" ( SET CYGWIN_OPT= %CYGWIN_OPT% -L @@ -334,8 +334,6 @@ IF "%GTK_FROM_SOURCES%"=="N" ( SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0 ) -ECHO ========== INSTALL CYGWIN ========== - REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES. REM Otherwise chmod won't work and e.g. the ocaml build will fail. REM Cygwin setup does not touch the ACLs of existing folders. @@ -349,7 +347,10 @@ IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" ( IF NOT "%CYGWIN_QUIET%" == "Y" ( SET RUNSETUP=Y ) + IF "%COQREGTESTING%" == "Y" ( + ECHO "========== REMOVE EXISTING CYGWIN ==========" + DEL /S /F /Q "%CYGWIN_INSTALLDIR_WFMT%" > NUL SET RUNSETUP=Y ) @@ -359,6 +360,8 @@ IF NOT "%APPVEYOR%" == "True" ( SET EXTRAPACKAGES=-P wget,curl,git,gcc-core,gcc-g++,automake1.5 ) +ECHO "========== INSTALL CYGWIN ==========" + IF "%RUNSETUP%"=="Y" ( %SETUP% ^ --proxy "%PROXY%" ^ @@ -436,10 +439,10 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -proxy ^<internet proxy^> ECHO -cygrepo ^<cygwin download repository^> ECHO -cygcache ^<local cygwin repository/cache^> - ECHO -cyglocal ^<Y or N^> install cygwin from cache + ECHO -cyglocal ^<Y or N^> install cygwin from cache ECHO -cygquiet ^<Y or N^> install cygwin without user interaction ECHO -srccache ^<local source code repository/cache^> - ECHO -coqver ^<Coq version to install^> + ECHO -coqver ^<Coq version to install^> ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version ECHO -threads ^<1..N^> Number of make threads ECHO -addon ^<name^> Enable building selected addon (can be repeated) @@ -452,9 +455,9 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -ocaml = %INSTALLOCAML% ECHO -installer= %MAKEINSTALLER% ECHO -make = %INSTALLMAKE% - ECHO -destcyg = %DESTCYG% - ECHO -destcoq = %DESTCOQ% - ECHO -setup = %SETUP% + ECHO -destcyg = %DESTCYG% + ECHO -destcoq = %DESTCOQ% + ECHO -setup = %SETUP% ECHO -proxy = %PROXY% ECHO -cygrepo = %CYGWIN_REPOSITORY% ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT% diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index da5ac2b15c..23eb6fbc63 100644..100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -18,6 +18,8 @@ set -o nounset set -o errexit set -x +# Print current wall time as part of the xtrace +export PS4='+\t ' # Set this to 1 if all module directories shall be removed before build (no incremental make) RMDIR_BEFORE_BUILD=1 @@ -119,7 +121,11 @@ mkdir -p "$PREFIXCOQ/bin" mkdir -p "$PREFIXOCAML/bin" # This is required for building addons and plugins +# This must be CFMT (/cygdrive/c/...) otherwise coquelicot 3.0.2 configure fails. +# coquelicot uses which ${COQBIN}/coqc to check if coqc exists. This does not work with COQBIN in MFMT. export COQBIN=$RESULT_INSTALLDIR_CFMT/bin/ +# This must be MFMT (C:/) otherwise bignums 68a7a3d7e0b21985913a6c3ee12067f4c5ac4e20 fails +export COQLIB=$RESULT_INSTALLDIR_MFMT/lib/coq/ ###################### Copy Cygwin Setup Info ##################### @@ -145,27 +151,64 @@ 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() { - "$@" > >(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() { - "$@" > >(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() { - "$@" > >(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 - "$@" > >(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) -} +# For an explanation of ${COQREGTESTING:-N} search for ${parameter:-word} in +# http://pubs.opengroup.org/onlinepubs/009695399/utilities/xcu_chap02.html + +if [ "${COQREGTESTING:-N}" == "Y" ] ; then + # If COQREGTESTING, log to log files only + # Log command output - take log target name from command name (like log1 make => log target is "<module>-make") + log1() { + { local -; set +x; } 2> /dev/null + "$@" >"$LOGS/$LOGTARGET-$1.log" 2>"$LOGS/$LOGTARGET-$1.err" + } + + # Log command output - take log target name from command name and first argument (like log2 make install => log target is "<module>-make-install") + log2() { + { local -; set +x; } 2> /dev/null + "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err" + } + + # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "<module>-ocaml--configure") + log_1_3() { + { local -; set +x; } 2> /dev/null + "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err" + } + + # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "<module>-untar") + logn() { + { local -; set +x; } 2> /dev/null + LOGTARGETEX=$1 + shift + "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err" + } +else + # If COQREGTESTING, log to log files and console + # Log command output - take log target name from command name (like log1 make => log target is "<module>-make") + log1() { + { local -; set +x; } 2> /dev/null + "$@" > >(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() { + { local -; set +x; } 2> /dev/null + "$@" > >(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() { + { local -; set +x; } 2> /dev/null + "$@" > >(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() { + { local -; set +x; } 2> /dev/null + LOGTARGETEX=$1 + shift + "$@" > >(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) + } +fi ###################### 'UNFIX' SED ##################### @@ -229,7 +272,7 @@ function get_expand_source_tar { if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" ] ; then cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" "$TARBALLS" else - wget "$1/$2.$3" + wget --progress=dot:giga "$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: @@ -260,8 +303,8 @@ function get_expand_source_tar { if [ "$3" == "zip" ] ; then 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 -- */* . + # move subfolders of root folders one level up + find "$(ls)" -mindepth 1 -maxdepth 1 -exec mv -- "{}" . \; else echo "Unzip strip count not supported" return 1 @@ -314,13 +357,13 @@ function build_prep { 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) LOGTARGET=$name - touch "flagfiles/$name.started" + touch "$FLAGFILES/$name.started" get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" @@ -344,9 +387,9 @@ function build_prep { # ------------------------------------------------------------------------------ function build_post { - if [ ! -f "flagfiles/$BUILD_PACKAGE_NAME.finished" ]; then + if [ ! -f "$FLAGFILES/$BUILD_PACKAGE_NAME.finished" ]; then cd "$BUILD_OLDPWD" - touch "flagfiles/$BUILD_PACKAGE_NAME.finished" + touch "$FLAGFILES/$BUILD_PACKAGE_NAME.finished" PATH=$BUILD_OLDPATH LOGTARGET=other fi @@ -384,19 +427,17 @@ function build_conf_make_inst { # Install all files given by a glob pattern to a given folder # # parameters -# $1 glob pattern (in '') -# $2 target folder +# $1 source path +# $2 pattern (in '') +# $3 target folder # ------------------------------------------------------------------------------ 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 + SRCDIR=$(realpath -m $1) + DESTDIR=$(realpath -m $3) + ( cd "$SRCDIR" && find . -maxdepth 1 -type f -name "$2" -exec install -D -T "$SRCDIR"/{} "$DESTDIR"/{} \; ) } - # ------------------------------------------------------------------------------ # Recursively Install all files given by a glob pattern to a given folder # @@ -407,12 +448,15 @@ function install_glob { # ------------------------------------------------------------------------------ function install_rec { - ( cd "$1" && find . -type f -name "$2" -exec install -D -T "$1"/{} "$3"/{} \; ) + SRCDIR=$(realpath -m $1) + DESTDIR=$(realpath -m $3) + ( cd "$SRCDIR" && find . -type f -name "$2" -exec install -D -T "$SRCDIR"/{} "$DESTDIR"/{} \; ) } # ------------------------------------------------------------------------------ # Write a file list of the target folder # The file lists are used to create file lists for the windows installer +# Don't overwrite an existing file list # # parameters # $1 name of file list @@ -425,6 +469,19 @@ function list_files { } # ------------------------------------------------------------------------------ +# Write a file list of the target folder +# The file lists are used to create file lists for the windows installer +# Do overwrite an existing file list +# +# parameters +# $1 name of file list +# ------------------------------------------------------------------------------ + +function list_files_always { + ( cd "$PREFIXCOQ" && find . -type f | sort > /build/filelists/"$1" ) +} + +# ------------------------------------------------------------------------------ # Compute the set difference of two file lists # # parameters @@ -777,15 +834,15 @@ function make_flex_dll_link { # For this purpose hard links are better. function make_ln { - if [ ! -f flagfiles/myln.finished ] ; then - touch flagfiles/myln.started + if [ ! -f $FLAGFILES/myln.finished ] ; then + touch $FLAGFILES/myln.started mkdir -p myln ( cd myln cp $PATCHES/ln.c . "$TARGET_ARCH-gcc" -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c install -D ln.exe "$PREFIXCOQ/bin/ln.exe" ) - touch flagfiles/myln.finished + touch $FLAGFILES/myln.finished fi } @@ -793,7 +850,7 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then + if build_prep https://github.com/ocaml/ocaml/archive 4.07.0 tar.gz 1 ocaml-4.07.0 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h @@ -848,7 +905,6 @@ function make_ocaml { function make_ocaml_tools { make_findlib - # make_menhir make_camlp5 } @@ -865,7 +921,7 @@ function make_ocaml_libs { function make_num { make_ocaml # We need this commit due to windows fixed, IMHO this is better than patching v1.1. - if build_prep https://github.com/ocaml/num/archive/ 7dd5e935aaa2b902585b3b2d0e55ad9b2442fff0 zip 1 num-1.1-7d; then + if build_prep https://github.com/ocaml/num/archive 7dd5e935aaa2b902585b3b2d0e55ad9b2442fff0 zip 1 num-1.1-7d; then log2 make all # log2 make test log2 make install @@ -874,17 +930,34 @@ function make_num { fi } +##### OCAMLBUILD ##### + +function make_ocamlbuild { + make_ocaml + if build_prep https://github.com/ocaml/ocamlbuild/archive 0.12.0 tar.gz 1 ocamlbuild-0.12.0; then + log2 make configure OCAML_NATIVE=true OCAMLBUILD_PREFIX=$PREFIXOCAML OCAMLBUILD_BINDIR=$PREFIXOCAML/bin OCAMLBUILD_LIBDIR=$PREFIXOCAML/lib + log1 make + log2 make install + build_post + fi +} + ##### FINDLIB Ocaml library manager ##### function make_findlib { make_ocaml - if build_prep https://opam.ocaml.org/archives ocamlfind.1.8.0+opam tar.gz 1 ; then + make_ocamlbuild + if build_prep https://opam.ocaml.org/1.2.2/archives ocamlfind.1.8.0+opam tar.gz 1 ; then logn configure ./configure -bindir "$PREFIXOCAML\\bin" -sitelib "$PREFIXOCAML\\libocaml\\site-lib" -config "$PREFIXOCAML\\etc\\findlib.conf" # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT log2 make all log2 make opt log2 make install log2 make clean + # Add Coq install library path to ocamlfind config file + # $(ocamlfind printconf conf | tr -d '\r') is the name of the config file + # printf "%q" "$PREFIXCOQ/lib" | sed -e 's/\\/\\\\/g' is the coq lib path double escaped for sed + sed -i -e 's|path="\(.*\)"|path="\1;'$(printf "%q" "$PREFIXCOQ/lib" | sed -e 's/\\/\\\\/g')'"|' $(ocamlfind printconf conf | tr -d '\r') build_post fi } @@ -894,15 +967,11 @@ function make_findlib { function make_menhir { make_ocaml make_findlib - # if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20151112 tar.gz 1 ; then - # For Ocaml 4.02 - # if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20151012 tar.gz 1 ; then - # For Ocaml 4.01 - if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20140422 tar.gz 1 ; then + make_ocamlbuild + if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20180530 tar.gz 1 ; then # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT log2 make all PREFIX="$PREFIXOCAML" log2 make install PREFIX="$PREFIXOCAML" - mv "$PREFIXOCAML/bin/menhir" "$PREFIXOCAML/bin/menhir.exe" build_post fi } @@ -1085,13 +1154,13 @@ function copy_coq_dlls { function copy_coq_objects { # copy objects only from folders which exist in the target lib directory 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" + if [ -e "$PREFIXCOQ/lib/coq/$FOLDER" ] ; then + install_glob "$FOLDER" '*.cmxa' "$PREFIXCOQ/lib/coq/$FOLDER" + install_glob "$FOLDER" '*.cmi' "$PREFIXCOQ/lib/coq/$FOLDER" + install_glob "$FOLDER" '*.cma' "$PREFIXCOQ/lib/coq/$FOLDER" + install_glob "$FOLDER" '*.cmo' "$PREFIXCOQ/lib/coq/$FOLDER" + install_glob "$FOLDER" '*.a' "$PREFIXCOQ/lib/coq/$FOLDER" + install_glob "$FOLDER" '*.o' "$PREFIXCOQ/lib/coq/$FOLDER" fi done } @@ -1103,10 +1172,10 @@ function copq_coq_gtk { echo 'gtk-fallback-icon-theme = "Tango"' >> "$PREFIX/etc/gtk-2.0/gtkrc" if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then - install_glob "$PREFIX/etc/gtk-2.0/"'*' "$PREFIXCOQ/gtk-2.0" - 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" + install_glob "$PREFIX/etc/gtk-2.0" '*' "$PREFIXCOQ/gtk-2.0" + 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 @@ -1136,7 +1205,7 @@ function copy_coq_license { install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" - install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" + install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true fi } @@ -1175,11 +1244,11 @@ function make_coq { then if [ "$INSTALLMODE" == "relocatable" ]; then # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path - ./configure -with-doc no -prefix ./ -libdir ./lib -mandir ./man + logn configure ./configure -with-doc no -prefix ./ -libdir ./lib/coq -mandir ./man elif [ "$INSTALLMODE" == "absolute" ]; then - ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + logn configure ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib/coq" -mandir "$PREFIXCOQ/man" else - ./configure -with-doc no -prefix "$PREFIXCOQ" + logn configure ./configure -with-doc no -prefix "$PREFIXCOQ" fi # The windows resource compiler binary name is hard coded @@ -1191,21 +1260,21 @@ function make_coq { log1 make else # shellcheck disable=SC2086 - make $MAKE_OPT + log1 make $MAKE_OPT fi if [ "$INSTALLMODE" == "relocatable" ]; then - ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man" + logn reconfigure ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib/coq" -mandir "$PREFIXCOQ/man" fi - make install - copy_coq_dlls + log2 make install + log1 copy_coq_dlls if [ "$INSTALLOCAML" == "Y" ]; then copy_coq_objects fi - copq_coq_gtk - copy_coq_license + log1 copq_coq_gtk + log1 copy_coq_license # make clean seems to be broken for 8.5pl2 # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile @@ -1213,8 +1282,8 @@ function make_coq { # make clean # Copy these files somewhere the plugin builds can find them - cp dev/ci/ci-basic-overlay.sh /build/ - cp -r dev/ci/user-overlays /build/ + logn copy-basic-overlays cp dev/ci/ci-basic-overlay.sh /build/ + logn copy-user-overlays cp -r dev/ci/user-overlays /build/ build_post fi @@ -1283,8 +1352,8 @@ function make_gcc { ##### Get sources for Cygwin MinGW packages ##### function get_cygwin_mingw_sources { - if [ ! -f flagfiles/cygwin_mingw_sources.finished ] ; then - touch flagfiles/cygwin_mingw_sources.started + if [ ! -f $FLAGFILES/cygwin_mingw_sources.finished ] ; then + touch $FLAGFILES/cygwin_mingw_sources.started # Find all installed files with mingw in the name and download the corresponding source code file from cygwin # Steps: @@ -1311,7 +1380,7 @@ function get_cygwin_mingw_sources { if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" ] ; then cp "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" $TARBALLS else - wget "$CYGWIN_REPOSITORY/$SOURCE" + wget --progress=dot:giga "$CYGWIN_REPOSITORY/$SOURCE" mv "$SOURCEFILE" "$TARBALLS" # Save the source archive in the source cache if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then @@ -1322,7 +1391,7 @@ function get_cygwin_mingw_sources { done - touch flagfiles/cygwin_mingw_sources.finished + touch $FLAGFILES/cygwin_mingw_sources.finished fi } @@ -1344,7 +1413,7 @@ function make_coq_installer { 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)$' + filter_files coq_objects_plugins coq_objects '/lib/coq/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 @@ -1387,12 +1456,12 @@ function make_coq_installer { # Provides BigN, BigZ, BigQ that used to be part of Coq standard library function make_addon_bignums { - bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_BRANCH" | cut -f 1) + bignums_SHA=$(git ls-remote "$bignums_CI_GITURL" "refs/heads/$bignums_CI_REF" | cut -f 1) if [[ "$bignums_SHA" == "" ]]; then - # $bignums_CI_BRANCH must have been a tag and not a branch - bignums_SHA="$bignums_CI_BRANCH" + # $bignums_CI_REF must have been a tag / commit and not a branch + bignums_SHA="$bignums_CI_REF" fi - if build_prep "${bignums_CI_GITURL}/archive" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then + if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1405,12 +1474,12 @@ function make_addon_bignums { # A new (experimental) tactic language function make_addon_ltac2 { - ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_BRANCH" | cut -f 1) + ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1) if [[ "$ltac2_SHA" == "" ]]; then - # $ltac2_CI_BRANCH must have been a tag and not a branch - ltac2_SHA="$ltac2_CI_BRANCH" + # $ltac2_CI_REF must have been a tag / commit and not a branch + ltac2_SHA="$ltac2_CI_REF" fi - if build_prep "${ltac2_CI_GITURL}/archive" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then + if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then log1 make all log2 make install build_post @@ -1421,12 +1490,12 @@ function make_addon_ltac2 { # A function definition plugin function make_addon_equations { - Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_BRANCH" | cut -f 1) + Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1) if [[ "$Equations_SHA" == "" ]]; then - # $Equations_CI_BRANCH must have been a tag and not a branch - Equations_SHA="$Equations_CI_BRANCH" + # $Equations_CI_REF must have been a tag / commit and not a branch + Equations_SHA="$Equations_CI_REF" fi - if build_prep "${Equations_CI_GITURL}/archive" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then + if build_prep "$Equations_CI_ARCHIVEURL" "$Equations_SHA" zip 1 "Equations-$Equations_SHA"; then # Note: PATH is autmatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile @@ -1448,10 +1517,10 @@ function make_addons { export CI_BRANCH="" export CI_PULL_REQUEST="" fi - . /build/ci-basic-overlay.sh for overlay in /build/user-overlays/*.sh; do . "$overlay" done + . /build/ci-basic-overlay.sh for addon in $COQ_ADDONS; do "make_addon_$addon" @@ -1460,6 +1529,8 @@ function make_addons { ###################### TOP LEVEL BUILD ##################### +ocamlfind list || true + make_sed make_ocaml make_ocaml_tools @@ -1477,7 +1548,7 @@ list_files ocaml_coq make_addons -list_files ocaml_coq_addons +list_files_always ocaml_coq_addons if [ "$MAKEINSTALLER" == "Y" ] ; then make_coq_installer diff --git a/dev/ci/README.md b/dev/ci/README.md index 45176581cd..3a179a9431 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -75,9 +75,6 @@ We are currently running tests on the following platforms: camlp5, and with warnings as errors; it runs the test-suite and tests the 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](../tools/pre-commit) is automatically installed by @@ -139,15 +136,41 @@ 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, built only in the `build:base` job. When submitting - a documentation PR, this can help reviewers checking the rendered result. +### Artifacts + +Build artifacts from GitLab can be linked / downloaded in a systematic +way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts) +for more information. For example, to access the documentation of the +`master` branch, you can do: + +https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + +Browsing artifacts is also possible: +https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + +Above, you can replace `master` and `job` by the desired GitLab branch and job name. + +Currently available artifacts are: + +- the Coq executables and stdlib, in four copies varying in + architecture and OCaml version used to build Coq: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base + + Additionally, an experimental Dune build is provided: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev + +- the Coq documentation, built in the `doc:*` jobs. When submitting + a documentation PR, this can help reviewers checking the rendered result: + + + Coq's Reference Manual [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman + + Coq's Standard Library Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman + + Coq's ML API Documentation [master branch] + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. + The dune job also provides its own API documentation using the newer `odoc` tool: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc ### GitLab and Windows @@ -165,8 +188,7 @@ 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`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml), +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) and [`Dockerfile`](docker/bionic_coq/Dockerfile) The Docker building job reuses the uploaded image if it is available, @@ -175,6 +197,6 @@ but if you wish to save more time you can skip the job by setting 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.. +it through the web interface. See also [`docker/README.md`](docker/README.md). diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 28321d13e2..63d5541f48 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -9,124 +9,147 @@ ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_BRANCH:=master}" +: "${mathcomp_CI_REF:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" -: "${oddorder_CI_BRANCH:=master}" +: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" + +: "${oddorder_CI_REF:=master}" : "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" +: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" ######################################################################## # UniMath ######################################################################## -: "${UniMath_CI_BRANCH:=master}" +: "${UniMath_CI_REF:=master}" : "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath}" +: "${UniMath_CI_ARCHIVEURL:=${UniMath_CI_GITURL}/archive}" ######################################################################## # Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_BRANCH:=master}" +: "${unicoq_CI_REF:=master}" : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" +: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" -: "${mtac2_CI_BRANCH:=master-sync}" +: "${mtac2_CI_REF:=master-sync}" : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" +: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" ######################################################################## # Mathclasses + Corn ######################################################################## -: "${math_classes_CI_BRANCH:=master}" -: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes}" +: "${math_classes_CI_REF:=master}" +: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" +: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" -: "${Corn_CI_BRANCH:=master}" -: "${Corn_CI_GITURL:=https://github.com/c-corn/corn}" +: "${Corn_CI_REF:=master}" +: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" +: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" ######################################################################## # Iris ######################################################################## -: "${stdpp_CI_BRANCH:=master}" +: "${stdpp_CI_REF:=master}" : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp}" +: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_BRANCH:=master}" +: "${Iris_CI_REF:=master}" : "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq}" +: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_BRANCH:=master}" +: "${lambdaRust_CI_REF:=master}" : "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq}" +: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" ######################################################################## # HoTT ######################################################################## -: "${HoTT_CI_BRANCH:=master}" +: "${HoTT_CI_REF:=master}" : "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" ######################################################################## # Ltac2 ######################################################################## -: "${ltac2_CI_BRANCH:=master}" +: "${ltac2_CI_REF:=master}" : "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2}" +: "${ltac2_CI_ARCHIVEURL:=${ltac2_CI_GITURL}/archive}" ######################################################################## # GeoCoq ######################################################################## -: "${GeoCoq_CI_BRANCH:=master}" +: "${GeoCoq_CI_REF:=master}" : "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" +: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" ######################################################################## # Flocq ######################################################################## -: "${Flocq_CI_BRANCH:=master}" +: "${Flocq_CI_REF:=master}" : "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" +: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" ######################################################################## # Coquelicot ######################################################################## -: "${Coquelicot_CI_BRANCH:=master}" +: "${Coquelicot_CI_REF:=master}" : "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" ######################################################################## # CompCert ######################################################################## -: "${CompCert_CI_BRANCH:=master}" +: "${CompCert_CI_REF:=master}" : "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert}" +: "${CompCert_CI_ARCHIVEURL:=${CompCert_CI_GITURL}/archive}" ######################################################################## # VST ######################################################################## -: "${VST_CI_BRANCH:=master}" +: "${VST_CI_REF:=master}" : "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" +: "${VST_CI_ARCHIVEURL:=${VST_CI_GITURL}/archive}" ######################################################################## # cross-crypto ######################################################################## -: "${cross_crypto_CI_BRANCH:=master}" +: "${cross_crypto_CI_REF:=master}" : "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" +: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" ######################################################################## # fiat_parsers ######################################################################## -: "${fiat_parsers_CI_BRANCH:=master}" +: "${fiat_parsers_CI_REF:=master}" : "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" +: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}" ######################################################################## # fiat_crypto ######################################################################## -: "${fiat_crypto_CI_BRANCH:=master}" +: "${fiat_crypto_CI_REF:=master}" : "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" +: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## # formal-topology ######################################################################## -: "${formal_topology_CI_BRANCH:=ci}" +: "${formal_topology_CI_REF:=ci}" : "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" +: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-master}" +: "${coq_dpdgraph_CI_REF:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" +: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" ######################################################################## # CoLoR ######################################################################## -: "${CoLoR_CI_BRANCH:=master}" +: "${CoLoR_CI_REF:=master}" : "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color}" +: "${CoLoR_CI_ARCHIVEURL:=${CoLoR_CI_GITURL}/archive}" ######################################################################## # SF @@ -138,53 +161,68 @@ ######################################################################## # TLC ######################################################################## -: "${tlc_CI_BRANCH:=master}" +: "${tlc_CI_REF:=master}" : "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc}" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_BRANCH:=master}" +: "${bignums_CI_REF:=master}" : "${bignums_CI_GITURL:=https://github.com/coq/bignums}" +: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_BRANCH:=master}" +: "${bedrock2_CI_REF:=master}" : "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" +: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" ######################################################################## # Equations ######################################################################## -: "${Equations_CI_BRANCH:=master}" +: "${Equations_CI_REF:=master}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" +: "${Equations_CI_ARCHIVEURL:=${Equations_CI_GITURL}/archive}" ######################################################################## # Elpi ######################################################################## -: "${Elpi_CI_BRANCH:=coq-master}" +: "${Elpi_CI_REF:=coq-master}" : "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" +: "${Elpi_CI_ARCHIVEURL:=${Elpi_CI_GITURL}/archive}" ######################################################################## # fcsl-pcm ######################################################################## -: "${fcsl_pcm_CI_BRANCH:=master}" +: "${fcsl_pcm_CI_REF:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" +: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## # pidetop ######################################################################## -: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_REF:=v8.9}" : "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" +: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" ######################################################################## # ext-lib ######################################################################## -: "${ext_lib_CI_BRANCH:=master}" +: "${ext_lib_CI_REF:=master}" : "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" +: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" + +######################################################################## +# simple-io +######################################################################## +: "${simple_io_CI_REF:=master}" +: "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" +: "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" ######################################################################## # quickchick ######################################################################## -: "${quickchick_CI_BRANCH:=master}" +: "${quickchick_CI_REF:=master}" : "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" +: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bedrock2.sh b/dev/ci/ci-bedrock2.sh index 447076e092..5205946261 100755 --- a/dev/ci/ci-bedrock2.sh +++ b/dev/ci/ci-bedrock2.sh @@ -3,9 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -bedrock2_CI_DIR="${CI_BUILD_DIR}/bedrock2" +FORCE_GIT=1 +git_download bedrock2 -git_checkout "${bedrock2_CI_BRANCH}" "${bedrock2_CI_GITURL}" "${bedrock2_CI_DIR}" -( cd "${bedrock2_CI_DIR}" && git submodule update --init --recursive ) - -( cd "${bedrock2_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/bedrock2" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index 0082919679..756f54dfbd 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -1,16 +1,8 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" -# 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 +git_download bignums -bignums_CI_DIR="${CI_BUILD_DIR}/Bignums" - -git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}" - -( cd "${bignums_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/bignums" && make && make install) diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 8ce5f2418f..dc696f69d9 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CoLoR_CI_DIR=${CI_BUILD_DIR}/color +git_download CoLoR -# Compile CoLoR -git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}" -( cd "${CoLoR_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/CoLoR" && make ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index a68cd0933e..7af648f0a6 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -20,10 +20,6 @@ else then export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST" export CI_BRANCH="$TRAVIS_BRANCH" - elif [ -n "${CIRCLECI}" ]; - then - export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" - export CI_BRANCH="$CIRCLE_BRANCH" else # assume local CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" export CI_BRANCH @@ -38,39 +34,48 @@ export COQBIN="$COQBIN/" ls "$COQBIN" -# Where we clone and build external developments +# Where we download and build external developments CI_BUILD_DIR="$PWD/_build_ci" -# shellcheck source=ci-basic-overlay.sh -. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" -mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" - -# git_checkout branch url dest will create a git repository -# in <dest> (if it does not exist already) and checkout the -# remote branch <branch> from <url> -git_checkout() +# [git_download project] will download [project] and unpack it +# in [$CI_BUILD_DIR/project] if the folder does not exist already; +# if it does, it will do nothing except print a warning (this can be +# useful when building locally). +# Note: when $FORCE_GIT is set to 1 or when $CI is unset or empty +# (local build), it uses git clone to perform the download. +git_download() { - local _BRANCH=${1} - local _URL=${2} - local _DEST=${3} - - # Allow an optional 4th argument for the commit - local _COMMIT=${4:-FETCH_HEAD} - local _DEPTH=() - if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi - - mkdir -p "${_DEST}" - ( cd "${_DEST}" && \ - if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ - echo "Checking out ${_DEST}" && \ - git fetch "${_URL}" "${_BRANCH}" && \ - git -c advice.detachedHead=false checkout "${_COMMIT}" && \ - echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) + local PROJECT=$1 + local DEST="$CI_BUILD_DIR/$PROJECT" + + if [ -d "$DEST" ]; then + echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." + elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then + local GITURL_VAR="${PROJECT}_CI_GITURL" + local GITURL="${!GITURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + git clone "$GITURL" "$DEST" + cd "$DEST" + git checkout "$REF" + else # When possible, we download tarballs to reduce bandwidth and latency + local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" + local ARCHIVEURL="${!ARCHIVEURL_VAR}" + local REF_VAR="${PROJECT}_CI_REF" + local REF="${!REF_VAR}" + mkdir -p "$DEST" + cd "$DEST" + wget "$ARCHIVEURL/$REF.tar.gz" + tar xvfz "$REF.tar.gz" --strip-components=1 + rm -f "$REF.tar.gz" + fi } make() @@ -88,31 +93,27 @@ make() # this installs just the ssreflect library of math-comp install_ssreflect() { - echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + echo 'Installing ssreflect' - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + git_download mathcomp - ( cd "${mathcomp_CI_DIR}/mathcomp" && \ + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ make Makefile.coq && \ make -f Makefile.coq ssreflect/all_ssreflect.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssr.install\\r' - } # this installs just the ssreflect + algebra library of math-comp install_ssralg() { - echo 'Installing ssralg' && echo -en 'travis_fold:start:ssralg.install\\r' + echo 'Installing ssralg' - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + git_download mathcomp - ( cd "${mathcomp_CI_DIR}/mathcomp" && \ + ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && \ make Makefile.coq && \ make -f Makefile.coq algebra/all_algebra.vo && \ make -f Makefile.coq install ) - echo -en 'travis_fold:end:ssralg.install\\r' - } diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 8d490591b6..01c35ceb4a 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" +git_download CompCert -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 "${CI_BUILD_DIR}/CompCert" && \ + ./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 5d57fce1c7..2373ea6c62 100755 --- a/dev/ci/ci-coq-dpdgraph.sh +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph" +git_download coq_dpdgraph -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 "${CI_BUILD_DIR}/coq_dpdgraph" && autoconf && ./configure && make && make test-suite ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index d86d61ef6a..5d8817491d 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -3,10 +3,9 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot" - install_ssreflect -git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}" +FORCE_GIT=1 +git_download Coquelicot -( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 9298fc70af..7d5d70cf90 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Corn_CI_DIR="${CI_BUILD_DIR}/corn" +git_download Corn -git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}" - -( cd "${Corn_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/Corn" && make && make install ) diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross-crypto.sh index a0d3aa6551..900d12c1dd 100755 --- a/dev/ci/ci-cross-crypto.sh +++ b/dev/ci/ci-cross-crypto.sh @@ -3,9 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -cross_crypto_CI_DIR="${CI_BUILD_DIR}/cross-crypto" +FORCE_GIT=1 +git_download 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 ) +( cd "${CI_BUILD_DIR}/cross_crypto" && git submodule update --init --recursive && make ) diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index 9c58034be1..9b4a06fd5b 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Elpi_CI_DIR="${CI_BUILD_DIR}/elpi" +git_download Elpi -git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}" - -( cd "${Elpi_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/Elpi" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 98735b4ec4..998d50faa7 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Equations_CI_DIR="${CI_BUILD_DIR}/Equations" +git_download Equations -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 "${CI_BUILD_DIR}/Equations" && 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 index cf212c2fb5..5eb167d97d 100755 --- a/dev/ci/ci-ext-lib.sh +++ b/dev/ci/ci-ext-lib.sh @@ -1,16 +1,8 @@ #!/usr/bin/env bash ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" -# 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 +git_download ext_lib -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) +( cd "${CI_BUILD_DIR}/ext_lib" && make && make install) diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl-pcm.sh index fdc4c729b6..cb951630c8 100755 --- a/dev/ci/ci-fcsl-pcm.sh +++ b/dev/ci/ci-fcsl-pcm.sh @@ -3,10 +3,8 @@ 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}" +git_download fcsl_pcm -( cd "${fcsl_pcm_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/fcsl_pcm" && make ) diff --git a/dev/ci/ci-fiat-crypto-legacy.sh b/dev/ci/ci-fiat-crypto-legacy.sh new file mode 100755 index 0000000000..e0395754e5 --- /dev/null +++ b/dev/ci/ci-fiat-crypto-legacy.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +FORCE_GIT=1 +git_download fiat_crypto + +fiat_crypto_legacy_CI_TARGETS1="print-old-pipeline-lite old-pipeline-lite lite-display" +fiat_crypto_legacy_CI_TARGETS2="print-old-pipeline-nobigmem old-pipeline-nobigmem nonautogenerated-specific nonautogenerated-specific-display" + +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + make ${fiat_crypto_legacy_CI_TARGETS1} && make -j 1 ${fiat_crypto_legacy_CI_TARGETS2} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 48a1366aba..7e8013be9b 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -3,12 +3,12 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" +FORCE_GIT=1 +git_download fiat_crypto -git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" +# We need a larger stack size to not overflow ocamlopt+flambda when +# building the executables. +# c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 -( 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} ) +( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ + ulimit -s 32768 && make new-pipeline c-files ) diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh index 35c2284050..ac74ebf667 100755 --- a/dev/ci/ci-fiat-parsers.sh +++ b/dev/ci/ci-fiat-parsers.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat" +FORCE_GIT=1 +git_download fiat_parsers -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 "${CI_BUILD_DIR}/fiat_parsers" && make parsers parsers-examples && make fiat-core ) diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index 8599e4d50e..e87483df0a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -Flocq_CI_DIR="${CI_BUILD_DIR}/flocq" +git_download Flocq -git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}" - -( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh index 118d151500..8be5a06ed2 100755 --- a/dev/ci/ci-formal-topology.sh +++ b/dev/ci/ci-formal-topology.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology" +git_download formal_topology -git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}" - -( cd "${formal_topology_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 24cd9c4272..8c57318477 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -3,10 +3,8 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" - -git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" - install_ssralg -( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make ) +git_download GeoCoq + +( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 6ded97984e..7eeeb09372 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT +git_download HoTT -git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" - -( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index 1af0f634c4..6960a8b98a 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -3,32 +3,28 @@ ci_dir="$(dirname "$0")" . "${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" - install_ssreflect # Setup lambdaRust first -git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}" +git_download lambdaRust # Extract required version of Iris -Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +Iris_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup Iris -git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}" +git_download Iris # Extract required version of std++ -stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') +stdpp_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/') # Setup std++ -git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}" +git_download stdpp # Build std++ -( cd "${stdpp_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/stdpp" && 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 ) +# Build and validate Iris +( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) # Build lambdaRust -( cd "${lambdaRust_CI_DIR}" && make && make install ) +( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 5981aaaae7..4df22bf249 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2" +git_download ltac2 -git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}" - -( cd "${ltac2_CI_DIR}" && make && make tests && make install ) +( cd "${CI_BUILD_DIR}/ltac2" && make && make tests && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 6a064b2971..ae31a8e7f8 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes" +git_download math_classes -git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}" - -( cd "${math_classes_CI_DIR}" && ./configure.sh && make && make install ) +( cd "${CI_BUILD_DIR}/math_classes" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 20328baf2a..a74f9fa4d3 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,11 +4,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" -oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" +git_download mathcomp -git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" -git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" +( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) -( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) -( cd "${oddorder_CI_DIR}/" && make ) +git_download oddorder + +( cd "${CI_BUILD_DIR}/oddorder" && make ) diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 1372acb8e5..7075d4d7f6 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,17 +3,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq -mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2 +git_download unicoq -# Setup UniCoq +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) -git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}" +git_download mtac2 -( 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 ) +( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index 32cba0808e..1a9a26843c 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -1,12 +1,9 @@ #!/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}" +git_download pidetop # Travis / Gitlab have different filesystem layout due to use of # `-local`. We need to improve this divergence but if we use Dune this @@ -17,6 +14,6 @@ else COQLIB="$COQBIN/../" fi -( cd "${pidetop_CI_DIR}" && jbuilder build @install ) +( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install ) -echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds +echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh index fc39e2685d..08686d7ced 100755 --- a/dev/ci/ci-quickchick.sh +++ b/dev/ci/ci-quickchick.sh @@ -1,18 +1,10 @@ #!/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" +. "${ci_dir}/ci-common.sh" install_ssreflect -git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}" +git_download quickchick -( cd "${quickchick_CI_DIR}" && make && make install) +( cd "${CI_BUILD_DIR}/quickchick" && make && make install) diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple-io.sh new file mode 100755 index 0000000000..e7bcd80de7 --- /dev/null +++ b/dev/ci/ci-simple-io.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download simple_io + +( cd "${CI_BUILD_DIR}/simple_io" && make build && make install) diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh deleted file mode 100755 index e77a553047..0000000000 --- a/dev/ci/ci-template.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -Template_CI_BRANCH=master -Template_CI_GITURL=https://github.com/Template/Template -Template_CI_DIR="${CI_BUILD_DIR}/Template" - -git_checkout "${Template_CI_BRANCH}" "${Template_CI_GITURL}" "${Template_CI_DIR}" - -( cd "${Template_CI_DIR}" && make ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 31387c8ddc..a2f0bea555 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,8 +3,7 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -tlc_CI_DIR="${CI_BUILD_DIR}/tlc" +FORCE_GIT=1 +git_download tlc -git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}" - -( cd "${tlc_CI_DIR}" && make ) +( cd "${CI_BUILD_DIR}/tlc" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index aa20fe1ff0..a7644fee23 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" +git_download UniMath -git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" - -( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) +( cd "${CI_BUILD_DIR}/UniMath" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 7a097eaab4..0fec19205a 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -3,8 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -VST_CI_DIR="${CI_BUILD_DIR}/VST" +git_download VST -git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" - -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true ) +( cd "${CI_BUILD_DIR}/VST" && make IGNORECOQVERSION=true ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 1361392dc8..8d0f69626e 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-07-11-V2" +# CACHEKEY: "bionic_coq-V2018-09-24-V01" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -7,50 +7,65 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ - m4 automake autoconf time wget rsync git gcc-multilib opam \ + # Dependencies of the image, the test-suite and external projects + m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip \ + # Dependencies of lablgtk (for CoqIDE) libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-science tipa \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ - python3-setuptools python3-wheel python3-pip + # Dependencies of stdlib and sphinx doc + texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ + xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + # Dependencies of source-doc and coq-makefile + texlive-science tipa -RUN pip3 install antlr4-python3-runtime +# More dependencies of the sphinx doc +RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 + +# We need to install OPAM 2.0 manually for now. +RUN wget https://github.com/ocaml/opam/releases/download/2.0.0/opam-2.0.0-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ + OPAMJOBS="2" \ OPAMROOT=/root/.opamcache \ - OPAMROOTISOK="true" + OPAMROOTISOK="true" \ + OPAMYES="true" # Base opam is the set of base packages required by Coq ENV COMPILER="4.02.3" -RUN opam init -a -y -j $NJOBS --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam config env) && opam update - # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.0.0 ounit.2.0.8" \ - CI_OPAM="menhir.20180530 elpi.1.0.4 ocamlgraph.1.8.8" +ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8" \ + CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV CAMLP5_VER="6.14" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" -RUN opam switch -y -j $NJOBS "$COMPILER" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER $COQIDE_OPAM $CI_OPAM +# The separate `opam install ocamlfind` workarounds an OPAM repository bug in 4.02.3 +RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ + opam install ocamlfind.1.8.0 && \ + opam install $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 +RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ + opam install ocamlfind.1.8.0 && \ + opam install $BASE_OPAM camlp5.$CAMLP5_VER # EDGE switch ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ - COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" + COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ + BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0" -RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE +RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ + opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. -RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM +RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ + opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + +RUN opam clean -a -c diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 973319de68..31bd65af08 100644..100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -2,6 +2,16 @@ REM This script builds and signs the Windows packages on Gitlab +ECHO "Start Time" +TIME /T + +REM List currently used cygwin and target folders for debugging / maintenance purposes + +ECHO "Currently used cygwin folders" +DIR C:\cygwin* +ECHO "Currently used target folders" +DIR C:\coq* + if %ARCH% == 32 ( SET ARCHLONG=i686 SET CYGROOT=C:\cygwin @@ -14,11 +24,15 @@ if %ARCH% == 64 ( SET SETUP=setup-x86_64.exe ) +SET DESTCOQ=C:\coq%ARCH%_inst + +CALL :MakeUniqueFolder %CYGROOT% CYGROOT +CALL :MakeUniqueFolder %DESTCOQ% DESTCOQ + 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 @@ -29,10 +43,24 @@ 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 ltac2 equations" -make=N ^ - -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorExit + -setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit + + +ECHO "Start Artifact Creation" +TIME /T + +mkdir artifacts -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 +CALL :CopyLogFiles + +copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" artifacts || GOTO ErrorExit +REM The open source archive is only required for release builds +IF DEFINED WIN_CERTIFICATE_PATH ( + 7z a artifacts\coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit +) ELSE ( + REM In non release builds, create a dummy file + ECHO "This is not a release build - open source archive not created / uploaded" > artifacts\coq-opensource-info.txt +) REM DO NOT echo the signing command below, as this would leak secrets in the logs IF DEFINED WIN_CERTIFICATE_PATH ( @@ -43,8 +71,49 @@ IF DEFINED WIN_CERTIFICATE_PATH ( ) ) +ECHO "Finished Artifact Creation" +TIME /T + +CALL :CleanupFolders + +ECHO "Finished Cleanup" +TIME /T + GOTO :EOF +:CopyLogFiles + ECHO Copy log files for artifact upload + MKDIR artifacts\buildlogs + COPY %CYGROOT%\build\buildlogs\* artifacts\buildlogs + MKDIR artifacts\filelists + COPY %CYGROOT%\build\filelists\* artifacts\filelists + MKDIR artifacts\flagfiles + COPY %CYGROOT%\build\flagfiles\* artifacts\flagfiles + GOTO :EOF + +:CleanupFolders + ECHO "Cleaning %CYGROOT%" + DEL /S /F /Q "%CYGROOT%" > NUL + ECHO "Cleaning %DESTCOQ%" + DEL /S /F /Q "%DESTCOQ%" > NUL + GOTO :EOF + +:MakeUniqueFolder + REM Create a uniquely named folder + REM This script is safe because folder creation is atomic - either we create it or fail + REM %1 = base path or directory (_%RANDOM%_%RANDOM% is appended to this) + REM %2 = name of the variable which receives the unique folder name + SET "UNIQUENAME=%1_%RANDOM%_%RANDOM%" + MKDIR "%UNIQUENAME%" + IF ERRORLEVEL 1 GOTO :MakeUniqueFolder + SET "%2=%UNIQUENAME%" + GOTO :EOF + +:ErrorCopyLogFilesAndExit + CALL :CopyLogFiles + REM fall through + :ErrorExit + CALL :CleanupFolders 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 e6a2c4460b..d812df3ec0 100644 --- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh +++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh @@ -1,6 +1,6 @@ #!/bin/sh if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_BRANCH=ssr-merge + mathcomp_CI_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh new file mode 100644 index 0000000000..575df07425 --- /dev/null +++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=pure-sharing-flag + +if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh new file mode 100644 index 0000000000..019cb8054d --- /dev/null +++ b/dev/ci/user-overlays/07257-herbelin-master+fix-yet-another-unif-dep-in-alphabet.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7257" ] || [ "$CI_BRANCH" = "master+fix-yet-another-unif-dep-in-alphabet" ]; then + cross_crypto_CI_REF=master+fix-coq7257-ascii-sensitive-unification + cross_crypto_CI_GITURL=https://github.com/herbelin/cross-crypto +fi diff --git a/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh new file mode 100644 index 0000000000..3a6480a5a1 --- /dev/null +++ b/dev/ci/user-overlays/07288-herbelin-master+new-module-pretyping-id-management.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "7288" ] || [ "$CI_BRANCH" = "master+new-module-pretyping-id-management" ]; then + + ltac2_CI_BRANCH=master+globenv-coq-pr7288 + ltac2_CI_GITURL=https://github.com/herbelin/ltac2 + +fi diff --git a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh b/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh deleted file mode 100644 index 56c0dc3433..0000000000 --- a/dev/ci/user-overlays/07941-bollu-questionmark-into-record-for-missing-record-field-error.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/sh - -if [ "$CI_PULL_REQUEST" = "7941" ] || [ "$CI_BRANCH" = "jun-27-missing-record-field-error-message-quickfix" ]; then - Equations_CI_BRANCH=overlay-question-mark-extended-for-missing-record-field - Equations_CI_GITURL=https://github.com/bollu/Coq-Equations -fi diff --git a/dev/ci/user-overlays/08552-gares-elpi-11.sh b/dev/ci/user-overlays/08552-gares-elpi-11.sh new file mode 100644 index 0000000000..c08f44fc50 --- /dev/null +++ b/dev/ci/user-overlays/08552-gares-elpi-11.sh @@ -0,0 +1,5 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8552" ] || [ "$CI_BRANCH" = "elpi-1.1" ]; then + Elpi_CI_REF=coq-master-elpi-1.1 +fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index d38d1b06d1..68afe7ee4a 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -7,10 +7,12 @@ request to test it with the adapted version of the external project. 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`](../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. +give the name of your branch / commit using a `_CI_REF` variable and the +location of your fork using a `_CI_GITURL` variable. The `_CI_GITURL` variable should be the URL of the repository without a trailing `.git`. +If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is +necessary to redefine the `_CI_ARCHIVEURL` variable as well. Moreover, the file contains very simple logic to test the pull request number or branch name and apply it only in this case. @@ -25,7 +27,7 @@ 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_REF=ssr-merge mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh new file mode 100644 index 0000000000..76aa37d380 --- /dev/null +++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then + HoTT_CI_REF=fix-for-numeral-notations + HoTT_CI_GITURL=https://github.com/JasonGross/HoTT + HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive +fi diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index abba13428f..b0a2b04121 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -1,5 +1,3 @@ - - HISTORY: ------- @@ -35,13 +33,41 @@ HISTORY: grammar.cma (and q_constr.cmo) directly, no need for a separate subcall to make nor awkward include-failed-and-retry. - ---------------------------------------------------------------------------- +* February - September 2018 (Emilio Jesús Gallego Arias) + + Dune support added. + + The build setup is mostly vanilla for the OCaml part, however the + `.v` to `.vo` compilation relies on `coq_dune` a `coqdep` wrapper + that will generate the necessary `dune` files. + + As a developer, you should not have to deal with Dune configuration + files on a regular basis unless adding a new library or plugin. + The vanilla setup declares all the Coq libraries and binaries [we + must respect proper containment/module implementation rules as to + allow packing], and we build custom preprocessors (based on `camlp5` + and `coqpp`) that will process the `ml4`/`mlg` files. + + This suffices to build `coqtop` and `coqide`, all that remains to + handle is `.vo` compilation. + + To teach Dune about the `.vo`, we use a small utility `coq_dune`, + that will generate a `dune` file for each directory in `plugins` and + `theories`. The code is pretty straightforward and declares build + and install rules for each `.v` straight out of `coqdep`. Thus, our + build strategy looks like this: + + 1. Use `dune` to build `coqdep` and `coq_dune`. + 2. Use `coq_dune` to generate `dune` files for each directory with `.v` files. + 3. ? + 4. Profit! [Seriously, at this point Dune has all the information to build Coq] + +--------------------------------------------------------------------------- -This file documents internals of the implementation of the build -system. For what a Coq developer needs to know about the build system, -see build-system.txt . +This file documents internals of the implementation of the make-based +build system. For what a Coq developer needs to know about the build +system, see build-system.txt and build-system.dune.md . .ml4 files ---------- diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md new file mode 100644 index 0000000000..85aaf317ef --- /dev/null +++ b/dev/doc/build-system.dune.md @@ -0,0 +1,103 @@ +This file documents what a Coq developer needs to know about the +Dune-based build system. If you want to enhance the build system +itself (or are curious about its implementation details), see +build-system.dev.txt, and in particular its initial HISTORY section. + +Dune +==== + +Coq can now be built using +[Dune](https://github.com/ocaml/dune). Contrary to other systems, +Dune, doesn't use a global`makefile` but local build files named +`dune` that are later composed to form a global build. + +As a developer, Dune should take care of all OCaml-related build tasks +including library management, merlin files, and link order. You are +are not supposed to modify the `dune` files unless you are adding a +new binary, library, or plugin. + +The current Dune setup also doesn't require a call to `configure`. The +auto-generated configuration files are properly included in the +dependency graph so it will be automatically generated by Dune with +reasonable developer defaults. You can still override the defaults by +manually calling `./configure`, but note that some configure options +such as install paths are not used by Dune. + +Dune uses a separate directory `_build` to store build artifacts; it +will generate an `.install` file so artifacts in the build can be +properly installed by package managers. + +## Targets + +The default dune target is `dune build` (or `dune build @install`), +which will scan all sources in the Coq tree and then build the whole +project, creating an "install" overlay in `_build/install/default`. + +You can build some other target by doing `dune build $TARGET`. + +In order to build a single package, you can do `dune build +$PACKAGE.install`. Dune also provides targets for documentation and +testing, see below. + +## Developer shell + +You can create a developer shell with `dune utop $library`, where +`$library` can be any directory in the current workspace. For example, +`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with +the right libraries already loaded. + +Note that you must invoke the `#rectypes;;` toplevel flag in order to +use Coq libraries. The provided `.ocamlinit` file does this +automatically. + +## Compositionality, developer and release modes. + +By default [in "developer mode"], Dune will compose all the packages +present in the tree and perform a global build. That means that for +example you could drop the `ltac2` folder under `plugins` and get a +build using `ltac2`, that will use the current Coq version. + +This is very useful to develop plugins and Coq libraries as your +plugin will correctly track dependencies and rebuild incrementally as +needed. + +However, it is not always desirable to go this way. For example, the +current Coq source tree contains two packages [Coq and CoqIDE], and in +the OPAM CoqIDE package we don't want to build CoqIDE against the +local copy of Coq. For this purpose, Dune supports the `-p` option, so +`dune build -p coqide` will build CoqIDE against the system-installed +version of Coq libs. + +## Stanzas + +`dune` files contain the so-called "stanzas", that may declare: + +- libraries, +- executables, +- documentation, arbitrary blobs. + +The concrete options for each stanza can be seen in the Dune manual, +but usually the default setup will work well with the current Coq +sources. Note that declaring a library or an executable won't make it +installed by default, for that, you need to provide a "public name". + +## Workspaces and Profiles + +Dune provides support for tree workspaces so the developer can set +global options --- such as flags --- on all packages, or build Coq +with different OPAM switches simultaneously [for example to test +compatibility]; for more information, please refer to the Dune manual. + +## Documentation and test targets + +The documentation and test suite targets for Coq are still not +implemented in Dune. + +## Planned and Advanced features + +Dune supports or will support extra functionality that may result very +useful to Coq, some examples are: + +- Cross-compilation. +- Automatic Generation of OPAM files. +- Multi-directory libraries. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 1eea2443fe..4f3d793ed4 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -219,7 +219,7 @@ General deprecation Proof engine - Due to the introduction of `EConstr` in 8.7, it is not necessary to +- Due to the introduction of `EConstr` in 8.7, it is not necessary to track "goal evar normal form status" anymore, thus the type `'a Proofview.Goal.t` loses its ghost argument. This may introduce some minor incompatibilities at the typing level. Code-wise, things diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs index 6166d24b70..8d78559c0d 100644 --- a/dev/doc/critical-bugs +++ b/dev/doc/critical-bugs @@ -109,6 +109,16 @@ Universes GH issue number: none risk: unlikely to be activated by chance + component: universe polymorphism + summary: universe polymorphism can capture global universes + impacted released versions: V8.5 to V8.8 + impacted coqchk versions: V8.5 to current (NOT FIXED) + fixed in: 2385b5c1ef + found by: Gaëtan Gilbert + exploit: test-suite/misc/poly-capture-global-univs + GH issue number: #8341 + risk: unlikely to be activated by chance (requires a plugin) + Primitive projections component: primitive projections, guard condition diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index b5dd8445db..45766293c7 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -21,6 +21,58 @@ and plug into the process perf record -g -p PID +### Per-component [flame graphs](https://github.com/brendangregg/FlameGraph) + +I (Andres Erbsen) have found it useful to look at library-wide flame graphs of +coq time consumption. As the Ltac interpreter stack is reflected in the OCaml +stack, calls to the same primitive can appear on top of multiple essentially +equivalent stacks. To make the profiles more readable, one could either try to +edit the stack trace to merge "equivalent" frames, or simply look at the +aggregate profile on a component-by-component basis. Here is how to do the +second for the standard library ([example output](https://cdn.rawgit.com/andres-erbsen/b29b29cb6480dfc6a662062e4fcd0ae3/raw/304fc3fea9630c8e453929aa7920ca8a2a570d0b/stdlib_categorized_outermost.svg)). + +~~~~~ +#!/bin/bash +make -f Makefile.dune clean +make -f Makefile.dune states +perf record -F99 `# ~1GB of data` --call-graph=dwarf -- make -f Makefile.dune world +perf script --time '0%-100%' | + stackcollapse-perf.pl | + grep Coqtop__compile | + sed -rf <(cat <<'EOF' + s/;caml/;/g + s/_[0-9]*;/;/g + s/Logic_monad__fun;//g + s/_apply[0-9];//g + s/;System/@&@/ + s/;Hashcons/@&@/ + s/;Grammar/@&@/ + s/;Declaremods/@&@/ + s/;Tactics/@&@/ + s/;Pretyping/@&@/ + s/;Typeops/@&@/ + s/;Reduction/@&@/ + s/;Unification/@&@/ + s/;Evarutil/@&@/ + s/;Evd/@&@/ + s/;EConstr/@&@/ + s/;Constr/@&@/ + s/;Univ/@&@/ + s/;Ugraph/@&@/ + s/;UState/@&@/ + s/;Micromega/@&@/ + s/;Omega/@&@/ + s/;Auto/@&@/ + s/;Ltac_plugin__Tacinterp/@&@/ + s/;Ltac_plugin__Rewrite/@&@/ + s/[^@]*@;([^@]*)@/\1;\1/ + s/@//g + :a; s/;([^;]+);\1;/;\1;/g;ta +EOF + ) | + flamegraph.pl +~~~~~ + ## Memory You first need a few commits atop trunk for this to work. diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index bccd3fefb4..85bb04efe0 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -37,7 +37,7 @@ if [ -z "$GUESS_CHECKER" ]; then -I $COQTOP/plugins/funind -I $COQTOP/plugins/groebner \ -I $COQTOP/plugins/interface -I $COQTOP/plugins/micromega \ -I $COQTOP/plugins/omega -I $COQTOP/plugins/quote \ - -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ + -I $COQTOP/plugins/ring \ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex index 6b7960c92f..dd3908c25f 100644 --- a/dev/v8-syntax/syntax-v8.tex +++ b/dev/v8-syntax/syntax-v8.tex @@ -765,8 +765,6 @@ Conflicts exists between integers and constrs. %% plugins/ring \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}} \nlsep \TERM{ring}~\STAR{\tacconstr} -%% plugins/romega -\nlsep \TERM{romega} \SEPDEF \DEFNT{orient} \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$} diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index c8385da618..ea126e2756 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -2,7 +2,6 @@ open Format open Term open Constr open Names -open Cbytecodes open Cemitcodes open Vmvalues @@ -11,13 +10,13 @@ let ppripos (ri,pos) = | Reloc_annot a -> let sp,i = a.ci.ci_ind in print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> print_string ("getglob "^(Constant.to_string kn)^"\n") | Reloc_proj_name p -> - print_string ("proj "^(Constant.to_string p)^"\n") + print_string ("proj "^(Projection.Repr.to_string p)^"\n") ); print_flush () |