From 9f99f33f7e8f30cf94ed041c7432fb26f23af70f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 23 Jul 2021 10:45:00 +0200
Subject: [PATCH] Makefile: allow alectryon to work in parallel
---
.gitignore | 1 +
.gitlab-ci.yml | 4 +---
scripts/Makefile.alectryon | 8 +++++---
scripts/alectryon.sh | 2 +-
4 files changed, 8 insertions(+), 7 deletions(-)
diff --git a/.gitignore b/.gitignore
index 9db2c48a6..9de11b140 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,4 @@ Makefile*
*.DS_Store
/proof-state
/with-proof-state
+/html-alectryon
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index f68c0e0a0..0db5e979d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -211,9 +211,7 @@ proof-state:
script:
- eval $(opam env "--switch=${COMPILER_EDGE}" --set-switch)
- ./create_makefile.sh --without-classic
- - make -j ${NJOBS}
- - make alectryon
- - mv html html-alectryon
+ - make -j ${NJOBS} alectryon
artifacts:
name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
paths:
diff --git a/scripts/Makefile.alectryon b/scripts/Makefile.alectryon
index ed365d8c5..4dffb482a 100644
--- a/scripts/Makefile.alectryon
+++ b/scripts/Makefile.alectryon
@@ -1,4 +1,6 @@
-alectryon: $(GLOBFILES) $(VFILES)
- $(SHOW)'Running alectryon on all .v files'
- $(HIDE)scripts/alectryon.sh $(VFILES)
+ALECTRYONFILES = $(patsubst %,html-alectryon/prosa.%,$(subst /,.,$(subst ./,,$(VFILES:.v=.html))))
+html-alectryon/%.html: $(VOFILES)
+ $(HIDE)scripts/alectryon.sh $(patsubst %,%.v,$(subst html-alectryon/prosa/,,$(subst .,/,$(@:.html=))))
+
+alectryon: $(ALECTRYONFILES)
diff --git a/scripts/alectryon.sh b/scripts/alectryon.sh
index fae6a0d6f..0dbcbf518 100755
--- a/scripts/alectryon.sh
+++ b/scripts/alectryon.sh
@@ -2,7 +2,7 @@
set -e
ALE="alectryon"
-OUT="./html"
+OUT="./html-alectryon"
mkdir -p "$OUT"
--
GitLab