fixes for v4.6.0-rc1

Modify logic for preferences

.vscode/ltex.dictionary.en-US.txt

@@ -0,0 +1,7 @@
+GameSkeleton
+HiddenTactic
+subgoals
+KaTex
+gameserver
+lakefile
+Zulip

README.md

@@ -1,6 +1,6 @@
 # Lean 4 Game
 
-This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
+This is the source code for a Lean game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de).
 
 ## Creating a Game
 
@@ -9,6 +9,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 * Step 5: [How to Run Games Locally](doc/running_locally.md)
 * Step 7: [How to Update an existing Game](doc/update_game.md)
 * Step 8: [How to Publishing a Game](doc/publish_game.md)
+* [Troubleshooting](doc/troubleshoot.md)
 
 ## Documentation
 
@@ -28,7 +29,9 @@ should be up-to-date:
 
 ### Backend
 
-not written yet
+not fully written yet.
+
+* [Server](doc/DOCUMENTATION.md): describes the server part (i.e. the content of `server/` und `relay/`).
 
 ## Contributing
 
@@ -40,7 +43,8 @@ Providing the use access to a Lean instance running on the server is a severe se
 
 ## Credits
 
-The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
+The project has pimarily been developed by Alexander Bentkamp and Jon Eugster.
+
+It is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game
 (NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)
-by Kevin Buzzard and Mohammad Pedramfar.
-The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).
+by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4).

client/src/app.tsx

@@ -8,45 +8,24 @@ import '@fontsource/roboto/700.css';
 
 import './css/reset.css';
 import './css/app.css';
-import { MobileContext } from './components/infoview/context';
-import { useMobile } from './hooks';
-import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
-import { connection } from './connection';
+import { PreferencesContext} from './components/infoview/context';
+import UsePreferences from "./state/hooks/use_preferences"
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
-  const { mobile, setMobile, lockMobile, setLockMobile } = useMobile();
 
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
 
-  const automaticallyAdjustLayout = () => {
-    const {width} = getWindowDimensions()
-    setMobile(width < AUTO_SWITCH_THRESHOLD)
-  }
-
-  React.useEffect(()=>{
-    if (!lockMobile){
-      void automaticallyAdjustLayout()
-      window.addEventListener('resize', automaticallyAdjustLayout)
-
-      return () => {
-        window.removeEventListener('resize', automaticallyAdjustLayout)
-      }
-    }
-  }, [lockMobile])
-
-  React.useEffect(() => {
-    connection.startLeanClient(gameId);
-  }, [gameId])
+  const {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences} = UsePreferences()
 
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile, lockMobile, setLockMobile}}>
-          <Outlet />
-        </MobileContext.Provider>
+          <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}}>
+            <Outlet />
+          </PreferencesContext.Provider>
       </GameIdContext.Provider>
     </div>
   )

client/src/components/app_bar.tsx

@@ -7,7 +7,7 @@ import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
   faArrowRight, faArrowLeft, faXmark, faBars, faCode,
   faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
-import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
+import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
 import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
 import { useAppDispatch, useAppSelector } from '../hooks'
@@ -162,7 +162,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
 }) {
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile, setMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const [navOpen, setNavOpen] = React.useState(false)
 
   return <div className="app-bar">
@@ -212,7 +212,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
 }) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const [navOpen, setNavOpen] = React.useState(false)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))

client/src/components/hints.tsx

@@ -1,7 +1,9 @@
-import { GameHint } from "./infoview/rpc_api";
+import { GameHint, InteractiveGoalsWithHints, ProofState } from "./infoview/rpc_api";
 import * as React from 'react';
 import Markdown from './markdown';
-import { ProofStep } from "./infoview/context";
+import { DeletedChatContext, ProofContext } from "./infoview/context";
+import { lastStepHasErrors } from "./infoview/goals";
+import { Button } from "./button";
 
 export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
@@ -16,7 +18,7 @@ export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} :
 }
 
 export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
-
+  if (!hints) {return <></>}
   const openHints = hints.filter(hint => !hint.hidden)
   const hiddenHints = hints.filter(hint => hint.hidden)
 
@@ -46,22 +48,52 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
 }
 
 /** Filter hints to not show consequtive identical hints twice.
- *
- * This function takes a `ProofStep[]` and extracts the hints in form of an
- * element of type `GameHint[][]` where it removes hints that are identical to hints
- * appearing in the previous step. Hidden hints are not filtered.
- *
- * This effectively means we prevent consequtive identical hints from being shown.
+ * Hidden hints are not filtered.
  */
-export function filterHints(proof: ProofStep[]): GameHint[][] {
-  return proof.map((step, i) => {
-    if (i == 0){
-      return step.hints
-    } else {
-      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
-      // good way to shallow-compare objects?
-      return step.hints.filter((hint) => hint.hidden ||
-        (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
-    }
-  })
+export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
+  if (!hints) {
+    return []}
+  else if (!prevHints) {
+    return hints }
+  else {
+    return hints.filter((hint) => hint.hidden ||
+    (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
+    )
+  }
+}
+
+
+function hasHiddenHints(step: InteractiveGoalsWithHints): boolean {
+  return step?.goals[0]?.hints.some((hint) => hint.hidden)
+}
+
+
+export function MoreHelpButton({selected=null} : {selected?: number}) {
+
+  const {proof, setProof} = React.useContext(ProofContext)
+  const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
+
+  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected
+
+  const activateHiddenHints = (ev) => {
+    // If the last step (`k`) has errors, we want the hidden hints from the
+    // second-to-last step to be affected
+    if (!(proof.steps.length)) {return}
+
+    // state must not be mutated, therefore we need to clone the set
+    let tmp = new Set(showHelp)
+    if (tmp.has(k)) {
+      tmp.delete(k)
+    } else {
+      tmp.add(k)
+    }
+    setShowHelp(tmp)
+    console.debug(`help: ${Array.from(tmp.values())}`)
+  }
+
+  if (hasHiddenHints(proof.steps[k]) && !showHelp.has(k)) {
+    return <Button to="" onClick={activateHiddenHints}>
+      Show more help!
+    </Button>
+  }
 }

client/src/components/infoview/context.ts

@@ -3,45 +3,48 @@
  */
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
-import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { InteractiveDiagnostic } from '@leanprover/infoview-api';
+import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
+import { PreferencesState } from '../../state/preferences';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
   null as any)
 
 export type InfoStatus = 'updating' | 'error' | 'ready';
 
-/** One step of the proof */
-export type ProofStep = {
-  /** The command in this step */
-  command : string
-  /** List of goals *after* this command */
-  goals: InteractiveGoal[]     // TODO: Add correct type
-  /** Story relevant messages */
-  hints: GameHint[]        // TODO: Add correct type
-  /** Errors and warnings */
-  errors: InteractiveDiagnostic[]       // TODO: Add correct type
-}
+// /** One step of the proof */
+// export type ProofStep = {
+//   /** The command in this step */
+//   command : string
+//   /** List of goals *after* this command */
+//   goals: InteractiveGoal[]     // TODO: Add correct type
+//   /** Story relevant messages */
+//   hints: GameHint[]        // TODO: Add correct type
+//   /** Errors and warnings */
+//   errors: InteractiveDiagnostic[]       // TODO: Add correct type
+// }
 
 /** The context storing the proof step-by-step for the command line mode */
 export const ProofContext = React.createContext<{
   /** The proof consists of multiple steps that are processed one after the other.
    * In particular multi-line terms like `match`-statements will not be supported.
    *
-   * Note that the first step will always have `null` as command
+   * Note that the first step will always have "" as command
    */
-  proof: ProofStep[],
-  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
+  proof: ProofState,
+  setProof: React.Dispatch<React.SetStateAction<ProofState>>
 }>({
-  proof: [],
-  setProof: () => {} // TODO: implement me
+  proof: {steps: [], diagnostics: [], completed: false},
+  setProof: () => {}
 })
 
+
+// TODO: Do we still need that?
 export interface ProofStateProps {
   // pos: DocumentPosition;
   status: InfoStatus;
   messages: InteractiveDiagnostic[];
-  goals?: InteractiveGoals;
+  goals?: InteractiveGoalsWithHints;
   termGoal?: InteractiveTermGoal;
   error?: string;
   // userWidgets: UserWidgetInstance[];
@@ -49,31 +52,31 @@ export interface ProofStateProps {
   // triggerUpdate: () => Promise<void>;
 }
 
-export const ProofStateContext = React.createContext<{
-  proofState : ProofStateProps,
-  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
-}>({
-  proofState : {
-    status: 'updating',
-    messages: [],
-    goals: undefined,
-    termGoal: undefined,
-    error: undefined},
-  setProofState: () => {},
-})
+// export const ProofStateContext = React.createContext<{
+//   proofState : ProofStateProps,
+//   setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
+// }>({
+//   proofState : {
+//     status: 'updating',
+//     messages: [],
+//     goals: undefined,
+//     termGoal: undefined,
+//     error: undefined},
+//   setProofState: () => {},
+// })
 
-export interface IMobileContext {
-  mobile : boolean,
-  setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
-  lockMobile: boolean,
-  setLockMobile: React.Dispatch<React.SetStateAction<Boolean>>,
+export interface IPreferencesContext extends PreferencesState{
+  mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.
+  setLayout: React.Dispatch<React.SetStateAction<PreferencesState["layout"]>>;
+  setIsSavePreferences: React.Dispatch<React.SetStateAction<Boolean>>;
 }
 
-export const MobileContext = React.createContext<IMobileContext>({
+export const PreferencesContext = React.createContext<IPreferencesContext>({
   mobile: false,
-  setMobile: () => {},
-  lockMobile: false,
-  setLockMobile: () => {}
+  layout: "auto",
+  isSavePreferences: false,
+  setLayout: () => {},
+  setIsSavePreferences: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{

client/src/components/infoview/goals.tsx

@@ -10,7 +10,10 @@ import { Locations, LocationsContext, SelectableLocation } from '../../../../nod
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
 import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
 import { InputModeContext } from './context';
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api';
+import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api';
+import { RpcSessionAtPos } from '@leanprover/infoview/*';
+import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
+import { DiagnosticSeverity } from 'vscode-languageserver-protocol';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -39,7 +42,11 @@ function goalToString(g: InteractiveGoal): string {
 }
 
 export function goalsToString(goals: InteractiveGoals): string {
-    return goals.goals.map(goalToString).join('\n\n')
+    return goals.goals.map(g => goalToString(g)).join('\n\n')
+}
+
+export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string {
+    return goals.goals.map(g => goalToString(g.goal)).join('\n\n')
 }
 
 interface GoalFilterState {
@@ -255,7 +262,7 @@ export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
 })
 
 interface GoalsProps {
-    goals: InteractiveGoals
+    goals: InteractiveGoalsWithHints
     filter: GoalFilterState
 }
 
@@ -264,7 +271,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g} filter={filter} />)}
+          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
         </>
     }
 }
@@ -276,7 +283,7 @@ interface FilteredGoalsProps {
      * When this is `undefined`, the component will not appear at all but will remember its state
      * by virtue of still being mounted in the React tree. When it does appear again, the filter
      * settings and collapsed state will be as before. */
-    goals?: InteractiveGoals
+    goals?: InteractiveGoalsWithHints
 }
 
 /**
@@ -291,7 +298,7 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
             data-id="copy-goal-to-comment"
             onClick={e => {
                 e.preventDefault();
-                if (goals) void ec.copyToComment(goalsToString(goals))
+                if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
             }}
             title="copy state to comment" />
 
@@ -336,3 +343,112 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
         </details>
     </div>
 })
+
+export function loadGoals(
+    rpcSess: RpcSessionAtPos,
+    uri: string,
+    setProof: React.Dispatch<React.SetStateAction<ProofState>>) {
+  console.info('sending rpc request to load the proof state')
+
+  rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then(
+    (proof : ProofState) => {
+      console.info(`received a proof state!`)
+      console.log(proof)
+      setProof(proof)
+
+
+
+
+      // let tmpProof : ProofStep[] = []
+
+      // let goalCount = 0
+
+      // steps.map((goals, i) => {
+      //   // The first step has an empty command and therefore also no error messages
+      //   // Usually there is a newline at the end of the editors content, so we need to
+      //   // display diagnostics from potentally two lines in the last step.
+      //   let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
+
+      //   // Filter out the 'unsolved goals' message
+      //   messages = messages.filter((msg) => {
+      //     return !("append" in msg.message &&
+      //       "text" in msg.message.append[0] &&
+      //       msg.message.append[0].text === "unsolved goals")
+      //   })
+
+      //   if (typeof goals == 'undefined') {
+      //     tmpProof.push({
+      //       command: i ? model.getLineContent(i) : '',
+      //       goals: [],
+      //       hints: [],
+      //       errors: messages
+      //     } as ProofStep)
+      //     console.debug('goals is undefined')
+      //     return
+      //   }
+
+      //   // If the number of goals reduce, show a message
+      //   if (goals.length && goalCount > goals.length) {
+      //     messages.unshift({
+      //       range: {
+      //         start: {
+      //           line: i-1,
+      //           character: 0,
+      //         },
+      //         end: {
+      //           line: i-1,
+      //           character: 0,
+      //         }},
+      //       severity: DiagnosticSeverity.Information,
+      //       message: {
+      //       text: 'intermediate goal solved 🎉'
+      //       }
+      //     })
+      //   }
+      //   goalCount = goals.length
+
+      //   // with no goals there will be no hints.
+      //   let hints : GameHint[] = goals.length ? goals[0].hints : []
+
+      //   console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+      //   console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+      //   console.debug(`Hints: (${i}): `, hints)
+      //   console.debug(`Errors: (${i}): `, messages)
+
+      //   tmpProof.push({
+      //     // the command of the line above. Note that `getLineContent` starts counting
+      //     // at `1` instead of `zero`. The first ProofStep will have an empty command.
+      //     command: i ? model.getLineContent(i) : '',
+      //     // TODO: store correct data
+      //     goals: goals.map(g => g.goal),
+      //     // only need the hints of the active goals in chat
+      //     hints: hints,
+      //     // errors and messages from the server
+      //     errors: messages
+      //   } as ProofStep)
+
+      // })
+      // // Save the proof to the context
+      // setProof(tmpProof)
+
+
+
+    }
+  )
+}
+
+
+export function lastStepHasErrors (proof : ProofState): boolean {
+  if (!proof?.steps.length) {return false}
+
+  let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics]
+
+  return diags.some(
+    (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
+  )
+}
+
+export function isLastStepWithErrors (proof : ProofState, i: number): boolean {
+  if (!proof?.steps.length) {return false}
+  return (i == proof.steps.length - 1) && lastStepHasErrors(proof)
+}

client/src/components/infoview/info.tsx

@@ -4,7 +4,7 @@ import * as React from 'react'
 import { CircularProgress } from '@mui/material'
 import type { Location, Diagnostic } from 'vscode-languageserver-protocol'
 import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
-  RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api'
+  RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api'
 import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
   mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util'
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'
@@ -14,7 +14,7 @@ import { GoalsLocation, Locations, LocationsContext } from '../../../../node_mod
 
 import { AllMessages, lspDiagToInteractive } from './messages'
 import { goalsToString, Goal, MainAssumptions, OtherGoals, ProofDisplay } from './goals'
-import { InteractiveGoals } from './rpc_api'
+import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api'
 import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from './context'
 
 // TODO: All about pinning could probably be removed
@@ -83,11 +83,11 @@ interface InfoDisplayContentProps extends PausableProps {
   error?: string
   userWidgets: UserWidgetInstance[]
   triggerUpdate: () => Promise<void>
-  proof? : string
+  proofString? : string
 }
 
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
-    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props
+    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props
 
     const hasWidget = userWidgets.length > 0
     const hasError = !!error
@@ -114,7 +114,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
 
     const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
-    return <>
+
+   return <>
         {hasError &&
             <div className='error' key='errors'>
                 Error updating:{' '}{error}.
@@ -137,7 +138,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
         {userWidgets.map(widget =>
           <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
             <summary className='mv2 pointer'>{widget.name}</summary>
-            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal) : []}
+            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
               termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
           </details>
         )}
@@ -166,6 +167,7 @@ interface InfoDisplayProps {
   pos: DocumentPosition,
   status: InfoStatus,
   messages: InteractiveDiagnostic[],
+  proof?: ProofState,
   goals?: InteractiveGoals,
   termGoal?: InteractiveTermGoal,
   error?: string,
@@ -175,7 +177,7 @@ interface InfoDisplayProps {
 }
 
 /** Displays goal state and messages. Can be paused. */
-function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) {
+function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     // Used to update the paused state *just once* if it is paused,
     // but a display update is triggered
     const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false)
@@ -214,7 +216,7 @@ function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable)
     {/* <details open> */}
         {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
         <div className="vscode-light">
-            <InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
+            <InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
         </div>
     {/* </details> */}
     </RpcContext.Provider>
@@ -252,7 +254,7 @@ function useIsProcessingAt(p: DocumentPosition): boolean {
 
 function InfoAux(props: InfoProps) {
 
-    const proofContext = React.useContext(ProofContext)
+    const { setProof } = React.useContext(ProofContext)
 
     const config = React.useContext(ConfigContext)
 
@@ -290,6 +292,8 @@ function InfoAux(props: InfoProps) {
     // with e.g. a new `pos`.
     type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
     const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => {
+
+        const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos))
         const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos))
         const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
         const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound)
@@ -308,6 +312,7 @@ function InfoAux(props: InfoProps) {
                 pos,
                 status: 'updating',
                 messages: lspDiagsHere.map(lspDiagToInteractive),
+                proof: undefined,
                 goals: undefined,
                 termGoal: undefined,
                 error: undefined,
@@ -318,11 +323,12 @@ function InfoAux(props: InfoProps) {
 
         // NB: it is important to await await reqs at once, otherwise
         // if both throw then one exception becomes unhandled.
-        Promise.all([goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
-            ([goals, termGoal, userWidgets, messages]) => resolve({
+        Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
+            ([proof, goals, termGoal, userWidgets, messages]) => resolve({
                 pos,
                 status: 'ready',
                 messages,
+                proof : proof as any,
                 goals: goals as any,
                 termGoal,
                 error: undefined,
@@ -353,6 +359,7 @@ function InfoAux(props: InfoProps) {
                     pos,
                     status: 'error',
                     messages: lspDiagsHere.map(lspDiagToInteractive),
+                    proof: undefined,
                     goals: undefined,
                     termGoal: undefined,
                     error: `Error fetching goals: ${errorString}`,
@@ -389,6 +396,7 @@ function InfoAux(props: InfoProps) {
         pos,
         status: 'updating',
         messages: [],
+        proof: undefined,
         goals: undefined,
         termGoal: undefined,
         error: undefined,
@@ -412,6 +420,11 @@ function InfoAux(props: InfoProps) {
           //   hintContext.setHints(state.value.goals.goals[0].hints)
           // }
           setDisplayProps({ ...state.value, triggerUpdate })
+
+          // Update the game's proof state
+          console.info('updating proof from editor mode.')
+          setProof(state.value.proof)
+
         } else if (state.state === 'rejected' && state.error !== 'retry') {
             // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception.
             console.warn('Unreachable code reached with error: ', state.error)

client/src/components/infoview/main.tsx

@@ -26,15 +26,16 @@ import Markdown from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
-import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
-import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
+import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
+import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
 import { CircularProgress } from '@mui/material';
-import { GameHint } from './rpc_api';
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { store } from '../../state/store';
-import { Hints, filterHints } from '../hints';
+import { Hints, MoreHelpButton, filterHints } from '../hints';
+import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
@@ -61,36 +62,35 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
   const gameId = React.useContext(GameIdContext)
   const { typewriterMode } = React.useContext(InputModeContext)
 
-  // Mark level as completed when server gives notification
+  const {proof, setProof} = React.useContext(ProofContext)
+
   const dispatch = useAppDispatch()
-  useServerNotificationEffect(
-    '$/game/completed',
-    (params: any) => {
-      if (ec.events.changedCursorLocation.current &&
-          ec.events.changedCursorLocation.current.uri === params.uri) {
-        dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
 
-        // On completion, add the names of all new items to the local storage
-        let newTiles = [
-          ...level?.tactics,
-          ...level?.lemmas,
-          ...level?.definitions
-        ].filter((tile) => tile.new).map((tile) => tile.name)
+  React.useEffect(() => {
+    if (proof.completed) {
+      dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
 
-        // Add the proven statement to the local storage as well.
-        if (level?.statementName != null) {
-          newTiles.push(level?.statementName)
-        }
+      // On completion, add the names of all new items to the local storage
+      let newTiles = [
+        ...level?.tactics,
+        ...level?.lemmas,
+        ...level?.definitions
+      ].filter((tile) => tile.new).map((tile) => tile.name)
 
-        let inv: string[] = selectInventory(gameId)(store.getState())
-
-        // add new items and remove duplicates
-        let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
-
-        dispatch(changedInventory({ game: gameId, inventory: newInv }))
+      // Add the proven statement to the local storage as well.
+      if (level?.statementName != null) {
+        newTiles.push(level?.statementName)
       }
-    }, [level]
-  )
+
+      let inv: string[] = selectInventory(gameId)(store.getState())
+
+      // add new items and remove duplicates
+      let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
+
+      dispatch(changedInventory({ game: gameId, inventory: newInv }))
+
+    }
+  }, [proof, level])
 
   /* Set up updates to the global infoview state on editor events. */
   const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
@@ -154,8 +154,21 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
 
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
+  const { proof, setProof } = React.useContext(ProofContext)
+  const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
+  const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
 
+
+  function toggleSelection(line: number) {
+    return (ev) => {
+      console.debug('toggled selection')
+      if (selectedStep == line) {
+        setSelectedStep(undefined)
+      } else {
+        setSelectedStep(line)
+      }
+    }
+  }
   console.debug(`template: ${props.data?.template}`)
 
   // React.useEffect (() => {
@@ -182,6 +195,19 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
 
   const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
+  const curPos: DocumentPosition | undefined =
+    useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined)
+
+  // Effect when the cursor changes in the editor
+  React.useEffect(() => {
+    // TODO: this is a bit of a hack and will yield unexpected behaviour if lines
+    // are indented.
+    let newPos = curPos?.line + (curPos?.character == 0 ? 0 : 1)
+
+    // scroll the chat along
+    setSelectedStep(newPos)
+  }, [curPos])
+
   useClientNotificationEffect(
     'textDocument/didClose',
     (params: DidCloseTextDocumentParams) => {
@@ -206,8 +232,13 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
     ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
   } else {
     ret = <div className="infoview vscode-light">
-      {completed && <div className="level-completed">Level completed! 🎉</div>}
+      {proof.completed && <div className="level-completed">Level completed! 🎉</div>}
       <Infos />
+      <Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints}
+        showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
+        selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
+        lastLevel={curPos?.line == proof.steps.length - 1}/>
+      <MoreHelpButton selected={curPos?.line}/>
     </div>
   }
 
@@ -223,15 +254,24 @@ const goalFilter = {
 }
 
 /** The display of a single entered lean command */
-function Command({ command, deleteProof }: { command: string, deleteProof: any }) {
+function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) {
   // The first step will always have an empty command
-  if (!command) { return <></> }
-  return <div className="command">
-    <div className="command-text">{command}</div>
-    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
-    </Button>
-  </div>
+  if (!proof?.steps[i]?.command) { return <></> }
+
+  if (isLastStepWithErrors(proof, i)) {
+    // If the last step has errors, we display the command in a different style
+    // indicating that it will be removed on the next try.
+    return <div className="failed-command">
+      <i>Failed command</i>: {proof.steps[i].command}
+    </div>
+  } else {
+    return <div className="command">
+      <div className="command-text">{proof.steps[i].command}</div>
+      <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+        <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
+      </Button>
+    </div>
+  }
 }
 
 // const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
@@ -286,10 +326,14 @@ function Command({ command, deleteProof }: { command: string, deleteProof: any }
 // }, fastIsEqual)
 
 /** The tabs of goals that lean ahs after the command of this step has been processed */
-function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: ProofStep, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
 
   const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
+  if (proofStep.goals.length == 0) {
+    return <></>
+  }
+
   return <div className="goal-tabs" onClick={onClick}>
     <div className={`tab-bar ${last ? 'current' : ''}`}>
       {proofStep.goals.map((goal, i) => (
@@ -300,7 +344,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte
       ))}
     </div>
     <div className="goal-tab vscode-light">
-      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]} />
+      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} />
     </div>
   </div>
 }
@@ -349,13 +393,12 @@ export function TypewriterInterface({props}) {
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
   const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
-  const {mobile} = React.useContext(MobileContext)
-  const { proof } = React.useContext(ProofContext)
+  const {mobile} = React.useContext(PreferencesContext)
+  const { proof, setProof } = React.useContext(ProofContext)
   const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
   const proofPanelRef = React.useRef<HTMLDivElement>(null)
-  const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
   // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
   // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
 
@@ -367,9 +410,11 @@ export function TypewriterInterface({props}) {
   function deleteProof(line: number) {
     return (ev) => {
       let deletedChat: Array<GameHint> = []
-      filterHints(proof).slice(line).map((hintsAtStep, i) => {
+      proof.steps.slice(line).map((step, i) => {
+        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+
         // Only add these hidden hints to the deletion stack which were visible
-        deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
+        deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
       })
       setDeletedChat(deletedChat)
 
@@ -382,7 +427,9 @@ export function TypewriterInterface({props}) {
         forceMoveMarkers: false
       }])
       setSelectedStep(undefined)
-      setTypewriterInput(proof[line].command)
+      setTypewriterInput(proof.steps[line].command)
+      // Reload proof on deleting
+      loadGoals(rpcSess, uri, setProof)
       ev.stopPropagation()
     }
   }
@@ -402,7 +449,7 @@ export function TypewriterInterface({props}) {
 
    // Scroll to the end of the proof if it is updated.
    React.useEffect(() => {
-    if (proof?.length > 1) {
+    if (proof.steps.length > 1) {
       proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
     } else {
       proofPanelRef.current?.scrollTo(0,0)
@@ -423,38 +470,8 @@ export function TypewriterInterface({props}) {
     }
   }, [selectedStep])
 
-  // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
-
-  // If the last step has errors, we want to treat it as if it is part of the second-to-last step
-  let k = proof.length - 1
-  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0
-
-  const activateHiddenHints = (ev) => {
-    // If the last step (`k`) has errors, we want the hidden hints from the
-    // second-to-last step to be affected
-    if (!(proof.length)) {return}
-
-    // state must not be mutated, therefore we need to clone the set
-    let tmp = new Set(showHelp)
-    if (tmp.has(k - withErr)) {
-      tmp.delete(k - withErr)
-    } else {
-      tmp.add(k - withErr)
-    }
-    setShowHelp(tmp)
-    console.debug(`help: ${Array.from(tmp.values())}`)
-  }
-
-  function hasHiddenHints(i : number): boolean {
-    let step = proof[i]
-
-    // For example if the proof isn't loaded yet
-    if(!step) {return false}
-
-    return step.hints.some((hint) => hint.hidden)
-  }
-
-  let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false
+  // TODO: superfluous, can be replaced with `withErr` from above
+  let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -474,20 +491,22 @@ export function TypewriterInterface({props}) {
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
-        {proof.length ?
+        {proof.steps.length ?
           <>
-            {proof.map((step, i) => {
-              if (i == proof.length - 1 && lastStepErrors) {
-                // if the last command contains an error, we only display the errors but not the
-                // entered command as it is still present in the command line.
-                // TODO: Should not use index as key.
-                return <div key={`proof-step-${i}`}>
-                  <Errors errors={step.errors} typewriterMode={true} />
-                </div>
-              } else {
+            {proof.steps.map((step, i) => {
+              let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+
+              // if (i == proof.steps.length - 1 && hasInteractiveErrors(step.diags)) {
+              //   // if the last command contains an error, we only display the errors but not the
+              //   // entered command as it is still present in the command line.
+              //   // TODO: Should not use index as key.
+              //   return <div key={`proof-step-${i}`} className={`step step-${i}`}>
+              //     <Errors errors={step.diags} typewriterMode={true} />
+              //   </div>
+              // } else {
                 return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
-                  <Command command={step.command} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} typewriterMode={true} />
+                  <Command proof={proof} i={i} deleteProof={deleteProof(i)} />
+                  <Errors errors={step.diags} typewriterMode={true} />
                   {mobile && i == 0 && props.data?.introduction &&
                     <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
                       <Markdown>{props.data?.introduction}</Markdown>
@@ -495,22 +514,21 @@ export function TypewriterInterface({props}) {
                   }
                   {mobile &&
                     <Hints key={`hints-${i}`}
-                      hints={step.hints} showHidden={showHelp.has(i)} step={i}
+                      hints={filteredHints} showHidden={showHelp.has(i)} step={i}
                       selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                   }
-                  <GoalsTabs proofStep={step} last={i == proof.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/>
-
-                  {mobile && i == proof.length - 1 &&
-                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
-                      Show more help!
-                    </Button>
+                  {/* <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
+                  {!(isLastStepWithErrors(proof, i)) &&
+                    <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+                  }
+                  {mobile && i == proof.steps.length - 1 &&
+                    <MoreHelpButton />
                   }
 
                   {/* Show a message that there are no goals left */}
-                  {!step.goals.length && (
+                  {/* {!step.goals.length && (
                     <div className="message information">
-                      {completed ?
+                      {proof.completed ?
                         <p>Level completed! 🎉</p> :
                         <p>
                           <b>no goals left</b><br />
@@ -518,11 +536,17 @@ export function TypewriterInterface({props}) {
                         </p>
                       }
                     </div>
-                  )}
+                  )} */}
                 </div>
               }
-            })}
-            {mobile && completed &&
+            //}
+            )}
+            {proof.diagnostics.length > 0 &&
+              <div key={`proof-step-remaining`} className="step step-remaining">
+                <Errors errors={proof.diagnostics} typewriterMode={true} />
+              </div>
+            }
+            {mobile && proof.completed &&
               <div className="button-row mobile">
                 {props.level >= props.worldSize ?
                   <Button to={`/${gameId}`}>
@@ -539,7 +563,7 @@ export function TypewriterInterface({props}) {
         }
       </div>
     </div>
-    <Typewriter hidden={!withErr && proof[proof.length - 1]?.goals.length == 0} disabled={disableInput || !proof.length}/>
+    <Typewriter disabled={disableInput || !proof.steps.length}/>
     </RpcContext.Provider>
   </div>
 }

client/src/components/infoview/messages.tsx

@@ -194,16 +194,24 @@ export function AllMessages() {
                 </a>
             </span>
         </summary> */}
-        <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} />
+        <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} />
     {/* </Details> */}
     </RpcContext.Provider>
     )
 }
 
 /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */
-function AllMessagesBody({uri, messages}: {uri: DocumentUri, messages: () => Promise<InteractiveDiagnostic[]>}) {
+function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise<InteractiveDiagnostic[]>}) {
     const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(undefined)
-    React.useEffect(() => { void messages().then(setMsgs) }, [messages])
+    React.useEffect(() => { void messages().then(
+        msgs => setMsgs(msgs.filter(
+            (d)=>{
+                //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`)
+
+                // Only show the messages from the line where the cursor is.
+                return d.range.start.line == curPos.line
+            }))
+    ) }, [messages, curPos])
     if (msgs === undefined) return <div>Loading messages...</div>
     else return <MessagesList uri={uri} messages={msgs}/>
 }

client/src/components/infoview/rpc_api.ts

@@ -3,46 +3,80 @@
  *
  * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
  */
-import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
-
-export interface GameHint {
-  text: string;
-  hidden: boolean;
-}
+import type { Range } from 'vscode-languageserver-protocol';
+import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
+import type { Diagnostic } from 'vscode-languageserver-protocol';
 
 export interface InteractiveHypothesisBundle {
   /** The pretty names of the variables in the bundle. Anonymous names are rendered
    * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
    * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
   names: string[];
-  /** Present since server version 1.1.2. */
   fvarIds?: FVarId[];
   type: CodeWithInfos;
   val?: CodeWithInfos;
   isInstance?: boolean;
   isType?: boolean;
-  isAssumption?: boolean;
   isInserted?: boolean;
   isRemoved?: boolean;
+  isAssumption?: boolean;
 }
 
 export interface InteractiveGoalCore {
   hyps: InteractiveHypothesisBundle[];
   type: CodeWithInfos;
-  /** Present since server version 1.1.2. */
   ctx?: ContextInfo;
 }
 
 export interface InteractiveGoal extends InteractiveGoalCore {
   userName?: string;
   goalPrefix?: string;
-  /** Present since server version 1.1.2. */
   mvarId?: MVarId;
   isInserted?: boolean;
   isRemoved?: boolean;
+}
+
+export interface InteractiveGoals extends InteractiveGoalCore {
+  goals: InteractiveGoals[];
+}
+
+export interface InteractiveTermGoal extends InteractiveGoalCore {
+  range?: Range;
+  term?: TermInfo;
+}
+
+export interface GameHint {
+  text: string;
+  hidden: boolean;
+}
+
+export interface InteractiveGoalWithHints {
+  goal: InteractiveGoal;
   hints: GameHint[];
 }
 
-export interface InteractiveGoals {
-  goals: InteractiveGoal[];
+export interface InteractiveGoalsWithHints {
+  goals: InteractiveGoalWithHints[];
+  command: string;
+  diags: InteractiveDiagnostic[];
+}
+
+/**
+ * The proof state as it is received from the server.
+ * Per proof step of the tactic proof, there is one `InteractiveGoalWithHints[]`.
+ */
+export interface ProofState {
+  /** The proof steps. step 0 is the state at the beginning of the proof. step one
+   * contains the goal after the first line has been evaluated.
+   *
+   * In particular `step[i]` is the proof step at the beginning of line `i` in vscode.
+   */
+  steps: InteractiveGoalsWithHints[];
+  /** The remaining diagnostics that are not in the steps. Usually this should only
+   * be the "unsolved goals" message, I believe.
+   */
+  diagnostics : InteractiveDiagnostic[];
+  completed : Boolean;
+  completedWithWarnings : Boolean;
 }

client/src/components/infoview/typewriter.tsx

@@ -5,7 +5,7 @@ import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { Registry } from 'monaco-textmate' // peer dependency
 import { wireTmGrammars } from 'monaco-editor-textmate'
-import { DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol';
+import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
 import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
 import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
@@ -13,13 +13,21 @@ import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
 import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
 import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
 import languageConfig from 'lean4/language-configuration.json';
-import { InteractiveDiagnostic, getInteractiveDiagnostics } from '@leanprover/infoview-api';
+import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api';
 import { Diagnostic } from 'vscode-languageserver-types';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
-import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'
-import { goalsToString } from './goals'
-import { GameHint, InteractiveGoals } from './rpc_api'
+import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
+import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
+import { GameHint, ProofState } from './rpc_api'
+
+export interface GameDiagnosticsParams {
+  uri: DocumentUri;
+  diagnostics: Diagnostic[];
+}
+
+
+
 
 /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
 
@@ -64,7 +72,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
 monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 /** The input field */
-export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boolean}) {
+export function Typewriter({disabled}: {disabled?: boolean}) {
 
   /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
@@ -89,98 +97,98 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   /** Load all goals an messages of the current proof (line-by-line) and save
    * the retrieved information into context (`ProofContext`)
    */
-  const loadAllGoals = React.useCallback(() => {
+  // const loadAllGoals = React.useCallback(() => {
 
-    let goalCalls = []
-    let msgCalls = []
+  //   let goalCalls = []
+  //   let msgCalls = []
 
-    // For each line of code ask the server for the goals and the messages on this line
-    for (let i = 0; i < model.getLineCount(); i++) {
-      goalCalls.push(
-        rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
-      )
-      msgCalls.push(
-        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
-      )
-    }
+  //   // For each line of code ask the server for the goals and the messages on this line
+  //   for (let i = 0; i < model.getLineCount(); i++) {
+  //     goalCalls.push(
+  //       rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
+  //     )
+  //     msgCalls.push(
+  //       getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
+  //     )
+  //   }
 
-    // Wait for all these requests to be processed before saving the results
-    Promise.all(goalCalls).then((steps : InteractiveGoals[]) => {
-      Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
-        let tmpProof : ProofStep[] = []
+  //   // Wait for all these requests to be processed before saving the results
+  //   Promise.all(goalCalls).then((steps : InteractiveGoalsWithHints[]) => {
+  //     Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
+  //       let tmpProof : ProofStep[] = []
 
-        let goalCount = 0
+  //       let goalCount = 0
 
-        steps.map((goals, i) => {
-          // The first step has an empty command and therefore also no error messages
-          // Usually there is a newline at the end of the editors content, so we need to
-          // display diagnostics from potentally two lines in the last step.
-          let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
+  //       steps.map((goals, i) => {
+  //         // The first step has an empty command and therefore also no error messages
+  //         // Usually there is a newline at the end of the editors content, so we need to
+  //         // display diagnostics from potentally two lines in the last step.
+  //         let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
 
-          // Filter out the 'unsolved goals' message
-          messages = messages.filter((msg) => {
-            return !("append" in msg.message &&
-              "text" in msg.message.append[0] &&
-              msg.message.append[0].text === "unsolved goals")
-          })
+  //         // Filter out the 'unsolved goals' message
+  //         messages = messages.filter((msg) => {
+  //           return !("append" in msg.message &&
+  //             "text" in msg.message.append[0] &&
+  //             msg.message.append[0].text === "unsolved goals")
+  //         })
 
-          if (typeof goals == 'undefined') {
-            tmpProof.push({
-              command: i ? model.getLineContent(i) : '',
-              goals: [],
-              hints: [],
-              errors: messages
-            } as ProofStep)
-            console.debug('goals is undefined')
-            return
-          }
+  //         if (typeof goals == 'undefined') {
+  //           tmpProof.push({
+  //             command: i ? model.getLineContent(i) : '',
+  //             goals: [],
+  //             hints: [],
+  //             errors: messages
+  //           } as ProofStep)
+  //           console.debug('goals is undefined')
+  //           return
+  //         }
 
-          // If the number of goals reduce, show a message
-          if (goals.goals.length && goalCount > goals.goals.length) {
-            messages.unshift({
-              range: {
-                start: {
-                  line: i-1,
-                  character: 0,
-                },
-                end: {
-                  line: i-1,
-                  character: 0,
-                }},
-              severity: DiagnosticSeverity.Information,
-              message: {
-              text: 'intermediate goal solved 🎉'
-              }
-            })
-          }
-          goalCount = goals.goals.length
+  //         // If the number of goals reduce, show a message
+  //         if (goals.length && goalCount > goals.length) {
+  //           messages.unshift({
+  //             range: {
+  //               start: {
+  //                 line: i-1,
+  //                 character: 0,
+  //               },
+  //               end: {
+  //                 line: i-1,
+  //                 character: 0,
+  //               }},
+  //             severity: DiagnosticSeverity.Information,
+  //             message: {
+  //             text: 'intermediate goal solved 🎉'
+  //             }
+  //           })
+  //         }
+  //         goalCount = goals.length
 
-          // with no goals there will be no hints.
-          let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
+  //         // with no goals there will be no hints.
+  //         let hints : GameHint[] = goals.length ? goals[0].hints : []
 
-          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
-          console.debug(`Goals: (${i}): `, goalsToString(goals)) //
-          console.debug(`Hints: (${i}): `, hints)
-          console.debug(`Errors: (${i}): `, messages)
+  //         console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+  //         console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+  //         console.debug(`Hints: (${i}): `, hints)
+  //         console.debug(`Errors: (${i}): `, messages)
 
-          tmpProof.push({
-            // the command of the line above. Note that `getLineContent` starts counting
-            // at `1` instead of `zero`. The first ProofStep will have an empty command.
-            command: i ? model.getLineContent(i) : '',
-            // TODO: store correct data
-            goals: goals.goals,
-            // only need the hints of the active goals in chat
-            hints: hints,
-            // errors and messages from the server
-            errors: messages
-          } as ProofStep)
+  //         tmpProof.push({
+  //           // the command of the line above. Note that `getLineContent` starts counting
+  //           // at `1` instead of `zero`. The first ProofStep will have an empty command.
+  //           command: i ? model.getLineContent(i) : '',
+  //           // TODO: store correct data
+  //           goals: goals.map(g => g.goal),
+  //           // only need the hints of the active goals in chat
+  //           hints: hints,
+  //           // errors and messages from the server
+  //           errors: messages
+  //         } as ProofStep)
 
-        })
-        // Save the proof to the context
-        setProof(tmpProof)
-      }).catch((error) => {console.debug("promise broken")})
-    }).catch((error) => {console.debug("promise broken")})
-  }, [editor, rpcSess, uri, model])
+  //       })
+  //       // Save the proof to the context
+  //       setProof(tmpProof)
+  //     }).catch((error) => {console.debug("promise broken")})
+  //   }).catch((error) => {console.debug("promise broken")})
+  // }, [editor, rpcSess, uri, model])
 
   // Run the command
   const runCommand = React.useCallback(() => {
@@ -201,6 +209,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
         forceMoveMarkers: false
       }])
       setTypewriterInput('')
+      // Load proof after executing edits
+      loadGoals(rpcSess, uri, setProof)
     }
 
     editor.setPosition(pos)
@@ -212,9 +222,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     }
   }, [typewriterInput])
 
+  /* Load proof on start/switching to typewriter */
   useEffect(() => {
-    if (proof.length && hasInteractiveErrors(proof[proof.length - 1].errors)) {
-      setTypewriterInput(proof[proof.length - 1].command)
+    loadGoals(rpcSess, uri, setProof)
+  }, [])
+
+  /** If the last step has an error, add the command to the typewriter. */
+  useEffect(() => {
+    if (lastStepHasErrors(proof)) {
+      setTypewriterInput(proof.steps[proof.steps.length - 1].command)
     }
   }, [proof])
 
@@ -222,7 +238,9 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == uri) {
       setProcessing(false)
-      loadAllGoals()
+      //loadGoals(rpcSess, uri, setProof)
+
+      // TODO: loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
         //setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
@@ -236,6 +254,15 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     // loadAllGoals()
   }, [uri]);
 
+  // React when answer from the server comes back
+  useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
+    console.log('Received game diagnostics')
+    console.log(`diag. uri : ${params.uri}`)
+    console.log(params.diagnostics)
+
+  }, [uri]);
+
+
   useEffect(() => {
     const myEditor = monaco.editor.create(inputRef.current!, {
       value: typewriterInput,
@@ -306,7 +333,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useEffect(() => {
     console.debug(`time to update: ${uri} \n ${rpcSess}`)
     console.debug(rpcSess)
-    loadAllGoals()
+    // console.debug('LOAD ALL GOALS')
+    // TODO: loadAllGoals()
   }, [rpcSess])
 
   /** Process the entered command */
@@ -315,7 +343,8 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
     runCommand()
   }
 
-  return <div className={`typewriter${hidden ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
+  // do not display if the proof is completed (with potential warnings still present)
+  return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
       <form onSubmit={handleSubmit}>
         <div className="typewriter-input-wrapper">
           <div ref={inputRef} className="typewriter-input" />
@@ -343,3 +372,14 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
     (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
   )
 }
+
+export function getInteractiveDiagsAt (proof: ProofState, k : number) {
+  if (k == 0) {
+    return []
+  } else if (k >= proof.steps.length-1) {
+    // TODO: Do we need that?
+    return proof.diagnostics.filter(msg => msg.range.start.line >= proof.steps.length-1)
+  } else {
+    return proof.diagnostics.filter(msg => msg.range.start.line == k-1)
+  }
+}

client/src/components/landing_page.tsx

@@ -134,7 +134,8 @@ function LandingPage() {
     "leanprover-community/nng4",
     "hhu-adam/robo",
     "djvelleman/stg4",
-    "miguelmarco/STG4",
+    "miguelmarco/stg4",
+    "trequetrum/lean4game-logic",
   ]
   let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 

client/src/components/level.tsx

@@ -18,7 +18,6 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
 
 import { GameIdContext } from '../app'
-import { ConnectionContext, connection, useLeanClient } from '../connection'
 import { useAppDispatch, useAppSelector } from '../hooks'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
 import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
@@ -28,11 +27,11 @@ import { Button } from './button'
 import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
-  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
+  ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
-import { GameHint } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, filterHints } from './hints'
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
+import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import path from 'path';
 
@@ -44,6 +43,16 @@ import 'lean4web/client/src/editor/infoview.css'
 import 'lean4web/client/src/editor/vscode.css'
 import '../css/level.css'
 import { LevelAppBar } from './app_bar'
+import { LeanClient } from 'lean4web/client/src/editor/leanclient'
+import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader'
+import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc'
+import { IConnectionProvider } from 'monaco-languageclient'
+import { monacoSetup } from 'lean4web/client/src/monacoSetup'
+import { onigasmH } from 'onigasm/lib/onigasmH'
+import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals'
+
+
+monacoSetup()
 
 function Level() {
   const params = useParams()
@@ -64,9 +73,9 @@ function Level() {
   </WorldLevelIdContext.Provider>
 }
 
-function ChatPanel({lastLevel}) {
+function ChatPanel({lastLevel, visible = true}) {
   const chatRef = useRef<HTMLDivElement>(null)
-  const {mobile} = useContext(MobileContext)
+  const {mobile} = useContext(PreferencesContext)
   const gameId = useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -75,9 +84,7 @@ function ChatPanel({lastLevel}) {
   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  // If the last step has errors, we want to treat it as if it is part of the second-to-last step
-  let k = proof.length - 1
-  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0
+  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -90,29 +97,6 @@ function ChatPanel({lastLevel}) {
     }
   }
 
-  function hasHiddenHints(i : number): boolean {
-    let step = proof[i]
-    // For example if the proof isn't loaded yet
-    if(!step) {return false}
-    return step.hints.some((hint) => hint.hidden)
-  }
-
-  const activateHiddenHints = (ev) => {
-    // If the last step (`k`) has errors, we want the hidden hints from the
-    // second-to-last step to be affected
-    if (!(proof.length)) {return}
-
-    // state must not be mutated, therefore we need to clone the set
-    let tmp = new Set(showHelp)
-    if (tmp.has(k - withErr)) {
-      tmp.delete(k - withErr)
-    } else {
-      tmp.add(k - withErr)
-    }
-    setShowHelp(tmp)
-    console.debug(`help: ${Array.from(tmp.values())}`)
-  }
-
   useEffect(() => {
     // TODO: For some reason this is always called twice
     console.debug('scroll chat')
@@ -138,29 +122,34 @@ function ChatPanel({lastLevel}) {
 
   let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
 
-  // experimental: Remove all hints that appeared identically in the previous step
-  // This effectively prevent consequtive hints being shown.
-  let modifiedHints : GameHint[][] = filterHints(proof)
-
-  return <div className="chat-panel">
+  return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
     <div ref={chatRef} className="chat">
       {introText?.filter(t => t.trim()).map(((t, i) =>
         // Show the level's intro text as hints, too
         <Hint key={`intro-p-${i}`}
           hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
       ))}
-      {modifiedHints.map((step, i) => {
+      {proof.steps.map((step, i) => {
+        let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
+        if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
+          return <Hints key={`hints-${i}`}
+          hints={filteredHints} showHidden={showHelp.has(i)} step={i}
+          selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
+        }
+      })}
+
+      {/* {modifiedHints.map((step, i) => {
         // It the last step has errors, it will have the same hints
         // as the second-to-last step. Therefore we should not display them.
-        if (!(i == proof.length - 1 && withErr)) {
+        if (!(i == proof.steps.length - 1 && withErr)) {
           // TODO: Should not use index as key.
           return <Hints key={`hints-${i}`}
             hints={step} showHidden={showHelp.has(i)} step={i}
-            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
         }
-      })}
+      })} */}
       <DeletedHints hints={deletedChat}/>
-      {completed &&
+      {proof.completed &&
         <>
           <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
             Level completed! 🎉
@@ -174,7 +163,7 @@ function ChatPanel({lastLevel}) {
       }
     </div>
     <div className="button-row">
-      {completed && (lastLevel ?
+      {proof.completed && (lastLevel ?
         <Button to={`/${gameId}`}>
           <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
         </Button> :
@@ -182,16 +171,13 @@ function ChatPanel({lastLevel}) {
           Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
         </Button>)
         }
-      {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
-        <Button to="" onClick={activateHiddenHints}>
-          Show more help!
-        </Button>
-      }
+      <MoreHelpButton />
     </div>
   </div>
 }
 
-function ExercisePanel({codeviewRef, visible=true}) {
+
+function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -207,14 +193,12 @@ function PlayableLevel({impressum, setImpressum}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
 
   const dispatch = useAppDispatch()
 
-  const difficulty = useSelector(selectDifficulty(gameId))
   const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
   const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
-  const inventory: Array<String> = useSelector(selectInventory(gameId))
 
   const typewriterMode = useSelector(selectTypewriterMode(gameId))
   const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
@@ -223,7 +207,7 @@ function PlayableLevel({impressum, setImpressum}) {
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
 
   // The state variables for the `ProofContext`
-  const [proof, setProof] = useState<Array<ProofStep>>([])
+  const [proof, setProof] = useState<ProofState>({steps: [], diagnostics: [], completed: false, completedWithWarnings: false})
   // When deleting the proof, we want to keep to old messages around until
   // a new proof has been entered. e.g. to consult messages coming from dead ends
   const [deletedChat, setDeletedChat] = useState<Array<GameHint>>([])
@@ -293,12 +277,6 @@ function PlayableLevel({impressum, setImpressum}) {
   // a hint at the beginning of the proof...
   const [selectedStep, setSelectedStep] = useState<number>()
 
-  // if the user inventory changes, notify the server
-  useEffect(() => {
-    let leanClient = connection.getLeanClient(gameId)
-    leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty})
-  }, [inventory])
-
   useEffect (() => {
     // Lock editor mode
     if (level?.data?.template) {
@@ -356,15 +334,15 @@ function PlayableLevel({impressum, setImpressum}) {
 
   useEffect(() => {
     // Forget whether hidden hints are displayed for steps that don't exist yet
-    if (proof.length) {
+    if (proof.steps.length) {
       console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length))))
     }
   }, [proof])
 
   // save showed help in store
   useEffect(() => {
-    if (proof.length) {
+    if (proof.steps.length) {
       console.debug(`showHelp:\n ${showHelp}`)
       dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
     }
@@ -372,7 +350,7 @@ function PlayableLevel({impressum, setImpressum}) {
 
   // Effect when command line mode gets enabled
   useEffect(() => {
-    if (editor && typewriterMode) {
+    if (onigasmH && editor && typewriterMode) {
       let code = editor.getModel().getLinesContent().filter(line => line.trim())
       editor.executeEdits("typewriter", [{
         range: editor.getModel().getFullModelRange(),
@@ -395,7 +373,7 @@ function PlayableLevel({impressum, setImpressum}) {
       //   editor.setSelection(monaco.Selection.fromPositions(endPos, endPos))
       // }
     }
-  }, [editor, typewriterMode])
+  }, [editor, typewriterMode, onigasmH == null])
 
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
@@ -441,7 +419,7 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
 
   let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
 
@@ -468,7 +446,7 @@ export default Level
 /** The site with the introduction text of a world */
 function Introduction({impressum, setImpressum}) {
   const gameId = React.useContext(GameIdContext)
-  const {mobile} = useContext(MobileContext)
+  const {mobile} = useContext(PreferencesContext)
 
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
@@ -531,21 +509,32 @@ function Introduction({impressum, setImpressum}) {
 
 function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
 
-  const connection = React.useContext(ConnectionContext)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
 
-
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
   const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
-  const [infoviewApi, setInfoviewApi] = useState<null|InfoviewApi>(null)
   const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)
 
-  // Create Editor
+  const uriStr = `file:///${worldId}/${levelId}`
+  const uri = monaco.Uri.parse(uriStr)
+
+  const inventory: Array<String> = useSelector(selectInventory(gameId))
+  const difficulty: number = useSelector(selectDifficulty(gameId))
+
   useEffect(() => {
+    const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
+    if (onDidChangeContent) {
+      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
+    }
+
     const editor = monaco.editor.create(codeviewRef.current!, {
+      model,
       glyphMargin: true,
       quickSuggestions: false,
+      lineDecorationsWidth: 5,
+      folding: false,
+      lineNumbers: 'on',
       lightbulb: {
         enabled: true
       },
@@ -557,11 +546,63 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
         enabled: false
       },
       lineNumbersMinChars: 3,
+      tabSize: 2,
       'semanticHighlighting.enabled': true,
       theme: 'vs-code-theme-converted'
     })
+    if (onDidChangeSelection) {
+      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
+    }
+    if (initialSelections) {
+      console.debug("Initial Selection: ", initialSelections)
+      // BUG: Somehow I get an `invalid arguments` bug here
+      // editor.setSelections(initialSelections)
+    }
+    setEditor(editor)
+    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
 
-    const infoProvider = new InfoProvider(connection.getLeanClient(gameId))
+    const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
+
+    const connectionProvider : IConnectionProvider = {
+      get: async () => {
+        return await new Promise((resolve, reject) => {
+          console.log(`connecting ${socketUrl}`)
+          const websocket = new WebSocket(socketUrl)
+          websocket.addEventListener('error', (ev) => {
+            reject(ev)
+          })
+          websocket.addEventListener('message', (msg) => {
+            // console.log(msg.data)
+          })
+          websocket.addEventListener('open', () => {
+            const socket = toSocket(websocket)
+            const reader = new DisposingWebSocketMessageReader(socket)
+            const writer = new WebSocketMessageWriter(socket)
+            resolve({
+              reader,
+              writer
+            })
+          })
+        })
+      }
+    }
+
+    // Following `vscode-lean4/webview/index.ts`
+    const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
+    const infoProvider = new InfoProvider(client)
+    // const div: HTMLElement = infoviewRef.current!
+    const imports = {
+      '@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
+      'react': `${window.location.origin}/react.production.min.js`,
+      'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
+      'react-dom': `${window.location.origin}/react-dom.production.min.js`,
+      'react-popper': `${window.location.origin}/react-popper.production.min.js`
+    }
+    // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
+    setInfoProvider(infoProvider)
+
+    // TODO: it looks like we get errors "File Changed" here.
+    client.restart("Lean4Game")
 
     const editorApi = infoProvider.getApi()
 
@@ -606,54 +647,27 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
 
     setEditor(editor)
     setInfoProvider(infoProvider)
-    setInfoviewApi(infoviewApi)
 
-    return () => { infoProvider.dispose(); editor.dispose() }
-  }, [])
+    infoProvider.openPreview(editor, infoviewApi)
+    const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
 
-  const {leanClient, leanClientStarted} = useLeanClient(gameId)
-  const uriStr = `file:///${worldId}/${levelId}`
-  const uri = monaco.Uri.parse(uriStr)
+    // TODO:
+    // setRestart(() => restart)
 
-  // Create model when level changes
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      if (!model) {
-        model = monaco.editor.createModel(initialCode, 'lean4', uri)
-      }
-      model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
-      editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
-      editor.setModel(model)
-      if (initialSelections) {
-        console.debug("Initial Selection: ", initialSelections)
-        // BUG: Somehow I get an `invalid arguments` bug here
-        // editor.setSelections(initialSelections)
-      }
-
-      return () => {
-        editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
-        model.dispose();
-      }
+    return () => {
+      editor.dispose();
+      model.dispose();
+      abbrevRewriter.dispose();
+      taskgutter.dispose();
+      infoProvider.dispose();
+      client.dispose();
     }
-  }, [editor, levelId, connection, leanClientStarted])
+  }, [gameId, worldId, levelId])
 
-
-  useEffect(() => {
-    if (editor && leanClientStarted) {
-
-      let model = monaco.editor.getModel(uri)
-      infoviewApi.serverRestarted(leanClient.initializeResult)
-
-      infoProvider.openPreview(editor, infoviewApi)
-
-      const taskGutter = new LeanTaskGutter(infoProvider.client, editor)
-      const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
-
-      return () => { abbrevRewriter.dispose(); taskGutter.dispose(); }
-    }
-  }, [editor, connection, leanClientStarted])
+  const showRestartMessage = () => {
+    // setRestartMessage(true)
+    console.log("TODO: SHOW RESTART MESSAGE")
+  }
 
   return {editor, infoProvider, editorConnection}
 }

client/src/components/popup/preferences.tsx

@@ -1,16 +1,42 @@
 import * as React from 'react'
 import { Input, Typography } from '@mui/material'
 import Markdown from '../markdown'
-import Switch from '@mui/material/Switch';
+import { Switch, Button, ButtonGroup } from '@mui/material';
+import Box from '@mui/material/Box';
+import Slider from '@mui/material/Slider';
+
 import FormControlLabel from '@mui/material/FormControlLabel';
 
-import { IMobileContext } from "../infoview/context"
+import { IPreferencesContext } from "../infoview/context"
 
-interface PreferencesPopupProps extends IMobileContext{
+interface PreferencesPopupProps extends Omit<IPreferencesContext, 'mobile'> {
     handleClose: () => void
-} 
+}
+
+export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) {
+
+    const marks = [
+        {
+            value: 0,
+            label: 'Mobile',
+            key: "mobile"
+        },
+        {
+            value: 1,
+            label: 'Auto',
+            key: "auto"
+        },
+        {
+            value: 2,
+            label: 'Desktop',
+            key: "desktop"
+        },
+    ];
+
+    const handlerChangeLayout = (_: Event, value: number) => {
+        setLayout(marks[value].key as IPreferencesContext["layout"])
+    }
 
-export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
     return <div className="modal-wrapper">
         <div className="modal-backdrop" onClick={handleClose} />
         <div className="modal">
@@ -18,34 +44,43 @@ export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile,
             <Typography variant="body1" component="div" className="settings">
                 <div className='preferences-category'>
                     <div className='category-title'>
-                        <h3>Mobile layout</h3>
+                        <h3>Layout</h3>
                     </div>
-                    <div className='preferences-item'>
+                    <div className='preferences-item first leave-left-gap'>
                         <FormControlLabel
                             control={
-                            <Switch
-                                checked={mobile}
-                                onChange={() => setMobile(!mobile)}
-                                name="checked"
-                                color="primary"
-                            />
+                                <Box sx={{ width: 300 }}>
+                                    <Slider
+                                        aria-label="Always visible"
+                                        value={marks.find(item => item.key === layout).value}
+                                        step={1}
+                                        marks={marks}
+                                        max={2}
+                                        sx={{
+                                            '& .MuiSlider-track': { display: 'none', },
+                                        }}
+                                        onChange={handlerChangeLayout}
+                                    />
+                                </Box>
                             }
-                            label="Enable"
-                            labelPlacement="start"
+                            label=""
                         />
                     </div>
+                </div>
+
+                <div className='preferences-category tail-category'>
                     <div className='preferences-item'>
                         <FormControlLabel
                             control={
-                            <Switch
-                                checked={!lockMobile}
-                                onChange={() => setLockMobile(!lockMobile)}
-                                name="checked"
-                                color="primary"
-                            />
+                                <Switch
+                                    checked={isSavePreferences}
+                                    onChange={() => setIsSavePreferences(!isSavePreferences)}
+                                    name="checked"
+                                    color="primary"
+                                />
                             }
-                            label="Auto"
-                            labelPlacement="start"
+                            label="Save my settings (in the browser store)"
+                            labelPlacement="end"
                         />
                     </div>
                 </div>

client/src/components/welcome.tsx

@@ -10,7 +10,7 @@ import { useAppDispatch, useAppSelector } from '../hooks'
 import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
-import { MobileContext } from './infoview/context'
+import { PreferencesContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/game_info'
@@ -27,7 +27,7 @@ import { Hint } from './hints'
 
 /** the panel showing the game's introduction text */
 function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
@@ -64,7 +64,9 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
+  const {layout, isSavePreferences, setLayout, setIsSavePreferences} = React.useContext(PreferencesContext)
+
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
@@ -134,7 +136,7 @@ function Welcome() {
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
-    {preferencesPopup ? <PreferencesPopup mobile={mobile} setMobile={setMobile} lockMobile={lockMobile} setLockMobile={setLockMobile} handleClose={closePreferencesPopup}/> : null}
+    {preferencesPopup ? <PreferencesPopup layout={layout} isSavePreferences={isSavePreferences} setLayout={setLayout} setIsSavePreferences={setIsSavePreferences} handleClose={closePreferencesPopup}/> : null}
   </>
 }
 

client/src/components/world_tree.tsx

@@ -11,11 +11,12 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch, useMobile } from '../hooks'
+import { useAppDispatch } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
 
 import '../css/world_tree.css'
+import { PreferencesContext } from './infoview/context'
 
 // Settings for the world tree
 cytoscape.use( klay )
@@ -197,7 +198,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
-  const { mobile } = useMobile()
+  const { mobile } = React.useContext(PreferencesContext)
 
 
   function label(x : number) {

client/src/connection.ts

@@ -1,68 +0,0 @@
-/**
- *  @fileOverview todo
- */
-
-import * as React from 'react';
-import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import { LeanClient } from 'lean4web/client/src/editor/leanclient';
-
-export class Connection {
-  private game: string = undefined // We only keep a connection to a single game at a time
-  private leanClient: LeanClient = null
-
-  getLeanClient(game): LeanClient {
-    if (this.game !== game) {
-      if (this.leanClient) {
-        this.leanClient.stop() // Stop previous Lean client
-      }
-      this.game = game
-      // Start a new Lean client for the new `gameId`.
-      const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + game
-      const uri = monaco.Uri.parse('file:///')
-      this.leanClient = new LeanClient(socketUrl, undefined, uri, () => {})
-    }
-
-    return this.leanClient
-  }
-
-  /** If not already started, starts the Lean client. resolves the returned promise as soon as a
-   * Lean client is running.
-   */
-  startLeanClient = (game) => {
-    return new Promise<LeanClient>((resolve) => {
-      const leanClient = this.getLeanClient(game)
-      if (leanClient.isRunning()) {
-        resolve(leanClient)
-      } else {
-        if (!leanClient.isStarted()) {
-          leanClient.start()
-        }
-        leanClient.restarted(() => {
-          // This keep alive message is not recognized by the server,
-          // but it makes sure that the websocket connection does not
-          // time out after 60 seconds.
-          setInterval(() => {leanClient.sendNotification('$/keepAlive', {}) }, 5000)
-          resolve(leanClient)
-        })
-      }
-    })
-  }
-}
-
-export const connection = new Connection()
-
-export const ConnectionContext = React.createContext(null);
-
-export const useLeanClient = (gameId) => {
-  const leanClient = connection.getLeanClient(gameId)
-  const [leanClientStarted, setLeanClientStarted] = React.useState(leanClient.isStarted())
-
-  React.useEffect(() => {
-    const t1 = leanClient.restarted(() => { console.log("START"); setLeanClientStarted(true) })
-    const t2 = leanClient.stopped(() => { console.log("STOP"); setLeanClientStarted(false) })
-
-    return () => {t1.dispose(); t2.dispose()}
-  }, [leanClient, setLeanClientStarted])
-
-  return {leanClientStarted, leanClient}
-}

client/src/css/infoview.css

@@ -188,6 +188,18 @@
   flex-direction: row;
 }
 
+.exercise .failed-command {
+  background-color: #eee;
+  padding: .5em;
+  border-radius: .2em;
+  /* TODO: It seems my browsers merge the margings of the proof steps,
+  so that it only shows once 0.5rem instead of twice. Thus have 1.5 here now.
+  */
+  margin-bottom: 1.5rem;
+  display: flex;
+  flex-direction: row;
+}
+
 .exercise .command-text {
   flex: 1;
   background-color: #fff;

client/src/css/level.css

@@ -368,3 +368,8 @@ td code  {
   min-width: 40px;
   text-align: center;
 }
+
+/* DEBUG */
+.proof .step {
+  border: 2px solid rgb(0, 123, 255);
+}

client/src/css/welcome.css

@@ -187,3 +187,15 @@ h5, h6 {
   margin-left: 0.3rem;
   margin-right: 0.3rem;
 }
+
+.preferences-category.tail-category{
+  margin-top: 2em;
+}
+
+.preferences-item.first{
+  margin-top: 1em;
+}
+
+.preferences-item.leave-left-gap{
+  margin-left: 3em;
+}

client/src/hooks.ts

@@ -1,30 +1,6 @@
 import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
 import type { RootState, AppDispatch } from './state/store'
 
-import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences"
-
 // Use throughout your app instead of plain `useDispatch` and `useSelector`
 export const useAppDispatch: () => AppDispatch = useDispatch
 export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector
-
-export const useMobile = () => {
-  const dispatch = useAppDispatch();
-
-  const mobile = useAppSelector((state) => state.preferences.mobile);
-  const lockMobile = useAppSelector((state) => state.preferences.lockMobile);
-
-  const setMobile = (val: boolean) => {
-    dispatch(setMobileState(val));
-  };
-
-  const setLockMobile = (val: boolean) => {
-    dispatch(setLockMobileState(val));
-  };
-
-  return {
-    mobile,
-    setMobile,
-    lockMobile,
-    setLockMobile,
-  };
-};

client/src/index.tsx

@@ -1,7 +1,6 @@
 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 type { RouteObject } from "react-router"
@@ -10,11 +9,8 @@ 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'
 
 
-monacoSetup()
-
 
 // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to
 // `/g/local/game`. This is used for the devcontainer setup
@@ -61,9 +57,7 @@ const root = createRoot(container!);
 root.render(
   <React.StrictMode>
     <Provider store={store}>
-      <ConnectionContext.Provider value={connection}>
-        <RouterProvider router={router} />
-      </ConnectionContext.Provider>
+      <RouterProvider router={router} />
     </Provider>
   </React.StrictMode>
 );

client/src/state/hooks/use_preferences.ts

@@ -0,0 +1,41 @@
+import React, { useState } from "react";
+import { useAppDispatch, useAppSelector } from "../../hooks";
+import { 
+    PreferencesState, 
+    setLayout as setPreferencesLayout, 
+    setIsSavePreferences as setPreferencesIsSavePreferences,
+    getWindowDimensions,
+    AUTO_SWITCH_THRESHOLD
+} from "../preferences";
+
+
+const UsePreferences = () => {
+    const dispatch = useAppDispatch()
+    const [mobile, setMobile] = React.useState<boolean>()
+
+    const layout = useAppSelector((state) => state.preferences.layout);
+    const setLayout = (layout: PreferencesState["layout"]) => dispatch(setPreferencesLayout(layout))
+
+    const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences);
+    const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave))
+
+    const automaticallyAdjustLayout = () => {
+        const {width} = getWindowDimensions()
+        setMobile(width < AUTO_SWITCH_THRESHOLD)
+    }
+
+    React.useEffect(()=>{
+        if (layout === "auto"){
+          void automaticallyAdjustLayout()
+          window.addEventListener('resize', automaticallyAdjustLayout)
+    
+          return () => window.removeEventListener('resize', automaticallyAdjustLayout)
+        } else {
+          setMobile(layout === "mobile")
+        }
+    }, [layout])
+
+    return {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}
+} 
+
+export default UsePreferences;

client/src/state/local_storage.ts

@@ -57,3 +57,12 @@ export function savePreferences(state: any) {
     // Ignore
   }
 }
+
+export function removePreferences() {
+  try {
+    localStorage.removeItem(PREFERENCES_KEY);
+  } catch (e) {
+    // Ignore
+  }
+}
+

client/src/state/preferences.ts

@@ -1,10 +1,10 @@
 import { createSlice } from "@reduxjs/toolkit";
 
-import { loadPreferences } from "./local_storage";
+import { loadPreferences, removePreferences, savePreferences } from "./local_storage";
 
-interface PreferencesState {
-  mobile: boolean;
-  lockMobile: boolean;
+export interface PreferencesState {
+  layout: "mobile" | "auto" | "desktop";
+  isSavePreferences: boolean;
 }
 
 export function getWindowDimensions() {
@@ -12,26 +12,24 @@ export function getWindowDimensions() {
   return {width, height}
 }
 
-const { width } = getWindowDimensions()
-
 export const AUTO_SWITCH_THRESHOLD = 800
 
-const initialState: PreferencesState = loadPreferences() ?? {
-    mobile: width < AUTO_SWITCH_THRESHOLD,
-    lockMobile: false
+const initialState: PreferencesState = loadPreferences() ??{
+    layout: "auto",
+    isSavePreferences: false
 }
 
 export const preferencesSlice = createSlice({
   name: "preferences",
   initialState,
   reducers: {
-    setMobile: (state, action) => {
-      state.mobile = action.payload;
+    setLayout: (state, action) => {
+      state.layout = action.payload;
     },
-    setLockMobile: (state, action) => {
-      state.lockMobile = action.payload;
+    setIsSavePreferences: (state, action) => {
+      state.isSavePreferences = action.payload;
     },
   },
 });
 
-export const { setMobile, setLockMobile } = preferencesSlice.actions;
+export const { setLayout, setIsSavePreferences } = preferencesSlice.actions;

client/src/state/progress.ts

@@ -53,22 +53,22 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false
 
 /** Add an empty skeleton with progress for the current game */
 function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) {
-  if (!state.games[action.payload.game]) {
-    state.games[action.payload.game] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
+  if (!state.games[action.payload.game.toLowerCase()]) {
+    state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
   }
-  if (!state.games[action.payload.game].data) {
-    state.games[action.payload.game].data = {}
+  if (!state.games[action.payload.game.toLowerCase()].data) {
+    state.games[action.payload.game.toLowerCase()].data = {}
   }
 }
 
 /** Add an empty skeleton with progress for the current level */
 function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
   addGameProgress(state, action)
-  if (!state.games[action.payload.game].data[action.payload.world]) {
-    state.games[action.payload.game].data[action.payload.world] = {}
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) {
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {}
   }
-  if (!state.games[action.payload.game].data[action.payload.world][action.payload.level]) {
-    state.games[action.payload.game].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) {
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
   }
 }
 
@@ -79,58 +79,58 @@ export const progressSlice = createSlice({
     /** put edited code in the state and set completed to false */
     codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].code = action.payload.code
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = false
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
     },
     /** TODO: docstring */
     changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].selections = action.payload.selections
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].selections = action.payload.selections
     },
     /** mark level as completed */
     levelCompleted(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = true
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = true
     },
     /** Set the list of rows where help is displayed */
     helpEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, help: number[]}>) {
       addLevelProgress(state, action)
       console.debug(`!setting help to: ${action.payload.help}`)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].help = action.payload.help
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].help = action.payload.help
     },
     /** delete all progress for this game */
     deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) {
-      state.games[action.payload.game] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
+      state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
     },
     /** delete progress for this level */
     deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level] = initalLevelProgressState
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = initalLevelProgressState
     },
     /** load progress, e.g. from external import */
     loadProgress(state: ProgressState, action: PayloadAction<{game: string, data:GameProgressState}>) {
       console.debug(`setting data to:\n ${action.payload.data}`)
-      state.games[action.payload.game] = action.payload.data
+      state.games[action.payload.game.toLowerCase()] = action.payload.data
     },
     /** set the current inventory */
     changedInventory(state: ProgressState, action: PayloadAction<{game: string, inventory: string[]}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].inventory = action.payload.inventory
+      state.games[action.payload.game.toLowerCase()].inventory = action.payload.inventory
     },
     /** set the difficulty */
     changedDifficulty(state: ProgressState, action: PayloadAction<{game: string, difficulty: number}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].difficulty = action.payload.difficulty
+      state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty
     },
     /** set the difficulty */
     changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].openedIntro = action.payload.openedIntro
+      state.games[action.payload.game.toLowerCase()].openedIntro = action.payload.openedIntro
     },
     /** set the typewriter mode */
     changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].typewriterMode = action.payload.typewriterMode
+      state.games[action.payload.game.toLowerCase()].typewriterMode = action.payload.typewriterMode
     }
   }
 })
@@ -138,74 +138,74 @@ export const progressSlice = createSlice({
 /** if the level does not exist, return default values */
 export function selectLevel(game: string, world: string, level: number) {
   return (state) =>{
-    if (!state.progress.games[game]) { return initalLevelProgressState }
-    if (!state.progress.games[game].data[world]) { return initalLevelProgressState }
-    if (!state.progress.games[game].data[world][level]) { return initalLevelProgressState }
-    return state.progress.games[game].data[world][level]
+    if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState }
+    return state.progress.games[game.toLowerCase()].data[world][level]
   }
 }
 
 /** return the code of the current level */
 export function selectCode(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).code
+    return selectLevel(game.toLowerCase(), world, level)(state).code
   }
 }
 
 /** return the current inventory */
 export function selectInventory(game: string) {
   return (state) => {
-    if (!state.progress.games[game]) { return [] }
-    return state.progress.games[game].inventory
+    if (!state.progress.games[game.toLowerCase()]) { return [] }
+    return state.progress.games[game.toLowerCase()].inventory
   }
 }
 
 /** return the code of the current level */
 export function selectHelp(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).help
+    return selectLevel(game.toLowerCase(), world, level)(state).help
   }
 }
 
 /** return the selections made in the current level */
 export function selectSelections(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).selections
+    return selectLevel(game.toLowerCase(), world, level)(state).selections
   }
 }
 
 /** return whether the current level is clompleted */
 export function selectCompleted(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).completed
+    return selectLevel(game.toLowerCase(), world, level)(state).completed
   }
 }
 
 /** return progress for the current game if it exists */
 export function selectProgress(game: string) {
   return (state) => {
-    return state.progress.games[game] ?? null
+    return state.progress.games[game.toLowerCase()] ?? null
   }
 }
 
 /** return difficulty for the current game if it exists */
 export function selectDifficulty(game: string) {
   return (state) => {
-    return state.progress.games[game]?.difficulty ?? DEFAULT_DIFFICULTY
+    return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
   }
 }
 
 /** return whether the intro has been read */
 export function selectOpenedIntro(game: string) {
   return (state) => {
-    return state.progress.games[game]?.openedIntro
+    return state.progress.games[game.toLowerCase()]?.openedIntro
   }
 }
 
 /** return typewriter mode for the current game if it exists */
 export function selectTypewriterMode(game: string) {
   return (state) => {
-    return state.progress.games[game]?.typewriterMode ?? true
+    return state.progress.games[game.toLowerCase()]?.typewriterMode ?? true
   }
 }
 

client/src/state/store.ts

@@ -8,7 +8,7 @@ import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
 import { preferencesSlice } from "./preferences"
-import { saveState, savePreferences } from "./local_storage";
+import { saveState, savePreferences, removePreferences} from "./local_storage";
 
 
 export const store = configureStore({
@@ -19,11 +19,7 @@ export const store = configureStore({
   },
   // Make connection available in thunks:
   middleware: getDefaultMiddleware =>
-    getDefaultMiddleware({
-      thunk: {
-        extraArgument: { connection }
-      }
-    }).concat(apiSlice.middleware),
+    getDefaultMiddleware().concat(apiSlice.middleware),
 });
 
 /**
@@ -33,7 +29,9 @@ export const store = configureStore({
 store.subscribe(
   debounce(() => {
     saveState(store.getState()[progressSlice.name]);
-    savePreferences(store.getState()[preferencesSlice.name]);
+
+    const preferencesState = store.getState()[preferencesSlice.name]
+    preferencesState.isSavePreferences ? savePreferences(preferencesState) : removePreferences()
   }, 800)
 );
 

doc/DOCUMENTATION.md

@@ -1,335 +1,67 @@
-**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)**
+# Server
 
-# Creating a game.
+The server is made out of two parts, named "relay" and "server".
 
-Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game.
+The former, "relay", is the server which
+sets up a socket connection to the client, starts the lean servers to work on files and
+relays messages between the lean server and the client. `index.mjs` is the file that needs to
+be run, which is done for example using `pm2` or by calling `npm run start_server` or
+`npm run production`, see more later.
 
-## Game Structure
+The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver"
+executable which is the lean server that handles the files the player plays on. The second job
+is to provide the lean commands which are used when creating a game. These are located in
+`Commands.lean`.
 
-A game consist of worlds which have multiple levels each. In the following we describe how to create a level file and how to combine these into a game.
 
-### Level
+## Integration into Games
 
-A level file is a lean file that imports at least `import GameServer.Commands` and starts with the following Lean commands.
+Games need the "server" as a lake-dependency, which is done in the game's lakefile.
+
+A game imports `GameServer.Commands` which provides to all the API required to
+create a game.
+
+In particular the lean command `MakeGame` compiles the entire game. Static information is
+stored as JSON files in `.lake/gamedata` for faster loading, while other data is only
+saved to lean env-extensions which the lean server has access to after loading the lean file.
+
+For games to be run successfully, it is important that the "gameserver" executable inside
+the game's `.lake` folder is actually built.
+Currently, this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
+(both commands are to be executed in the game's directory!)
+
+## Modifying the server
+
+### Starting the server
+
+When using the [manual installation](running_locally.md#manual-installation) you can run the server
+using
 
-```lean
-Game "NNG"
-World "Addition"
-Level 1
-Title "The rfl tactic"
 ```
-
-Note that the levels inside a world must have consecutive numbering starting with `1`. The `Game`
-and `World` strings can be anything, see below.
-
-#### Statement
-
-The core of a level is the `Statement`, which is the exercise that should be proven.
-
-```lean
-/-- For all natural numbers $n$, we have $0 + n = n$. -/
-@[simp]
-Statement MyNat.zero_add
-    (n : ℕ) : 0 + n = n := by
-  Hint "You can start a proof by `induction n`."
-  induction n with n hn
-  · Hint "This is the base case."
-    rw [add_zero]
-    rfl
-  · Hint "This is the induction hypothesis"
-    rw [add_succ]
-    Branch
-      simp
-      Hint "A branch is an alternative tactic sequence. Does not need to finish the proof."
-    rw [hn]
-    rfl
-```
-
-##### Proof
-
-The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
-
-There are a few extra tactics that help you structuring the proof:
-
-- `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
-  the one where `Hint` is placed. For more options about hints, see below.
-- `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different   places. The `Branch` does not affect the main
-  proof and does not need to finish any goals.
-- `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
-  will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
-  having a `Template` will force the user to use Editor-mode for this level.
-
-##### Statement Name (optional)
-
-If you specify a name (`MyNat.zero_add`), this lemma will be available in future levels.
-(Note that a future level must also import this level,
-so that Lean knows about the added statement).
-
-The name must be *fully qualified*. (TODO: is that still true? Did we implement namespaces?)
-
-##### Doc Comment (optional)
-
-There are three places where the documentation comment appears:
-
-1. as doc comment when hovering over the theorem
-2. as exercise description at the top of the level: ``Theorem `zero_add`: yada yada.``
-3. in the inventory. This can be overwritten by using
-  `LemmaDoc MyNat.zero_add "different yada yada"` as one might want to add a more detailed
-  description there including examples etc.
-
-Both latter points support Markdown (including katex).
-
-##### Attributes (optional)
-
-the `@[ attributes ]` prefix should work just like you know it from the `theorem` keyword.
-
-#### Introduction/Conclusion
-
-Optionally, you can add an `Introduction "some text"` and `Conclusion "some text"` to your level.
-The introduction will be shown at the beginning, the conclusion is displayed once the level
-is solved.
-
-#### Theorems/Tactics/Definitions
-
-Only enabled theorems/tactics/definitions (called "items" here) are available in a level.
-
-To add a new item in a level, you can add
-
-```lean
-NewTactic rfl simp
-NewLemma MyNat.add_zero MyNat.add_succ
-NewDefinition Nat Pow Mul
-```
-
-Once added, items will be available in all future levels/worlds,
-unless you disable them for a particular level with
-
-```lean
-DisabledTactic tauto
-DisabledLemma MyNat.add_zero
-```
-
-or specify explicitly which items should be available with
-
-```lean
-OnlyTactic rw rfl apply
-OnlyLemma MyNat.add_zero
-```
-
-Lastly, all items need documentation entries (which are imported in the level),
-see more about that below. There is also explains the `LemmaTab` keyword.
-
-### World
-
-Multiple levels are combined into a world and the worlds are then added to the game. It is recommended that all levels of a world are inside one folder (e.g. `NNG/Levels/Addition/`) and
-then there is one world file (`NNG/Levels/Addition.lean`) which contains the following
-
-```lean
-import NNG.Levels.Addition.Level_1
-import NNG.Levels.Addition.Level_2
-
-Game "NNG"
-World "Addition"
-Title "Addition World"
-
-Introduction "some text"
-```
-
-The `Title` is the world's display title. The `Introduction` is displayed before loading level 1.
-Note that all levels of a world should be imported by the world file.
-
-BUG: A level **must not** be imported in a different world's level. Instead, you have to import an entire world there: `import NNG.Levels.Addition`
-
-### Game
-
-The Game itself (i.e. the main file of you lake project, `NNG.lean`) should import all worlds and have the following layout, concluding with `MakeGame`:
-
-```lean
-import NNG.Levels.Addition
-import NNG.Levels.Multiplication
-import NNG.Levels.Power
-
-Game "NNG"
-Title "Natural Number Game"
-Introduction "some text"
-
-MakeGame
-```
-
-The game will automatically compute the order of the worlds depending on the sample proofs of the Levels (ignoring anything inside a `Branch`). You can add additional dependencies manually by adding `Dependency PowerWorld → ImpossibleWorld` before `MakeGame`.
-The order of worlds influences which tactics and lemmas will be unlocked in a given level.
-
-`MakeGame` will display warnings about things in the game that need to be fixed, like missing
-documentation or if a tactic is never introduced.
-
-### Documentation
-
-Each tactic, theorem, or definition (all called items here) that is introduced in the game
-needs a documentation entry. These are statements of the following form:
-
-```lean
-LemmaDoc MyNat.add_squared as "add_squared" in "Pow"
-"(missing)"
-
-TacticDoc constructor
-"(missing)"
-
-DefinitionDoc One as "1"
-"(missing)"
-```
-
-Notes:
-
-* The lemma name must be **fully qualified**. The string display name can be arbitrary.
-* Tactics must have their proper name. use `TacticDoc «have» ""` if it does not work
-  without french quotes.
-* Definition names can be arbitrary. E.g. I used `DefinitionDoc Symbol.Fun as "fun x ↦ x" "(missing)"` once.
-
-Moreover, the lemmas are in sorted in tabs (the `in "Pow`) part. In each level file, you
-can define which tab is open when the level is loaded by adding `LemmaTab "Pow"`.
-
-There will be features added to get automatic information from mathlib!
-
-## Escaping
-(TODO: Move)
-
-
-Inside the doc comment you don't need to escape the backslashes:
-
-```lean
-/-- $\operatorname{succ}(n)$. notation for naturals is `\N`. -/
-Statement ...
-```
-
-However, inside interpolated strings (e.g. in `Hint`, `Introduction` and `Conclusion`)
-you do need to escape backslashes
-with `\\` and `{` with `\{`:
-
-```lean
-Hint "This code has some $\\operatorname\{succ}(n)$ math. The value of `h` is {h}.
-Notation for naturals is `\\N`."
-```
-
-## Game design
-Here are some things you should consider designing a new game:
-
-* A world with more than 16 levels will be displayed with the levels spiraling outwards,
-  it might be desirable to stay below that bound. Above 22 levels the spiral start getting out
-  of control.
-
-# Running Games Locally
-
-The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
-
-## VSCode Dev Containers
-
-1.  **Install Docker and Dev Containers** *(once)*:<br/>
-    See [official instructions](https://code.visualstudio.com/docs/devcontainers/containers#_getting-started).
-    Explicitly this means:
-    * Install docker engine if you have not yet: [Instructions](https://docs.docker.com/engine/install/).
-      I followed the "Server" instructions for linux.
-    * Note that on Linux you need to add your user to the `docker` group
-      ([see instructions](https://docs.docker.com/engine/install/linux-postinstall/)) and probably reboot.
-    * Open the games folder in VSCode: `cd NNG4 && code .` or "Open Folder" within VSCode
-    * a message appears prompting you to install the "Dev Containers" extension (by Microsoft).
-
-2.  **Open Project in Dev Container** *(everytime)*:<br/>
-    Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode.
-    A message appears asking you to "Reopen in Container".
-
-    * The first start will take a while, ca. 2-10 minutes. After the first
-      start this should be very quickly.
-    * Once built, it should open a tab "Simple Browser" inside VSCode displaying
-      the game. (Alternatively, open http://localhost:3000 in your browser).
-
-3.  **Editing Files** *(everytime)*:<br/>
-    After editing some files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`.
-    Now you can reload your browser to see the changes.
-
-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-
-
-## Without Dev Containers
-Install `nvm`:
-```bash
-curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.2/install.sh | bash
-```
-then reopen bash and test with `command -v nvm` if it is available (Should print "nvm").
-
-Now install node:
-```bash
-nvm install node
-```
-
-Clone the game (e.g. `NNG4` here):
-```bash
-git clone https://github.com/hhu-adam/NNG4.git
-# or: git clone git@github.com:hhu-adam/NNG4.git
-```
-
-Download dependencies and build the game:
-```bash
-cd NNG4
-lake update
-lake exe cache get   # if your game depends on mathlib
-lake build
-```
-
-Clone the game repository into a directory next to the game:
-```bash
-cd ..
-git clone https://github.com/leanprover-community/lean4game.git
-# or: git clone git@github.com:leanprover-community/lean4game.git
-```
-The folders `NNG4` and `lean4game` must be in the same directory!
-
-In `lean4game`, install dependencies:
-```bash
-cd lean4game
-npm install
-```
-
-TODO: This is outdated!
-If you are developing a game other than `Robo` or `NNG4`, adapt the
-code at the beginning of `lean4game/relay/index.mjs`:
-```typescript
-const games = {
-    "g/hhu-adam/robo": {
-        dir: "../../../../Robo",
-        queueLength: 5
-    },
-    "g/hhu-adam/nng4": {
-        dir: "../../../../NNG4",
-        queueLength: 5
-    }
-}
-```
-
-Run the game:
-```bash
 npm start
 ```
 
-This takes a little time. Eventually, the server is available on http://localhost:3000/
-and the game is available on http://localhost:3000/#/g/hhu-adam/NNG4.
+This way any changes to files in `client/` or `relay/` will cause the server to restart automatically.
 
-### Modifying the GameServer
+Alternative, you can run `npm run build` followed by the commands
 
-When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with this
-setup by setting `export NODE_ENV=development` inside your local game before building it:
-
-```bash
-cd NNG4
-export NODE_ENV=development
-lake update
-lake build
 ```
-This causes lake to search locally for the `GameServer` lake package instead of using the version from github.
+npm run start_client
+npm run production
+```
+
+(in two separate terminals) to test the production mode of the server. This way it will only
+change once you build and restart the server.
+
+### Modifying the lean server
+
+To test a modified lean server (i.e. content of `server/`), you can use the local dev setup and call
+`lake update -R -Klean4game.local` in your game followed by `lake build`.
+This will cause lake to look for the
+local lean server as a dependency instead of the version it downloaded from git.
+
+You can play a local game at https://localhost:3000/#/g/local/{FolderName} where you replace `{FolderName}` with the game folder name.
+
+After modifications in `server/`, you will need to call `lake build gameserver` (called in `server/` or in your game's folder) to rebuild
+the gameserver executable and
+`lake build` (called in the game's folder) to rebuild the game.

doc/changelog.md

@@ -0,0 +1,9 @@
+# Changelog
+
+## v4.5.0
+
+### Breaking changes
+
+* Fix (#183): local store accepts case insensitive URL. The game progress has previously been saved under case sensitive URLs. You might need to recover old progress from your browser storage.
+
+## Other

doc/create_game.md

@@ -98,7 +98,7 @@ This introduction text is shown when one first enters a world.
 1. Use the template above and make sure you import all levels of this world.
 1. In `Game.lean` import the world with `import Game.Levels.MyWorld`
 
-Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
+Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently, it shows
 
 ```text
 No world introducing sorry, but required by MyWorld
@@ -125,23 +125,32 @@ The player has an inventory with tactics, theorems, and definitions that unlock
 
 ```lean
 NewTactic induction simp
-NewLemma Nat.zero_mul
+NewTheorem Nat.zero_mul
 NewDefinition Pow
 ```
 
+**Important:** All commands in this section 6a) expect the `Name` they take as input
+to be **fully qualified**. For example `NewTheorem Nat.zero_mul` and not `NewTheorem zero_mul`.
+
 #### Doc entries
 
-You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
+You'll see a warning about a missing Theorem documentation. You can fix it by adding doc-entries like the following somewhere above it.
 
 ```lean
-LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
-"some description"
+/--
+some description
+-/
+TheoremDoc Nat.zero_mul as "zero_mul" in "Mul"
 
+/--
+some description
+-/
 TacticDoc simp
-"some description"
 
+/--
+some description
+-/
 DefinitionDoc Pow as "^"
-"some description"
 ```
 
 (e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
@@ -153,7 +162,7 @@ If you do not provide any content for the inventory, the game will try to find a
 You have a few options to disable inventory items that have been unlocked in previous levels:
 
 ```lean
-DisableTactic, DisableLemma, OnlyTactic, OnlyLemma
+DisabledTactic, DisabledTheorem, OnlyTactic, OnlyTheorem
 ```
 
 have the same syntax as above. The former two disable items for this level, the latter two
@@ -161,7 +170,7 @@ disable all items except the ones specified.
 
 #### Theorem Tab
 
-Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
+Theorems are sorted into tabs. With `TheoremTab "Mul"` you specify which tab should be open by default in this level.
 
 #### HiddenTactic
 
@@ -176,12 +185,14 @@ and only `rw` would show up in the inventory.
 
 ### 6. b) Statement
 
-The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
+The statement is the exercise of the level. The basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
 
 #### Name
 
 You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
 
+You can but a `Statement` inside namespaces like you would with `theorem`.
+
 #### Doc String / Exercise statement
 
 Add a docstring that contains the exercise statement in natural language. If you do this, it will appear at the top of the exercise. It supports Latex.
@@ -205,12 +216,12 @@ Statement my_simp_lemma ...
 
 The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
 
-There are a few extra tactics that help you structuring the proof:
+There are a few extra tactics that help you with structuring the proof:
 
 - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
   the one where `Hint` is placed. For more options about hints, see below.
 - `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different places. The `Branch` does not affect the main
+  helps to set `Hints` in different places. The `Branch` does not affect the main
   proof and does not need to finish any goals.
 - `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
   will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
@@ -225,23 +236,23 @@ Most important for game development are probably the `Hints`.
 The hints will be displayed whenever the player's current goal matches the goal the hint is
 placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands.
 
-Read [More about Hints](doc/hints.md) for how they work and what the options are.
+Read [More about Hints](hints.md) for how they work and what the options are.
 
 ### 6. e) Extra: Images
 You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game.
 
-The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"` 
+The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"`
 in one of the files you created in 2), 3), or 4) (i.e. game/world/level).
 
 NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world.
 
 ## 7. Update your game
 
-In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md).
+In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](update_game.md).
 
 ## 8. Publish your game
 
-To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
+To publish your game on the official server, see [Publishing a game](publish_game.md)
 
 There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page:
 
@@ -253,7 +264,7 @@ Prerequisites "NNG"
 CoverImage "images/cover.png"
 ```
 * `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
-* `CaptionShort`: One catch phrase. Appears above the image.
+* `CaptionShort`: One catchphrase. Appears above the image.
 * `CaptionLong`: 2-4 sentences to describe the game.
 * `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text.
 * `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens.

doc/hints.md

@@ -10,6 +10,8 @@ Statement .... := by
   ...
 ```
 
+Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof.
+
 ## 1. When do hints show?
 
 A hint will be displayed if the player's goal matches the one where the hint was placed in the
@@ -17,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in
 player's context. The player's context may contain additional items.
 
 This means if you have multiple identical
-subgoals, you should only place a single hint in one of them and it will be displayed in
+subgoals, you should only place a single hint in one of them, and it will be displayed in
 all of them.
 
 However, identical (non-hidden) hints which where already present in the step
@@ -30,12 +32,12 @@ Hidden hints are not filtered.
 You can use `Branch` to place hints
 in dead ends or alternative proof strands.
 
-A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end
+A proof inside a `Branch`-block is normally evaluated by lean, but it's discarded at the end
 so that no progress has been made on proofing the goal.
 
 ```
 Statement .... := by
-  Hint "Huse `rw` or `rewrite`."
+  Hint "use `rw` or `rewrite`."
   Branch
     rewrite [h]
     Hint "now you still need `rfl`"

doc/publish_game.md

@@ -1,6 +1,6 @@
 # Publishing games
 
-You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple
+You can publish your game on the official [Lean Game Server](https://adam.math.hhu.de) in a few simple
 steps.
 
 ## 1. Upload Game to github
@@ -11,7 +11,7 @@ tab.
 
 ## 2. Import the game
 
-You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
+You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call
 the URL of the form
 
 > adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}

doc/running_locally.md

@@ -2,6 +2,8 @@
 
 The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
 
+Please also consult the [Troubleshooting Collection](troubleshoot.md), where some known pitfalls are collected.
+
 There are several options to play a game locally:
 
 1. VSCode Dev Container: needs `docker` installed on your machine
@@ -31,24 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
 
     * The first start will take a while, ca. 2-15 minutes. After the first
       start this should be very quickly.
-    * Once built, you can open http://localhost:3000 in your browser. which should load the game.
+    * Once built, you can open http://localhost:3000 in your browser, which should load the game.
 
 3.  **Editing Files** *(everytime)*:<br/>
     After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes.
 
-### Errors
-
-* If you don't get the pop-up, you might have disabled them and you can reenable it by
-  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
-* If the starting the container fails, in particular with a message `Error: network xyz not found`,
-  you might have deleted stuff from docker via your shell. Try deleting the container and image
-  explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
-  container. (this will again take some time)
-* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
-
 ## Codespaces
 
-You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
+You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser".
 
 Note: You have to wait until npm started properly, which might take a good while.
 
@@ -108,6 +100,29 @@ Run the game:
 npm start
 ```
 
+You should see a message like this:
+```bash
+[server] > lean4-game@0.1.0 start_server
+[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
+[server]
+[client]
+[client] > lean4-game@0.1.0 start_client
+[client] > cross-env NODE_ENV=development vite --host
+[client]
+[server] [nodemon] 3.0.#
+[server] [nodemon] to restart at any time, enter `rs`
+[server] [nodemon] watching path(s): *.*
+[server] [nodemon] watching extensions: mjs
+[server] [nodemon] starting `node ./index.mjs`
+[client]
+[client]   VITE v4.5.1  ready in \#\#\# ms
+[client]
+[client]   ➜  Local:   http://localhost:3000/
+[client]   ➜  Network: http://###.###.###.##:3000/
+[client] [vite-plugin-static-copy] Collected 7 items.
+[server] (node:#####) [DEP0040] [server] Listening on 8080
+```
+
 This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game.
 
 ## Modifying the GameServer

doc/server.md

@@ -6,7 +6,7 @@ In order to set up the server to allow imports, one needs to create a
 repos will suffice.
 
 You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN`
-with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if
+with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if
 you're using `pm2`
 
 Then people can call:
@@ -22,7 +22,7 @@ where you replace:
 
 > https://{website}/#/g/{owner}/{repo}
 
-## data management
+## Data management
 Everything downloaded remains in the folder `lean4game/games`.
-the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
+The subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
 The other folders should only contain the built lean-games, sorted by owner and repo.

doc/troubleshoot.md

@@ -0,0 +1,28 @@
+# Troubleshooting
+
+Here are some issues experienced by users.
+
+# VSCode Dev-Container
+* If you don't get the pop-up, you might have disabled them, and you can reenable it by
+  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
+* If the starting the container fails, in particular with a message `Error: network xyz not found`,
+  you might have deleted stuff from docker via your shell. Try deleting the container and image
+  explicitly in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the
+  container. (this will again take some time)
+* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible.
+
+
+# Manual Installation
+Here are known issues/pitfalls with the local setup using `npm`.
+
+* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display
+  ```
+  [server] sh: line 0: cd: server: No such file or directory
+  [server] npm run start_server exited with code 1
+  ```
+  As a fix you might need to delete your manually set `CDPATH` environment variable.
+
+# Publication
+Errors concerning uploads to the server.
+
+* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable".

doc/update_game.md

@@ -9,8 +9,8 @@ Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https:
 
 Then, depending on the setup you use, do one of the following:
 
-* Dev Container: Rebuild the VSCode Devcontainer.
-* Local Setup: in your game's folder run the following:
+* **Dev Container**: Rebuild the VSCode Devcontainer (without Cache!).
+* **Local Setup**: in your game's folder run the following:
   ```
   lake update -R
   lake build
@@ -24,7 +24,7 @@ Then, depending on the setup you use, do one of the following:
     npm install
     ```
     where `{VERSION_TAG}` is the tag from above of the form `v4.X.0`
-* Gitpod/Codespaces: Create a fresh one
+* **Gitpod/Codespaces**: Create a fresh one
 
 This will update your game (and the mathlib version you might be using) to the new lean version.
 

package.json

@@ -28,8 +28,8 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web",
-    "octokit": "^2.0.14",
+    "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
+    "octokit": "^3.1.2",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",

relay/index.mjs

@@ -19,7 +19,8 @@ import { importTrigger, importStatus } from './import.mjs'
 const queueLength = {
   "g/hhu-adam/robo": 2,
   "g/hhu-adam/nng4": 5,
-  "g/djvelleman/stg4": 2,
+  "g/djvelleman/stg4": 0,
+  "g/trequetrum/lean4game-logic": 0,
 }
 
 const __filename = url.fileURLToPath(import.meta.url);

relay/unpack.sh

@@ -28,3 +28,7 @@ do
   #tar -xvzf $f -C games/${OWNER}/${REPO}
   unzip -q -o $f -d ${OWNER}/${REPO}
 done
+
+# Delete temporary files
+rm -f tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip
+rm -fr tmp/${OWNER}_${REPO}_${ARTIFACT_ID}

server/GameServer.lean

@@ -1,5 +1,4 @@
 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`
@@ -10,13 +9,9 @@ unsafe def main : List String → IO UInt32 := fun args => do
 
   Lean.enableInitializersExecution
 
+  -- TODO: remove this argument
   if args[0]? == some "--server" then
-    MyServer.Watchdog.watchdogMain args
-  else if args[0]? == some "--worker" then
-    MyServer.FileWorker.workerMain {}
+    GameServer.FileWorker.workerMain {} args
   else
-    e.putStrLn s!"Expected `--server` or `--worker`"
+    e.putStrLn s!"Expected `--server`"
     return 1
-
-
--- TODO: Potentially it could be useful to pass in the `gameName` via the websocket connection

server/GameServer/EnvExtensions.lean

@@ -293,6 +293,7 @@ structure LevelInfo where
   descrText : Option String := none
   descrFormat : String := ""
   lemmaTab : Option String
+  module : Name
   displayName : Option String
   statementName : Option String
   template : Option String
@@ -317,6 +318,7 @@ def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo :=
       | some tile => tile.category
       | none => none
     statementName := lvl.statementName.toString
+    module := lvl.module
     displayName := match lvl.statementName with
       | .anonymous => none
       | name => match (inventoryExt.getState env).find?
@@ -381,7 +383,7 @@ structure GameTile where
 
   TODO: What's the format? -/
   image: String := default
-deriving Inhabited, ToJson
+deriving Inhabited, ToJson, FromJson
 
 structure Game where
   /-- Internal name of the game. -/
@@ -401,7 +403,7 @@ structure Game where
   tile : GameTile := default
   /-- The path to the background image of the world. -/
   image : String := default
-deriving Inhabited, ToJson
+deriving Inhabited, ToJson, FromJson
 
 def getGameJson (game : «Game») : Json := Id.run do
   let gameJson : Json := toJson game

server/GameServer/FileWorker.lean

@@ -1,9 +1,12 @@
-/- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/
+/- This file is adapted from `Lean/Server/FileWorker.lean`. -/
 import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
+import GameServer.SaveData
+import GameServer.EnvExtensions
 
 namespace MyModule
+
 open Lean
 open Elab
 open Parser
@@ -17,7 +20,7 @@ private def mkEOI (pos : String.Pos) : Syntax :=
   mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
-  (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
+  (mps : ModuleParserState) (messages : MessageLog) :
     Syntax × ModuleParserState × MessageLog × String.Pos := Id.run do
   let mut pos := mps.pos
   let mut recovering := mps.recovering
@@ -47,7 +50,8 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
 
 end MyModule
 
-namespace MyServer.FileWorker
+namespace GameServer.FileWorker
+
 open Lean
 open Lean.Server
 open Lean.Server.FileWorker
@@ -56,88 +60,137 @@ open IO
 open Snapshots
 open JsonRpc
 
+/--
+Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
+used by the Lean server.
+-/
+structure WorkerState :=
+  /--
+  Collection of items which are considered unlocked.
+  Tactics and theorems are mixed together.
+  -/
+  inventory : Array String
+  /--
+  Difficulty determines whether tactics/theorems can be locked.
+  * 0: do not check
+  * 1: give warnings when locked items are used
+  * 2: give errors when locked items are used
+  -/
+  difficulty : Nat
+  /--
+  `levelInfo` contains all the (static) information about the level which is not influenced
+  by the user's progress.
+  -/
+  levelInfo : LevelInfo
+deriving ToJson, FromJson
+
+/--
+Pack the our custom `WorkerState` on top of the normal worker monad
+`Server.FileWorker.WorkerM`.
+-/
+abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
+
 section Elab
 
-def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
+/-- Add a message. use `(severity := .warning)` to specify the severity-/
+def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
+    (severity := MessageSeverity.warning) (s : MessageData) :
     Elab.Command.CommandElabM Unit := do
   modify fun st => { st with
-      messages := st.messages.add {
-        fileName := inputCtx.fileName
-        severity := MessageSeverity.error
-        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-        data     := s
-      }
-    }
+    messages := st.messages.add {
+      fileName := inputCtx.fileName
+      severity := severity
+      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      data     := s }}
 
 -- TODO: use HashSet for allowed tactics?
-/-- Find all tactics in syntax object that are forbidden according to a
-set `allowed` of allowed tactics. -/
-partial def findForbiddenTactics (inputCtx : Parser.InputContext)
-    (levelParams : Game.DidOpenLevelParams) (stx : Syntax) :
-    Elab.Command.CommandElabM Unit := do
+/--
+Find all tactics in syntax object that are forbidden according to a
+set `allowed` of allowed tactics.
+-/
+partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : WorkerState)
+    (stx : Syntax) : Elab.Command.CommandElabM Unit := do
+  let levelInfo := workerState.levelInfo
+  -- Parse the syntax object and look for tactics and declarations.
   match stx with
   | .missing => return ()
   | .node _info _kind args =>
+    -- Go inside a node.
     for arg in args do
-      findForbiddenTactics inputCtx levelParams arg
+      findForbiddenTactics inputCtx workerState arg
   | .atom info val =>
-    -- ignore syntax elements that do not start with a letter
-    -- and ignore "with" keyword
-    let allowed := ["with", "fun", "at", "only", "by", "to"]
+    -- Atoms might be tactic names or other keywords.
+    -- Note: We whitelisted known keywords because we cannot
+    -- distinguish keywords from tactic names.
+    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
+    -- Ignore syntax elements that do not start with a letter or are listed above.
     if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
-      let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp`
-      match levelParams.tactics.find? (·.name.toString == val) with
+      -- Treat `simp?` and `simp!` like `simp`
+      let val := val.dropRightWhile (fun c => c == '!' || c == '?')
+      match levelInfo.tactics.find? (·.name.toString == val) with
       | none =>
-        -- Note: This case means that the tactic will never be introduced in the game.
-        match levelParams.inventory.find? (· == val) with
+        -- Tactic will never be introduced in the game.
+        match workerState.inventory.find? (· == val) with
+        | some _ =>
+          -- Tactic is in the inventory, allow it.
+          -- Note: This case shouldn't be possible...
+          pure ()
         | none =>
-          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
-        | some _ => pure () -- tactic is in the inventory, allow it.
+          -- Tactic is not in the inventory.
+          addMessageByDifficulty info s!"The tactic '{val}' is not available in this game!"
       | some tac =>
-        if tac.locked then
-          match levelParams.inventory.find? (· == val) with
+        -- Tactic is introduced at some point in the game.
+        if tac.disabled then
+          -- Tactic is disabled in this level.
+          addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!"
+        else if tac.locked then
+          match workerState.inventory.find? (· == val) with
           | none =>
-            addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
-          | some _ => pure () -- tactic is in the inventory, allow it.
-        else if tac.disabled then
-          addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
+            -- Tactic is marked as locked and not in the inventory.
+            addMessageByDifficulty info s!"You have not unlocked the tactic '{val}' yet!"
+          | some _ =>
+            -- Tactic is in the inventory, allow it.
+            pure ()
   | .ident info _rawVal val _preresolved =>
-      let ns ←
-        try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
-      for n in ns do
-        let some (.thmInfo ..) := (← getEnv).find? n
-          | return () -- not a theorem -> ignore
+    -- Try to resolve the name
+    let ns ←
+      try resolveGlobalConst (mkIdent val)
+      -- Catch "unknown constant" error
+      catch | _ => pure []
+    for n in ns do
+      let some (.thmInfo ..) := (← getEnv).find? n
+        -- Not a theorem, no checks needed.
+        | return ()
+      if some n = levelInfo.statementName then
         -- Forbid the theorem we are proving currently
-        if n = levelParams.statementName then
-          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+        addMessage info inputCtx (severity := .error)
+          s!"Structural recursion: you can't use '{n}' to proof itself!"
+      let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+      match theoremsAndDefs.find? (·.name == n) with
+      | none =>
+        -- Theorem will never be introduced in this game
+        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+      | some thm =>
+        -- Theorem is introduced at some point in the game.
+        if thm.disabled then
+          -- Theorem is disabled in this level.
+          addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
+        else if thm.locked then
+          -- Theorem is still locked.
+          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
 
-        let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
-        match lemmasAndDefs.find? (fun l => l.name == n) with
-        | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
-        | some lem =>
-          if lem.locked then
-            addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
-          else if lem.disabled then
-            addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
-where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := levelParams.difficulty
+where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
+  -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
+  -- deppending on difficulty.
+  let difficulty := workerState.difficulty
   if difficulty > 0 then
-    modify fun st => { st with
-      messages := st.messages.add {
-        fileName := inputCtx.fileName
-        severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning
-        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-        data     := s
-      }
-    }
+    addMessage info inputCtx (if difficulty > 1 then .error else .warning) s
   else pure ()
--- where addErrorMessage (info : SourceInfo) (s : MessageData) :=
---   pure ()
 
 open Elab Meta Expr in
+
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (levelParams : Game.DidOpenLevelParams)
+    (couldBeEndSnap : Bool) (gameWorkerState : WorkerState)
     (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -168,7 +221,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     Elab.Command.catchExceptions
       (getResetInfoTrees *> do
         let some level ← GameServer.getLevelByFileName? initParams inputCtx.fileName
-          | throwError "Level not found: {inputCtx.fileName}"
+          | panic! s!"Level not found: {inputCtx.fileName} / {GameServer.levelIdFromFileName? initParams inputCtx.fileName}"
         let scope := level.scope
 
         -- use open namespaces and options as in the level file
@@ -186,12 +239,12 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
             currNamespace := scope.currNamespace,
             openDecls := scope.openDecls }
           let (tacticStx, cmdParserState, msgLog, endOfWhitespace) :=
-            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog couldBeEndSnap
+            MyModule.parseTactic inputCtx pmctx snap.mpState snap.msgLog
           modify (fun s => { s with messages := msgLog })
           parseResultRef.set (tacticStx, cmdParserState)
 
           -- Check for forbidden tactics
-          findForbiddenTactics inputCtx levelParams tacticStx
+          findForbiddenTactics inputCtx gameWorkerState tacticStx
 
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
@@ -219,6 +272,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
     }
 
   let (tacticStx, cmdParserState) ← parseResultRef.get
+  if tacticStx.isMissing then throwServerError "Tactic execution went wrong. No stx found."
 
   let postCmdSnap : Snapshot := {
     beginPos := tacticStx.getPos?.getD 0
@@ -245,7 +299,7 @@ where
   private def publishIleanInfo (method : String) (m : DocumentMeta) (hOut : FS.Stream)
       (snaps : Array Snapshot) : IO Unit := do
     let trees := snaps.map fun snap => snap.infoTree
-    let references := findModuleRefs m.text trees (localVars := true)
+    let references ← findModuleRefs m.text trees (localVars := true) |>.toLspModuleRefs
     let param := { version := m.version, references : LeanIleanInfoParams }
     hOut.writeLspNotification { method, param }
 
@@ -259,6 +313,79 @@ where
     uri : String
   deriving ToJson, FromJson
 
+structure GameDiagnostics where
+  diagnostics : List Diagnostic
+deriving ToJson, FromJson
+
+structure GameParams where
+  uri : String
+  diagnostics : GameDiagnostics
+deriving ToJson, FromJson
+
+/-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
+def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
+    IO Unit := do
+  -- let text := m.text
+
+  -- -- `snap` is the one snapshot containing the entire proof.
+  -- let mut goals : Array <| InteractiveGoalsWithHints := #[]
+  -- for pos in text.positions do
+  --   let source := text.getLineBefore pos
+  --   -- iterate over all newlines in the proof and get the goals and hints at each position
+  --   if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? text pos then
+  --     pure ()
+  --     let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
+  --       fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
+  --         -- TODO: What does this function body do?
+  --         -- let ciAfter := { ci with mctx := ti.mctxAfter }
+  --         let ci := if useAfter then
+  --             { ci with mctx := tacticInfo.mctxAfter }
+  --           else
+  --             { ci with mctx := tacticInfo.mctxBefore }
+  --         -- compute the interactive goals
+  --         let goalMvars : List MVarId ← ci.runMetaM {} do
+  --           return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
+
+  --         let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
+  --           goalMvars.mapM fun goal => do
+  --             let hints ← findHints goal m initParams
+  --             let interactiveGoal ← goalToInteractive goal
+  --             return ⟨interactiveGoal, hints⟩
+  --         -- TODO: This code is way old, can it be deleted?
+  --         -- compute the goal diff
+  --         -- let goals ← ciAfter.runMetaM {} (do
+  --         --     try
+  --         --       Widget.diffInteractiveGoals useAfter ti goals
+  --         --     catch _ =>
+  --         --       -- fail silently, since this is just a bonus feature
+  --         --       return goals
+  --         -- )
+  --         return interactiveGoals
+  --     let goalAtPos : Array InteractiveGoalWithHints := ⟨goalAtPos.foldl (· ++ ·) []⟩
+  --     goals := goals.push ⟨goalAtPos, source⟩
+  --   else
+  --     -- No goals present
+  --     goals := goals.push default
+
+  -- -- Question: Is there a difference between the diags of this snap and the last snap?
+  -- -- Should we get the diags from there?
+  -- let diag : Array Widget.InteractiveDiagnostic := snap.interactiveDiags.toArray
+
+  -- -- Level is completed if there are no errrors or warnings
+  -- let completed : Bool := ¬ diag.any (fun d =>
+  --   d.severity? == some .error ∨ d.severity? == some .warning)
+
+  -- let param : ProofState := {
+  --   steps := goals,
+  --   diagnostics := diag,
+  --   completed := completed }
+
+  -- TODO
+  let param := { uri := m.uri : GameCompletedParams}
+
+
+  hOut.writeLspNotification { method := "$/game/publishProofState", param }
+
   /-- Checks whether game level has been completed and sends a notification to the client -/
   def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
     -- check if there is any error or warning
@@ -268,319 +395,364 @@ where
     let param := { uri := m.uri : GameCompletedParams}
     hOut.writeLspNotification { method := "$/game/completed", param }
 
-  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
-  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (levelParams : Game.DidOpenLevelParams) (initParams : Lsp.InitializeParams)
-      : AsyncElabM (Option Snapshot) := do
+  /-- copied from `Lean.Server.FileWorker.nextCmdSnap`. -/
+  -- @[inherit_doc Lean.Server.FileWorker.nextCmdSnap] -- cannot inherit from private
+  private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams) :
+      AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
     let .some lastSnap := s.snaps.back? | panic! "empty snapshots"
     if lastSnap.isAtEnd then
-      publishGameCompleted m ctx.hOut s.snaps
       publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
       publishProgressDone m ctx.hOut
-      -- This will overwrite existing ilean info for the file, in case something
-      -- went wrong during the incremental updates.
       publishIleanInfoFinal m ctx.hOut s.snaps
       return none
     publishProgressAtPos m lastSnap.endPos ctx.hOut
+
+    -- (modified part)
     -- Make sure that there is at least one snap after the head snap, so that
     -- we can see the current goal even on an empty document
     let couldBeEndSnap := s.snaps.size > 1
     let snap ← compileProof m.mkInputContext lastSnap ctx.clientHasWidgets couldBeEndSnap
-      levelParams initParams
+      gameWorkerState initParams
+
     set { s with snaps := s.snaps.push snap }
-    -- TODO(MH): check for interrupt with increased precision
     cancelTk.check
-    /- NOTE(MH): This relies on the client discarding old diagnostics upon receiving new ones
-      while preferring newer versions over old ones. The former is necessary because we do
-      not explicitly clear older diagnostics, while the latter is necessary because we do
-      not guarantee that diagnostics are emitted in order. Specifically, it may happen that
-      we interrupted this elaboration task right at this point and a newer elaboration task
-      emits diagnostics, after which we emit old diagnostics because we did not yet detect
-      the interrupt. Explicitly clearing diagnostics is difficult for a similar reason,
-      because we cannot guarantee that no further diagnostics are emitted after clearing
-      them. -/
-    -- NOTE(WN): this is *not* redundant even if there are no new diagnostics in this snapshot
-    -- because empty diagnostics clear existing error/information squiggles. Therefore we always
-    -- want to publish in case there was previously a message at this position.
+    publishProofState m snap initParams ctx.hOut
     publishDiagnostics m snap.diagnostics.toArray ctx.hOut
     publishIleanInfoUpdate m ctx.hOut #[snap]
     return some snap
 
-  /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
-  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (levelParams : Game.DidOpenLevelParams)
+  -- Copied from `Lean.Server.FileWorker.unfoldCmdSnaps` using our own `nextCmdSnap`.
+  @[inherit_doc Lean.Server.FileWorker.unfoldCmdSnaps]
+  def unfoldCmdSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
     if headerSnap.msgLog.hasErrors then
-      -- Treat header processing errors as fatal so users aren't swamped with
-      -- followup errors
       publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
       publishIleanInfoFinal m ctx.hOut #[headerSnap]
       return AsyncList.ofList [headerSnap]
     else
-      -- This will overwrite existing ilean info for the file since this has a
-      -- higher version number.
       publishIleanInfoUpdate m ctx.hOut snaps
       return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
         IO.sleep startAfterMs
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk levelParams ctx.initParams) { snaps })
+        AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
-structure GameWorkerState :=
-(levelParams : Game.DidOpenLevelParams)
-
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
-
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
-  def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
-    let s ← get
-    let levelParams := s.levelParams
-    let ctx ← read
-    let oldDoc := (← StateT.lift get).doc
-    oldDoc.cancelTk.set
-    let initHeaderStx := (← StateT.lift get).initHeaderStx
-    let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
-    let cancelTk ← CancelToken.new
-    let headSnapTask := oldDoc.cmdSnaps.waitHead?
-    let newSnaps ← if initHeaderStx != newHeaderStx then
-      EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
-        IO.sleep ctx.initParams.editDelay.toUInt32
-        cancelTk.check
-        IO.Process.exit 2
-    else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
-      -- There is always at least one snapshot absent exceptions
-      let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
-      let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
-      let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
-      -- Ignore exceptions, we are only interested in the successful snapshots
-      let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
-      -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
-      -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
-      let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
-      if h : validSnaps.length ≤ 1 then
-        validSnaps := [newHeaderSnap]
-      else
-        /- When at least one valid non-header snap exists, it may happen that a change does not fall
-           within the syntactic range of that last snap but still modifies it by appending tokens.
-           We check for this here. We do not currently handle crazy grammars in which an appended
-           token can merge two or more previous commands into one. To do so would require reparsing
-           the entire file. -/
-        have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
-        let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
-        let preLastSnap :=
-          have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
-          have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
-          validSnaps[validSnaps.length - 2]
-        let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
-        if newLastStx != lastSnap.stx then
-          validSnaps := validSnaps.dropLast
-      -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
-      -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-      unfoldSnaps newMeta validSnaps.toArray cancelTk levelParams ctx
-        (startAfterMs := ctx.initParams.editDelay.toUInt32)
-    StateT.lift <| modify fun st => { st with
-      doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
+def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
+  let s ← get
+  let ctx ← read
+  let oldDoc := (← StateT.lift get).doc
+  oldDoc.cancelTk.set
+  let initHeaderStx := (← StateT.lift get).initHeaderStx
+  let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
+  let cancelTk ← CancelToken.new
+  let headSnapTask := oldDoc.cmdSnaps.waitHead?
+  let newSnaps ← if initHeaderStx != newHeaderStx then
+    EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+      IO.sleep ctx.initParams.editDelay.toUInt32
+      cancelTk.check
+      IO.Process.exit 2
+  else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
+    -- There is always at least one snapshot absent exceptions
+    let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
+    let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
+    let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
+    -- Ignore exceptions, we are only interested in the successful snapshots
+    let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
+    -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
+    -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
+    let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
+    if h : validSnaps.length ≤ 1 then
+      validSnaps := [newHeaderSnap]
+    else
+      /- When at least one valid non-header snap exists, it may happen that a change does not fall
+          within the syntactic range of that last snap but still modifies it by appending tokens.
+          We check for this here. We do not currently handle crazy grammars in which an appended
+          token can merge two or more previous commands into one. To do so would require reparsing
+          the entire file. -/
+      have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
+      let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
+      let preLastSnap :=
+        have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
+        have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
+        validSnaps[validSnaps.length - 2]
+      let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
+      if newLastStx != lastSnap.stx then
+        validSnaps := validSnaps.dropLast
+    -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
+    -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
+    unfoldCmdSnaps newMeta validSnaps.toArray cancelTk s ctx
+      (startAfterMs := ctx.initParams.editDelay.toUInt32)
+  StateT.lift <| modify fun st => { st with
+    doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
 
 end Updates
 
 section Initialization
 
-  def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
-    input    := "" -- No header!
-    fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
-    fileMap  := default
+def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
+  input    := "" -- No header!
+  fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
+  fileMap  := default
 
-  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
-      (levelParams : Game.DidOpenLevelParams) (initParams : InitializeParams) :
-      IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
-    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-    let out ← IO.Process.output
-      { cwd := levelParams.gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-    if out.exitCode != 0 then
-      throwServerError s!"Error while running Lake: {out.stderr}"
+/-- `gameDir` and `module` were added.
 
-    -- Make the paths relative to the current directory
-    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-    let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (levelParams.gameDir : System.FilePath) / p
+TODO: In general this resembles little similarity with the
+original code, and I don't know why...
+-/
+-- @[inherit_doc Lean.Server.FileWorker.compileHeader]
+def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
+    (gameDir : String) (module : Name):
+    IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
+  -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
+  let out ← IO.Process.output
+    { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+  if out.exitCode != 0 then
+    throwServerError s!"Error while running Lake: {out.stderr}"
 
-    -- Set the search path
-    Lean.searchPathRef.set paths
+  -- Make the paths relative to the current directory
+  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
+  let currentDir ← IO.currentDir
+  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
 
-    let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }]
-    -- return (env, paths)
+  -- Set the search path
+  Lean.searchPathRef.set paths
 
-    -- use empty header
-    let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
-      {m.mkInputContext with
-        input := ""
-        fileMap := FileMap.ofString ""}
-    (headerStx, ·) <$> EIO.asTask do
-      let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
-      let headerEnv := env
-      let mut headerEnv := headerEnv
-      try
-        if let some path := System.Uri.fileUriToPath? m.uri then
-          headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
-      catch _ => pure ()
-      let cmdState := Elab.Command.mkState headerEnv {} opts
-      let cmdState := { cmdState with infoState := {
-        enabled := true
-        trees := #[Elab.InfoTree.context ({
-          env     := headerEnv
-          fileMap := m.text
-          ngen    := { namePrefix := `_worker }
-        }) (Elab.InfoTree.node
-            (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
-            (headerStx[1].getArgs.toList.map (fun importStx =>
-              Elab.InfoTree.node (Elab.Info.ofCommandInfo {
-                elaborator := `import
-                stx := importStx
-              }) #[].toPArray'
-            )).toPArray'
-        )].toPArray'
-      }}
-      let headerSnap := {
-        beginPos := 0
-        stx := headerStx
-        mpState := {}
-        cmdState := cmdState
-        interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
-        tacticCache := (← IO.mkRef {})
-      }
-      publishDiagnostics m headerSnap.diagnostics.toArray hOut
-      return (headerSnap, srcSearchPath)
+  let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
 
-  def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-       (levelParams : Game.DidOpenLevelParams) : IO (WorkerContext × WorkerState) := do
-    let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
-    let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      levelParams initParams
-    let cancelTk ← CancelToken.new
-    let ctx :=
-      { hIn  := i
-        hOut := o
-        hLog := e
-        headerTask
-        initParams
-        clientHasWidgets
-      }
-    let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk levelParams ctx (startAfterMs := 0)
-      | Except.error e   => throw (e : ElabTaskError))
-    let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-    return (ctx,
-    { doc             := doc
-      initHeaderStx   := headerStx
-      pendingRequests := RBMap.empty
-      rpcSessions     := RBMap.empty
-    })
+  -- use empty header
+  let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
+    {m.mkInputContext with
+      input := ""
+      fileMap := FileMap.ofString ""}
+  (headerStx, ·) <$> EIO.asTask do
+    let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
+    let headerEnv := env
+    let mut headerEnv := headerEnv
+    try
+      if let some path := System.Uri.fileUriToPath? m.uri then
+        headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
+    catch _ => pure ()
+    let cmdState := Elab.Command.mkState headerEnv {} opts
+    let cmdState := { cmdState with infoState := {
+      enabled := true
+      trees := #[Elab.InfoTree.context (.commandCtx {
+        env     := headerEnv
+        fileMap := m.text
+        ngen    := { namePrefix := `_worker }
+      }) (Elab.InfoTree.node
+          (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
+          (headerStx[1].getArgs.toList.map (fun importStx =>
+            Elab.InfoTree.node (Elab.Info.ofCommandInfo {
+              elaborator := `import
+              stx := importStx
+            }) #[].toPArray'
+          )).toPArray'
+      )].toPArray'
+    }}
+    let headerSnap := {
+      beginPos := 0
+      stx := headerStx
+      mpState := {} -- was `headerParserState`
+      cmdState := cmdState
+      interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
+      tacticCache := (← IO.mkRef {})
+    }
+    publishDiagnostics m headerSnap.diagnostics.toArray hOut
+    return (headerSnap, srcSearchPath)
+
+/-- Copied from `Lean.Server.FileWorker.initializeWorker`. Added `gameDir` and
+`gameWorkerState` arguments and use custom `unfoldCmdSnaps`. -/
+-- @[inherit_doc Lean.Server.FileWorker.initializeWorker]
+def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
+    (gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
+  let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
+  let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
+    (gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
+  let cancelTk ← CancelToken.new
+  let ctx := {
+    hIn  := i
+    hOut := o
+    hLog := e
+    headerTask
+    initParams
+    clientHasWidgets
+  }
+  let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
+    | Except.ok (s, _) => unfoldCmdSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | Except.error e   => throw (e : ElabTaskError))
+  let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
+  return (ctx, {
+    doc                := doc
+    initHeaderStx      := headerStx
+    currHeaderStx      := headerStx
+    importCachingTask? := none
+    pendingRequests    := RBMap.empty
+    rpcSessions        := RBMap.empty
+  })
 
 end Initialization
 
 section NotificationHandling
 
-  def handleDidChange (p : DidChangeTextDocumentParams) : GameWorkerM Unit := do
-    let docId := p.textDocument
-    let changes := p.contentChanges
-    let oldDoc := (← StateT.lift get).doc
-    let some newVersion ← pure docId.version?
-      | throwServerError "Expected version number"
-    if newVersion ≤ oldDoc.meta.version then
-      -- TODO(WN): This happens on restart sometimes.
-      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, .always⟩
+/-- Copied from `Lean.Server.FileWorker.handleDidChange` but with our custom `WorkerM` and
+`updateDocument` -/
+-- @[inherit_doc Lean.Server.FileWorker.handleDidChange]
+def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
+  let docId := p.textDocument
+  let changes := p.contentChanges
+  let oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
+  let newVersion := docId.version?.getD 0
+  if ¬ changes.isEmpty then
+    let newDocText := foldDocumentChanges changes oldDoc.meta.text
+    -- modification: set the `DependencyBuildMode` from
+    -- `oldDoc.meta.dependencyBuildMode` to `.always`
+    updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
 
 section MessageHandling
 
-  def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do
-    let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) =>
-      (StateT.lift <| parseParams paramType params) >>= handler
-    match method with
-    | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
-    | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
-    | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
-    | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
-    | _                        => throwServerError s!"Got unsupported notification method: {method}"
+
+/--
+Modified notification handler.
+
+Compare to `Lean.Server.FileWorker.handleNotification`.
+We use the modified `WorkerM` and use our custom `handleDidChange`.
+
+-/
+def handleNotification (method : String) (params : Json) : WorkerM Unit := do
+  let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
+    (StateT.lift <| parseParams paramType params) >>= handler
+  match method with
+  -- Modified `textDocument/didChange`, using a custom `handleDidChange`
+  | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
+  -- unmodified
+  | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+  -- unmodified
+  | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
+  -- unmodified
+  | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
+  -- New. TODO: What is this for?
+  | "$/setTrace"        => pure ()
+  | _                        => throwServerError s!"Got unsupported notification method: {method}"
 
 end MessageHandling
 
 section MainLoop
-  partial def mainLoop : GameWorkerM Unit := do
-    let ctx ← read
-    let mut st ← StateT.lift get
-    let msg ← ctx.hIn.readLspMessage
-    let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
-        : IO PendingRequestMap := do
-      if (← hasFinished task) then
-        /- Handler tasks are constructed so that the only possible errors here
-        are failures of writing a response into the stream. -/
-        if let Except.error e := task.get then
-          throwServerError s!"Failed responding to request {id}: {e}"
-        pure <| acc.erase id
-      else pure acc
-    let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
-    st := { st with pendingRequests }
 
-    -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
-    for (id, seshRef) in st.rpcSessions do
-      let sesh ← seshRef.get
-      if (← sesh.hasExpired) then
-        st := { st with rpcSessions := st.rpcSessions.erase id }
+/--
+The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
+as custom `handleNotification`.
+-/
+--@[inherit_doc Lean.Server.FileWorker.mainLoop]
+partial def mainLoop : WorkerM Unit := do
+  let ctx ← read
+  let mut st ← StateT.lift get
+  let msg ← ctx.hIn.readLspMessage
+  -- Erase finished tasks if there are no errors.
+  let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
+      : IO PendingRequestMap := do
+    if (← hasFinished task) then
+      if let Except.error e := task.get then
+        throwServerError s!"Failed responding to request {id}: {e}"
+      pure <| acc.erase id
+    else pure acc
+  let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
+  st := { st with pendingRequests }
+  for (id, seshRef) in st.rpcSessions do
+    let sesh ← seshRef.get
+    if (← sesh.hasExpired) then
+      st := { st with rpcSessions := st.rpcSessions.erase id }
 
-    set st
-    match msg with
-    | Message.request id method (some params) =>
-      handleRequest id method (toJson params)
-      mainLoop
-    | Message.notification "exit" none =>
-      let doc := st.doc
-      doc.cancelTk.set
-      return ()
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams Game.SetInventoryParams (toJson params))
-      let s ← get
+  set st
+  -- Process the RPC-message and restart main-loop.
+  match msg with
+  | Message.request id "shutdown" none =>
+    --added. TODO: why do we need that? Or has it just removed in Lean since when we started?
+    ctx.hOut.writeLspResponse ⟨id, Json.null⟩
+    mainLoop
+  | Message.request id method (some params) =>
+    -- Requests are handled by the unmodified lean server.
+    handleRequest id method (toJson params)
+    mainLoop
+  | Message.notification "exit" none =>
+    let doc := st.doc
+    doc.cancelTk.set
+    doc.cmdSnaps.cancel
+    return ()
+  | Message.notification method (some params) =>
+    -- Custom notification handler
+    handleNotification method (toJson params)
+    mainLoop
+  | _ =>
+    throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
 
-      set {s with levelParams := {s.levelParams with
-        inventory := p.inventory,
-        difficulty := p.difficulty}}
-      mainLoop
-    | Message.notification method (some params) =>
-      handleNotification method (toJson params)
-      mainLoop
-    | _ => throwServerError "Got invalid JSON-RPC message"
 end MainLoop
 
-def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
+/-- Modified from `Lean.Server.FileWorker.initAndRunWorker`.
+Added `gameDir` argument, -/
+-- @[inherit_doc Lean.Server.FileWorker.initAndRunWorker]
+def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
-  let initParams ← i.readLspRequestAs "initialize" InitializeParams
+
+
+  -- BIG MODIFICATION
+  let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
+  o.writeLspResponse {
+    id     := initRequest.id
+    result := {
+      capabilities := Watchdog.mkLeanServerCapabilities
+      serverInfo?  := some {
+        name     := "Lean 4 Game Server"
+        version? := "0.1.1"
+      }
+      : InitializeResult
+    }
+  }
+  discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
-  let ⟨_, levelParams⟩ ← i.readLspNotificationAs "$/game/didOpenLevel" Game.DidOpenLevelParams
+
 
   let doc := param.textDocument
-  /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
-    "\n", which should be enough to handle both LF and CRLF correctly.
-    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. -/
+  -- modification: using `.always`
   let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
-    let (ctx, st) ← initializeWorker meta i o e initParams.param opts levelParams
+
+
+    -- BIG MODIFICATION
+    let game ← loadGameData gameDir
+    -- TODO: We misuse the `rootUri` field to the gameName
+    let rootUri? : Option String := some (toString game.name)
+    let initParams := {initRequest.param.toLeanInternal with rootUri?}
+    let some (levelId : LevelId) := GameServer.levelIdFromFileName?
+        initParams meta.mkInputContext.fileName
+      | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
+    let levelInfo ← loadLevelData gameDir levelId.world levelId.level
+    let some initializationOptions := initRequest.param.initializationOptions?
+      | throwServerError "no initialization options found"
+    let gameWorkerState : WorkerState := {
+      inventory := initializationOptions.inventory
+      difficulty := initializationOptions.difficulty
+      levelInfo
+    }
+    let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
+    -- Run the main loop
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
-      StateT.run (s := {levelParams := levelParams}) <| (mainLoop)
+      StateT.run (s := gameWorkerState) <| (mainLoop)
+
+
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -590,14 +762,22 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) : IO UInt32 := do
       message := e.toString }] o
     return (1 : UInt32)
 
-def workerMain (opts : Options) : IO UInt32 := do
+/--
+The main function. Simply wrapping `initAndRunWorker`.
+
+Copied from `Lean.Server.FileWorker.workerMain`. We add `args` as an argument to pass on
+the `gameDir`.
+
+TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
+-/
+-- @[inherit_doc Lean.Server.FileWorker.workerMain]
+def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
   let e ← IO.getStderr
   try
-    let exitCode ← initAndRunWorker i o e opts
-    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
-    -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
+    let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
+    let exitCode ← initAndRunWorker i o e opts gameDir
     o.flush
     e.flush
     IO.Process.exit exitCode.toUInt8
@@ -605,4 +785,4 @@ def workerMain (opts : Options) : IO UInt32 := do
     e.putStrLn s!"worker initialization error: {err}"
     return (1 : UInt32)
 
-end MyServer.FileWorker
+end GameServer.FileWorker

server/GameServer/Game.lean

@@ -25,75 +25,56 @@ open Lsp
 open JsonRpc
 open IO
 
-structure DidOpenLevelParams where
-  uri : String
-  gameDir : String
-  levelModule : Name
-  tactics : Array InventoryTile
-  lemmas : Array InventoryTile
-  definitions : Array InventoryTile
-  inventory : Array String
-  /--
-  Check for tactics/theorems that are not unlocked.
-  0: no check
-  1: give warnings
-  2: give errors
-  -/
+/- Game-specific version of `InitializeParams` that allows for extra options: -/
+
+structure InitializationOptions extends Lean.Lsp.InitializationOptions :=
   difficulty : Nat
-  /-- The name of the theorem to be proven in this level. -/
-  statementName : Name
+  inventory : Array String
   deriving ToJson, FromJson
 
-structure SetInventoryParams where
-  inventory : Array String
-  difficulty : Nat
-deriving ToJson, FromJson
+structure InitializeParams where
+  processId? : Option Int := none
+  clientInfo? : Option ClientInfo := none
+  /- We don't support the deprecated rootPath
+  (rootPath? : Option String) -/
+  rootUri? : Option String := none
+  initializationOptions? : Option InitializationOptions := none
+  capabilities : ClientCapabilities
+  /-- If omitted, we default to off. -/
+  trace : Trace := Trace.off
+  workspaceFolders? : Option (Array WorkspaceFolder) := none
+  deriving ToJson
 
-def handleDidOpenLevel (params : Json) : GameServerM Unit := do
-  let p ← parseParams _ params
-  let m := p.textDocument
-  -- Execute the regular handling of the `didOpen` event
-  handleDidOpen p
-  let fw ← findFileWorker! m.uri
-  -- let s ← get
-  let c ← read
-  let some lvl ← GameServer.getLevelByFileName? c.initParams ((System.Uri.fileUriToPath? m.uri).getD m.uri |>.toString)
-    | do
-      c.hLog.putStr s!"Level not found: {m.uri} {c.initParams.rootUri?}"
-      c.hLog.flush
-  -- Send an extra notification to the file worker to inform it about the level data
-  let s ← get
-  fw.stdin.writeLspNotification {
-    method := "$/game/didOpenLevel"
-    param  := {
-      uri := m.uri
-      gameDir := s.gameDir
-      levelModule := lvl.module
-      tactics := lvl.tactics.tiles
-      lemmas := lvl.lemmas.tiles
-      definitions := lvl.definitions.tiles
-      inventory := s.inventory
-      difficulty := s.difficulty
-      statementName := lvl.statementName
-      : DidOpenLevelParams
-    }
+instance : FromJson InitializeParams where
+  fromJson? j := do
+    let processId? := j.getObjValAs? Int "processId"
+    let clientInfo? := j.getObjValAs? ClientInfo "clientInfo"
+    let rootUri? := j.getObjValAs? String "rootUri"
+    let initializationOptions? := j.getObjValAs? InitializationOptions "initializationOptions"
+    let capabilities ← j.getObjValAs? ClientCapabilities "capabilities"
+    let trace := (j.getObjValAs? Trace "trace").toOption.getD Trace.off
+    let workspaceFolders? := j.getObjValAs? (Array WorkspaceFolder) "workspaceFolders"
+    return ⟨
+      processId?.toOption,
+      clientInfo?.toOption,
+      rootUri?.toOption,
+      initializationOptions?.toOption,
+      capabilities,
+      trace,
+      workspaceFolders?.toOption⟩
+
+def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.InitializeParams :=
+{
+  processId? := p.processId?
+  clientInfo? := p.clientInfo?
+  rootUri? := p.rootUri?
+  initializationOptions? := p.initializationOptions?.map fun o => {
+    editDelay? := o.editDelay?
+    hasWidgets? := o.hasWidgets?
   }
-
-partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do
-  match ev with
-  | ServerEvent.clientMsg msg =>
-    match msg with
-    | Message.notification "$/game/setInventory" params =>
-      let p := (← parseParams SetInventoryParams (toJson params))
-      let s ← get
-      set {s with inventory := p.inventory, difficulty := p.difficulty}
-      let st ← read
-      let workers ← st.fileWorkersRef.get
-      for (_, fw) in workers do
-        fw.stdin.writeLspMessage msg
-
-      return true
-    | _ => return false
-  | _ => return false
+  capabilities := p.capabilities
+  trace := p.trace
+  workspaceFolders? := p.workspaceFolders?
+}
 
 end Game

server/GameServer/Graph.lean

@@ -18,6 +18,14 @@ instance [ToJson β] : ToJson (Graph Name β) := {
   ]
 }
 
+-- Just a dummy implementation for now:
+instance : FromJson (Graph Name β) := {
+  fromJson? := fun _ => .ok {
+    nodes := {}
+    edges := {}
+  }
+}
+
 instance  : EmptyCollection (Graph α β) := ⟨default⟩
 
 def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=

server/GameServer/InteractiveGoal.lean

@@ -1,74 +1,19 @@
-/- This file is mostly copied from `Lean/Widget/InteractiveGoal.lean`. -/
+import GameServer.Structures
 
-import Lean.Widget.InteractiveGoal
+/-!
+This file is a modified copy of `Lean.Widget.InteractiveGoal`.
 
-/-! Functionality related to tactic-mode and term-mode goals with embedded `CodeWithInfos`. -/
+Note that the structures have been moved to `Structures.lean`, but most of the
+functions here must be duplicated from `Lean.Widget.InteractiveGoal` in order
+to use the duplicated structures.
+-/
 
 namespace GameServer
+
 open Lean Lean.Widget Lean.Server
 
-structure GameHint where
-  text : String
-  hidden : Bool
-deriving FromJson, ToJson
-
-/-- In the infoview, if multiple hypotheses `h₁`, `h₂` have the same type `α`, they are rendered
-as `h₁ h₂ : α`. We call this a 'hypothesis bundle'. We use `none` instead of `some false` for
-booleans to save space in the json encoding. -/
-structure InteractiveHypothesisBundle where
-  /-- The user-friendly name for each hypothesis. -/
-  names : Array Name
-  /-- The ids for each variable. Should have the same length as `names`. -/
-  fvarIds : Array FVarId
-  type : CodeWithInfos
-  /-- The value, in the case the hypothesis is a `let`-binder. -/
-  val? : Option CodeWithInfos := none
-  /-- The hypothesis is a typeclass instance. -/
-  isInstance? : Option Bool := none
-  /-- The hypothesis is a type. -/
-  isType? : Option Bool := none
-  /-- The hypothesis's type is of type `Prop` -/
-  isAssumption? : Option Bool := none
-  /-- If true, the hypothesis was not present on the previous tactic state.
-  Only present in tactic-mode goals. -/
-  isInserted? : Option Bool := none
-  /-- If true, the hypothesis will be removed in the next tactic state.
-  Only present in tactic-mode goals. -/
-  isRemoved? : Option Bool := none
-  deriving Inhabited, RpcEncodable
-
-/-- The shared parts of interactive term-mode and tactic-mode goals. -/
-structure InteractiveGoalCore where
-  hyps : Array InteractiveHypothesisBundle
-  /-- The target type. -/
-  type : CodeWithInfos
-  /-- Metavariable context that the goal is well-typed in. -/
-  ctx : WithRpcRef Elab.ContextInfo
-
-/-- An interactive tactic-mode goal. -/
-structure InteractiveGoal extends InteractiveGoalCore where
-  /-- The name `foo` in `case foo`, if any. -/
-  userName? : Option String
-  /-- The symbol to display before the target type. Usually `⊢ ` but `conv` goals use `∣ `
-  and it could be extended. -/
-  goalPrefix : String
-  /-- Identifies the goal (ie with the unique name of the MVar that it is a goal for.) -/
-  mvarId : MVarId
-  /-- If true, the goal was not present on the previous tactic state. -/
-  isInserted? : Option Bool := none
-  /-- If true, the goal will be removed on the next tactic state. -/
-  isRemoved? : Option Bool := none
-  hints : Array GameHint := #[]
-  deriving RpcEncodable
-
-/-- An interactive term-mode goal. -/
-structure InteractiveTermGoal extends InteractiveGoalCore where
-  /-- Syntactic range of the term. -/
-  range : Lsp.Range
-  /-- Information about the term whose type is the term-mode goal. -/
-  term : WithRpcRef Elab.TermInfo
-  deriving RpcEncodable
-
+-- duplicated with custom `InteractiveGoalCore`
+-- @[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
 def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option String)
     (goalPrefix : String) : Format := Id.run do
   let indent := 2 -- Use option
@@ -79,8 +24,7 @@ def InteractiveGoalCore.pretty (g : InteractiveGoalCore) (userName? : Option Str
     ret := addLine ret
     let names := hyp.names
         |>.toList
-        |>.filter (not ∘ Name.isAnonymous)
-        |>.map toString
+        |>.filter (· != toString Name.anonymous)
         |> " ".intercalate
     match names with
     | "" =>
@@ -97,16 +41,24 @@ where
   addLine (fmt : Format) : Format :=
     if fmt.isNil then fmt else fmt ++ Format.line
 
+-- duplicated with custom `InteractiveGoal`
+-- @[inherit_doc Lean.Widget.InteractiveGoal.pretty]
 def InteractiveGoal.pretty (g : InteractiveGoal) : Format :=
   g.toInteractiveGoalCore.pretty g.userName? g.goalPrefix
 
+-- duplicated with custom `InteractiveTermGoal`
+-- @[inherit_doc Lean.Widget.InteractiveTermGoal.pretty]
 def InteractiveTermGoal.pretty (g : InteractiveTermGoal) : Format :=
   g.toInteractiveGoalCore.pretty none "⊢ "
 
+-- duplicated with custom `InteractiveGoal`
+-- @[inherit_doc Lean.Widget.InteractiveGoals]
 structure InteractiveGoals where
   goals : Array InteractiveGoal
   deriving RpcEncodable
 
+-- duplicated with custom `InteractiveGoals`
+-- @[inherit_doc Lean.Widget.InteractiveGoals.append]
 def InteractiveGoals.append (l r : InteractiveGoals) : InteractiveGoals where
   goals := l.goals ++ r.goals
 
@@ -114,9 +66,10 @@ instance : Append InteractiveGoals := ⟨InteractiveGoals.append⟩
 instance : EmptyCollection InteractiveGoals := ⟨{goals := #[]}⟩
 
 open Meta in
-/-- Extend an array of hypothesis bundles with another bundle. -/
+-- duplicated with custom `InteractiveHypothesisBundle` and therefore added `isAssumption?`
+@[inherit_doc Lean.Widget.addInteractiveHypothesisBundle]
 def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
-    (ids : Array (Name × FVarId)) (type : Expr) (value? : Option Expr := none) :
+    (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) :
     MetaM (Array InteractiveHypothesisBundle) := do
   if ids.size == 0 then
     throwError "Can only add a nonzero number of ids as an InteractiveHypothesisBundle."
@@ -125,11 +78,12 @@ def addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle)
   return hyps.push {
     names
     fvarIds
-    type           := (← ppExprTagged type)
-    val?           := (← value?.mapM ppExprTagged)
-    isInstance?    := if (← isClass? type).isSome then true else none
-    isType?        := if (← instantiateMVars type).isSort then true else none
-    isAssumption?  := if (← inferType type).isProp then true else none
+    type        := (← ppExprTagged type)
+    val?        := (← value?.mapM ppExprTagged)
+    isInstance? := if (← isClass? type).isSome then true else none
+    isType?     := if (← instantiateMVars type).isSort then true else none
+    -- Added:
+    isAssumption? := if (← inferType type).isProp then true else none
   }
 
 open Meta in
@@ -142,13 +96,15 @@ def withGoalCtx (goal : MVarId) (action : LocalContext → MetavarDecl → n α)
   withLCtx lctx mvarDecl.localInstances (action lctx mvarDecl)
 
 open Meta in
-/-- A variant of `Meta.ppGoal` which preserves subexpression information for interactivity. -/
-def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM InteractiveGoal := do
+
+-- Duplicated from `Lean.Widget.goalToInteractive` with custom structures
+@[inherit_doc Lean.Widget.goalToInteractive]
+def goalToInteractive (mvarId : MVarId) : MetaM InteractiveGoal := do
   let ppAuxDecls := pp.auxDecls.get (← getOptions)
   let ppImplDetailHyps := pp.implementationDetailHyps.get (← getOptions)
   let showLetValues := pp.showLetValues.get (← getOptions)
   withGoalCtx mvarId fun lctx mvarDecl => do
-    let pushPending (ids : Array (Name × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
+    let pushPending (ids : Array (String × FVarId)) (type? : Option Expr) (hyps : Array InteractiveHypothesisBundle)
         : MetaM (Array InteractiveHypothesisBundle) :=
       if ids.isEmpty then
         pure hyps
@@ -156,7 +112,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
         match type? with
         | none      => pure hyps
         | some type => addInteractiveHypothesisBundle hyps ids type
-    let mut varNames : Array (Name × FVarId) := #[]
+    let mut varNames : Array (String × FVarId) := #[]
     let mut prevType? : Option Expr := none
     let mut hyps : Array InteractiveHypothesisBundle := #[]
     for localDecl in lctx do
@@ -165,7 +121,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
       else
         match localDecl with
         | LocalDecl.cdecl _index fvarId varName type _ _ =>
-          let varName := varName.simpMacroScopes
+          let varName := toString varName
           let type ← instantiateMVars type
           if prevType? == none || prevType? == some type then
             varNames := varNames.push (varName, fvarId)
@@ -174,7 +130,7 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
             varNames := #[(varName, fvarId)]
           prevType? := some type
         | LocalDecl.ldecl _index fvarId varName type val _ _ => do
-          let varName := varName.simpMacroScopes
+          let varName := toString varName
           hyps ← pushPending varNames prevType? hyps
           let type ← instantiateMVars type
           let val? ← if showLetValues then pure (some (← instantiateMVars val)) else pure none
@@ -190,11 +146,10 @@ def goalToInteractive (mvarId : MVarId) (hints : Array GameHint): MetaM Interact
     return {
       hyps
       type := goalFmt
-      ctx := ⟨← Elab.ContextInfo.save⟩
+      ctx := ⟨{← Elab.CommandContextInfo.save with }⟩
       userName?
       goalPrefix := getGoalPrefix mvarDecl
       mvarId
-      hints
     }
 
 end GameServer

server/GameServer/RpcHandlers.lean

@@ -1,5 +1,6 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
+import Std.Data.Array.Init.Basic
 
 open Lean
 open Server
@@ -7,7 +8,6 @@ open Widget
 open RequestM
 open Meta
 
-
 /-! ## GameGoal -/
 
 namespace GameServer
@@ -113,10 +113,10 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu
 
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
-def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
+def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
   goal.withContext do
-    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
-      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
+    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
+      | throwError "Level not found: {m.mkInputContext.fileName}"
     let hints ← level.hints.filterMapM fun hint => do
       openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
         if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
@@ -134,18 +134,183 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams :
           return none
     return hints
 
-open RequestM in
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
+-- TODO: no need to have `RequestM`, just anything where `mut` works
+/-- Add custom diagnostics about whether the level is completed. -/
+def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : Bool)
+    (completedWithWarnings : Bool) (pos : Lsp.Position)
+    (startDiags : Array InteractiveDiagnostic := #[]) :
+    RequestM <| Array InteractiveDiagnostic := do
+  let mut out : Array InteractiveDiagnostic := startDiags
+  if goalCount == 0 then
+    if completed then
+      out := out.push {
+        message := .text "level completed! 🎉"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+    else if completedWithWarnings then
+      out := out.push {
+        message := .text "level completed with warnings… 🎭"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information }
+    else
+      pure ()
+  else if goalCount < prevGoalCount then
+    out := out.push {
+      message := .text "intermediate goal solved! 🎉"
+      range := {
+        start := pos
+        «end» := pos
+        }
+      severity? := Lsp.DiagnosticSeverity.information
+    }
+  return out
+
+def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
+    Array InteractiveDiagnostic :=
+  a.filter (fun d => match d.message with
+  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
+  | _ => true)
+
+/-- Request that returns the goals at the end of each line of the tactic proof
+plus the diagnostics (i.e. warnings/errors) for the proof.
+ -/
+def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option ProofState)) := do
   let doc ← readDoc
   let rc ← readThe RequestContext
   let text := doc.meta.text
+
+  -- BUG: trimming here is a problem, since the snap might already be evaluated before
+  -- the trimming and then the positions don't match anymore :((
+
+  withWaitFindSnap
+    doc
+    -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking
+    -- for the first snap with goals here.
+    -- NOTE (Jon): The entire proof is in one snap, so hoped that Position `0` is good enough.
+    (fun snap => ¬ (snap.infoTree.goalsAt? doc.meta.text 0).isEmpty)
+    (notFoundX := return none)
+    fun snap => do
+      -- `snap` is the one snapshot containing the entire proof.
+      let mut steps : Array <| InteractiveGoalsWithHints := #[]
+
+      -- Question: Is there a difference between the diags of this snap and the last snap?
+      -- Should we get the diags from there?
+      -- Answer: The last snap only copied the diags from the end of this snap
+      let mut diag : Array InteractiveDiagnostic := snap.interactiveDiags.toArray
+
+      -- Level is completed if there are no errrors or warnings
+      let completedWithWarnings : Bool := ¬ diag.any (·.severity? == some .error)
+      let completed : Bool := completedWithWarnings ∧ ¬ diag.any (·.severity? == some .warning)
+
+      let mut intermediateGoalCount := 0
+
+      -- only the positions that have non-whitespace characters since the last position
+      -- should add a new proof step.
+      let positionsWithSource : Array (String.Pos × String) :=
+        text.positions.zipWithIndex.filterMap (
+          fun (pos, i) => match i with
+          | 0 => some (pos, "")
+          | i' + 1 =>
+            let source : String := Substring.toString ⟨text.source, text.positions.get! i', pos⟩
+            if source.trim.length == 0 then
+              none
+            else
+              some (pos, source))
+
+      -- Drop the last position as we ensured that there is always a newline at the end
+      for ((pos, source), i) in positionsWithSource.zipWithIndex do
+        -- iterate over all steps in the proof and get the goals and hints at each position
+
+        -- diags are labeled in Lsp-positions, which differ from the lean-internal
+        -- positions by `1`.
+        let lspPosAt := text.utf8PosToLspPos pos
+
+        let mut diagsAtPos : Array InteractiveDiagnostic := filterUnsolvedGoal <|
+          -- `+1` for getting the errors after the line.
+          match i with
+          | 0 =>
+            -- `lspPosAt` is `(0, 0)`
+            diag.filter (fun d => d.range.start == lspPosAt )
+          | i' + 1 =>
+            diag.filter (fun d =>
+              ((text.utf8PosToLspPos <| (positionsWithSource.get! i').1) ≤ d.range.start) ∧
+              d.range.start < lspPosAt )
+
+        if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text pos then
+          let goalsAtPos' : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
+            fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
+              -- TODO: What does this function body do?
+              -- let ciAfter := { ci with mctx := ti.mctxAfter }
+              let ci := if useAfter then
+                  { ci with mctx := tacticInfo.mctxAfter }
+                else
+                  { ci with mctx := tacticInfo.mctxBefore }
+              -- compute the interactive goals
+              let goalMvars : List MVarId ← ci.runMetaM {} do
+                return if useAfter then tacticInfo.goalsAfter else tacticInfo.goalsBefore
+
+              let interactiveGoals : List InteractiveGoalWithHints ← ci.runMetaM {} do
+                goalMvars.mapM fun goal => do
+                  let hints ← findHints goal doc.meta rc.initParams
+                  let interactiveGoal ← goalToInteractive goal
+                  return ⟨interactiveGoal, hints⟩
+              -- TODO: This code is way old, can it be deleted?
+              -- compute the goal diff
+              -- let goals ← ciAfter.runMetaM {} (do
+              --     try
+              --       Widget.diffInteractiveGoals useAfter ti goals
+              --     catch _ =>
+              --       -- fail silently, since this is just a bonus feature
+              --       return goals
+              -- )
+              return interactiveGoals
+          let goalsAtPos : Array InteractiveGoalWithHints := ⟨goalsAtPos'.foldl (· ++ ·) []⟩
+
+          diagsAtPos ← completionDiagnostics goalsAtPos.size intermediateGoalCount
+            completed completedWithWarnings lspPosAt diagsAtPos
+
+          intermediateGoalCount := goalsAtPos.size
+
+          steps := steps.push ⟨goalsAtPos, source, diagsAtPos, lspPosAt.line, lspPosAt.character⟩
+        else
+          -- No goals present
+          steps := steps.push ⟨#[], source, diagsAtPos, lspPosAt.line, none⟩
+
+      -- Filter out the "unsolved goals" message
+      diag := filterUnsolvedGoal diag
+
+      let lastPos := text.utf8PosToLspPos positionsWithSource.back.1
+      let remainingDiags : Array InteractiveDiagnostic :=
+        diag.filter (fun d => lastPos ≤ d.range.start)
+
+      return some {
+        steps := steps,
+        diagnostics := remainingDiags,
+        completed := completed,
+        completedWithWarnings := completedWithWarnings,
+        lastPos := lastPos.line
+        }
+
+open RequestM in
+
+-- The editor apparently uses this
+def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option <| InteractiveGoals)) := do
+  let doc ← readDoc
+  -- let rc ← readThe RequestContext
+  let text := doc.meta.text
   let hoverPos := text.lspPosToUtf8Pos p.position
   -- TODO: I couldn't find a good condition to find the correct snap. So we are looking
   -- for the first snap with goals here:
   withWaitFindSnap doc (fun s => ¬ (s.infoTree.goalsAt? doc.meta.text hoverPos).isEmpty)
     (notFoundX := return none) fun snap => do
       if let rs@(_ :: _) := snap.infoTree.goalsAt? doc.meta.text hoverPos then
-        let goals : List InteractiveGoals ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
+        let goals : List <| Array InteractiveGoal ← rs.mapM fun { ctxInfo := ci, tacticInfo := ti, useAfter := useAfter, .. } => do
           let ciAfter := { ci with mctx := ti.mctxAfter }
           let ci := if useAfter then ciAfter else { ci with mctx := ti.mctxBefore }
           -- compute the interactive goals
@@ -153,8 +318,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
             return List.toArray <| if useAfter then ti.goalsAfter else ti.goalsBefore
           let goals ← ci.runMetaM {} do
              goals.mapM fun goal => do
-              let hints ← findHints goal doc rc.initParams
-              return ← goalToInteractive goal hints
+              -- let hints ← findHints goal doc.meta rc.initParams
+              return ← goalToInteractive goal
           -- compute the goal diff
           -- let goals ← ciAfter.runMetaM {} (do
           --     try
@@ -163,8 +328,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           --       -- fail silently, since this is just a bonus feature
           --       return goals
           -- )
-          return {goals}
-        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
+          return goals
+        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
       else
         return none
 
@@ -172,7 +337,16 @@ builtin_initialize
   registerBuiltinRpcProcedure
     `Game.getInteractiveGoals
     Lsp.PlainGoalParams
-    (Option InteractiveGoals)
+    (Option <| InteractiveGoals
+    )
     getInteractiveGoals
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Game.getProofState
+    Lsp.PlainGoalParams
+    (Option ProofState)
+    getProofState
+
+
 end GameServer

server/GameServer/SaveData.lean

@@ -22,16 +22,21 @@ def copyImages : IO Unit := do
         let content ← readBinFile file
         writeBinFile outFile content
 
+namespace GameData
+  def gameDataPath : System.FilePath := ".lake" / "gamedata"
+  def gameFileName := s!"game.json"
+  def docFileName := fun (inventoryType : InventoryType) (name : Name) => s!"doc__{inventoryType}__{name}.json"
+  def levelFileName := fun (worldId : Name) (levelId : Nat) => s!"level__{worldId}__{levelId}.json"
+  def inventoryFileName := s!"inventory.json"
+end GameData
 
--- TODO: I'm not sure this should be happening here...
-#eval IO.FS.createDirAll ".lake/gamedata/"
-
+open GameData in
 -- TODO: register all of this as ToJson instance?
 def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
     (inventory : InventoryOverview): CommandElabM Unit := do
   let game ← getCurGame
   let env ← getEnv
-  let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata"
+  let path := (← IO.currentDir) / gameDataPath
 
   if ← path.isDir then
     IO.FS.removeDirAll path
@@ -42,14 +47,32 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   for (worldId, world) in game.worlds.nodes.toArray do
     for (levelId, level) in world.levels.toArray do
-      IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env)))
+      IO.FS.writeFile (path / levelFileName worldId levelId) (toString (toJson (level.toInfo env)))
 
-  IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game))
+  IO.FS.writeFile (path / gameFileName) (toString (getGameJson game))
 
   for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do
     for name in allItemsByType.findD inventoryType {} do
       let some item ← getInventoryItem? name inventoryType
         | throwError "Expected item to exist: {name}"
-      IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item))
+      IO.FS.writeFile (path / docFileName inventoryType name) (toString (toJson item))
 
-  IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory))
+  IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
+
+open GameData
+
+def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do
+  let str ← IO.FS.readFile f
+  let json ← match Json.parse str with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  let data ← match fromJson? json with
+  | .ok v => pure v
+  | .error e => throw (IO.userError e)
+  return data
+
+def loadGameData (gameDir : System.FilePath) : IO Game :=
+  loadData (gameDir / gameDataPath / gameFileName) Game
+
+def loadLevelData (gameDir : System.FilePath) (worldId : Name) (levelId : Nat) : IO LevelInfo :=
+  loadData (gameDir / gameDataPath / levelFileName worldId levelId) LevelInfo

server/GameServer/Structures.lean

@@ -0,0 +1,93 @@
+import Lean.Widget.InteractiveGoal
+import Lean.Widget.InteractiveDiagnostic
+import Lean.Data.Lsp.Diagnostics
+
+/-!
+This file contains the custom data structures use by the server.
+
+Some of them overwrite built-in structures from Lean.
+
+In particular, the structures from `Lean.Widget.InteractiveGoal` are duplicated with
+the following extension:
+
+* `isAssumption?` in `InteractiveHypothesisBundle`: stores if a hypothesis is of type `Prop`.
+
+NOTE: Changes here need to be reflected in  the corresponding `interface` in `rcp_api.ts`
+on the client-side.
+-/
+
+open Lean Server Widget
+
+namespace GameServer
+
+/-- Extend the interactive hypothesis bundle with an option to distinguish
+"assumptions" from "objects". "Assumptions" are hypotheses of type `Prop`. -/
+-- @[inherit_doc Lean.Widget.InteractiveHypothesisBundle]
+structure InteractiveHypothesisBundle extends Lean.Widget.InteractiveHypothesisBundle where
+  /-- The hypothesis's type is of type `Prop` -/
+  isAssumption? : Option Bool := none
+deriving RpcEncodable
+
+-- duplicated but with custom `InteractiveHypothesisBundle`
+@[inherit_doc Lean.Widget.InteractiveGoalCore]
+structure InteractiveGoalCore where
+  hyps : Array InteractiveHypothesisBundle
+  type : CodeWithInfos
+  ctx : WithRpcRef Elab.ContextInfo
+
+-- duplicated but with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveGoal]
+structure InteractiveGoal extends InteractiveGoalCore where
+  userName? : Option String
+  goalPrefix : String
+  mvarId : MVarId
+  isInserted? : Option Bool := none
+  isRemoved? : Option Bool := none
+deriving RpcEncodable
+
+-- duplicated with custom `InteractiveGoalCore`
+@[inherit_doc Lean.Widget.InteractiveTermGoal]
+structure InteractiveTermGoal extends InteractiveGoalCore where
+  range : Lsp.Range
+  term : WithRpcRef Elab.TermInfo
+deriving RpcEncodable
+
+/-- A hint in the game at the corresponding goal. -/
+structure GameHint where
+  text : String
+  hidden : Bool
+deriving FromJson, ToJson
+
+/-- Bundled `InteractiveGoal` together with an array of hints that apply at this stage. -/
+structure InteractiveGoalWithHints where
+  goal : InteractiveGoal
+  /-- Extended the `InteractiveGoal` by an array of hints at that goal. -/
+  hints : Array GameHint
+deriving RpcEncodable
+
+structure InteractiveGoalsWithHints where
+  goals : Array InteractiveGoalWithHints
+  /-- The content of the line evaluated. -/
+  command : String
+  diags : Array InteractiveDiagnostic := default
+  line : Option Nat -- only for debugging
+  column : Option Nat -- only for debugging
+
+deriving RpcEncodable
+
+instance : Inhabited InteractiveGoalsWithHints := ⟨default, default, default, none, none⟩
+
+/-- Collected goals throughout the proof. Used for communication with the game client. -/
+structure ProofState where
+  /-- goals after each line. includes the hints. -/
+  steps : Array <| InteractiveGoalsWithHints
+  /-- diagnostics contains all errors and warnings.
+
+  TODO: I think they contain information about which line they belong to. Verify this.
+  -/
+  diagnostics : Array InteractiveDiagnostic := default
+  /-- Whether the level is considered solved. -/
+  completed : Bool
+  completedWithWarnings : Bool
+  lastPos : Nat -- only for debugging
+deriving RpcEncodable

server/GameServer/Watchdog.lean

@@ -1,158 +0,0 @@
-/- This file is mostly copied from `Lean/Server/Watchdog.lean`. -/
-import Lean.Server.Watchdog
-import GameServer.Game
-
-namespace MyServer.Watchdog
-open Lean
-open Server
-open Watchdog
-open IO
-open Lsp
-open JsonRpc
-open System.Uri
-
-  partial def mainLoop (clientTask : Task ServerEvent) : GameServerM Unit := do
-    let st ← read
-    let workers ← st.fileWorkersRef.get
-    let mut workerTasks := #[]
-    for (_, fw) in workers do
-      if let WorkerState.running := fw.state then
-        workerTasks := workerTasks.push <| fw.commTask.map (ServerEvent.workerEvent fw)
-
-    let ev ← IO.waitAny (clientTask :: workerTasks.toList)
-
-    if ← Game.handleServerEvent ev then -- handle Game requests
-      mainLoop (←runClientTask)
-    else
-      match ev with
-      | ServerEvent.clientMsg msg =>
-        match msg with
-        | Message.request id "shutdown" _ =>
-          shutdown
-          st.hOut.writeLspResponse ⟨id, Json.null⟩
-        | Message.request id method (some params) =>
-          handleRequest id method (toJson params)
-          mainLoop (←runClientTask)
-        | Message.response .. =>
-          -- TODO: handle client responses
-          mainLoop (←runClientTask)
-        | Message.responseError _ _ e .. =>
-          throwServerError s!"Unhandled response error: {e}"
-        | Message.notification method (some params) =>
-          if method == "textDocument/didOpen" then
-            -- for lean4game, we need to pass in extra information when a level is opened:
-            Game.handleDidOpenLevel (← parseParams _ (toJson params))
-          else
-            handleNotification method (toJson params)
-          mainLoop (←runClientTask)
-        | _ => throwServerError "Got invalid JSON-RPC message"
-      | ServerEvent.clientError e => throw e
-      | ServerEvent.workerEvent fw ev =>
-        match ev with
-        | WorkerEvent.ioError e =>
-          throwServerError s!"IO error while processing events for {fw.doc.uri}: {e}"
-        | WorkerEvent.crashed _ =>
-          handleCrash fw.doc.uri #[]
-          mainLoop clientTask
-        | WorkerEvent.terminated =>
-          throwServerError "Internal server error: got termination event for worker that should have been removed"
-        | .importsChanged =>
-          startFileWorker fw.doc
-          mainLoop clientTask
-
-def initAndRunWatchdogAux : GameServerM Unit := do
-  let st ← read
-  try
-    discard $ st.hIn.readLspNotificationAs "initialized" InitializedParams
-    let clientTask ← runClientTask
-    mainLoop clientTask
-  catch err =>
-    shutdown
-    throw err
-  /- NOTE(WN): It looks like instead of sending the `exit` notification,
-  VSCode just closes the stream. In that case, pretend we got an `exit`. -/
-  let Message.notification "exit" none ←
-    try st.hIn.readLspMessage
-    catch _ => pure (Message.notification "exit" none)
-    | throwServerError "Got `shutdown` request, expected an `exit` notification"
-
-def createEnv (gameDir : String) (module : String) : IO Environment := do
-  -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-  let out ← IO.Process.output
-    { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-  if out.exitCode != 0 then
-    throwServerError s!"Error while running Lake: {out.stderr}"
-
-  -- Make the paths relative to the current directory
-  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-  let currentDir ← IO.currentDir
-  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
-
-  -- Set the search path
-  Lean.searchPathRef.set paths
-
-  let env ← importModules #[{ module := `Init : Import }, { module := module : Import }] {} 0
-  return env
-
-def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do
-  if args.length < 2 then
-    throwServerError s!"Expected 1-3 command line arguments in addition to `--server`:
-      game directory, the name of the main module (optional), and the name of the game (optional)."
-  let gameDir := args[1]!
-  let module := if args.length < 3 then defaultGameModule else args[2]!
-  let gameName := if args.length < 4 then defaultGameName else args[3]!
-  let workerPath := "./gameserver"
-  -- TODO: Do the following commands slow us down?
-  let srcSearchPath ← initSrcSearchPath (← getBuildDir)
-  let references ← IO.mkRef (← loadReferences)
-  let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap)
-  let i ← maybeTee "wdIn.txt" false i
-  let o ← maybeTee "wdOut.txt" true o
-  let e ← maybeTee "wdErr.txt" true e
-  let state := {
-    env := ← createEnv gameDir module,
-    game := gameName,
-    gameDir := gameDir,
-    inventory := #[]
-    difficulty := 0
-    }
-  let initRequest ← i.readLspRequestAs "initialize" InitializeParams
-  -- We misuse the `rootUri` field to the gameName
-  let rootUri? := gameName
-  let initRequest := {initRequest with param := {initRequest.param with rootUri?}}
-  o.writeLspResponse {
-    id     := initRequest.id
-    result := {
-      capabilities := mkLeanServerCapabilities
-      serverInfo?  := some {
-        name     := "Lean 4 Game Server"
-        version? := "0.1.1"
-      }
-      : InitializeResult
-    }
-  }
-  let context : ServerContext := {
-    hIn            := i
-    hOut           := o
-    hLog           := e
-    args           := args
-    fileWorkersRef := fileWorkersRef
-    initParams     := initRequest.param
-    workerPath
-    srcSearchPath
-    references
-  }
-  discard $ ReaderT.run (StateT.run initAndRunWatchdogAux state) context
-
-def watchdogMain (args : List String) : IO UInt32 := do
-  let i ← IO.getStdin
-  let o ← IO.getStdout
-  let e ← IO.getStderr
-  try
-    initAndRunWatchdog args i o e
-    return 0
-  catch err =>
-    e.putStrLn s!"Watchdog error: {err}"
-    return 1
-
-end MyServer.Watchdog

server/lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.3.0",
+   "inputRev": "v4.6.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lakefile.lean

@@ -8,6 +8,8 @@ def leanVersion : String := s!"v{Lean.versionString}"
 
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
 
+-- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion
+
 lean_lib GameServer
 
 @[default_target]

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.6.0-rc1