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 <[email protected]>
rems-project · Jul 10, 2024 · 053b37d · 053b37d
1 parent 793b9ab
commit 053b37d
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 8 deletions.
diff --git 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
@@ -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. 
diff --git 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
@@ -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 ];