Merge PR #12359: [ci] Add mit-plv/engine-bench

Reviewed-by: SkySkimmer

4 files changed, 19 insertions, 0 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 4139a0dbe5..fe8370e849 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -698,6 +698,9 @@ library:ci-coquelicot:
 library:ci-cross_crypto:
   extends: .ci-template
 
+library:ci-engine_bench:
+  extends: .ci-template
+
 library:ci-fcsl_pcm:
   extends: .ci-template
 
diff --git a/Makefile.ci b/Makefile.ci
index af92d476ba..9b7008f765 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -23,6 +23,7 @@ CI_TARGETS= \
     ci-coq_tools \
     ci-coqprime \
     ci-elpi \
+    ci-engine_bench \
     ci-ext_lib \
     ci-equations \
     ci-fcsl_pcm \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5f7d0b5789..19ba9de245 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -239,6 +239,13 @@
 : "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}"
 
 ########################################################################
+# Engine-Bench
+########################################################################
+: "${engine_bench_CI_REF:=master}"
+: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}"
+: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}"
+
+########################################################################
 # fcsl-pcm
 ########################################################################
 : "${fcsl_pcm_CI_REF:=master}"
diff --git a/dev/ci/ci-engine_bench.sh b/dev/ci/ci-engine_bench.sh
new file mode 100755
index 0000000000..fda7649f88
--- /dev/null
+++ b/dev/ci/ci-engine_bench.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download engine_bench
+
+( cd "${CI_BUILD_DIR}/engine_bench" && make coq && make coq-perf-Sanity )