From 628ed5960ab22a0cac040c536c99d5d4e38d43d8 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Sun, 7 Jun 2020 14:35:06 +0200 Subject: Windows: fix menhir and coq-menhirlib build for latest version. --- dev/build/windows/makecoq_mingw.sh | 16 +++++++--------- dev/ci/ci-basic-overlay.sh | 3 ++- 2 files changed, 9 insertions(+), 10 deletions(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 4a6555a4f7..43ffb37477 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1087,11 +1087,10 @@ function make_menhir { make_ocaml make_findlib make_ocamlbuild - # This is the version required by latest CompCert - if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20190626 menhir-20190626 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" + if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20200525 menhir-20200525 tar.gz 1 ; then + # ToDo: don't know if this is the intended / most reliable to do it, but it works + log2 dune build @install + log2 dune install menhir menhirSdk menhirLib build_post fi } @@ -1712,10 +1711,8 @@ function make_addon_menhir { 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/" + install_glob "$PREFIXOCAML/doc/menhir/" '*.pdf' "$PREFIXCOQ/doc/menhir/" touch "$FLAGFILES/menhir-addon.finished" LOGTARGET=other installer_addon_end @@ -1730,7 +1727,8 @@ function make_addon_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 + # ToDo: dune also doesn't seem to work for the coq files + cd coq-menhirlib/src echo -R . MenhirLib > _CoqProject ls -1 *.v >> _CoqProject log1 coq_makefile -f _CoqProject -o Makefile.coq diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4ebc637a68..9737e1b2e0 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -283,8 +283,9 @@ ######################################################################## # menhirlib ######################################################################## +# Note: menhirlib is now in subfolder coq-menhirlib of menhir : "${menhirlib_CI_REF:=master}" -: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/coq-menhirlib}" +: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}" : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" ######################################################################## -- cgit v1.2.3 From 3b556e1ad3b757f8a22248ac068e84e5b4082883 Mon Sep 17 00:00:00 2001 From: Michael Soegtrop Date: Tue, 9 Jun 2020 23:01:28 +0200 Subject: Windows: fix build of Gappa C++ tool --- dev/build/windows/makecoq_mingw.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 43ffb37477..1a5a8b29fd 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1928,7 +1928,9 @@ function make_addon_gappa_tool { install_boost if build_prep_overlay gappa_tool; then installer_addon_section gappa_tool "Gappa tool" "Stand alone tool for automated generation of numerical arithmetic proofs" "" - logn autogen ./autogen.sh + log1 autoreconf + # Note: configure.in seems to reference this file + touch stamp-config_h.in logn configure ./configure --build="$HOST" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ" logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake -d install -- cgit v1.2.3 From 85999bcd0df91b8cd9fd7fc07d1bc780a92c0225 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 5 Jun 2020 12:01:23 +0200 Subject: Fix Coquelicot build in Windows add-ons. Adapted from 747936a9d9a7402f537e1e1a857c7591d8e88d2a --- dev/build/windows/makecoq_mingw.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 1a5a8b29fd..8c2e87ddb7 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1814,7 +1814,7 @@ function make_addon_coquelicot { installer_addon_dependency_end if build_prep_overlay coquelicot; then installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" "" - logn autogen ./autogen.sh + log1 autoreconf -i -s logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot" logn remake ./remake logn remake-install ./remake install -- cgit v1.2.3 From e2afb5b493612e96e0c86e769d9486486494580c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 5 Jun 2020 16:44:34 +0200 Subject: Call autoreconf in interval, flocq and gappa-plugin. --- dev/build/windows/makecoq_mingw.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 8c2e87ddb7..fca8cd6120 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1880,7 +1880,7 @@ function make_addon_quickchick { function make_addon_flocq { if build_prep_overlay flocq; then installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" "" - log1 autoconf + log1 autoreconf logn configure ./configure logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake install @@ -1899,7 +1899,7 @@ function make_addon_interval { installer_addon_dependency_end if build_prep_overlay interval; then installer_addon_section interval "Interval" "Coq library and tactic for proving real inequalities" "" - logn autogen ./autogen.sh + log1 autoreconf logn configure ./configure logn remake ./remake --jobs=$MAKE_THREADS logn install ./remake install @@ -1947,7 +1947,7 @@ function make_addon_gappa { installer_addon_dependency_end if build_prep_overlay gappa_plugin ; then installer_addon_section gappa "Gappa plugin" "Coq plugin for the Gappa tool" "" - logn autogen ./autogen.sh + log1 autoreconf logn configure ./configure logn remake ./remake logn install ./remake install -- cgit v1.2.3 From ba8c793ed4947b04ee3f8157e8a3d1dd8d529eeb Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 10 Jun 2020 15:45:15 +0200 Subject: Fix the build of Elpi by calling Dune directly. --- dev/build/windows/makecoq_mingw.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dev') diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fca8cd6120..6ceb7f54b2 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1193,10 +1193,10 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then + if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then - log2 make build DUNE_OPTS="-p elpi" - log2 make install DUNE_OPTS="-p elpi" + log2 dune build -p elpi + log2 dune install elpi build_post -- cgit v1.2.3