Merge PR coq#18648: Add autosubst-ocaml to CI

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

.gitlab-ci.yml

@@ -865,6 +865,9 @@ plugin:ci-aac_tactics:
 plugin:ci-atbr:
   extends: .ci-template-flambda
 
+plugin:ci-autosubst_ocaml:
+  extends: .ci-template-flambda
+
 plugin:ci-itauto:
   extends: .ci-template
 

Makefile.ci

@@ -15,6 +15,7 @@ CI_TARGETS= \
     ci-async_test \
     ci-atbr \
     ci-autosubst \
+    ci-autosubst_ocaml \
     ci-bbv \
     ci-bedrock2 \
     ci-bignums \

dev/ci/ci-autosubst_ocaml.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+set -e
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download autosubst_ocaml
+
+if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
+
+export COQEXTRAFLAGS='-native-compiler no'
+( cd "${CI_BUILD_DIR}/autosubst_ocaml"
+  dune build @install -p coq-autosubst-ocaml
+  dune install -p coq-autosubst-ocaml --prefix="$CI_INSTALL_DIR"
+)

dev/ci/ci-basic-overlay.sh

@@ -524,3 +524,9 @@ project ltac2_compiler "https://github.com/SkySkimmer/coq-ltac2-compiler" "main"
 ########################################################################
 project waterproof "https://github.com/impermeable/coq-waterproof" "coq-master"
 # Contact @jellooo038, @jim-portegies on github
+
+########################################################################
+# Autosubst (2) OCaml
+########################################################################
+project autosubst_ocaml "https://github.com/uds-psl/autosubst-ocaml" "master"
+# Contact @yforster on github