From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- dev/build/windows/makecoq_mingw.sh | 84 +++++++++++++++++++++++++++----------- 1 file changed, 61 insertions(+), 23 deletions(-) (limited to 'dev/build/windows/makecoq_mingw.sh') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 86cc5f2d..070af6b4 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -159,19 +159,19 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then # Log command output - take log target name from command name (like log1 make => log target is "-make") log1() { { local -; set +x; } 2> /dev/null - "$@" >"$LOGS/$LOGTARGET-$1.log" 2>"$LOGS/$LOGTARGET-$1.err" + "$@" >"$LOGS/$LOGTARGET-$1_log.txt" 2>"$LOGS/$LOGTARGET-$1_err.txt" } # Log command output - take log target name from command name and first argument (like log2 make install => log target is "-make-install") log2() { { local -; set +x; } 2> /dev/null - "$@" >"$LOGS/$LOGTARGET-$1-$2.log" 2>"$LOGS/$LOGTARGET-$1-$2.err" + "$@" >"$LOGS/$LOGTARGET-$1-$2_log.txt" 2>"$LOGS/$LOGTARGET-$1-$2_err.txt" } # Log command output - take log target name from command name and second argument (like log_1_3 ocaml setup.ml -configure => log target is "-ocaml--configure") log_1_3() { { local -; set +x; } 2> /dev/null - "$@" >"$LOGS/$LOGTARGET-$1-$3.log" 2>"$LOGS/$LOGTARGET-$1-$3.err" + "$@" >"$LOGS/$LOGTARGET-$1-$3_log.txt" 2>"$LOGS/$LOGTARGET-$1-$3_err.txt" } # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "-untar") @@ -179,26 +179,26 @@ if [ "${COQREGTESTING:-N}" == "Y" ] ; then { local -; set +x; } 2> /dev/null LOGTARGETEX=$1 shift - "$@" >"$LOGS/$LOGTARGET-$LOGTARGETEX.log" 2>"$LOGS/$LOGTARGET-$LOGTARGETEX.err" + "$@" >"$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" 2>"$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" } 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 "-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) + "$@" > >(tee "$LOGS/$LOGTARGET-$1_log.txt" | sed -e "s/^/$LOGTARGET-$1_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1_err.txt" | sed -e "s/^/$LOGTARGET-$1_err.txt: /" 1>&2) } # Log command output - take log target name from command name and first argument (like log2 make install => log target is "-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) + "$@" > >(tee "$LOGS/$LOGTARGET-$1-$2_log.txt" | sed -e "s/^/$LOGTARGET-$1-$2_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$2_err.txt" | sed -e "s/^/$LOGTARGET-$1-$2_err.txt: /" 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 "-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) + "$@" > >(tee "$LOGS/$LOGTARGET-$1-$3_log.txt" | sed -e "s/^/$LOGTARGET-$1-$3_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-$1-$3_err.txt" | sed -e "s/^/$LOGTARGET-$1-$3_err.txt: /" 1>&2) } # Log command output - log target name is first argument (like logn untar tar xvaf ... => log target is "-untar") @@ -206,7 +206,7 @@ else { 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) + "$@" > >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_log.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_log.txt: /") 2> >(tee "$LOGS/$LOGTARGET-${LOGTARGETEX}_err.txt" | sed -e "s/^/$LOGTARGET-${LOGTARGETEX}_err.txt: /" 1>&2) } fi @@ -238,9 +238,10 @@ fi # $1 file server name including protocol prefix # $2 file name (without extension) # $3 file extension -# $4 number of path levels to strip from tar (usually 1) -# $5 module name (if different from archive) -# $6 expand folder name (if different from module name) +# $4 [optional] number of path levels to strip from tar (usually 1) +# $5 [optional] module name (if different from archive) +# $6 [optional] expand folder name (if different from module name) +# $7 [optional] module base name (used as 2nd choice for patches, defaults to $5) # ------------------------------------------------------------------------------ function get_expand_source_tar { @@ -263,6 +264,12 @@ function get_expand_source_tar { folder=$name fi + if [ "$#" -ge 7 ] ; then + basename=$7 + else + basename=$name + fi + # Set logging target logtargetold=$LOGTARGET LOGTARGET=$name @@ -314,8 +321,11 @@ function get_expand_source_tar { fi # Patch if patch file exists + # First try specific patch file name then generic patch file name if [ -f "$PATCHES/$name.patch" ] ; then log1 patch -p1 -i "$PATCHES/$name.patch" + elif [ -f "$PATCHES/$basename.patch" ] ; then + log1 patch -p1 -i "$PATCHES/$basename.patch" fi # Go back to base folder @@ -340,6 +350,7 @@ function get_expand_source_tar { # $3 file extension # $4 [optional] number of path levels to strip from tar (usually 1) # $5 [optional] module name (if different from archive) +# $6 [optional] module base name (used as 2nd choice for patches, defaults to $5) # ------------------------------------------------------------------------------ function build_prep { @@ -356,6 +367,12 @@ function build_prep { name=$2 fi + if [ "$#" -ge 6 ] ; then + basename=$6 + else + basename=$name + fi + # Set installer section to not set by default installersection= @@ -368,7 +385,7 @@ function build_prep { touch "$FLAGFILES/$name.started" - get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" + get_expand_source_tar "$1" "$2" "$3" "$strip" "$name" "$name" "$basename" cd "$name" @@ -409,7 +426,7 @@ function build_prep_overlay { # $1_CI_REF must have been a tag or hash, not a branch ver="$ref" fi - build_prep "$url" "$ver" tar.gz 1 "$1-$ver" + build_prep "$url" "$ver" tar.gz 1 "$1-$ver" "$1" } # ------------------------------------------------------------------------------ @@ -666,6 +683,17 @@ function installer_addon_end { fi } +# ------------------------------------------------------------------------------ +# Set all timeouts in all .v files to 1000 +# Since timeouts can lead to CI failures, this is useful +# +# parameters: none +# ------------------------------------------------------------------------------ + +function coq_set_timeouts_1000 { + find . -type f -name '*.v' -print0 | xargs -0 sed -i 's/timeout\s\+[0-9]\+/timeout 1000/g' +} + ###################### MODULE BUILD FUNCTIONS ##################### ##### SED ##### @@ -1343,11 +1371,10 @@ function copy_coq_license { install -D doc/LICENSE "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt" install -D LICENSE "$PREFIXCOQ/license_readme/coq/License.txt" install -D plugins/micromega/LICENSE.sos "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt" - install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true - install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true - install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true - install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true - install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" + # FIXME: this is not the micromega license + # It only applies to code that was copied into one single file! + install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" + install -D CHANGES.md "$PREFIXCOQ/license_readme/coq/Changes.md" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true fi @@ -1620,7 +1647,7 @@ function make_addon_equations { installer_addon_dependency equations if build_prep_overlay Equations; then installer_addon_section equations "Equations" "Coq plugin for defining functions by equations" "" - # Note: PATH is autmatically saved/restored by build_prep / build_post + # Note: PATH is automatically saved/restored by build_prep / build_post PATH=$COQBIN:$PATH logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile log1 make @@ -1668,7 +1695,7 @@ function make_addon_ssreflect { function make_addon_ltac2 { installer_addon_dependency ltac2 if build_prep_overlay ltac2; then - installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactics language" "" + installer_addon_section ltac2 "Ltac-2" "Coq plugin with the Ltac-2 enhanced tactic language" "" log1 make all log2 make install build_post @@ -1680,6 +1707,7 @@ function make_addon_ltac2 { function make_addon_unicoq { installer_addon_dependency unicoq if build_prep_overlay unicoq; then + installer_addon_section unicoq "Unicoq" "Coq plugin for an enhanced unification algorithm" "" log1 coq_makefile -f Make -o Makefile log1 make log2 make install @@ -1694,6 +1722,7 @@ function make_addon_mtac2 { make_addon_unicoq installer_addon_dependency_end if build_prep_overlay mtac2; then + installer_addon_section mtac2 "Mtac-2" "Coq plugin for a typed tactic language for Coq." "" log1 coq_makefile -f _CoqProject -o Makefile log1 make log2 make install @@ -1778,8 +1807,8 @@ function install_addon_vst { install_glob "progs" '*.v' "$VSTDEST/progs/" install_glob "progs" '*.c' "$VSTDEST/progs/" install_glob "progs" '*.h' "$VSTDEST/progs/" - install_glob "veric" '*.v' "$VSTDEST/msl/" - install_glob "veric" '*.vo' "$VSTDEST/msl/" + install_glob "veric" '*.v' "$VSTDEST/veric/" + install_glob "veric" '*.vo' "$VSTDEST/veric/" # Install VST documentation files install_glob "." 'LICENSE' "$VSTDEST" @@ -1792,11 +1821,20 @@ function install_addon_vst { install_glob "." '_CoqProject-export' "$VSTDEST/progs" } +function vst_patch_compcert_refs { + find . -type f -name '*.v' -print0 | xargs -0 sed -E -i \ + -e 's/(Require\s+(Import\s+|Export\s+)*)compcert\./\1VST.compcert./g' \ + -e 's/From compcert Require/From VST.compcert Require/g' +} + function make_addon_vst { installer_addon_dependency vst if build_prep_overlay VST; then installer_addon_section vst "VST" "ATTENTION: SOME INCLUDED COMPCERT PARTS ARE NOT OPEN SOURCE! Verified Software Toolchain for verifying C code" "off" - log1 make IGNORECOQVERSION=true $MAKE_OPT + # log1 coq_set_timeouts_1000 + log1 vst_patch_compcert_refs + # The usage of the shell variable ARCH in VST collides with the usage in this shellscript + logn make env -u ARCH make IGNORECOQVERSION=true $MAKE_OPT log1 install_addon_vst build_post fi -- cgit v1.2.3