Pisa

Pisa is a Django website for teachers to design and assign programming and proof assignments in Lean4, Microsoft's open-source proof assistant.

Install

This project uses Docker.

Starting the project

Build and run with Docker:

docker compose up --build

Open the app at http://127.0.0.1:8000/.

If you need to run migrations later:

docker compose exec web python manage.py migrate

To stop the environment, run:

docker compose down

Self-hosting

Pisa can run on your own server and domain with automatic HTTPS. The production stack (docker-compose.prod.yml) bundles Caddy, which fetches and renews a Let's Encrypt certificate for your domain and proxies HTTP and the Lean WebSocket to the app (served by daphne).

You need a server with Docker, ports 80 and 443 open, and a domain whose DNS A/AAAA record points at the server.

1. Configure. Copy the example env file and fill it in:

   cp .env.example .env
   # SECRET_KEY:  python -c "import secrets; print(secrets.token_urlsafe(50))"
   # PISA_DOMAIN: your hostname, e.g. lean.school.edu
   # DEBUG:       False

   Optionally set DJANGO_SUPERUSER_USERNAME / DJANGO_SUPERUSER_PASSWORD to create an admin on first boot.

2. Launch. The app container runs as a non-root user (uid/gid 1000), so ./data and ./media need to exist and be owned by that uid before the first up, or Docker creates them as root on first mount and the container can't write to them:

   mkdir -p data media
   sudo chown -R 1000:1000 data media  # skip sudo if you're already uid 1000
   docker compose -f docker-compose.prod.yml up -d --build

   The image bakes in the Lean toolchain, runs migrations, and collects static files on start; Caddy provisions TLS for PISA_DOMAIN automatically (this can take a few seconds on first run). Open https://your-domain/.

3. Create the first admin (if you didn't use the env vars above):

   docker compose -f docker-compose.prod.yml exec web python manage.py createsuperuser

Data & backups

SQLite and uploaded media live on the host in ./data and ./media; Caddy's certificates live in a Docker volume. Back up ./data, ./media, and the caddy_data volume.

Notes

• The stack runs a single app process with an in-memory channel layer and SQLite, which provides more than enough storage for a class or department. To scale across multiple processes you'd move to Postgres, a Redis channel layer, and a shared store for the per-user Lean-instance cap. See TODO.md for the deferred roadmap (scale-out, Lean performance, and more).
• Updating: git pull then re-run the up -d --build command above.

Contributing

Install Lean locally for development

If you want to run Lean on the host outside Docker, install elan:

curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh
source ~/.elan/env
lean --version

License

AGPL-3.0-or-later. See LICENSE.