Skip to content

Commit

Permalink
Split the ci-elpi_hb makefile in two.
Browse files Browse the repository at this point in the history
This would wreak havoc with the overlay files, and elpi is sensitive enough
as a plugin for this to be extremely annoying.
  • Loading branch information
ppedrot committed Nov 20, 2023
1 parent 2cf22c1 commit 9954d73
Show file tree
Hide file tree
Showing 3 changed files with 29 additions and 9 deletions.
15 changes: 13 additions & 2 deletions Makefile.ci
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,9 @@ CI_TARGETS= \
ci-coq_tools \
ci-coqprime \
ci-deriving \
ci-elpi_hb \
ci-elpi \
ci-elpi_test \
ci-hb \
ci-hb_test \
ci-engine_bench \
ci-ext_lib \
Expand Down Expand Up @@ -97,7 +98,10 @@ CI_TARGETS= \
ci-vst \
ci-waterproof

.PHONY: ci-all $(CI_TARGETS)
CI_VIRTUAL_TARGETS= \
ci-elpi_hb

.PHONY: ci-all $(CI_TARGETS) $(CI_VIRTUAL_TARGETS)

ci-help:
echo '*** Coq CI system, please specify a target to build.'
Expand Down Expand Up @@ -135,6 +139,8 @@ ci-finmap: ci-mathcomp_1
ci-bigenough: ci-mathcomp_1
ci-analysis: ci-elpi_hb ci-finmap ci-bigenough

ci-hb: ci-elpi

ci-elpi_test: ci-elpi_hb
ci-hb_test: ci-elpi_hb

Expand Down Expand Up @@ -167,6 +173,10 @@ ci-serapi_test: ci-mathcomp_1 ci-serapi

ci-coq_lsp: ci-serapi

# Virtual targets used by the CI to group compilation of rules in a single job

ci-elpi_hb: ci-elpi ci-hb

# Generic rule, we use make to ease CI integration
$(CI_TARGETS): ci-%:
+./dev/ci/ci-wrapper.sh $*
Expand All @@ -178,6 +188,7 @@ $(CI_TARGETS): ci-%:
NON_CI_GOALS:=$(strip $(filter-out ci-%,$(MAKECMDGOALS)))
ifneq (,$(NON_CI_GOALS))
$(CI_TARGETS): $(NON_CI_GOALS)
$(CI_VIRTUAL_TARGETS): $(NON_CI_GOALS)
endif

# For emacs:
Expand Down
16 changes: 16 additions & 0 deletions dev/ci/ci-elpi.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
#!/usr/bin/env bash

set -e

ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"

git_download elpi

if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi

( cd "${CI_BUILD_DIR}/elpi"
make build-core
make build-apps
make install
)
7 changes: 0 additions & 7 deletions dev/ci/ci-elpi_hb.sh → dev/ci/ci-hb.sh
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,10 @@ set -e
ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"

git_download elpi
git_download hierarchy_builder

if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi

( cd "${CI_BUILD_DIR}/elpi"
make build-core
make build-apps
make install
)

( cd "${CI_BUILD_DIR}/hierarchy_builder"
make config
make build
Expand Down

0 comments on commit 9954d73

Please sign in to comment.