Makefile

#### Directory variables ####
SOURCE_DIR := src
SCRIPTS_DIR := scripts
# Website assets
WEBSITE_DIR := website
WEBSITE_CSS := $(WEBSITE_DIR)/css
WEBSITE_IMAGES := $(WEBSITE_DIR)/images
WEBSITE_JS := $(WEBSITE_DIR)/js
WEBSITE_THEME := website/theme

# MDBOOK directory
MDBOOK_DIR := book
# MDBOOK input, corresponds to the `src` variable in `book.toml`
MDBOOK_SRC := $(MDBOOK_DIR)/src
# Base directory where Agda interface files are stored
AGDA_BUILD := _build
# Agda profiling directory
TEMP_DIR := temp
AGDA_PROFILING_OUTPUT := $(TEMP_DIR)/typecheck_output.txt
# Docs
DOCS_DIR := docs
TABLES_DIR := $(DOCS_DIR)/tables
METAFILES := \
	CONTRIBUTING.md \
	LICENSE.md \
	README.md
# Meta
CONTRIBUTORS_FILE := CONTRIBUTORS.toml

# 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 --rewriting

# use "$ export SKIPAGDA=1" or "make SKIPAGDA=1 ..." to skip Agda processing
# when building the website
SKIPAGDA ?=

# use "$ export SKIPAUX=1" or "make SKIPAUX=1 ..." to skip generating auxiliary
# files, i.e., the Agda dependency graph SVG when building the website
SKIPAUX ?=

# When SKIPAUX=1 we don't require the auxiliary files.
ifeq ($(SKIPAUX),1)
AUX_TARGETS :=
else
AUX_TARGETS := ./$(WEBSITE_IMAGES)/agda_dependency_graph.svg ./$(WEBSITE_IMAGES)/agda_dependency_graph_legend.html
endif

ifeq ($(CI),)
	AGDA_MIN_HEAP ?= 2G
else
	AGDA_MIN_HEAP ?= 4G
endif

AGDARTS := +RTS -H$(AGDA_MIN_HEAP) -M8G -RTS
AGDAFILES := $(shell find $(SOURCE_DIR) -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)

# 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 highlight=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=$(MDBOOK_SRC) --css=$(WEBSITE_CSS)/Agda.css --only-scope-checking
AGDAPROFILEFLAGS ?= --profile=modules +RTS -s -RTS
AGDA ?= agda $(AGDARTS)
TIME ?= time

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

.PHONY: ./$(SOURCE_DIR)/everything.lagda.md
$(SOURCE_DIR)/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 " public"}' \
		>> $@ ;\
	echo "\`\`\`" >> $@ ;

.PHONY: check
check: ./$(SOURCE_DIR)/everything.lagda.md
	${TIME} ${AGDA} $?

.PHONY: check-profile
check-profile: $(SOURCE_DIR)/everything.lagda.md
	@# Remove cached build data
	@rm -Rf ./$(AGDA_BUILD)/
	${AGDA} ${AGDAPROFILEFLAGS} $<

# Convert module path to directory path (replace dots with slashes)
MODULE_DIR = $(subst .,/,$(MODULE))


# Default agda arguments for `profile-module`
PROFILE_MODULE_AGDA_ARGS ?= --profile=definitions
# Target for profiling the typechecking a single module
.PHONY: profile-module
profile-module:
	@if [ -z "$(MODULE)" ]; then \
		echo "\033[0;31mError: MODULE variable is not set.\033[0m"; \
		echo "\033[0;31mUsage: make check-module MODULE=\"YourModuleName\"\033[0m"; \
		exit 1; \
	fi
	@# Attempt to delete the interface file only if the build directory exists
	@echo "\033[0;32mAttempting to delete interface file for $(MODULE)\033[0m"
	@find ./$(AGDA_BUILD) -type f -path "*/agda/$(SOURCE_DIR)/$(MODULE_DIR).agdai" -exec rm -f {} \+ 2>/dev/null || \
		echo "\033[0;31m$(AGDA_BUILD) directory does not exist, skipping deletion of interface files.\033[0m"
	@# Ensure the temporary directory exists
	@mkdir -p ./$(TEMP_DIR)
	@# Profile typechecking the module and capture the output in the temp directory, also display on terminal
	@echo "\033[0;32mProfiling typechecking of $(MODULE)\033[0m"
	@$(AGDA) $(PROFILE_MODULE_AGDA_ARGS) $(SOURCE_DIR)/$(MODULE_DIR).lagda.md 2>&1 | tee ./$(AGDA_PROFILING_OUTPUT)
	@# Check for additional modules being typechecked by looking for any indented "Checking" line
	@if grep -E "^\s+Checking " ./$(AGDA_PROFILING_OUTPUT) > /dev/null; then \
		echo "\033[0;31mOther modules were also checked. Repeating profiling after deleting interface file again.\033[0m"; \
		find ./$(AGDA_BUILD) -type f -path "*/agda/$(SOURCE_DIR)/$(MODULE_DIR).agdai" -exec rm -f {} \+; \
		$(AGDA) $(PROFILE_MODULE_AGDA_ARGS) $(SOURCE_DIR)/$(MODULE_DIR).lagda.md; \
	else \
		echo "\033[0;32mOnly $(MODULE) was checked. Profiling complete.\033[0m"; \
	fi

	@# Cleanup
	@rm -f ./$(AGDA_PROFILING_OUTPUT)

agda-html: ./$(SOURCE_DIR)/everything.lagda.md
	@rm -rf ./$(MDBOOK_SRC)/
	@mkdir -p ./$(MDBOOK_SRC)/
# Use bash if instead of ifeq, because we want to change SKIPAGDA with rules
	@if [ -z "$(SKIPAGDA)" ];\
	then ${AGDA} ${AGDAHTMLFLAGS} ./$(SOURCE_DIR)/everything.lagda.md; \
	else python3 ./$(SCRIPTS_DIR)/generate_noagda_html.py ./$(MDBOOK_SRC)/; \
	fi

./$(MDBOOK_SRC)/SUMMARY.md: ${AGDAFILES} ./$(SCRIPTS_DIR)/generate_mdbook_summary.py
	@python3 ./$(SCRIPTS_DIR)/generate_mdbook_summary.py $@

./$(MDBOOK_SRC)/MAINTAINERS.md: ${CONTRIBUTORS_FILE} ./$(SCRIPTS_DIR)/generate_maintainers.py
	@python3 ./$(SCRIPTS_DIR)/generate_maintainers.py ${CONTRIBUTORS_FILE} $@

./$(MDBOOK_SRC)/CONTRIBUTORS.md: ${AGDAFILES} ${CONTRIBUTORS_FILE} ./$(SCRIPTS_DIR)/generate_contributors.py
	@python3 ./$(SCRIPTS_DIR)/generate_contributors.py ${CONTRIBUTORS_FILE} $@

$(WEBSITE_CSS)/Agda-highlight.css: ./$(SCRIPTS_DIR)/generate_agda_css.py ./$(WEBSITE_THEME)/catppuccin.css
	@python3 ./$(SCRIPTS_DIR)/generate_agda_css.py

$(WEBSITE_IMAGES)/agda_dependency_graph.svg $(WEBSITE_IMAGES)/agda_dependency_graph_legend.html &: ${AGDAFILES}
	@echo Generating dependency graph art by Fredrik
	@python3 ./$(SCRIPTS_DIR)/generate_dependency_graph_rendering.py $(WEBSITE_IMAGES)/agda_dependency_graph svg || true

.PHONY: website-prepare
website-prepare: agda-html ./$(MDBOOK_SRC)/SUMMARY.md ./$(MDBOOK_SRC)/CONTRIBUTORS.md ./$(MDBOOK_SRC)/MAINTAINERS.md \
								 ./$(WEBSITE_CSS)/Agda-highlight.css $(AUX_TARGETS)
	@rm -f ./docs/CONTRIBUTORS.md ./docs/MAINTAINERS.md ./docs/SUMMARY.md # Remove old autogenerated metafile copies

	@mkdir -p ./$(MDBOOK_SRC)/website

	@cp $(METAFILES) ./$(MDBOOK_SRC)/

	@# Copies the files from `$(DOCS_DIR)` to `$(MDBOOK_SRC)`, not just the literal `$(DOCS_DIR)` directory
	@# The following works consistently across BSD (MacOS) and GNU (Linux)
	@cp -r ./$(DOCS_DIR)/. ./$(MDBOOK_SRC)
	@cp -r ./$(WEBSITE_IMAGES) ./$(MDBOOK_SRC)/website
	@cp -r ./$(WEBSITE_CSS) ./$(MDBOOK_SRC)/website
	@cp -r ./$(WEBSITE_JS) ./$(MDBOOK_SRC)/website

.PHONY: website
website: website-prepare
	@MDBOOK_PREPROCESSOR__CONCEPTS__SKIP_AGDA=$(SKIPAGDA) \
		mdbook build

.PHONY: serve-website
serve-website: website-prepare
	@MDBOOK_PREPROCESSOR__CONCEPTS__SKIP_AGDA=$(SKIPAGDA) \
		mdbook serve -p 8080 --open -d ./$(MDBOOK_DIR)/html

$(MDBOOK_SRC)/dependency.dot : ./$(SOURCE_DIR)/everything.lagda.md ${AGDAFILES}
	${AGDA} ${AGDAHTMLFLAGS} --dependency-graph=$@ $<

.PHONY: graph
graph: $(MDBOOK_SRC)/dependency.dot

.PHONY: clean-website
clean-website:
	@rm -Rf ./$(MDBOOK_DIR)/ ./docs/CONTRIBUTORS.md ./docs/MAINTAINERS.md ./docs/SUMMARY.md

.PHONY: clean
clean: clean-website
	@rm -Rf ./$(AGDA_BUILD)/ ./$(TEMP_DIR)/ ./$(SOURCE_DIR)/everything.lagda.md ./$(SCRIPTS_DIR)/__pycache__

.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:
	@echo
	@echo Installing website dependencies
	@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:
	@echo
	@echo Removing unused imports
	@python3 ./$(SCRIPTS_DIR)/remove_unused_imports.py
	@echo
	@echo Demoting foundation imports
	@python3 ./$(SCRIPTS_DIR)/demote_foundation_imports.py