From fd6e3bdbefbc014eb4eb68f213269b298e118f6c Mon Sep 17 00:00:00 2001
From: Zhaofeng Li <hello@zhaofeng.li>
Date: Fri, 30 Aug 2024 12:32:10 -0400
Subject: [PATCH] Add CI-agnostic helper scripts

---
 .ci/.gitignore     |  1 +
 .ci/cache-shell.sh |  5 +++++
 .ci/common.sh      |  7 +++++++
 .ci/run            | 10 ++++++++++
 4 files changed, 23 insertions(+)
 create mode 100644 .ci/.gitignore
 create mode 100755 .ci/cache-shell.sh
 create mode 100644 .ci/common.sh
 create mode 100755 .ci/run

diff --git a/.ci/.gitignore b/.ci/.gitignore
new file mode 100644
index 0000000..1fd44ac
--- /dev/null
+++ b/.ci/.gitignore
@@ -0,0 +1 @@
+/cached-shell
diff --git a/.ci/cache-shell.sh b/.ci/cache-shell.sh
new file mode 100755
index 0000000..b810324
--- /dev/null
+++ b/.ci/cache-shell.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+source "$(dirname "${BASH_SOURCE[0]}")/common.sh"
+
+>&2 echo "Caching dev shell"
+nix print-dev-env "${base}#" >"${cached_shell}"
diff --git a/.ci/common.sh b/.ci/common.sh
new file mode 100644
index 0000000..1c8d67c
--- /dev/null
+++ b/.ci/common.sh
@@ -0,0 +1,7 @@
+# Use as:
+#
+# source "$(dirname "${BASH_SOURCE[0]}")/common.sh"
+
+set -euo pipefail
+base="$(readlink -f $(dirname "${BASH_SOURCE[0]}")/..)"
+cached_shell="${base}/.ci/cached-shell"
diff --git a/.ci/run b/.ci/run
new file mode 100755
index 0000000..67b60b0
--- /dev/null
+++ b/.ci/run
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+source "$(dirname "${BASH_SOURCE[0]}")/common.sh"
+
+if [[ ! -f "${cached_shell}" ]]; then
+	>&2 echo "No cached shell in ${cached_shell}"
+	exit 1
+fi
+
+. "${cached_shell}"
+exec "$@"