From cb885e8c70a75043ff89e117c29cbb5dc22ff16f Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Fri, 15 Jun 2018 18:57:00 +0200 Subject: Fix for issue 7707: include Ltac2 and Equations in Windows build On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin. --- .github/CODEOWNERS | 3 +++ dev/build/plugin-versions/bignums.sh | 12 ++++++++++ dev/build/plugin-versions/equations.sh | 12 ++++++++++ dev/build/plugin-versions/ltac2.sh | 12 ++++++++++ dev/build/plugin-versions/readme.md | 42 ++++++++++++++++++++++++++++++++++ dev/build/windows/MakeCoq_MinGW.bat | 8 ++++++- dev/build/windows/makecoq_mingw.sh | 36 ++++++++++++++++++++++++++++- 7 files changed, 123 insertions(+), 2 deletions(-) create mode 100755 dev/build/plugin-versions/bignums.sh create mode 100755 dev/build/plugin-versions/equations.sh create mode 100755 dev/build/plugin-versions/ltac2.sh create mode 100644 dev/build/plugin-versions/readme.md mode change 100644 => 100755 dev/build/windows/MakeCoq_MinGW.bat diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 3a762b42a..0278df72f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -339,6 +339,9 @@ /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes +/dev/build/plugin-versions @MSoegtropIMC +# Secondary maintainer @maximedenes + # This file belongs to CI /Makefile.ci @ejgallego # Secondary maintainer @SkySkimmer diff --git a/dev/build/plugin-versions/bignums.sh b/dev/build/plugin-versions/bignums.sh new file mode 100755 index 000000000..8a4ddf5fc --- /dev/null +++ b/dev/build/plugin-versions/bignums.sh @@ -0,0 +1,12 @@ +#!/bin/sh +case "$1" in + git-master|/cygdrive*) + # First get the SHA of master/HEAD and then download a zip of exactly this state + BIGNUMS_SHA=$(git ls-remote 'https://github.com/coq/bignums' refs/heads/master | cut -f 1) + + echo https://github.com/coq/bignums/archive "$BIGNUMS_SHA" zip 1 "bignums-$BIGNUMS_SHA" + ;; + *) + echo https://github.com/coq/bignums/archive V8.8.0 zip 1 bignums-V8.8+beta1 + ;; +esac diff --git a/dev/build/plugin-versions/equations.sh b/dev/build/plugin-versions/equations.sh new file mode 100755 index 000000000..9fc2e237a --- /dev/null +++ b/dev/build/plugin-versions/equations.sh @@ -0,0 +1,12 @@ +#!/bin/sh +case "$1" in + git-master|/cygdrive*) + # First get the SHA of master/HEAD and then download a zip of exactly this state + EQUATIONS_SHA=$(git ls-remote 'https://github.com/mattam82/Coq-Equations' refs/heads/master | cut -f 1) + + echo https://github.com/mattam82/Coq-Equations/archive "$EQUATIONS_SHA" zip 1 "equations-$EQUATIONS_SHA" + ;; + *) + echo https://github.com/mattam82/Coq-Equations/archive v1.1-8.8 zip 1 equations-v1.1-8.8 + ;; +esac diff --git a/dev/build/plugin-versions/ltac2.sh b/dev/build/plugin-versions/ltac2.sh new file mode 100755 index 000000000..feee3c92c --- /dev/null +++ b/dev/build/plugin-versions/ltac2.sh @@ -0,0 +1,12 @@ +#!/bin/sh +case "$1" in + git-master|/cygdrive*) + # First get the SHA of master/HEAD and then download a zip of exactly this state + LTAC2_SHA=$(git ls-remote 'https://github.com/ppedrot/ltac2' refs/heads/master | cut -f 1) + + echo https://github.com/ppedrot/ltac2/archive "$LTAC2_SHA" zip 1 "ltac2-$LTAC2_SHA" + ;; + *) + echo https://github.com/ppedrot/ltac2/archive v8.8 zip 1 ltac2-v8.8 + ;; +esac diff --git a/dev/build/plugin-versions/readme.md b/dev/build/plugin-versions/readme.md new file mode 100644 index 000000000..39277d09b --- /dev/null +++ b/dev/build/plugin-versions/readme.md @@ -0,0 +1,42 @@ +# Controlling the versions of plugins + +The shell scripts in this folder each return (to stdout) the source URL and some extra +information for a specific plugin with a version appropriate for this version of Coq. + +This mechanism is only intended for plugins and libraries which need a tight coupling to the version of Coq. + +The shell scripts get the Coq version as first argument. +Examples for possible values are: + +* git-v8.8.1 +* git-master +* 8.5pl3 +* 8.8.1 +* /cygdrive/ + +Scripts can simply echo an URL, but more advanced processing is possible. + +The output format is the same as the command line to the function build_prep in makecoq_mingw.sh. Here is an example: + +``` +#!/bin/sh +echo 'https://github.com/ppedrot/ltac2/archive' 'v8.8' 'zip' '1' 'ltac2-v8.8' +``` + +The arguments are: +* URL path without file name +* file name +* file extension +* number of path levels to strip from archive (optional, default is 1) +* module name, in case the file name just gives a version but no module name + +## Handling master versions + +In case a master version is returned, the module name should contain the SHA code of the revision downloaded. +Below is an example of how to achieve this (thanks to SkySkimmer): + +``` +BIGNUMS_SHA=$(git ls-remote 'https://github.com/coq/bignums' refs/heads/master | cut -f 1) + +echo https://github.com/coq/bignums/archive "$BIGNUMS_SHA" zip 1 "bignums-$BIGNUMS_SHA" +``` diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat old mode 100644 new mode 100755 index f960ff008..5af0fcff3 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -255,6 +255,7 @@ IF NOT "%~0" == "" ( IF NOT EXIST %SETUP% ( ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html. + ECHO If the setup is in a different folder, set the full path to %SETUP% using the -setup option. GOTO :EOF ) @@ -385,7 +386,6 @@ IF "%RUNSETUP%"=="Y" ( MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs" ) - IF NOT "%CYGWIN_QUIET%" == "Y" ( REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it. REM This is not required with the -cygquiet=Y and the resulting --no-admin option. @@ -396,6 +396,12 @@ IF NOT "%CYGWIN_QUIET%" == "Y" ( ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ========== +REM In case this batch file is called from a cygwin bash (e.g. a git repo) we need to clear +REM HOME (otherwise we get to the home directory of the other installation) +REM PROFILEREAD (this is set to true if the /etc/profile has been read, which creates user) +SET "HOME=" +SET "PROFILEREAD=" + copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit %BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 508dcf5fb..4fabf3161 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -118,6 +118,9 @@ mkdir -p "$PREFIX/bin" mkdir -p "$PREFIXCOQ/bin" mkdir -p "$PREFIXOCAML/bin" +# This is required for building addons and plugins +export COQBIN=$RESULT_INSTALLDIR_CFMT/bin/ + ###################### Copy Cygwin Setup Info ##################### # Copy Cygwin repo ini file and installed files db to tarballs folder. @@ -1211,6 +1214,9 @@ function make_coq { # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)" # make clean + # Copy plugin version files somewhere, where the plugin builds can find them + cp -r dev/build/plugin-versions /build/ + build_post fi } @@ -1378,8 +1384,11 @@ function make_coq_installer { ###################### ADDONS ##################### +# The bignums library +# Provides BigN, BigZ, BigQ that used to be part of Coq standard library + function make_addon_bignums { - if build_prep https://github.com/coq/bignums/archive/ V8.8+beta1 zip 1 bignums-8.8+beta1; then + if build_prep $(/build/plugin-versions/bignums.sh "$COQ_VERSION"); then # To make command lines shorter :-( echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local log1 make all @@ -1388,6 +1397,31 @@ function make_addon_bignums { fi } +# Ltac-2 plugin +# A new (experimental) tactic language + +function make_addon_ltac2 { + if build_prep $(/build/plugin-versions/ltac2.sh "$COQ_VERSION"); then + log1 make all + log2 make install + build_post + fi +} + +# Equations plugin +# A function definition plugin + +function make_addon_equations { + if build_prep $(/build/plugin-versions/equations.sh "$COQ_VERSION"); 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 + log1 make + log2 make install + build_post + fi +} + function make_addons { for addon in $COQ_ADDONS; do "make_addon_$addon" -- cgit v1.2.3