The deployed website lives on the master
branch of this repository.
To make changes to the website, please fork the repository and make a PR against the
lean4
branch.
Once your PR is merged, CI will automatically deploy the changes to the master
branch.
pip install -r requirements.txt
Building the bibliography requires bibtool
.
In order to rebuild the CSS from SCSS, you also need:
The website relies on several components which are built in other repositories:
mathlib_stats
lean4web
mathlib4_docs
(built by CI in doc-gen4)
- Build CSS if needed:
sass scss/lean.scss > css/lean.css
- Build site using
make_site.py
. Use option--local
for local viewing (internal url will be prefixed by local file path). Use option--reload
to continuously build when templates are changed (this won't work for watching changes indata/
).
If you want to retrieve the list of Zulip users to get the users map, the
environment variable ZULIP_KEY
should be set with the Zulip API key of the
map scraper bot.
If you want to work on a new feature, there are several helpful tricks to know.
First you will very quickly hit the GitHub API rate limit without
authentication. You can
create a personal access token
and run GITHUB_TOKEN=my_token_copied_from_github ./make_site --local
during
your experiments.
You can also run the script once normally and then run
NODOWNLOAD=1 ./make_site --local
to build the website using the information
previously downloaded. This information is stored into the data_cache
folder.
If you need the script to download something but not everything you can
temporarily change the relevant if DOWNLOAD:
into a if not DOWNLOAD:
.
You can also choose to render only certain templates using
./make_site --local --only my_template.html
.
This argument can actually be a regular expression, but giving one template
name is the most common use case.
- Better integration with API docs
- Use webpack or similar to bundle all the javascript?
The files and history for the leanprover-community Lean 3 website can be found in the
lean3
branch of this repo.
The files and history for the old leanprover-community website can be found in the
oldsite
branch of this repo.