Additional installation instructions
The repository contains the following additional directory and files:
docs: directory for generating a websitedocs/javascripts: directory for added Javascript filesdocs/stylesheets: directory for added CSS filesdocs/.nav.yml: configuration file for navigation panelsdocs/nav.md: the home page of the generated websitedocs/installation-guide.md: this page
Makefile: automation of website generationmkdocs.yml: configuration file for the generated website
The repository does not contain any generated files.
The Makefile generates files in the docs directory:
docs/*.html: HTML filesdocs/**/index.md: Markdown files
Moreover, building and deploying the generated website creates the directories
site and temp.
When they are not needed for browsing or deploying the website, the generated
files can be removed by make -f Makefile clean-all.
The following files need to be generated or updated before checking the library code and generating a website:
Everything.agdaEverythingSafe.agdaindex.agda
To do that, run the following commands:
cp .github/tooling/index.* .
cabal run GenerateEverything
./index.sh
To avoid committing generated files to the current branch, the following lines
have been added to .gitignore:
/docs/*.css
/docs/*.html
/docs/*.js
/docs/**/index.md
/index.agda
/index.sh
/site/
Additional software dependencies
- Awesome-nav (3.2.0)
- GNU Make (3.81)
- Material for MkDocs (9.7.1)
- mike (2.0.0)
- MkDocs (1.6.1)
- pip (25.3)
- Python 3 (3.14.0)
- sd (1.0.0)
Platform dependencies
The website generation has been developed and tested on MacBook laptops with Apple M1 and M3 chips running macOS Sequoia (15.6) with CLI Tools.