NNG/DEBUG_NOTES.md

Debug Notes: Nix Flake Server Issues

Current Status

The Nix flake successfully sets up the environment and starts the server, but the game doesn't fully load in the browser. The page loads but displays errors.

What Works ✅

• nix develop - Development shell with all tools (elan, lake, node, npm)
• nix build - Successfully builds the Lean game
• setup-nng4-workspace - Copies lean4game, installs 1662 npm packages
• lake build - Compiles the NNG4 game successfully (286 jobs)
• Server starts on ports 3000 (Vite) and 8080 (relay)
• HTML page loads at http://localhost:3000
• i18n translation files are accessible

What's Broken ❌

• Browser shows "broken" game page with JavaScript errors
• i18next-http-backend errors in browser console
• Relay server API endpoints return 404:
  • GET /api/games → Cannot GET /api/games
  • GET /api/game/NNG4 → Cannot GET /api/game/NNG4

Root Cause Analysis

Issue 1: Missing .lake/gamedata/ directory

The game requires a .lake/gamedata/ directory with JSON files containing level metadata. This directory is NOT created by lake build.

Evidence:

$ ls .lake/gamedata/
ls: cannot access '.lake/gamedata/': No such file or directory

What should be there:

• game.json - Game metadata
• level__<world>__<level>.json - Individual level data

Referenced in code:

• relay/src/index.ts:64 - Serves game data from .lake/gamedata
• relay/src/serverProcess.ts:280-285 - Checks for game.json existence
• relay/src/serverProcess.ts:213 - Reads level data from JSON files

Issue 2: Directory Structure Mismatch

The relay server expects games to be in a sibling relationship to lean4game, but our structure is:

Current:

NNG4/
├── .lean4game-nix/    (lean4game platform)
│   └── relay/
└── Game/              (game code)

Relay expects (for local games):

parent/
├── lean4game/
│   └── relay/
└── NNG4/              (game directory)

Path resolution in relay:

• relay/src/serverProcess.ts:260-261:

  if(owner == 'local') {
    game_dir = path.join(this.dir, '..', '..', '..', '..', repo)
  }
  

• this.dir = .lean4game-nix/relay/dist/src
• Goes up 4 levels → /home/greg/code/experiments/Languages/Lean/NNG4
• Then appends repo (NNG4) → /home/greg/code/experiments/Languages/Lean/NNG4/NNG4 ❌

Actual game location: /home/greg/code/experiments/Languages/Lean/NNG4 ✅

How gamedata Gets Generated

Based on the relay server code, gamedata is generated when lake serve runs:

1. Modern games (v4.7.0+): Use lake serve --

   • Starts Lean server with GameServer library
   • GameServer library generates JSON data dynamically

2. Legacy games (≤ v4.7.0): Use custom binary

   • .lake/packages/GameServer/server/.lake/build/bin/gameserver
   • Binary called with --server <game_dir>

Our situation: NNG4 uses v4.23.0, so it should use lake serve --

Test result:

$ timeout 10 lake serve --
Watchdog error: Cannot read LSP request: Stream was closed

The command exits immediately - it needs an actual LSP client connection to work properly.

Attempted Fixes

Fix 1: Symlink approach (in progress)

Modified flake.nix to create a symlink so the relay server can find the game:

PARENT_DIR=$(dirname "$GAME_DIR")
ln -s "$GAME_DIR" "$PARENT_DIR/$GAME_NAME"

This would make /home/greg/code/experiments/Languages/Lean/NNG4/NNG4 point back to itself.

Status: Implemented in flake.nix but not tested yet.

Potential Solutions

Option A: Fix the directory structure

1. Move the game to be a proper sibling of lean4game
2. Change structure to:

   workspace/
   ├── .lean4game-nix/
   └── NNG4/  (symlink to actual game)
   

Option B: Fix the relay server path resolution

Create a patched version of the relay server that correctly resolves local game paths for our structure.

Option C: Use environment variable override

Check if lean4game relay server supports env vars to override game directory paths.

Option D: Generate gamedata separately

Find a way to pre-generate the .lake/gamedata/ directory before starting the server, possibly by:

• Running a special lake command
• Manually creating the JSON files
• Using a GameServer script

Next Steps

1. Verify gamedata generation:

   • Start the server properly
   • Connect to WebSocket
   • Check if .lake/gamedata/ gets created dynamically

2. Test symlink fix:

   • Rebuild flake
   • Run nix run
   • Verify the symlink is created correctly
   • Check if relay can find the game

3. Inspect GameServer source:

   • Check .lake/packages/GameServer/server/ for data generation code
   • Look for documentation on how gamedata is supposed to be created

4. Compare with working setup:

   • Check if Docker/devcontainer approach does something special
   • Look at lean4game's own test games to see their structure

Files Modified

• flake.nix - Added symlink creation logic to run-nng4-server script (lines 97-107)

Browser Console Errors

fetchIt2 @ i18next-http-backend.js
requestWithFetch2 @ i18next-http-backend.js
request2 @ i18next-http-backend.js
loadUrl @ i18next-http-backend.js

These errors are likely secondary issues caused by the game not loading properly due to missing gamedata.

Related Documentation

• lean4game running_locally.md
• Relay server source: .lean4game-nix/relay/src/index.ts
• Game manager: .lean4game-nix/relay/src/serverProcess.ts
• GameServer package: .lake/packages/GameServer/server/

Environment Info

• Lean version: 4.23.0
• lean4game version: v4.23.0 (matching tag)
• Node.js: 20.19.5
• npm packages: 1662 installed
• Platform: Linux x86_64