diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 8900bc764eb8..7d6a5cb098da 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -799,6 +799,8 @@ library:ci-vst:
   needs:
   - build:edge+flambda
   - library:ci-flocq
+  - library:ci-menhir
+  - library:ci-compcert
   timeout: 2h
 
 library:ci-deriving:
diff --git a/Makefile.ci b/Makefile.ci
index eea9b7d27053..95bca51b3861 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -157,7 +157,7 @@ ci-equations_test: ci-equations
 
 ci-metacoq: ci-equations
 
-ci-vst: ci-flocq
+ci-vst: ci-compcert
 
 ci-compcert: ci-menhir ci-flocq
 
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 9c8d12d0fec8..418289a52bd2 100644
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -9,9 +9,12 @@ git_download compcert
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
+# CompCert does compile with -native-compiler yes
+# but with excessive memory requirements
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert"
-  [ -e Makefile.config ] || ./configure -ignore-coq-version x86_32-linux -use-external-MenhirLib -use-external-Flocq
+  [ -e Makefile.config ] || ./configure -ignore-coq-version x86_32-linux -install-coqdev -clightgen -use-external-MenhirLib -use-external-Flocq -prefix ${CI_INSTALL_DIR} -coqdevdir ${CI_INSTALL_DIR}/lib/coq/user-contrib/compcert
   make
   make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)'
+  make install
 )
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index addc6a238345..14afef3d8455 100644
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -9,11 +9,13 @@ git_download vst
 
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
-export COMPCERT=bundled
+# sometimes (rarely) CompCert master can break VST and it can take
+# weeks or months for VST to catch up, in this case, just uncomment
+# the line below to use the compcert version bundled in VST
+# export COMPCERT=bundled
 
-ulimit -s
-ulimit -s 65536
-ulimit -s
+# See ci-compcert.sh
+export COQEXTRAFLAGS='-native-compiler no'
 ( cd "${CI_BUILD_DIR}/vst"
-  make IGNORECOQVERSION=true
+  make IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
 )
diff --git a/dev/ci/user-overlays/18039-proux01-vst.sh b/dev/ci/user-overlays/18039-proux01-vst.sh
new file mode 100644
index 000000000000..afb0659dffbb
--- /dev/null
+++ b/dev/ci/user-overlays/18039-proux01-vst.sh
@@ -0,0 +1 @@
+overlay vst https://github.com/proux01/VST depflags 18039