{
  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")

          # Create a symlink in parent directory if it doesn't exist
          # This allows the relay server to find the game correctly
          PARENT_DIR=$(dirname "$GAME_DIR")
          if [ ! -e "$PARENT_DIR/$GAME_NAME" ] || [ ! "$(readlink -f "$PARENT_DIR/$GAME_NAME")" = "$(readlink -f "$GAME_DIR")" ]; then
            if [ -L "$PARENT_DIR/$GAME_NAME" ]; then
              rm "$PARENT_DIR/$GAME_NAME"
            fi
            if [ ! -e "$PARENT_DIR/$GAME_NAME" ]; then
              ln -s "$GAME_DIR" "$PARENT_DIR/$GAME_NAME" 2>/dev/null || echo "Note: Could not create symlink, game may already exist"
            fi
          fi

          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";
        };
      }
    );
}