greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add Nix flake for local development without Docker/VSCode

Browse Source 
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>
This commit is contained in:
Greg Shuflin
2025-11-11 02:07:34 -08:00
parent e55da341a6
commit ac9a60d137
5 changed files with 618 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@@ -4,3 +4,6 @@ lake-packages/
**/.DS_Store
.i18n/**/*.mo
*~
# Nix flake build artifacts
.lean4game-nix/

313
FLAKE_USAGE.md Normal file
View File

@@ -0,0 +1,313 @@
# 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:
```bash
nix run
```
This single command will:
1. Set up the lean4game platform in `.lean4game-nix/`
2. Install all npm dependencies
3. Build the Lean game (if needed)
4. 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:
```bash
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:
```bash
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:
```bash
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:
```bash
setup-nng4-workspace
```
This script:
1. Copies lean4game to `.lean4game-nix/`
2. Installs npm dependencies
3. Updates Lake dependencies
4. Fetches mathlib cache (speeds up compilation significantly)
5. 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:
```bash
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:
1. **Fetches lean4game** at the matching version (v4.23.0) from GitHub
2. **Creates a development shell** with:
- Lean 4.23.0 via elan
- Node.js 20
- Build tools (git, curl, etc.)
3. **Sets up the workspace** by:
- Copying lean4game to `.lean4game-nix/` (sibling structure)
- Installing npm dependencies
- Building your game with Lake
4. **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
1. Make changes to your game code in `Game/`
2. Rebuild: `nix develop -c lake build`
3. Restart server: `nix run`
4. View changes at `http://localhost:3000/#/g/local/NNG4`
### Starting from Scratch
If you clone this repository fresh:
```bash
# 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:
```bash
nix develop
lake clean
lake build
run-nng4-server
```
### Remove Build Artifacts
```bash
# 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:
```bash
nix develop
lake exe cache get
lake build
```
### Port 3000 or 8080 already in use
Stop any other processes using these ports:
```bash
lsof -ti:3000 | xargs kill -9
lsof -ti:8080 | xargs kill -9
```
### Changes to game code not reflected
Rebuild the game:
```bash
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:
1. Edit `flake.nix`:
```nix
lean4game = {
url = "github:leanprover-community/lean4game/v4.XX.0"; # Change version
flake = false;
};
```
2. Update the lock file:
```bash
nix flake update lean4game
```
3. Rebuild:
```bash
rm -rf .lean4game-nix/
nix run
```
### Use Local lean4game Clone
If you want to develop lean4game itself, you can point to a local clone:
1. Clone lean4game:
```bash
cd ..
git clone https://github.com/leanprover-community/lean4game.git
```
2. Edit `flake.nix`:
```nix
lean4game = {
url = "path:../lean4game"; # Local path
flake = false;
};
```
3. Rebuild:
```bash
nix flake lock --update-input lean4game
nix run
```
### Multi-System Support
The flake supports:
- `x86_64-linux` (tested)
- `aarch64-linux`
- `x86_64-darwin` (macOS Intel)
- `aarch64-darwin` (macOS Apple Silicon)
All platforms should work identically.
## Contributing
When contributing changes:
1. **Keep flake.nix in sync** with the Lean version in `lean-toolchain`
2. **Commit flake.lock** to ensure reproducible builds
3. **Test with** `nix flake check` before committing
## Resources
- [Nix Flakes Manual](https://nixos.org/manual/nix/stable/command-ref/new-cli/nix3-flake.html)
- [lean4game Documentation](https://github.com/leanprover-community/lean4game)
- [NNG4 README](./README.md)
- [Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)

10
README.md
View File

@@ -13,6 +13,16 @@ You can develop the game as any lean project and use `lake build` to build it.
Moreover, there are multiple ways to run the game while developing it, which are described in
[Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
### Nix Flake
If you use Nix, you can run the game locally without Docker or VSCode:
```bash
nix run # Start the game server at http://localhost:3000
```
See [FLAKE_USAGE.md](./FLAKE_USAGE.md) for complete documentation.
## Contributing
PRs/Issues fixing typos, inconsistencies, missing hints, etc. are very welcome!

79
flake.lock generated Normal file
View File

@@ -0,0 +1,79 @@
{
"nodes": {
"flake-utils": {
"inputs": {
"systems": "systems"
},
"locked": {
"lastModified": 1731533236,
"narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"lean4game": {
"flake": false,
"locked": {
"lastModified": 1758355902,
"narHash": "sha256-SPgCAddEXtHhXC8AqkLw+MwwCr8186Sot5k4ePxu0mQ=",
"owner": "leanprover-community",
"repo": "lean4game",
"rev": "36aa0824532ba3a3788d6d2e7cf72905e891cf14",
"type": "github"
},
"original": {
"owner": "leanprover-community",
"ref": "v4.23.0",
"repo": "lean4game",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1762596750,
"narHash": "sha256-rXXuz51Bq7DHBlfIjN7jO8Bu3du5TV+3DSADBX7/9YQ=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "b6a8526db03f735b89dd5ff348f53f752e7ddc8e",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-utils": "flake-utils",
"lean4game": "lean4game",
"nixpkgs": "nixpkgs"
}
},
"systems": {
"locked": {
"lastModified": 1681028828,
"narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
"owner": "nix-systems",
"repo": "default",
"rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
"type": "github"
},
"original": {
"owner": "nix-systems",
"repo": "default",
"type": "github"
}
}
},
"root": "root",
"version": 7
}

213
flake.nix Normal file
View File

@@ -0,0 +1,213 @@
{
description = "Lean4 Natural Number Game - Development Environment";
inputs = {
nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
flake-utils.url = "github:numtide/flake-utils";
# Fetch lean4game at the matching version
lean4game = {
url = "github:leanprover-community/lean4game/v4.23.0";
flake = false;
};
};
outputs = { self, nixpkgs, flake-utils, lean4game }:
flake-utils.lib.eachDefaultSystem (system:
let
pkgs = nixpkgs.legacyPackages.${system};
# Node.js 20 to match Docker setup
nodejs = pkgs.nodejs_20;
# Lean toolchain (we'll use elan to manage it)
elan = pkgs.elan;
# Helper script to set up the workspace
setupWorkspace = pkgs.writeShellScriptBin "setup-nng4-workspace" ''
set -e
WORKSPACE_ROOT="$(pwd)"
GAME_DIR="$WORKSPACE_ROOT"
LEAN4GAME_DIR="$WORKSPACE_ROOT/.lean4game-nix"
echo "Setting up NNG4 workspace..."
# Create lean4game directory if it doesn't exist
if [ ! -d "$LEAN4GAME_DIR" ]; then
echo "Copying lean4game to $LEAN4GAME_DIR..."
cp -r ${lean4game} "$LEAN4GAME_DIR"
chmod -R u+w "$LEAN4GAME_DIR"
fi
# Install npm dependencies in lean4game
if [ ! -d "$LEAN4GAME_DIR/node_modules" ]; then
echo "Installing npm dependencies in lean4game..."
cd "$LEAN4GAME_DIR"
npm install
fi
# Set up Lean toolchain
cd "$GAME_DIR"
if [ ! -d ".lake" ]; then
echo "Setting up Lean dependencies..."
echo "This may take a while on first run..."
# Update Lake dependencies
lake update -R
# Fetch mathlib cache (speeds up build significantly)
echo "Fetching mathlib cache..."
lake exe cache get || echo "Warning: Failed to fetch cache, build will be slower"
# Build the game
echo "Building the game..."
lake build
else
echo "Lake dependencies already set up. Run 'lake clean && lake build' to rebuild."
fi
echo ""
echo "✓ Workspace setup complete!"
echo ""
echo "To start the game server, run:"
echo " nix run"
echo ""
echo "Or manually:"
echo " cd .lean4game-nix && npm start"
'';
# Script to run the game server
runGameServer = pkgs.writeShellScriptBin "run-nng4-server" ''
set -e
WORKSPACE_ROOT="$(pwd)"
GAME_DIR="$WORKSPACE_ROOT"
LEAN4GAME_DIR="$WORKSPACE_ROOT/.lean4game-nix"
# Ensure workspace is set up
if [ ! -d "$LEAN4GAME_DIR/node_modules" ]; then
echo "Workspace not set up. Running setup..."
setup-nng4-workspace
fi
# Get the game name from the directory
GAME_NAME=$(basename "$GAME_DIR")
echo "Starting NNG4 game server..."
echo "Game: $GAME_NAME"
echo ""
cd "$LEAN4GAME_DIR"
# Set environment variables for single-game mode
export VITE_LEAN4GAME_SINGLE=true
export VITE_LEAN4GAME_SINGLE_NAME="$GAME_NAME"
export NODE_ENV=development
# Start the server
echo "Server will be available at: http://localhost:3000/#/g/local/$GAME_NAME"
echo ""
npm start
'';
# Build derivation for the game
buildGame = pkgs.stdenv.mkDerivation {
pname = "nng4";
version = "4.23.0";
src = ./.;
nativeBuildInputs = [
elan
pkgs.git
pkgs.curl
];
buildPhase = ''
# Set up elan home
export ELAN_HOME=$TMPDIR/elan
export PATH="$ELAN_HOME/bin:$PATH"
# Lake will read the lean-toolchain file
lake update -R
# Try to fetch cache (may fail, that's ok)
lake exe cache get || echo "Cache fetch failed, continuing..."
# Build the game
lake build
'';
installPhase = ''
mkdir -p $out
cp -r .lake $out/
cp -r Game $out/
cp Game.lean $out/
cp lakefile.lean $out/
cp lean-toolchain $out/
'';
};
in {
# Development shell with all tools
devShells.default = pkgs.mkShell {
buildInputs = [
# Lean toolchain
elan
# Node.js and npm
nodejs
# Build tools
pkgs.git
pkgs.curl
pkgs.cacert
# Helper scripts
setupWorkspace
runGameServer
];
shellHook = ''
echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
echo " Lean4 Natural Number Game - Development Environment"
echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
echo ""
echo "Available commands:"
echo " setup-nng4-workspace - Set up lean4game and build the game"
echo " run-nng4-server - Start the game server"
echo " lake - Lean build tool"
echo " elan - Lean toolchain manager"
echo ""
echo "Quick start:"
echo " 1. setup-nng4-workspace (first time only, ~5-15 min)"
echo " 2. run-nng4-server (start the game)"
echo ""
echo "Or use:"
echo " nix run (does both steps)"
echo ""
# Set up elan environment
export ELAN_HOME="$HOME/.elan"
export PATH="$ELAN_HOME/bin:$PATH"
# Ensure elan is initialized
if [ ! -d "$ELAN_HOME" ]; then
echo "Initializing elan..."
elan default stable
fi
'';
};
# Default package - builds the game
packages.default = buildGame;
# Run app - starts the game server
apps.default = {
type = "app";
program = "${runGameServer}/bin/run-nng4-server";
};
}
);
}