Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
[ci] make compcert use flocq and menhir
(cherry picked from commit dc8e605)
  • Loading branch information
gares committed Nov 26, 2020
1 parent e5bae8b commit e0ed28b
Show file tree
Hide file tree
Showing 4 changed files with 10 additions and 2 deletions.
5 changes: 5 additions & 0 deletions .gitlab-ci.yml
Expand Up @@ -713,7 +713,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
Expand Down
3 changes: 3 additions & 0 deletions Makefile.ci
Expand Up @@ -40,6 +40,7 @@ CI_TARGETS= \
ci-iris \
ci-math_classes \
ci-mathcomp \
ci-menhir \
ci-metacoq \
ci-mtac2 \
ci-paramcoq \
Expand Down Expand Up @@ -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 $*
Expand Down
2 changes: 1 addition & 1 deletion dev/build/windows/makecoq_mingw.sh
Expand Up @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion dev/ci/ci-compcert.sh
Expand Up @@ -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)')

0 comments on commit e0ed28b

Please sign in to comment.