test: server respecting CPATH/C_INCLUDE_PATH

test.sh

@@ -1,7 +1,10 @@
 #!/usr/bin/env bash
-set -exo pipefail
+set -euxo pipefail
 
-${LAKE:-lake} build
+LAKE=${LAKE:-lake}
+SCRIPT_DIR=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" &> /dev/null && pwd)
+
+$LAKE build
 
 pushd examples/my_add
 ./test.sh
@@ -15,6 +18,11 @@ pushd tests/compile
 ./test.sh
 popd
 
-find tests/run -type f -name "*.lean" | xargs -n1 ${LAKE:-lake} env lean
+find tests/run -type f -name "*.lean" | xargs -n1 $LAKE env lean
+
+# https://github.com/tydeu/lean4-alloy/issues/6
+$LAKE env lean tests/envIncludePath.lean && false || true
+CPATH=$SCRIPT_DIR/tests $LAKE env lean tests/envIncludePath.lean
+C_INCLUDE_PATH=$SCRIPT_DIR/tests $LAKE env lean tests/envIncludePath.lean
 
 echo "all done"

tests/envIncludePath.lean

@@ -0,0 +1,7 @@
+import Alloy.C
+open scoped Alloy.C
+
+#eval Alloy.C.addServerFlag "--language=c"
+
+set_option Alloy.shimDiagnostics.serverOnly false in
+alloy c include "includePath.h"

tests/run/includePath.lean

@@ -4,7 +4,7 @@ open Alloy.C
 open Lean Elab Command in
 #eval show CommandElabM _ from do
   let leanFile ← IO.FS.realPath <| System.FilePath.mk (← getFileName)
-  let includeDir := leanFile.parent.get!
+  let includeDir := leanFile.parent.bind (·.parent) |>.get!
   logInfo includeDir.toString
   addServerIncludePath includeDir