Lab 2025 (#362)

* Fix matches against emp

* Handle commands that have both success and error results

* Attempt to produce binaries in CI

* CI refactor

* Attempt to improve Docker CI

Author: NatKarmios

.github/workflows/ci.yml

@@ -1,5 +1,5 @@
 ifdef GITHUB_ACTIONS
-	VERIFY=opam exec -- gillian-c verify
+	VERIFY=gillian-c verify
 else
 	VERIFY=dune exec -- gillian-c verify
 endif
@@ -53,4 +53,4 @@ t:
 		header.c edk.c array_list.c ec.c byte_buf.c \
 		hash_table.c string.c allocator.c \
 		error.c base.c \
-		--fstruct-passing --no-lemma-proof --proc aws_cryptosdk_hdr_parse -l disabled --dump-smt
+		--fstruct-passing --no-lemma-proof --proc aws_cryptosdk_hdr_parse -l disabled --dump-smt

Dockerfile

@@ -1,5 +1,5 @@
 ifdef GITHUB_ACTIONS
-	ACT=opam exec -- gillian-c act
+	ACT=gillian-c act
 else
 	ACT=dune exec -- gillian-c act
 endif
@@ -12,4 +12,4 @@ default:
 		--fstruct-passing --ignore-undef --specs-to-stdout -l disabled
 
 clean:
-	rm -rf *.i *.deps
+	rm -rf *.i *.deps

Gillian-C/examples/amazon/Makefile

@@ -2,7 +2,7 @@
 
 set -e
 
-ACT="opam exec -- gillian-c act"
+ACT="gillian-c act"
 
 echo "--- bi-abducing SLL ---"
 time $ACT act/sll.c -l disabled
@@ -26,4 +26,4 @@ printf "\n\n"
 
 echo "--- bi-abducing BST ---"
 time $ACT act/bst.c -l disabled
-printf "\n\n"
+printf "\n\n"

Gillian-C/examples/amazon_bi/Makefile

@@ -1,3 +1,3 @@
 #!/bin/bash
 
-opam exec -- gillian-c bulk-exec concrete
+gillian-c bulk-exec concrete

Gillian-C/scripts/testACT.sh

@@ -3,7 +3,7 @@
 folder=$1
 count=$2
 
-WPST="opam exec -- gillian-c wpst"
+WPST="gillian-c wpst"
 
 for filename in $folder/*.c; do
     [ -f "$filename" ] || break
@@ -13,4 +13,4 @@ for filename in $folder/*.c; do
     else
         time $WPST "$filename" -l disabled
     fi
-done
+done

Gillian-C/scripts/testConcrete.sh

@@ -8,7 +8,7 @@ set -e
 # printf "\n\n"
 
 echo "--- verifying BST ---"
-opam exec -- gillian-c verify -l disabled multifile/verification/sll_a.c multifile/verification/sll_b.c
+gillian-c verify -l disabled multifile/verification/sll_a.c multifile/verification/sll_b.c
 printf "\n\n"
 
 # echo "--- bi-abducing BST ---"

Gillian-C/scripts/testFolder.sh

@@ -2,7 +2,7 @@
 
 set -e
 
-WPST="time opam exec -- gillian-c wpst"
+WPST="time gillian-c wpst"
 
 # TODO (Alexis): Make incremental analysis thread-safe to allow the use of --parallel
 echo "--- testing SLL ---"

Gillian-C/scripts/testMultifile.sh

@@ -1,6 +1,6 @@
 #!/bin/bash
 
-VERIFY="time opam exec -- gillian-c verify"
+VERIFY="time gillian-c verify"
 
 echo "--- verifying SLL ---"
 $VERIFY verification/sll.c -l disabled
@@ -16,4 +16,4 @@ printf "\n\n"
 
 echo "--- verifying sort ---"
 $VERIFY verification/sort.c -l disabled
-printf "\n\n"
+printf "\n\n"