workaround for html generation: simple bash script that generates a Everything.agda

Author: felixwellen

.gitignore

@@ -2,3 +2,4 @@
 *~
 \.*#*
 \#*
+/Cubical/Everything.agda

GNUmakefile

@@ -25,7 +25,7 @@ fix-whitespace:
 check-whitespace:
 	$(FIX_WHITESPACE) --check
 
-# typechecking and generating listings for all files imported in README
+# typechecking and generating listings for all files
 
 .PHONY : check
 check:
@@ -37,7 +37,9 @@ timings: clean
 
 .PHONY : listings
 listings: $(wildcard Cubical/**/*.agda)
-	$(AGDA) --build-library -i. -isrc --html -v0
+	rm -f Cubical/Everything.agda
+	./generate-everything.sh > Cubical/Everything.agda
+	$(AGDA) Cubical/Everything.agda -i. -isrc --html -v0
 
 .PHONY : clean
 clean:

README.md

@@ -1,7 +1,7 @@
 A standard library for Cubical Agda
 ===================================
 
-The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.README.html).
+The source code has a glorious clickable [rendered version](https://agda.github.io/cubical/Cubical.Everything.html).
 
 There is also a [discord server](https://discord.gg/yjTKHzepMx), shared with [agda-unimath](https://unimath.github.io/agda-unimath/) and the [1lab](https://1lab.dev/).
 

generate-everything.sh

@@ -0,0 +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 /'