From 9c111b3ed2dd16b86cc8e187b5e35ebdd482668f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2020 09:53:41 +0200 Subject: [win] Coq trunk is now called master The old script was still working but downloading an old version, probably there is a git ref called trunk somewhere --- dev/build/windows/MakeCoq_master_installer.bat | 26 ++++++++++++++++++++++++++ dev/build/windows/MakeCoq_trunk_installer.bat | 26 -------------------------- 2 files changed, 26 insertions(+), 26 deletions(-) create mode 100755 dev/build/windows/MakeCoq_master_installer.bat delete mode 100755 dev/build/windows/MakeCoq_trunk_installer.bat (limited to 'dev') diff --git a/dev/build/windows/MakeCoq_master_installer.bat b/dev/build/windows/MakeCoq_master_installer.bat new file mode 100755 index 0000000000..72640d5d79 --- /dev/null +++ b/dev/build/windows/MakeCoq_master_installer.bat @@ -0,0 +1,26 @@ +@ECHO OFF + +REM ========== COPYRIGHT/COPYLEFT ========== + +REM (C) 2016 Intel Deutschland GmbH +REM Author: Michael Soegtrop + +REM Released to the public by Intel under the +REM GNU Lesser General Public License Version 2.1 or later +REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html + +REM ========== BUILD COQ ========== + +call MakeCoq_SetRootPath + +call MakeCoq_MinGW.bat ^ + -arch=64 ^ + -installer=Y ^ + -coqver=git-master ^ + -destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^ + -destcoq="%ROOTPATH%\coq64_trunk_inst" + +IF %ERRORLEVEL% NEQ 0 ( + ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL% + EXIT /b %ERRORLEVEL% +) diff --git a/dev/build/windows/MakeCoq_trunk_installer.bat b/dev/build/windows/MakeCoq_trunk_installer.bat deleted file mode 100755 index f4f5827328..0000000000 --- a/dev/build/windows/MakeCoq_trunk_installer.bat +++ /dev/null @@ -1,26 +0,0 @@ -@ECHO OFF - -REM ========== COPYRIGHT/COPYLEFT ========== - -REM (C) 2016 Intel Deutschland GmbH -REM Author: Michael Soegtrop - -REM Released to the public by Intel under the -REM GNU Lesser General Public License Version 2.1 or later -REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html - -REM ========== BUILD COQ ========== - -call MakeCoq_SetRootPath - -call MakeCoq_MinGW.bat ^ - -arch=64 ^ - -installer=Y ^ - -coqver=git-trunk ^ - -destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^ - -destcoq="%ROOTPATH%\coq64_trunk_inst" - -IF %ERRORLEVEL% NEQ 0 ( - ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL% - EXIT /b %ERRORLEVEL% -) -- cgit v1.2.3 From d93b46d73b65135ab2714fa58044f53966bc4050 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2020 10:10:01 +0200 Subject: [win] since 4.07 the seq package is part of ocaml --- dev/build/windows/makecoq_mingw.sh | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 859b3e3166..5c3155cd16 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -983,6 +983,15 @@ function make_ocaml { cp Changes "$PREFIXOCAML/license_readme/ocaml/Changes.txt" fi + # Since 4.07 this library is part of ocaml + mkdir -p "$PREFIXOCAML/libocaml/site-lib/seq/" + cat > "$PREFIXOCAML/libocaml/site-lib/seq/META" < repeat until success sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile # shellcheck disable=SC2086 log1 make world.opt $MAKE_OPT log2 make install + cp lib/*.a "$PREFIXOCAML/libocaml/camlp5/" log2 make clean # For some reason META is not built / copied, but it is required log2 make -C etc META -- cgit v1.2.3 From f4e2b0b809efe0bc0e4ce1c6124a95bb1e6091aa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2020 10:13:20 +0200 Subject: [win] rules to build Elpi --- dev/build/windows/makecoq_mingw.sh | 41 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 10c85c686e..b6424dbfb4 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1164,6 +1164,47 @@ function make_lablgtk { fi } +##### Elpi ##### + +function make_seq { + make_ocaml + # since 4.07 this package is part of ocaml + +} + +function make_re { + make_ocaml + make_dune + make_seq + + if build_prep https://github.com/ocaml/ocaml-re/archive 1.9.0 tar.gz 1 ocaml-re; then + + log2 dune build -p re + log2 dune install re + + build_post + fi + +} + +function make_elpi { + make_ocaml + make_findlib + make_camlp5 + make_dune + make_re + + if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then + + log2 make build DUNE_OPTS="-p elpi" + log2 make install DUNE_OPTS="-p elpi" + + build_post + + fi + +} + ##### COQ ##### # Copy one DLLfrom cygwin MINGW packages to Coq install folder -- cgit v1.2.3 From 40e7685b20e385749d9de1097e43f404fc24c285 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2020 10:14:06 +0200 Subject: [win] addon for elpi --- dev/build/windows/makecoq_mingw.sh | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index b6424dbfb4..8fbd8dec20 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1955,6 +1955,21 @@ function make_addon_gappa { fi } +# Elpi: extension language for Coq based. It lets one define commands in tactics +# in a high level programming language with support for binders and unification +# variables. + +function make_addon_elpi { + make_elpi + installer_addon_dependency elpi + if build_prep_overlay elpi ; then + installer_addon_section elpi "Elpi extension language" "Coq plugin for the Elpi extension language" "" + logn build make + logn installe make install + build_post + fi +} + # Main function for building addons function make_addons { -- cgit v1.2.3 From a8fbe8b04bd53d4bf1575db0822b321d405cf83d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2020 10:14:51 +0200 Subject: [win] addon for Hierarchy Builder --- dev/build/windows/makecoq_mingw.sh | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8fbd8dec20..963b0e6387 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1970,6 +1970,21 @@ function make_addon_elpi { fi } +# Hierarchy Builder: high level language to declare a hierarchy of structures +# compiled down to records and canonical structures. + +function make_addon_HB { + installer_addon_dependency_beg elpi_hb + make_addon_elpi + installer_addon_dependency_end + if build_prep_overlay elpi_hb ; then + installer_addon_section elpi_hb "Hierarchy Builder" "Coq library to declare algebraic hierarchies" "" + logn build make + logn install make install VFILES=structures.v + build_post + fi +} + # Main function for building addons function make_addons { -- cgit v1.2.3 From 64cce2763b7ed767c735aa2cd64f4243623a5848 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Apr 2020 10:15:14 +0200 Subject: [win] CI build addons Coq-Elpi Hierarchy-Builder --- dev/ci/gitlab.bat | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat index 3998fc6514..dc6423332f 100755 --- a/dev/ci/gitlab.bat +++ b/dev/ci/gitlab.bat @@ -54,7 +54,9 @@ IF "%WINDOWS%" == "enabled_all_addons" ( -addon=flocq ^ -addon=interval ^ -addon=gappa_tool ^ - -addon=gappa + -addon=gappa ^ + -addon=elpi ^ + -addon=HB ) ELSE ( SET "EXTRA_ADDONS= " ) -- cgit v1.2.3