fixup: make generate-everything.sh predicative

Due to the order in which shells do things, `find > foo` will find
`foo`. This means that `generate-everything.sh` puts everything on the
table including the table, resulting in a dependency cycle.

This change fixes that by excluding `Cubical/Everything.agda` from
"everything". Also sorts the modules alphabetically and makes
`make listing` display "Checking" messages so we know what it's doing.

Author: ncfavier

GNUmakefile

@@ -37,9 +37,8 @@ timings: clean
 
 .PHONY : listings
 listings: $(wildcard Cubical/**/*.agda)
-	rm -f Cubical/Everything.agda
 	./generate-everything.sh > Cubical/Everything.agda
-	$(AGDA) Cubical/Everything.agda -i. -isrc --html -v0
+	$(AGDA) Cubical/Everything.agda -i. -isrc --html -vhtml:0
 
 .PHONY : clean
 clean:

generate-everything.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env sh
 
 printf 'module Cubical.Everything where\n\n'
-find Cubical/ -type f -name "*.agda" | sed -e 's/\//./g' -e 's/\.agda$//g' -e 's/^/import /'
+find Cubical/ -type f -name "*.agda" '!' -path "Cubical/Everything.agda" | sort | sed -e 's/\//./g' -e 's/\.agda$//g' -e 's/^/import /'