From dc8e605d9cadf0d7ead78481e0e68756713f7aa0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Nov 2020 09:46:54 +0100
Subject: [ci] make compcert use flocq and menhir

---
 dev/build/windows/makecoq_mingw.sh | 2 +-
 dev/ci/ci-compcert.sh              | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 6f6b3cd6d2..6cc91ace81 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1749,7 +1749,7 @@ function make_addon_compcert {
   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
+    logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin -use-external-MenhirLib -use-external-Flocq
     log1 make $MAKE_OPT
     log2 make install
     logn install-license-1 install -D -T  "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE"
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 6b09726606..3c8d65f5c1 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -7,6 +7,6 @@ git_download compcert
 
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert" && \
-      ./configure -ignore-coq-version x86_32-linux && \
+      ./configure -ignore-coq-version x86_32-linux -use-external-MenhirLib -use-external-Flocq && \
       make && \
       make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
-- 
cgit v1.2.3