greg/NNG

Files

Greg Shuflin ac9a60d137 Add Nix flake for local development without Docker/VSCode

Provides flake.nix with nix run, nix develop, and nix build commands.
Automatically sets up lean4game platform and starts game server at
http://localhost:3000. See FLAKE_USAGE.md for complete documentation.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude <noreply@anthropic.com>

2025-11-11 02:07:34 -08:00

6.9 KiB

Raw Permalink Blame History

Nix Flake Usage for NNG4

This flake provides a complete development and runtime environment for the Lean4 Natural Number Game without requiring Docker or VSCode.

Quick Start

The fastest way to get started:

nix run

This single command will:

Set up the lean4game platform in .lean4game-nix/
Install all npm dependencies
Build the Lean game (if needed)
Start the game server at http://localhost:3000

First run takes 5-15 minutes due to dependency downloads and Lean compilation. Subsequent runs are much faster.

Available Commands

`nix run` - Start the Game Server

Starts the complete game server with web interface:

nix run

The game will be available at: http://localhost:3000/#/g/local/NNG4

Press Ctrl+C to stop the server.

`nix develop` - Development Shell

Enter a development environment with all tools available:

nix develop

This provides:

elan - Lean toolchain manager
lake - Lean build tool
node and npm (Node.js 20)
Helper scripts (see below)

`nix build` - Build the Game

Build the Lean game and create a ./result symlink:

nix build

The compiled game will be in ./result/.

Helper Scripts

When inside nix develop, additional commands are available:

`setup-nng4-workspace`

Sets up the workspace for the first time:

setup-nng4-workspace

This script:

Copies lean4game to .lean4game-nix/
Installs npm dependencies
Updates Lake dependencies
Fetches mathlib cache (speeds up compilation significantly)
Builds the game with lake build

Note: Only needed if you want to manually set up before running the server.

`run-nng4-server`

Starts the game server:

run-nng4-server

Same as nix run but from within the dev shell.

Directory Structure

The flake sets up the following structure:

NNG4/                          # Your game repository
├── flake.nix                  # Nix flake configuration
├── flake.lock                 # Locked dependency versions
├── .lean4game-nix/            # lean4game platform (created by setup)
│   ├── client/                # React frontend
│   ├── relay/                 # Node.js relay server
│   ├── server/                # Lean GameServer
│   └── node_modules/          # npm dependencies
├── Game/                      # Your game source code
├── lakefile.lean              # Lake build configuration
└── lean-toolchain             # Lean version (v4.23.0)

How It Works

The flake:

Fetches lean4game at the matching version (v4.23.0) from GitHub
Creates a development shell with:
- Lean 4.23.0 via elan
- Node.js 20
- Build tools (git, curl, etc.)
Sets up the workspace by:
- Copying lean4game to .lean4game-nix/ (sibling structure)
- Installing npm dependencies
- Building your game with Lake
Runs the server with:
- Environment variables for single-game mode
- Relay server on port 8080
- Vite dev server on port 3000
- Lean server for proof verification

Workflow Examples

Daily Development

Make changes to your game code in Game/
Rebuild: nix develop -c lake build
Restart server: nix run
View changes at http://localhost:3000/#/g/local/NNG4

Starting from Scratch

If you clone this repository fresh:

# One command does it all:
nix run

# Or step by step:
nix develop
setup-nng4-workspace
run-nng4-server

Clean Rebuild

To force a complete rebuild:

nix develop
lake clean
lake build
run-nng4-server

Remove Build Artifacts

# Remove the lean4game platform
rm -rf .lean4game-nix/

# Remove Lean build artifacts
lake clean

# Next nix run will rebuild everything

Troubleshooting

"npm install" takes forever

This is normal on first run. The lean4game platform has 1600+ npm packages. Subsequent runs reuse the installed packages.

Mathlib builds are slow

On first build, run this to fetch prebuilt mathlib:

nix develop
lake exe cache get
lake build

Port 3000 or 8080 already in use

Stop any other processes using these ports:

lsof -ti:3000 | xargs kill -9
lsof -ti:8080 | xargs kill -9

Changes to game code not reflected

Rebuild the game:

nix develop -c lake build

Then reload the browser (hard refresh: Ctrl+Shift+R).

"Git tree is dirty" warning

This is harmless. Nix warns when the git repository has uncommitted changes. The flake still works correctly.

Technical Details

Version Pinning

Lean: 4.23.0 (from lean-toolchain)
lean4game: v4.23.0 tag (from GitHub)
Node.js: 20.x (matching Dockerfile)
npm packages: Locked in lean4game's package-lock.json

Why `.lean4game-nix/`?

The lean4game platform expects to be a sibling directory to your game. Since Nix works with immutable store paths, we copy it to a local directory that can be modified (for npm install, etc.).

Differences from Docker Setup

Docker approach:

Uses containers with Ubuntu base
Requires Docker daemon
Builds image with all dependencies
Mounts volumes for development

Nix approach:

Uses Nix store for dependencies
No daemon needed
Declarative, reproducible environment
Direct file access, no volumes

Both produce the same result: a working game server at http://localhost:3000.

Advanced Usage

Update lean4game Version

To update lean4game to a newer version:

Edit flake.nix:

lean4game = {
  url = "github:leanprover-community/lean4game/v4.XX.0";  # Change version
  flake = false;
};

Update the lock file:
```
nix flake update lean4game
```
Rebuild:
```
rm -rf .lean4game-nix/
nix run
```

Use Local lean4game Clone

If you want to develop lean4game itself, you can point to a local clone:

Clone lean4game:

cd ..
git clone https://github.com/leanprover-community/lean4game.git