# 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:**
```bash
$ 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`:
  ```typescript
  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:**
```bash
$ 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:
```bash
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](https://github.com/leanprover-community/lean4game/blob/main/doc/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