diff --git a/.gitignore b/.gitignore
index 9db2c48a6d4d5b5a7b959467112a00f777d7d6ad..9de11b1409ae1bc46101579057c01af6272b655c 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 f68c0e0a01e8e17740889a8756785d4d56d782d9..0db5e979dd081002ec632d3938b0b032d9cb04ed 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 ed365d8c51ad496619c001ffd34e66acacbf2ad0..4dffb482a5ee73ea1f99016e15249a8e0f4ba548 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 fae6a0d6fc0aa561a018122f204605b89a6ed579..0dbcbf518ccb628f7365012e5096118b567c8994 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"