Development Setup

Get your environment ready to explore and contribute to Cryptography Academy.

Prerequisites

  • macOS, Linux, or WSL on Windows
  • Node.js 24+ (for the website)
  • Git

1. Clone the Repository

git clone https://github.com/cryptographyacademy/cryptographyacademy.github.io.git
cd cryptographyacademy.github.io

2. Run Setup Script

The quickest way to set up everything:

./scripts/setup-all.sh
View source →

This script will:

  • Install elan (Lean version manager)
  • Download the Lean toolchain
  • Download Mathlib4 cache
  • Build the Lean project
  • Install npm dependencies
  • Build the website

Or run individual setup scripts:

./scripts/setup-lean.sh
View source → Lean setup (elan, toolchain, Mathlib) 
./scripts/setup-web.sh
View source → Web setup (Node.js, npm)

3. Verify Installation

./scripts/verify-setup.sh
View source →

4. Start Development Server

make serve

Open http://localhost:4321 in your browser.

Editor Setup

VS Code (Recommended)

  1. Install the lean4 extension (ID: leanprover.lean4)
  2. Open the lean/ folder in VS Code
  3. Wait for the Lean server to start

Neovim

Use nvim-lspconfig with the Lean 4 LSP: 

-- In your init.lua
require('lspconfig').lean4.setup

Emacs

Install lean4-mode: 

;; In your init.el
(use-package lean4-mode
  :straight (lean4-mode
             :type git
             :host github
             :repo "leanprover-community/lean4-mode"))

Available Commands

Command Description
make help Show all available commands
make build Build Lean proofs and website
make serve Start development server
make test Run all tests
make lint Run linters
make format Format code
make clean Clean build artifacts

Troubleshooting

Mathlib cache download is slow

The initial Mathlib download can take time. The cache is stored in lean/.lake/.

Lean server not starting

Make sure you're opening the lean/ directory, not the project root. The lakefile.toml must be in the root of the opened folder.

Need more help?

Open an issue on GitHub