diff options
| author | Enrico Tassi | 2020-11-24 09:46:54 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-25 15:59:42 +0100 |
| commit | dc8e605d9cadf0d7ead78481e0e68756713f7aa0 (patch) | |
| tree | e24089d1b512f080c5cfaa03a235715fdfd669a8 | |
| parent | 94abc3dce396b77e98900e604e3117986dd2ab60 (diff) | |
[ci] make compcert use flocq and menhir
| -rw-r--r-- | .gitlab-ci.yml | 5 | ||||
| -rw-r--r-- | Makefile.ci | 3 | ||||
| -rwxr-xr-x | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 2 |
4 files changed, 10 insertions, 2 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7dd9a37f59..3c09d0a8c8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -711,7 +711,12 @@ library:ci-color: - plugin:ci-bignums library:ci-compcert: + stage: stage-3 extends: .ci-template-flambda + needs: + - build:edge+flambda + - library:ci-flocq + - library:ci-menhir library:ci-coq_performance_tests: extends: .ci-template diff --git a/Makefile.ci b/Makefile.ci index af78f252df..759462f509 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -40,6 +40,7 @@ CI_TARGETS= \ ci-iris \ ci-math_classes \ ci-mathcomp \ + ci-menhir \ ci-metacoq \ ci-mtac2 \ ci-paramcoq \ @@ -85,6 +86,8 @@ ci-metacoq: ci-equations ci-vst: ci-flocq +ci-compcert: ci-menhir ci-flocq + # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* 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)') |