CI check for axioms and for leftover interactive commands

.github/workflows/build.yml

@@ -34,6 +34,8 @@ jobs:
         run: tools/runner.sh configure
       - name: Build
         run: tools/runner.sh build
+      - name: Hygiene
+        run: tools/runner.sh hygiene
       - name: Test default configuration
         run: tools/runner.sh test1
       - name: Test alternate configuration

Makefile

@@ -389,7 +389,12 @@ distclean:
 	rm -f Makefile.config
 
 check-admitted: $(FILES)
-	@grep -w 'admit\|Admitted\|ADMITTED' $^ || echo "Nothing admitted."
+	@if grep -w 'admit\|Admitted\|ADMITTED' $^; \
+         then exit 2; else echo "Nothing admitted."; fi
+
+check-leftovers: $(FILES)
+	@if grep -w '^Check\|^Print\|^Search' $^; \
+         then exit 2; else echo "No leftover interactive commands."; fi
 
 check-proof: $(FILES)
 	$(COQCHK) compcert.driver.Complements

tools/runner.sh

@@ -210,6 +210,12 @@ case "$target,$os" in
 esac
 }
 
+# Check for things that should not be in the Coq sources (admits, etc)
+
+Hygiene () {
+  make check-admitted && make check-leftovers
+}
+
 case "$1" in
   system_install) System_install;;
   opam_install) shift; OPAM_install "$@";;
@@ -220,6 +226,7 @@ case "$1" in
   test3) Run_test_round 3;;
   build_ccomp) Build_ccomp;;
   check_proof) Check_proof;;
+  hygiene) Hygiene;;
   *) Fatal "Unknown CI instruction: $1"; exit 1;;
 esac