Merge PR coq#18039: [CI] Remove fake dependency of VST on Flocq

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

.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:

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
 

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
 )

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
 )

dev/ci/user-overlays/18039-proux01-vst.sh

@@ -0,0 +1 @@
+overlay vst https://github.com/proux01/VST depflags 18039