Improve the error message when a file hasn't been type checked (#643)

Author: WhatisRT

default.nix

@@ -101,7 +101,7 @@ rec {
     '';
     postInstall = ''
       cp -r latex/ Makefile typecheck.time $out
-      sh checkTypeChecked.sh
+      sh checkTypeChecked.sh -m
     '';
     extraExtensions = [ "hs" "cabal" "py" ];
   };

src/checkTypeChecked.sh

@@ -4,8 +4,10 @@ echo "Checking that all Agda files have been typechecked..."
 for agdaFn in $(find . -name '*.*agda'); do
   agdaiFn="_build/2.7.0/agda/${agdaFn%.*agda}.agdai"
   if [ "$(( $(stat -c "%Y" $agdaiFn) - $(stat -c "%Y" $agdaFn) ))" -lt "0" ]; then
-    echo "        FAIL: $agdaiFn is not up-to-date"
+    if [ "$1" = "-m" ]; then
+      echo "        FAIL: $agdaiFn does not exist. Please remove the corresponding agda file or import it somewhere, e.g. from the Everything module."
+    fi
     exit 1
   fi
 done
-echo "        PASS: all Agda files have been typechecked"
+echo "        PASS: all Agda files have been typechecked."