Use shared support for running cpp2v via docker

.gitignore

@@ -14,6 +14,3 @@ mutexes.pdf
 mutexes.synctex.gz
 comment.cut
 _RocqProject
-
-# Only at the root, since it comes from enabling `dune.disabled` locally
-/dune

README.md

@@ -7,30 +7,14 @@ Specifications of the C++ standard library in BRiCk.
 To develop on these specifications, you'll need clang, the GNU C++ library (not
 clang's own version), and Skylabs AI's verification toolchain.
 
-With access to our release image, you can:
-- Open this repo in a devcontainer using our Docker release image; see `.devcontainer/README.md`.
-
 If you have access to our automation sources, you can check this out as part of
 https://github.com/SkyLabsAI/workspace. After `make vendored-pull fmdeps-pull`,
-you'll find a copy of this repository in `fmdeps/brick-libcpp`. Then:
-
-- on Linux with a suitable clang + GNU C++ library toolchain, you can build this
-  directly.
-- on any platform, you can route AST generation through our Docker image. Use
-  this route when local AST generation fails because libstdc++ headers such as
-  `<cassert>` cannot be found.
+you'll find a copy of this repository in `fmdeps/brick-libcpp`. Build from the
+composed workspace root:
 
-To enable Docker-backed AST generation in the composed workspace, go to
-`workspace` and run
+```sh
+dune build fmdeps/brick-libcpp
 ```
-cd fmdeps/brick-libcpp; cp dune.disabled dune
-```
-
-The copied `dune` file is a local, ignored opt-in. It makes Dune use
-`rocq-brick-libstdcpp/cpp2v_docker` as `cpp2v` for the libstdc++ specs and
-tests, so Docker must be running and accessible to the build.
 
-The setup can be especially useful when one needs to use `libstdc++`
-which is not available on all platforms. To reduce demands on the
-docker virtual machines, one can enable its use selectively. See
-`rocq-brick-libstdcpp/cpp2v_docker.in` for more details.
+For Docker-backed builds, see the
+[BRiCk Docker setup documentation](https://github.com/SkyLabsAI/BRiCk/blob/main/rocq-skylabs-cpp2v/scripts/README.md).

rocq-brick-libstdcpp/dune

@@ -1,35 +1,24 @@
 (rule
- (target cpp2v_docker)
+ (target cpp_environment)
  (deps
   (universe)
-  (:sha1sum %{bin:sha1sum})
-  (:template cpp2v_docker.in))
+  (env_var CPP2V_DOCKER_ENABLED)
+  (env_var CPP2V_DOCKER_IMAGE)
+  (env_var CPP2V_DOCKER_USER))
  (action
-  (progn
-   (with-stdout-to
-    %{target}
-    (bash
-     "set -eu
-hash=$(%{sha1sum} %{bin:cpp2v} | cut -d ' ' -f 1)
-image_id=
-if command -v docker >/dev/null 2>&1; then
-  image_id=$(docker inspect --format='{{.Id}}' %{env:CPP2V_DOCKER_IMAGE=} 2>/dev/null || true)
-fi
-sed -e \"s/@CPP2V_SHA1@/$hash/g\" -e \"s/@CPP2V_DOCKER_IMAGE_ID@/$image_id/g\" %{template}"))
-   (run chmod +x %{target}))))
+  (with-stdout-to %{target}
+   (run %{bin:cpp2v-toolchain} configure
+    --default-image skylabsai/fm-releases:fm-release-nightly
+    --platform linux/amd64 --opam))))
 
 (env
  (sl_timing
   (binaries (../../BRiCk/rocq-tools/bin/rocq_perf.exe as rocq))
-  (env-vars
-   (CPP2V_DOCKER_IMAGE "skylabsai/fm-releases:fm-release-nightly"))
   (rocq
    (rocqdep_flags :standard -w +all)
    (flags :standard %{read-lines:flags/coqc} -w +sl-transparent-constants)))
  ; Same, but without rocq_perf
  (_
-  (env-vars
-   (CPP2V_DOCKER_IMAGE "skylabsai/fm-releases:fm-release-nightly"))
   (rocq
    (rocqdep_flags :standard -w +all)
    (flags :standard %{read-lines:flags/coqc} -w +sl-transparent-constants))))

rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh

@@ -3,7 +3,7 @@
 
 usage() {
 	cat >&2 <<-EOF
-		usage: $(basename "$0") [ -t ] <filename>.<ext> <cpp2v-options> -- [ <clang-options> ]
+		usage: $(basename "$0") [ --toolchain CONFIG ] [ -t ] <filename>.<ext> <cpp2v-options> -- [ <clang-options> ]
 
 		This will output (to stdout) dune rules for building <filename>.<ext>,
 		passing <options> to cpp2v. Redirect output to dune.inc and
@@ -39,7 +39,13 @@ outRule() {
 	# if [ "$system" = 1 ]; then
 	# 	universe=" (universe)"
 	# fi
-	local cpp2v="cpp2v -v %{input} -o ${module} --no-elaborate"
+	local cpp2v="cpp2v"
+	local action_indent=$'\t '
+	if [ -n "$toolchain" ]; then
+		action_indent=" "
+		cpp2v="%{bin:cpp2v-run} --config %{dep:${toolchain}} --host-tool %{bin:cpp2v} --container-tool cpp2v --"
+	fi
+	cpp2v="${cpp2v} -v %{input} -o ${module} --no-elaborate"
 
 	if [ "$gen_names" = 1 ]; then
 		local names="${name}_${ext}_names.v"
@@ -61,10 +67,9 @@ outRule() {
 		 (alias test_ast)
 		 (deps
 		  (:input ${name}.${ext})
-		  (env_var CPP2V_DOCKER_ENABLED)
 		  (glob_files_rec ${prefix}*.hpp)${universe})
 		 (action
-		 	 (with-stderr-to ${module}.stderr ${action})))
+		 ${action_indent}(with-stderr-to ${module}.stderr ${action})))
 		(alias (name srcs) (deps ${name}.${ext}))
 	EOF
 	# TODO: maybe drop @srcs alias, seems leftover from !2613
@@ -85,7 +90,12 @@ traverse() {
 		#echo DIR $firstDir
 		#echo REST $rest
 		echo "${indent}(subdir ${firstDir}"
-		(cd "${firstDir}"; traverse " $indent" "$rest" "$@")
+		(
+			cd "${firstDir}" || exit
+			# Resolve CONFIG relative to each generated subdir scope.
+			case "$toolchain" in ""|/*) ;; *) toolchain="../$toolchain" ;; esac
+			traverse " $indent" "$rest" "$@"
+		) || return
 		echo "${indent})"
 	fi
 }
@@ -94,9 +104,15 @@ gen_names=0
 templates=0
 system=0
 prefix="../"
+toolchain=""
 while :
 do
 	case "$1" in
+	--toolchain)
+		[ $# -ge 2 ] && [ -n "$2" ] || usage
+		toolchain="$2"
+		shift 2
+		;;
 	-n)
 		gen_names=1
 		shift

rocq-brick-libstdcpp/proof/dune

@@ -37,6 +37,17 @@
  ))
 (include dune.inc)
 
+; Expose the existing configuration once for configured inline quotations in
+; this theory and its clients. The .v target orders generation before rocq dep.
+(rule
+ (targets cpp_environment cpp_environment_dependency.v)
+ (deps (:config ../cpp_environment))
+ (action
+  (progn
+   (copy %{config} cpp_environment)
+   (write-file cpp_environment_dependency.v
+    "(* Builds the inline toolchain configuration before rocq dep. *)\n"))))
+
 (rule
  (action (with-stdout-to dune.inc.gen (run ./dune-gen.sh)))
  (deps (glob_files_rec *.{h,c,hpp,cpp,sh})))

rocq-brick-libstdcpp/proof/dune-gen.sh

@@ -24,5 +24,5 @@ while read i; do
   if [[ $i =~ ^./(algorithms|vector)/.* ]]; then
      args+="-t"
   fi
-  ./cpp2v-dune-gen.sh -t -s ${args} -- $i -- -std=c++20 -stdlib=libstdc++
+  ./cpp2v-dune-gen.sh --toolchain ../cpp_environment -t -s ${args} -- $i -- -std=c++20 -stdlib=libstdc++
 done