fix redirect from landing page in dev container #145

client/src/index.tsx

@@ -1,29 +1,45 @@
-import * as React from 'react';
+import * as React from 'react'
-import { createRoot } from 'react-dom/client';
+import { createRoot } from 'react-dom/client'
-import App from './app';
+import App from './app'
 import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
+import { store } from './state/store'
-import { Provider } from 'react-redux';
+import { Provider } from 'react-redux'
-import {
+import type { RouteObject } from "react-router"
-  createHashRouter,
+import { createHashRouter, RouterProvider, Route, redirect } from "react-router-dom"
-  RouterProvider,
+import ErrorPage from './components/error_page'
-  Route,
+import Welcome from './components/welcome'
-} from "react-router-dom";
+import LandingPage from './components/landing_page'
-import ErrorPage from './components/error_page';
+import Level from './components/level'
-import Welcome from './components/welcome';
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
-import LandingPage from './components/landing_page';
+
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
 
 monacoSetup()
 
+// // Do not show the landing page in the dev-container context
+// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? {
+//   path: "/",
+//   loader: () => redirect("/g/local/game")
+// } : {
+//   path: "/",
+//   element: <LandingPage />,
+// }
+
+
+// If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
+// `/g/local/game`. This is used for the devcontainer setup
+let single_game = (import.meta.env.VITE_LEAN4GAME_SINGLE == "true")
+let root_object: RouteObject = single_game ? {
+  path: "/",
+  loader: () => redirect("/g/local/game")
+} : {
+  path: "/",
+  element: <LandingPage />,
+}
+
 const router = createHashRouter([
+  root_object,
   {
-    path: "/",
+    // For backwards compatibility
-    element: <LandingPage />,
-  },
-  {
     path: "/game/nng",
     loader: () => redirect("/g/hhu-adam/NNG4")
   },

client/src/index_local.tsx

@@ -1,55 +0,0 @@
-// This file is a copy of `index.tsx` where the path "/" is redirected to "/g/local/game".
-// It is used for the dev. setup where there is only one game in a folder called `game`.
-import * as React from 'react';
-import { createRoot } from 'react-dom/client';
-import App from './app';
-import { ConnectionContext, connection } from './connection'
-import { store } from './state/store';
-import { Provider } from 'react-redux';
-import {
-  createHashRouter,
-  RouterProvider,
-  Route,
-} from "react-router-dom";
-import ErrorPage from './components/error_page';
-import Welcome from './components/welcome';
-import LandingPage from './components/landing_page';
-import Level from './components/level';
-import { monacoSetup } from 'lean4web/client/src/monacoSetup';
-import { redirect } from 'react-router-dom';
-
-monacoSetup()
-
-const router = createHashRouter([
-  {
-    path: "/",
-    loader: () => redirect("/g/local/game")
-  },
-  {
-    path: "/g/:owner/:repo",
-    element: <App />,
-    errorElement: <ErrorPage />,
-    children: [
-      {
-        path: "/g/:owner/:repo",
-        element: <Welcome />,
-      },
-      {
-        path: "/g/:owner/:repo/world/:worldId/level/:levelId",
-        element: <Level />,
-      },
-    ],
-  },
-]);
-
-const container = document.getElementById('root');
-const root = createRoot(container!);
-root.render(
-  <React.StrictMode>
-    <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
-    </Provider>
-  </React.StrictMode>
-);

env.d.ts

@@ -0,0 +1,10 @@
+/// <reference types="vite/client" />
+
+interface ImportMetaEnv {
+  readonly VITE_LEAN4GAME_SINGLE: string
+  // more env variables...
+}
+
+interface ImportMeta {
+  readonly env: ImportMetaEnv
+}

server/GameServer/FileWorker.lean

@@ -496,7 +496,7 @@ section NotificationHandling
       IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
     else if ¬ changes.isEmpty then
       let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText⟩
+      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
 
@@ -573,7 +573,7 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
     This is because LSP always refers to characters by (line, column),
     so if we get the line number correct it shouldn't matter that there
     is a CR there. -/
-  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap⟩
+  let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try

server/Main.lean

@@ -1,5 +1,9 @@
 import GameServer.FileWorker
 import GameServer.Watchdog
+import GameServer.Commands
+
+-- TODO: The only reason we import `Commands` is so that it gets built to on `lake build`
+-- should we have a different solution?
 
 unsafe def main : List String → IO UInt32 := fun args => do
   let e ← IO.getStderr

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.1.0
+leanprover/lean4:v4.2.0