diff options
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 472 | ||||
| -rw-r--r-- | dev/build/windows/patches_coq/coq_new.nsi | 188 | ||||
| -rwxr-xr-x | dev/build/windows/patches_coq/quickchick.patch | 26 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 25 | ||||
| -rwxr-xr-x | dev/ci/gitlab.bat | 16 |
5 files changed, 636 insertions, 91 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 74dd4d41c1..fcb3d8144e 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -2,7 +2,7 @@ ###################### COPYRIGHT/COPYLEFT ###################### -# (C) 2016 Intel Deutschland GmbH +# (C) 2016..2018 Intel Deutschland GmbH # Author: Michael Soegtrop # # Released to the public by Intel under the @@ -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,15 @@ 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= + # Check if build is already done if [ ! -f "$FLAGFILES/$name.finished" ] ; then BUILD_PACKAGE_NAME=$name @@ -365,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" @@ -381,6 +401,61 @@ function build_prep { } # ------------------------------------------------------------------------------ +# Like build_prep, but gets the data from an entry in ci-basic-overlay.sh +# This assumes the following definitions exist in ci-basic-overlay.sh, +# or in a file in the user-overlays folder: +# $1_CI_REF +# $1_CI_ARCHIVEURL +# $1_CI_GITURL +# ATTENTION: variables in ci-basic-overlay.sh are loaded by load_overlay_data. +# load_overlay_data is is called at the end of make_coq (even if the build is skipped) +# +# Parameters +# $1 base name of module in ci-basic-overlay.sh, e.g. mathcomp, bignums, ... +# ------------------------------------------------------------------------------ + +function build_prep_overlay { + urlvar=$1_CI_ARCHIVEURL + gitvar=$1_CI_GITURL + refvar=$1_CI_REF + url=${!urlvar} + git=${!gitvar} + ref=${!refvar} + ver=$(git ls-remote "$git" "refs/heads/$ref" | cut -f 1) + if [[ "$ver" == "" ]]; then + # $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" "$1" +} + +# ------------------------------------------------------------------------------ +# Load overlay version variables from ci-basic-overlay.sh and user-overlays/*.sh +# ------------------------------------------------------------------------------ + +function load_overlay_data { + if [ -n "${GITLAB_CI+}" ]; then + export CI_BRANCH="$CI_COMMIT_REF_NAME" + if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then + export CI_PULL_REQUEST="${CI_BRANCH#pr-}" + else + export CI_PULL_REQUEST="" + fi + else + export CI_BRANCH="" + export CI_PULL_REQUEST="" + # Used when building 8.8.0 with the latest scripts + export TRAVIS_BRANCH="" + export TRAVIS_PULL_REQUEST="" + fi + + for overlay in /build/user-overlays/*.sh; do + . "$overlay" + done + . /build/ci-basic-overlay.sh +} + +# ------------------------------------------------------------------------------ # Finalize a module build # - create name.finished # - go back to base folder @@ -392,6 +467,7 @@ function build_post { touch "$FLAGFILES/$BUILD_PACKAGE_NAME.finished" PATH=$BUILD_OLDPATH LOGTARGET=other + installer_addon_end fi } @@ -522,6 +598,101 @@ function files_to_nsis { tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh" } +# ------------------------------------------------------------------------------ +# Create an nsis installer addon section +# +# parameters +# $1 identifier of installer section and base name of file list files +# $2 human readable name of section +# $3 description of section +# $4 flags (space separated list of keywords): off = default off +# +# $1 must be a valid NSIS identifier! +# ------------------------------------------------------------------------------ + +function installer_addon_section { + installersection=$1 + list_files "addon_pre_$installersection" + + echo 'LangString' "DESC_$1" '${LANG_ENGLISH}' "\"$3\"" >> "/build/filelists/addon_strings.nsh" + + echo '!insertmacro MUI_DESCRIPTION_TEXT' '${'"Sec_$1"'}' '$('"DESC_$1"')' >> "/build/filelists/addon_descriptions.nsh" + + local sectionoptions= + if [[ "$4" == *off* ]] ; then sectionoptions+=" /o" ; fi + + echo "Section $sectionoptions \"$2\" Sec_$1" >> "/build/filelists/addon_sections.nsh" + echo 'SetOutPath "$INSTDIR\"' >> "/build/filelists/addon_sections.nsh" + echo '!include "..\..\..\filelists\addon_'"$1"'.nsh"' >> "/build/filelists/addon_sections.nsh" + echo 'SectionEnd' >> "/build/filelists/addon_sections.nsh" +} + +# ------------------------------------------------------------------------------ +# Start an installer addon dependency group +# +# parameters +# $1 identifier of the section which depends on other sections +# The parameters must match the $1 parameter of a installer_addon_section call +# ------------------------------------------------------------------------------ + +dependencysections= + +function installer_addon_dependency_beg { + installer_addon_dependency "$1" + dependencysections="$1 $dependencysections" +} + +# ------------------------------------------------------------------------------ +# End an installer addon dependency group +# ------------------------------------------------------------------------------ + +function installer_addon_dependency_end { + set -- $dependencysections + shift + dependencysections="$*" +} + +# ------------------------------------------------------------------------------ +# Create an nsis installer addon dependency entry +# This needs to be bracketed with installer_addon_dependencies_beg/end +# +# parameters +# $1 identifier of the section on which other sections might depend +# The parameters must match the $1 parameter of a installer_addon_section call +# ------------------------------------------------------------------------------ + +function installer_addon_dependency { + for section in $dependencysections ; do + echo '${CheckSectionDependency} ${Sec_'"$section"'} ${Sec_'"$1"'} '"'$section' '$1'" >> "/build/filelists/addon_dependencies.nsh" + done +} + +# ------------------------------------------------------------------------------ +# Finish an installer section after an addon build +# +# This creates the file list files +# +# parameters: none +# ------------------------------------------------------------------------------ + +function installer_addon_end { + if [ -n "$installersection" ]; then + list_files "addon_post_$installersection" + diff_files "addon_$installersection" "addon_post_$installersection" "addon_pre_$installersection" + files_to_nsis "addon_$installersection" + 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/' +} ###################### MODULE BUILD FUNCTIONS ##################### @@ -1287,6 +1458,8 @@ function make_coq { build_post fi + + load_overlay_data } ##### GNU Make for MinGW ##### @@ -1450,18 +1623,15 @@ function make_coq_installer { fi } -###################### ADDONS ##################### +###################### ADDON COQ LIBRARIES / PLUGINS / TOOLS ##################### # The bignums library # 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_REF" | cut -f 1) - if [[ "$bignums_SHA" == "" ]]; then - # $bignums_CI_REF must have been a tag / commit and not a branch - bignums_SHA="$bignums_CI_REF" - fi - if build_prep "$bignums_CI_ARCHIVEURL" "$bignums_SHA" zip 1 "bignums-$bignums_SHA"; then + installer_addon_dependency bignums + if build_prep_overlay bignums; then + installer_addon_section bignums "Bignums" "Coq library for fast arbitrary size numbers" "" # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1470,61 +1640,275 @@ function make_addon_bignums { fi } +# Equations plugin +# A function definition plugin + +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 + PATH=$COQBIN:$PATH + logn coq_makefile ${COQBIN}coq_makefile -f _CoqProject -o Makefile + log1 make + log2 make install + build_post + fi +} + +# mathcomp - ssreflect and mathematical components library + +function make_addon_mathcomp { + installer_addon_dependency mathcomp + if build_prep_overlay mathcomp; then + installer_addon_section mathcomp "Math-Components" "Coq library with mathematical components" "" + cd mathcomp + log1 make $MAKE_OPT + log2 make install + build_post + fi +} + +# ssreflect part of mathcomp + +function make_addon_ssreflect { + # if mathcomp addon is requested, build this instead + if [[ "$COQ_ADDONS" == *mathcomp* ]]; then + make_addon_mathcomp + else + # Note: since either mathcomp or ssreflect is defined, it is fine to name both mathcomp + installer_addon_dependency ssreflect + if build_prep_overlay mathcomp; then + installer_addon_section ssreflect "SSReflect" "Coq support library for small scale reflection plugin" "" + cd mathcomp + logn make-makefile make Makefile.coq + logn make-ssreflect make $MAKE_OPT -f Makefile.coq ssreflect/all_ssreflect.vo + logn make-install make -f Makefile.coq install + build_post + fi + fi +} + # Ltac-2 plugin # A new (experimental) tactic language function make_addon_ltac2 { - ltac2_SHA=$(git ls-remote "$ltac2_CI_GITURL" "refs/heads/$ltac2_CI_REF" | cut -f 1) - if [[ "$ltac2_SHA" == "" ]]; then - # $ltac2_CI_REF must have been a tag / commit and not a branch - ltac2_SHA="$ltac2_CI_REF" - fi - if build_prep "$ltac2_CI_ARCHIVEURL" "$ltac2_SHA" zip 1 "ltac2-$ltac2_SHA"; then + 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" "" log1 make all log2 make install build_post fi } -# Equations plugin -# A function definition plugin - -function make_addon_equations { - Equations_SHA=$(git ls-remote "$Equations_CI_GITURL" "refs/heads/$Equations_CI_REF" | cut -f 1) - if [[ "$Equations_SHA" == "" ]]; then - # $Equations_CI_REF must have been a tag / commit and not a branch - Equations_SHA="$Equations_CI_REF" +# UniCoq plugin +# An alternative unification algorithm +function make_addon_unicoq { + installer_addon_dependency unicoq + if build_prep_overlay unicoq; then + log1 coq_makefile -f Make -o Makefile + log1 make + log2 make install + build_post fi - 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 +} + +# Mtac2 plugin +# An alternative typed tactic language +function make_addon_mtac2 { + installer_addon_dependency_beg mtac2 + make_addon_unicoq + installer_addon_dependency_end + if build_prep_overlay mtac2; then + log1 coq_makefile -f _CoqProject -o Makefile log1 make log2 make install build_post fi } -function make_addons { - if [ -n "$GITLAB_CI" ]; then - export CI_BRANCH="$CI_COMMIT_REF_NAME" - if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]; then - export CI_PULL_REQUEST="${CI_BRANCH#pr-}" - else - export CI_PULL_REQUEST="" +# Menhir parser generator + +function make_addon_menhir { + make_menhir + # If COQ and OCaml are installed to the same folder, there is nothing to do + installer_addon_dependency menhir + if [ "$PREFIXOCAML" != "$PREFIXCOQ" ] ; then + # Just install menhir files required for COQ to COQ target folder + if [ ! -f "$FLAGFILES/menhir-addon.finished" ] ; then + installer_addon_section menhir "Menhir" "Menhir parser generator windows executable and libraries" "" + LOGTARGET=menhir-addon + touch "$FLAGFILES/menhir-addon.started" + # Menhir executable + install_glob "$PREFIXOCAML/bin" 'menhir.exe' "$PREFIXCOQ/bin/" + # Menhir Standard library + install_glob "$PREFIXOCAML/share/menhir/" '*.mly' "$PREFIXCOQ/share/menhir/" + # Menhir PDF doc + install_glob "$PREFIXOCAML/share/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/" + touch "$FLAGFILES/menhir-addon.finished" + LOGTARGET=other + installer_addon_end fi - else - export CI_BRANCH="" - export CI_PULL_REQUEST="" fi - for overlay in /build/user-overlays/*.sh; do - . "$overlay" - done - . /build/ci-basic-overlay.sh +} + +# COQ library for Menhir + +function make_addon_menhirlib { + installer_addon_dependency menhirlib + if build_prep_overlay menhirlib; then + installer_addon_section menhirlib "Menhirlib" "Coq support library for using Menhir generated parsers in Coq" "" + # The supplied makefiles don't work in any way on cygwin + cd src + echo -R . MenhirLib > _CoqProject + ls -1 *.v >> _CoqProject + log1 coq_makefile -f _CoqProject -o Makefile.coq + log1 make -f Makefile.coq all + logn make-install make -f Makefile.coq install + build_post + fi +} + +# CompCert + +function make_addon_compcert { + installer_addon_dependency_beg compcert + make_menhir + make_addon_menhirlib + installer_addon_dependency_end + if build_prep_overlay CompCert; then + installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off" + logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin + log1 make + log2 make install + logn install-license-1 install -D -T "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE" + logn install-license-2 install -D -T "LICENSE" "$PREFIXCOQ/lib/compcert/LICENSE" + build_post + fi +} + +# Princeton VST + +function install_addon_vst { + VSTDEST="$PREFIXCOQ/lib/coq/user-contrib/VST" + + # Install VST .v, .vo, .c and .h files + install_rec compcert '*.v' "$VSTDEST/compcert/" + install_rec compcert '*.vo' "$VSTDEST/compcert/" + install_glob "msl" '*.v' "$VSTDEST/msl/" + install_glob "msl" '*.vo' "$VSTDEST/msl/" + install_glob "sepcomp" '*.v' "$VSTDEST/sepcomp/" + install_glob "sepcomp" '*.vo' "$VSTDEST/sepcomp/" + install_glob "floyd" '*.v' "$VSTDEST/floyd/" + install_glob "floyd" '*.vo' "$VSTDEST/floyd/" + 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 VST documentation files + install_glob "." 'LICENSE' "$VSTDEST" + install_glob "." '*.md' "$VSTDEST" + install_glob "compcert" '*' "$VSTDEST/compcert" + install_glob "doc" '*.pdf' "$VSTDEST/doc" + + # Install VST _CoqProject files + install_glob "." '_CoqProject*' "$VSTDEST" + install_glob "." '_CoqProject-export' "$VSTDEST/progs" +} + +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 coq_set_timeouts_1000 + log1 make IGNORECOQVERSION=true $MAKE_OPT + log1 install_addon_vst + build_post + fi +} + +# coquelicot Real analysis + +function make_addon_coquelicot { + installer_addon_dependency_beg coquelicot + make_addon_ssreflect + installer_addon_dependency_end + if build_prep_overlay Coquelicot; then + installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" "" + logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot" + logn remake ./remake + logn remake-install ./remake install + build_post + fi +} + +# AAC associative / commutative rewriting + +function make_addon_aactactics { + installer_addon_dependency aac + if build_prep_overlay aactactis; then + installer_addon_section aac "AAC" "Coq plugin for extensible associative and commutative rewriting" "" + log1 make + log2 make install + build_post + fi +} + +# extlib + +function make_addon_extlib { + installer_addon_dependency extlib + if build_prep_overlay ext_lib; then + installer_addon_section extlib "Ext-Lib" "Coq library with many reusable general purpose components" "" + log1 make $MAKE_OPT + log2 make install + build_post + fi +} + +# SimpleIO + +function make_addon_simple_io { + installer_addon_dependency simpleIO + if build_prep_overlay simple_io; then + installer_addon_section simpleIO "SimpleIO" "Coq plugin for reading and writing files directly from Coq code" "" + log1 make $MAKE_OPT + log2 make install + build_post + fi +} + +# Quickchick Randomized Property-Based Testing Plugin for Coq + +function make_addon_quickchick { + installer_addon_dependency_beg quickchick + make_addon_ssreflect + make_addon_extlib + make_addon_simple_io + make_ocamlbuild + installer_addon_dependency_end + if build_prep_overlay quickchick; then + installer_addon_section quickchick "QuickChick" "Coq plugin for randomized testing and counter example search" "" + log1 make + log2 make install + build_post + fi +} + +# Main function for building addons + +function make_addons { + # Note: ':' is the empty command, which does not produce any output + : > "/build/filelists/addon_dependencies.nsh" for addon in $COQ_ADDONS; do "make_addon_$addon" done + + sort -u -o "/build/filelists/addon_dependencies.nsh" "/build/filelists/addon_dependencies.nsh" } ###################### TOP LEVEL BUILD ##################### diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index 55fba6d5ab..9947965c28 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -38,43 +38,20 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \ ;Folder selection page InstallDir "C:\${MY_PRODUCT}" - + ;Remember install folder InstallDirRegKey HKCU "Software\${MY_PRODUCT}" "" ;-------------------------------- -;Modern UI Configuration - - !define MUI_ICON "${COQ_ICON}" - - !insertmacro MUI_PAGE_WELCOME - !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt" - !insertmacro MUI_PAGE_COMPONENTS - !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces." - !insertmacro MUI_PAGE_DIRECTORY - !insertmacro MUI_PAGE_INSTFILES - !insertmacro MUI_PAGE_FINISH - - !insertmacro MUI_UNPAGE_WELCOME - !insertmacro MUI_UNPAGE_CONFIRM - !insertmacro MUI_UNPAGE_INSTFILES - !insertmacro MUI_UNPAGE_FINISH - -;-------------------------------- -;Languages - - !insertmacro MUI_LANGUAGE "English" - -;-------------------------------- -;Language Strings +;Extra license pages - ;Description - LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." - LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}" - ;LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." - LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." - LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." - LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." +!macro MUI_PAGE_LICENSE_EXTRA Licensefile Header Subheader Bottom SelFunc + !define MUI_PAGE_HEADER_TEXT "${Header}" + !define MUI_PAGE_HEADER_SUBTEXT "${Subheader}" + !define MUI_LICENSEPAGE_TEXT_BOTTOM "${Bottom}" + !define MUI_PAGE_CUSTOMFUNCTION_PRE ${SelFunc} + !insertmacro MUI_PAGE_LICENSE "${Licensefile}" +!macroend ;-------------------------------- ; Check for white spaces @@ -95,7 +72,6 @@ FunctionEnd ;-------------------------------- ;Installer Sections - Section "Coq" Sec1 SetOutPath "$INSTDIR\" @@ -105,7 +81,7 @@ Section "Coq" Sec1 ;Store install folder WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR - + ;Create uninstaller WriteUninstaller "$INSTDIR\Uninstall.exe" WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \ @@ -123,7 +99,7 @@ Section "Coq" Sec1 ; Create start menu entries ; SetOutPath is required for the path in the .lnk files - SetOutPath "$INSTDIR" + SetOutPath "$INSTDIR" CreateDirectory "$SMPROGRAMS\Coq" ; The first shortcut set here is treated as main application by Windows 7/8. ; Use CoqIDE as main application @@ -138,24 +114,23 @@ SectionEnd ;OCAML Section "Ocaml for native compute and plugin development" Sec2 ;OCAML SetOutPath "$INSTDIR\" ;OCAML !include "..\..\..\filelists\ocaml.nsh" -;OCAML +;OCAML ;OCAML ; Create a few slash / backslash variants of the source and install path ;OCAML ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR} ;OCAML !insertmacro StrRep $COQ_SRC_PATH_BS ${COQ_SRC_PATH} "/" "\" ;OCAML !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\" ;OCAML !insertmacro StrRep $INSTDIR_DBS $INSTDIR "\" "\\" -;OCAML +;OCAML ;OCAML ; Replace absolute paths in some OCaml config files ;OCAML ; These are not all, see ReadMe.txt ;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/" "\" ;OCAML !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS" "$INSTDIR" ;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS" ;OCAML SectionEnd - -Section "Coq packages" Sec2 - SetOutPath "$INSTDIR\" - !include "..\..\..\filelists\coq_addons.nsh" -SectionEnd + +SectionGroup "Coq addons" Sec2 + !include "..\..\..\filelists\addon_sections.nsh" +SectionGroupEnd Section "Coq files for plugin developers" Sec3 SetOutPath "$INSTDIR\" @@ -179,6 +154,130 @@ SectionEnd ;OCAML SectionEnd ;-------------------------------- +;Section dependencies + +; Parameters on the stack: +; top-0 : section B on which section A dependencies +; top-1 : section A, which depends on section B +; top-2 : name of section B +; top-3 : name of section A + +Function CheckSectionDependency + ; stack=nameB nameA secB secA rest + Exch $R3 ; stack=$R3 nameA secB secA rest; $R3=nameB + Exch ; stack=nameA $R3 secB secA rest + Exch $R2 ; stack=$R2 $R3 secB secA rest; $R2=nameA + Exch 2 ; stack=secB $R3 $R2 secA rest + Exch $R1 ; stack=$R1 $R3 $R2 secA rest; $R1=secB + Exch 3 ; stack=secA $R3 $R2 $R1 rest; + Exch $R0 ; stack=$R0 $R3 $R2 $R1 rest; $R0=secA + ; Take care of save order when popping the stack! + Push $R4 + Push $R5 + + SectionGetFlags $R0 $R0 + IntOp $R0 $R0 & ${SF_SELECTED} + + SectionGetFlags $R1 $R4 + IntOp $R5 $R4 & ${SF_SELECTED} + + ${If} $R0 == ${SF_SELECTED} + ${AndIf} $R5 != ${SF_SELECTED} + + IntOp $R5 $R4 | ${SF_SELECTED} + SectionSetFlags $R1 $R5 + MessageBox MB_OK '"$R3" has been selected, because "$R2" depends on it' + + ${EndIf} + + Pop $R5 + Pop $R4 + Pop $R0 + Pop $R3 + Pop $R2 + Pop $R1 +FunctionEnd + +!macro CheckSectionDependency secA secB nameA nameB + Push "${secA}" + Push "${secB}" + Push "${nameA}" + Push "${nameB}" + Call CheckSectionDependency +!macroend + +!define CheckSectionDependency "!insertmacro CheckSectionDependency" + +Function .onSelChange + !include "..\..\..\filelists\addon_dependencies.nsh" +FunctionEnd + +;-------------------------------- +;Modern UI Configuration + +; Note: this must be placed after the sections, because below we need to check at compile time +; if sections exist (by !ifdef <section_index_var>) to decide if the license page must be included. +; The section index variables are only defined after the section definitions. + + !define MUI_ICON "${COQ_ICON}" + + !insertmacro MUI_PAGE_WELCOME + !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt" + !insertmacro MUI_PAGE_COMPONENTS + + !ifdef Sec_compcert + !define LicCompCert_Title "CompCert License Agreement" + !define LicCompCert_SubTitle "You selected the CompCert addon. CompCert is not open source. Please review the license terms before installing CompCert!" + !define LicCompCert_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the CompCert addon." + !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/compcert/LICENSE" "${LicCompCert_Title}" "${LicCompCert_SubTitle}" "${LicCompCert_Bottom}" SelFuncCompCert + + Function SelFuncCompCert + ${Unless} ${SectionIsSelected} ${Sec_compcert} + Abort + ${EndUnless} + FunctionEnd + !endif + + !ifdef Sec_vst + !define LicVST_Title "Princeton VST License Agreement" + !define LicVST_SubTitle "You selected the VST addon. VST contains parts of CompCert which are not open source. Please review the license terms before installing VST!" + !define LicVST_Bottom "If you accept the terms of the agreement, click I Agree to continue. Otherwise go back and unselect the VST addon." + !insertmacro MUI_PAGE_LICENSE_EXTRA "${COQ_SRC_PATH}/lib/coq/user-contrib/VST/LICENSE" "${LicVST_Title}" "${LicVST_SubTitle}" "${LicVST_Bottom}" SelFuncVST + + Function SelFuncVST + ${Unless} ${SectionIsSelected} ${Sec_vst} + Abort + ${EndUnless} + FunctionEnd + !endif + + !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq. The path MUST NOT include spaces." + !insertmacro MUI_PAGE_DIRECTORY + !insertmacro MUI_PAGE_INSTFILES + !insertmacro MUI_PAGE_FINISH + + !insertmacro MUI_UNPAGE_WELCOME + !insertmacro MUI_UNPAGE_CONFIRM + !insertmacro MUI_UNPAGE_INSTFILES + !insertmacro MUI_UNPAGE_FINISH + +;-------------------------------- +;Languages + + !insertmacro MUI_LANGUAGE "English" + +;-------------------------------- +;Language Strings + + ;Description + LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." + LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}" + LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." + ; LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." + ; LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." + !include "..\..\..\filelists\addon_strings.nsh" + +;-------------------------------- ;Descriptions !insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN @@ -187,8 +286,9 @@ SectionEnd !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5) + !include "..\..\..\filelists\addon_descriptions.nsh" !insertmacro MUI_FUNCTION_DESCRIPTION_END - + ;-------------------------------- ;Uninstaller Section @@ -214,7 +314,7 @@ Section "Uninstall" Delete "$SMPROGRAMS\Coq\The Coq HomePage.url" Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url" Delete "$INSTDIR\Uninstall.exe" - + ; Registry keys DeleteRegKey HKCU "Software\${MY_PRODUCT}" DeleteRegKey HKLM "SOFTWARE\Coq" diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch new file mode 100755 index 0000000000..1afa6e7f95 --- /dev/null +++ b/dev/build/windows/patches_coq/quickchick.patch @@ -0,0 +1,26 @@ +diff/patch file created on Mon, Aug 27, 2018 9:21:52 AM with: +difftar-folder.sh tarballs/quickchick-v1.0.2.tar.gz quickchick-v1.0.2 1 +TARFILE= tarballs/quickchick-v1.0.2.tar.gz +FOLDER= quickchick-v1.0.2 +TARSTRIP= 1 +TARPREFIX= QuickChick-1.0.2/ +ORIGFOLDER= quickchick-v1.0.2.orig +--- quickchick-v1.0.2.orig/Makefile 2018-08-22 18:21:39.000000000 +0200 ++++ quickchick-v1.0.2/Makefile 2018-08-27 09:21:04.710461100 +0200 +@@ -2,7 +2,7 @@ + .PHONY: plugin install install-plugin clean quickChickTool + + QCTOOL_DIR=quickChickTool +-QCTOOL_EXE=quickChickTool.byte ++QCTOOL_EXE=quickChickTool.native + QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \ + $(QCTOOL_DIR)/quickChickToolTypes.ml \ + $(QCTOOL_DIR)/quickChickToolLexer.mll \ +@@ -32,7 +32,7 @@ + install: all + $(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE) + # Manually copying the remaining files +- $(V)cp $(QCTOOL_EXE) $(shell opam config var bin)/quickChick ++ $(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick" + # $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick + # $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 8620b01b26..1b1aeafa0d 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -92,8 +92,15 @@ ######################################################################## # Coquelicot ######################################################################## -: "${Coquelicot_CI_REF:=master}" +# The URL for downloading a tgz snapshot of the master branch is +# https://scm.gforge.inria.fr/anonscm/gitweb?p=coquelicot/coquelicot.git;a=snapshot;h=refs/heads/master;sf=tgz +# See https://gforge.inria.fr/scm/browser.php?group_id=3599 +# Since this URL doesn't fit to our standard mechanism and since Coquelicot doesn't seem to change frequently, +# we use a fixed version, which has a download path which does fit to our standard mechanism. +# ATTENTION: The archive URL might depend on the version! +: "${Coquelicot_CI_REF:=coquelicot-3.0.2}" : "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}" +: "${Coquelicot_CI_ARCHIVEURL:=https://gforge.inria.fr/frs/download.php/file/37523}" ######################################################################## # CompCert @@ -228,8 +235,22 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# quickchick +# plugin_tutorial ######################################################################## : "${plugin_tutorial_CI_REF:=master}" : "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" : "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" + +######################################################################## +# menhirlib +######################################################################## +: "${menhirlib_CI_REF:=master}" +: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}" +: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" + +######################################################################## +# aac-tactics +######################################################################## +: "${aactactis_CI_REF:=master}" +: "${aactactis_CI_GITURL:=https://github.com/coq-community/aac-tactics}" +: "${aactactis_CI_ARCHIVEURL:=${aactactis_CI_GITURL}/archive}" diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 09e9762261..deda42e2b7 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -43,9 +43,23 @@ if exist %DESTCOQ%\ rd /s /q %DESTCOQ% call %CI_PROJECT_DIR%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-arch=%ARCH% -installer=Y -coqver=%CI_PROJECT_DIR_CFMT% ^
-destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
- -addon="bignums ltac2 equations" -make=N ^
+ -addon=bignums ^
+ -addon=equations ^
+ -addon=ltac2 ^
+ -addon=mtac2 ^
+ -addon=mathcomp ^
+ -addon=menhir ^
+ -addon=menhirlib ^
+ -addon=compcert ^
+ -addon=extlib ^
+ -addon=quickchick ^
+ -addon=coquelicot ^
+ -make=N ^
-setup %CI_PROJECT_DIR%\%SETUP% || GOTO ErrorCopyLogFilesAndExit
+REM addons with build issues
+REM -addon=vst ^
+REM -addon=aactactics ^
ECHO "Start Artifact Creation"
TIME /T
|