Makefile

# Options added to the autogenerated `everything.lagda.md` file.
# We put options that apply to all files into the `agda-unimath.agda-lib` file,
# but there are some options that we want to enable only for specific source
# files, and if these options are pervasive (i.e. they need to be enabled in all
# modules that include the modules that have them enabled), then they need to be
# added to the everything file as well.
everythingOpts := --guardedness --cohesion --flat-split
# use "$ export AGDAVERBOSE=-v20" if you want to see all
AGDAVERBOSE ?= -v1
AGDARTS := +RTS -M4.0G -RTS
AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)
CONTRIBUTORS_FILE := CONTRIBUTORS.toml

# All our code is in literate Agda, so we could set highlight=code and drop the
# css flag, which only affects how files with the .agda extension are processed.
# However, the HTML backend also processes referenced library files
# (Agda.Primitive at the time of writing), which is a pure Agda file, and
# setting higlight=code would make it not recognized as code at all, so the
# resulting page looks garbled. With highlight=auto and the default Agda.css, it
# at is at least in a proper code block with syntax highlighting, albeit without
# the agda-unimath chrome.
AGDAHTMLFLAGS ?= --html --html-highlight=auto --html-dir=docs --css=website/css/Agda.css --only-scope-checking
AGDA ?= agda $(AGDAVERBOSE) $(AGDARTS)
TIME ?= time

METAFILES := \
  ART.md \
  CITE-THIS-LIBRARY.md \
  CODINGSTYLE.md \
  CONTRIBUTING.md \
  CONTRIBUTORS.md \
  FILE-CONVENTIONS.md \
  DESIGN-PRINCIPLES.md \
  GRANT-ACKNOWLEDGEMENTS.md \
  HOME.md \
  HOWTO-INSTALL.md \
  LICENSE.md \
  MIXFIX-OPERATORS.md \
  MAINTAINERS.md \
  README.md \
  STATEMENT-OF-INCLUSION.md \
  SUMMARY.md \
  TEMPLATE.lagda.md \
  USERS.md \

.PHONY: agdaFiles
agdaFiles:
	@rm -rf $@
	@rm -rf ./src/everything.lagda.md
	@git ls-files src | grep '\.lagda.md$$' > $@
	@sort -o $@ $@
	@wc -l $@
	@echo "$(shell (git ls-files src | grep '.lagda.md$$' | xargs cat) | wc -l) LOC"

.PHONY: ./src/everything.lagda.md
src/everything.lagda.md: agdaFiles
	@echo "\`\`\`agda" > $@ ;\
	echo "{-# OPTIONS $(everythingOpts) #-}" >> $@ ;\
	echo "" >> $@ ;\
	echo "module everything where" >> $@ ;\
	cat agdaFiles \
		| cut -c 5-               \
		| cut -f1 -d'.'           \
		| sed 's/\//\./g'         \
		| awk 'BEGIN { FS = "."; OFS = "."; lastdir = "" } { if ($$1 != lastdir) { print ""; lastdir = $$1 } print "open import " $$0 }' \
		>> $@ ;\
	echo "\`\`\`" >> $@ ;

.PHONY: check
check: ./src/everything.lagda.md
	${TIME} ${AGDA} $?

agda-html: ./src/everything.lagda.md
	@rm -rf ./docs/
	@mkdir -p ./docs/
	@${AGDA} ${AGDAHTMLFLAGS} ./src/everything.lagda.md

SUMMARY.md: ${AGDAFILES} ./scripts/generate_main_index_file.py
	@python3 ./scripts/generate_main_index_file.py

MAINTAINERS.md: ${CONTRIBUTORS_FILE} ./scripts/generate_maintainers.py
	@python3 ./scripts/generate_maintainers.py

CONTRIBUTORS.md: ${AGDAFILES} ${CONTRIBUTORS_FILE} ./scripts/generate_contributors.py
	@python3 ./scripts/generate_contributors.py

website/css/Agda-highlight.css: ./scripts/generate_agda_css.py ./theme/catppuccin.css
	@python3 ./scripts/generate_agda_css.py

.PHONY: website-prepare
website-prepare: agda-html ./SUMMARY.md ./CONTRIBUTORS.md ./MAINTAINERS.md ./website/css/Agda-highlight.css
	@cp $(METAFILES) ./docs/
	@mkdir -p ./docs/website
	@cp -r ./website/images ./docs/website/
	@cp -r ./website/css ./docs/website/
	@cp -r ./website/js ./docs/website/
	@cp -r ./tables ./docs

.PHONY: website
website: website-prepare
	@mdbook build

.PHONY: serve-website
serve-website: website-prepare
	@mdbook serve -p 8080 --open -d ./book/html

docs/dependency.dot : ./src/everything.lagda.md ${AGDAFILES}
	${AGDA} ${AGDAHTMLFLAGS} --dependency-graph=$@ $<

.PHONY: graph
graph: docs/dependency.dot

.PHONY: clean
clean:
	@rm -Rf ./_build/ ./book/ ./docs/

.PHONY: pre-commit
pre-commit:
	@pre-commit run --all-files
	@echo
	@echo Typechecking library
	@make check

# Keep versions in sync with .github/workflows/pages.yaml
install-website-dev:
	@cargo install mdbook@0.4.34
	@cargo install mdbook-linkcheck@0.7.7
	@cargo install mdbook-katex@0.5.7
	@cargo install mdbook-pagetoc@0.1.7
	@cargo install mdbook-catppuccin@1.2.0

.PHONY: unused-imports
unused-imports:
	python3 ./scripts/remove_unused_imports.py
	python3 ./scripts/demote_foundation_imports.py