From 053b37d34e82b92d133372cf18c4df107b4adf9f Mon Sep 17 00:00:00 2001
From: Cole Schlesinger <63367934+thatplguy@users.noreply.github.com>
Date: Tue, 9 Jul 2024 17:34:10 -0700
Subject: [PATCH] Add `make check` target (#14)

Adds `make check`, `make check-tutorial` and `make check-archive` targets. Also makes it possible to call these targets non-locally eg. `make -f some/path/cn-tutorial/Makefile check`

(Note that other targets do not work unless called locally)

---------

Co-authored-by: Mike Dodds <miked@galois.com>
---
 Makefile                         | 20 +++++++++++++++++++-
 README.md                        |  8 ++++++--
 check.sh                         |  4 +++-
 src/example-archive/check-all.sh |  8 ++++----
 4 files changed, 32 insertions(+), 8 deletions(-)

diff --git a/Makefile b/Makefile
index a446ce7e..c8fa399f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,6 @@
-.PHONY: default clean exercises 
+.PHONY: default check-archive check-tutorial check clean exercises
+
+MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 default: build exercises build/tutorial.html build/exercises.zip
 
@@ -39,6 +41,22 @@ build/solutions/%: src/examples/%
 build/exercises.zip: $(EXERCISES)
 	cd build; zip -r exercises.zip exercises > /dev/null
 
+
+##############################################################################
+# Check that the examples all run correctly 
+
+CN_PATH ?= cn 
+
+check-archive: 
+	@echo Check archive examples
+	@$(MAKEFILE_DIR)/src/example-archive/check-all.sh "$(CN_PATH)"
+
+check-tutorial:
+	@echo Check tutorial examples
+	@$(MAKEFILE_DIR)/check.sh "$(CN_PATH)"
+
+check: check-tutorial check-archive 
+
 ##############################################################################
 # Tutorial document
 
diff --git a/README.md b/README.md
index a33ace09..a94df9b7 100644
--- a/README.md
+++ b/README.md
@@ -8,8 +8,12 @@ Install dependencies: [asciidoctor](https://asciidoctor.org/).
 
 Run `make` to produce `build/tutorial.html` and its dependencies: especially, `build/exercises/*.c` and `build/solutions/*c`.
 
-Run `./check.sh` to check that all examples have working solutions (except tests with names `*.broken.c`, which are expected to fail). Note that this step will not work until after you have installed CN, which is the first part of the tutorial.
+Run `make check-tutorial` to check that all examples in the tutorial have working solutions (except tests with names `*.broken.c`, which are expected to fail). Note that this step will not work until after you have installed CN, which is the first part of the tutorial.
+
+Run `make check` to checks both the tutorial and archive examples (see below). 
 
 ## CN Example Archive 
 
-The subdirectory `src/example-archive` includes many more examples of CN proofs, both working and broken. See [the README](./src/example-archive/README.md) for a description how these examples are organized and instructions for running CN on them. 
+The subdirectory `src/example-archive` includes many more examples of CN proofs, both working and broken. See [the README](./src/example-archive/README.md) for a description how these examples are organized. 
+
+Run `make check-archive` to check all examples in the example archive. 
\ No newline at end of file
diff --git a/check.sh b/check.sh
index 3a3f198a..3b4c51d8 100755
--- a/check.sh
+++ b/check.sh
@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 
+SCRIPT_DIR="$(dirname "$(readlink -f "$0")")"
+
 if [ -n "$1" ]
 then
     echo "using CN=$1 in $PWD"
@@ -11,7 +13,7 @@ fi
 good=0
 bad=0
 
-for file in src/examples/*c;
+for file in $SCRIPT_DIR/src/examples/*c;
 do
     echo "Checking $file ..."
     $CN $file 
diff --git a/src/example-archive/check-all.sh b/src/example-archive/check-all.sh
index e05c55e8..2784fb3e 100755
--- a/src/example-archive/check-all.sh
+++ b/src/example-archive/check-all.sh
@@ -1,5 +1,7 @@
 #!/usr/bin/env bash 
 
+SCRIPT_DIR="$(dirname "$(readlink -f "$0")")"
+
 if [ -n "$1" ]
 then
     echo "check-all.sh: using CN=$1 in $PWD"
@@ -21,16 +23,14 @@ subdirs=(
 FAILURE=0 
 
 for subdir in "${subdirs[@]}"; do
-  cd "$subdir" || continue
+  cd "$SCRIPT_DIR/$subdir" || continue
 
-  ../check.sh "$CN" 
+  ../check.sh "$CN"
 
   if [ $? != 0 ]
   then 
     FAILURE=1
   fi 
-
-  cd ..
 done
 
 if [ $FAILURE -eq 0 ];