Merge pull request #27 from coord-e/coord-e/include-pcsat-in-devcontainer

Enable to run all specs in DevContainer

Author: coord-e

.devcontainer/devcontainer.json

@@ -9,5 +9,8 @@
       ]
     }
   },
+  "features": {
+    "ghcr.io/devcontainers/features/docker-in-docker:2": {}
+  },
   "postCreateCommand": "rustup show"
 }

.github/workflows/ci.yml

@@ -26,32 +26,12 @@ jobs:
     permissions:
       contents: read
     env:
+      # see tests/thrust-pcsat-wrapper
       COAR_IMAGE: ghcr.io/hiroshi-unno/coar@sha256:73144ed27a02b163d1a71b41b58f3b5414f12e91326015600cfdca64ff19f011
     steps:
       - uses: actions/checkout@v4
       - uses: ./.github/actions/setup-z3
-      - name: Setup thrust-pcsat-wrapper
-        run: |
-          docker pull "$COAR_IMAGE"
-
-          cat <<"EOF" > thrust-pcsat-wrapper
-          #!/bin/bash
-
-          smt2=$(mktemp -p . --suffix .smt2)
-          trap "rm -f $smt2" EXIT
-          cp "$1" "$smt2"
-          out=$(
-            docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \
-              main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2"
-          )
-          exit_code=$?
-          echo "${out%,*}"
-          exit "$exit_code"
-          EOF
-          chmod +x thrust-pcsat-wrapper
-
-          mkdir -p ~/.local/bin
-          mv thrust-pcsat-wrapper ~/.local/bin/thrust-pcsat-wrapper
+      - run: docker pull "$COAR_IMAGE"
       - run: rustup show
       - uses: Swatinem/rust-cache@v2
       - run: cargo test

tests/thrust-pcsat-wrapper

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+COAR_IMAGE=${COAR_IMAGE:-ghcr.io/hiroshi-unno/coar:main}
+
+smt2=$(mktemp -p . --suffix .smt2)
+trap "rm -f $smt2" EXIT
+cp "$1" "$smt2"
+out=$(
+docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \
+    main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2"
+)
+exit_code=$?
+echo "${out%,*}"
+exit "$exit_code"

tests/ui/fail/annot_exists.rs

@@ -1,6 +1,6 @@
 //@error-in-other-file: Unsat
 //@compile-flags: -C debug-assertions=off
-//@rustc-env: THRUST_SOLVER=thrust-pcsat-wrapper
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
 
 #[thrust::trusted]
 #[thrust::callable]

tests/ui/pass/annot_exists.rs

@@ -1,6 +1,6 @@
 //@check-pass
 //@compile-flags: -C debug-assertions=off
-//@rustc-env: THRUST_SOLVER=thrust-pcsat-wrapper
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
 
 #[thrust::trusted]
 #[thrust::callable]