bump to v4.6.1

This reverts commit 381930e547.

.github/workflows/build.yml

@@ -1,6 +1,8 @@
 name: Build
 run-name: Build the project
-on: [push]
+on:
+  workflow_dispatch:
+  push:
 jobs:
   build:
     runs-on: ubuntu-latest

client/src/components/hints.tsx

@@ -1,22 +1,42 @@
-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";
+
+/** Plug-in the variable names in a hint. We do this client-side to prepare
+ * for i18n in the future. i.e. one should be able translate the `rawText`
+ * and have the variables substituted just before displaying.
+ */
+function getHintText(hint: GameHint): string {
+  if (hint.rawText) {
+    // Replace the variable names used in the hint with the ones used by the player
+    // variable names are marked like `«{g}»` inside the text.
+    return hint.rawText.replaceAll(/«\{(.*?)\}»/g, ((_, v) =>
+      // `hint.varNames` contains tuples `[oldName, newName]`
+      (hint.varNames.find(x => x[0] == v))[1]))
+  } else {
+    // hints created in the frontend do not have a `rawText`
+    // TODO: `hint.text` could be removed in theory.
+    return hint.text
+  }
+}
 
 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}>
-    <Markdown>{hint.text}</Markdown>
+    <Markdown>{getHintText(hint)}</Markdown>
   </div>
 }
 
 export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
   return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
-    <Markdown>{hint.text}</Markdown>
+    <Markdown>{getHintText(hint)}</Markdown>
   </div>
 }
 
 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)
 
@@ -29,7 +49,7 @@ export function Hints({hints, showHidden, step, selected, toggleSelection, lastL
 
 export function DeletedHint({hint} : {hint: GameHint}) {
   return <div className="message information deleted-hint">
-    <Markdown>{hint.text}</Markdown>
+    <Markdown>{getHintText(hint)}</Markdown>
   </div>
 }
 
@@ -46,22 +66,54 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
 }
 
 /** Filter hints to not show consequtive identical hints twice.
- *
+ * Hidden hints are not filtered.
- * 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.
  */
-export function filterHints(proof: ProofStep[]): GameHint[][] {
+export function filterHints(hints: GameHint[], prevHints: GameHint[]): GameHint[] {
-  return proof.map((step, i) => {
+  if (!hints) {
-    if (i == 0){
+    return []}
-      return step.hints
+  else if (!prevHints) {
-    } else {
+    return hints }
-      // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
+  else {
-      // good way to shallow-compare objects?
+    return hints.filter((hint) => hint.hidden ||
-      return step.hints.filter((hint) => hint.hidden ||
+    (prevHints.find(x => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)
-        (proof[i-1].hints.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 = proof?.steps.length ?
+    ((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
+    : 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?.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,8 +3,9 @@
  */
 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 { InteractiveDiagnostic } from '@leanprover/infoview-api';
-import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { Diagnostic } from 'vscode-languageserver-types'
+import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
@@ -12,37 +13,49 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
 
 export type InfoStatus = 'updating' | 'error' | 'ready';
 
-/** One step of the proof */
+// /** One step of the proof */
-export type ProofStep = {
+// export type ProofStep = {
-  /** The command in this step */
+//   /** The command in this step */
-  command : string
+//   command : string
-  /** List of goals *after* this command */
+//   /** List of goals *after* this command */
-  goals: InteractiveGoal[]     // TODO: Add correct type
+//   goals: InteractiveGoal[]     // TODO: Add correct type
-  /** Story relevant messages */
+//   /** Story relevant messages */
-  hints: GameHint[]        // TODO: Add correct type
+//   hints: GameHint[]        // TODO: Add correct type
-  /** Errors and warnings */
+//   /** Errors and warnings */
-  errors: InteractiveDiagnostic[]       // TODO: Add correct type
+//   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[],
+  proof: ProofState,
-  setProof: React.Dispatch<React.SetStateAction<Array<ProofStep>>>
+  setProof: React.Dispatch<React.SetStateAction<ProofState>>
+  /** TODO: Workaround to capture a crash of the gameserver. */
+  interimDiags: Diagnostic[],
+  setInterimDiags: React.Dispatch<React.SetStateAction<Array<Diagnostic>>>
+  /** TODO: Workaround to capture a crash of the gameserver. */
+  crashed: Boolean,
+  setCrashed: React.Dispatch<React.SetStateAction<Boolean>>
 }>({
-  proof: [],
+  proof: {steps: [], diagnostics: [], completed: false, completedWithWarnings: false},
-  setProof: () => {} // TODO: implement me
+  setProof: () => {},
+  interimDiags: [],
+  setInterimDiags: () => {},
+  crashed: false,
+  setCrashed: () => {}
 })
 
+
+// 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[];
@@ -50,18 +63,18 @@ export interface ProofStateProps {
   // triggerUpdate: () => Promise<void>;
 }
 
-export const ProofStateContext = React.createContext<{
+// export const ProofStateContext = React.createContext<{
-  proofState : ProofStateProps,
+//   proofState : ProofStateProps,
-  setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
+//   setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
-}>({
+// }>({
-  proofState : {
+//   proofState : {
-    status: 'updating',
+//     status: 'updating',
-    messages: [],
+//     messages: [],
-    goals: undefined,
+//     goals: undefined,
-    termGoal: undefined,
+//     termGoal: undefined,
-    error: undefined},
+//     error: undefined},
-  setProofState: () => {},
+//   setProofState: () => {},
-})
+// })
 
 export interface IPreferencesContext extends PreferencesState{
   mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.

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,16 +262,16 @@ export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
 })
 
 interface GoalsProps {
-    goals: InteractiveGoals
+    goals: InteractiveGoalsWithHints
     filter: GoalFilterState
 }
 
 export function Goals({ goals, filter }: GoalsProps) {
     if (goals.goals.length === 0) {
-        return <>No goals</>
+        return <></>
     } 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,45 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
         </details>
     </div>
 })
+
+export function loadGoals(
+  rpcSess: RpcSessionAtPos,
+  uri: string,
+  setProof: React.Dispatch<React.SetStateAction<ProofState>>,
+  setCrashed: React.Dispatch<React.SetStateAction<Boolean>>) {
+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) => {
+    if (typeof proof !== 'undefined') {
+      console.info(`received a proof state!`)
+      console.log(proof)
+      setProof(proof)
+      setCrashed(false)
+    } else {
+      console.warn('received undefined proof state!')
+      setCrashed(true)
+      // setProof(undefined)
+    }
+  }
+).catch((error) => {
+  setCrashed(true)
+  console.warn(error)
+})
+}
+
+
+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,10 @@ 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)).catch((error) => {
+            console.warn(error)
+          })
         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 +314,7 @@ function InfoAux(props: InfoProps) {
                 pos,
                 status: 'updating',
                 messages: lspDiagsHere.map(lspDiagToInteractive),
+                proof: undefined,
                 goals: undefined,
                 termGoal: undefined,
                 error: undefined,
@@ -318,11 +325,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(
+        Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
-            ([goals, termGoal, userWidgets, messages]) => resolve({
+            ([proof, goals, termGoal, userWidgets, messages]) => resolve({
                 pos,
                 status: 'ready',
                 messages,
+                proof : proof as any,
                 goals: goals as any,
                 termGoal,
                 error: undefined,
@@ -353,6 +361,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 +398,7 @@ function InfoAux(props: InfoProps) {
         pos,
         status: 'updating',
         messages: [],
+        proof: undefined,
         goals: undefined,
         termGoal: undefined,
         error: undefined,
@@ -412,6 +422,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,17 @@ import Markdown from '../markdown';
 
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
-import { Goal } from './goals';
+import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals';
-import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, SelectionContext, WorldLevelIdContext } from './context';
-import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
+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';
+import { DiagnosticSeverity } from 'vscode-languageclient';
 
 /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
  * always present, or the monaco editor cannot start.
@@ -61,36 +63,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
+  React.useEffect(() => {
-        let newTiles = [
+    if (proof?.completed) {
-          ...level?.tactics,
+      dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
-          ...level?.lemmas,
-          ...level?.definitions
-        ].filter((tile) => tile.new).map((tile) => tile.name)
 
-        // Add the proven statement to the local storage as well.
+      // On completion, add the names of all new items to the local storage
-        if (level?.statementName != null) {
+      let newTiles = [
-          newTiles.push(level?.statementName)
+        ...level?.tactics,
-        }
+        ...level?.lemmas,
+        ...level?.definitions
+      ].filter((tile) => tile.new).map((tile) => tile.name)
 
-        let inv: string[] = selectInventory(gameId)(store.getState())
+      // Add the proven statement to the local storage as well.
-
+      if (level?.statementName != null) {
-        // add new items and remove duplicates
+        newTiles.push(level?.statementName)
-        let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i)
-
-        dispatch(changedInventory({ game: gameId, inventory: newInv }))
       }
-    }, [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 +155,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 +196,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 +233,17 @@ 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?.completedWithWarnings &&
+        <div className="level-completed">
+          {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
+        </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 +259,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 <></> }
+  if (!proof?.steps[i]?.command) { return <></> }
-  return <div className="command">
+
-    <div className="command-text">{command}</div>
+  if (isLastStepWithErrors(proof, i)) {
-    <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
+    // If the last step has errors, we display the command in a different style
-      <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
+    // indicating that it will be removed on the next try.
-    </Button>
+    return <div className="failed-command">
-  </div>
+      <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 +331,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 +349,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>
 }
@@ -350,12 +399,11 @@ export function TypewriterInterface({props}) {
   const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
   const {mobile} = React.useContext(PreferencesContext)
-  const { proof } = React.useContext(ProofContext)
+  const { proof, setProof, crashed, setCrashed, interimDiags } = 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 +415,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 +432,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, setCrashed)
       ev.stopPropagation()
     }
   }
@@ -402,7 +454,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 +475,8 @@ export function TypewriterInterface({props}) {
     }
   }, [selectedStep])
 
-  // TODO: This about hidden hints is all copied from `level.tsx`. Can we move that into `hints.tsx`?
+  // TODO: superfluous, can be replaced with `withErr` from above
-
+  let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
-  // 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
 
 
   useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -474,20 +496,43 @@ export function TypewriterInterface({props}) {
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
-        {proof.length ?
+        {crashed ? <div>
-          <>
+          <p className="crashed_message">Crashed! Go to editor mode and fix your proof!
-            {proof.map((step, i) => {
+          Last server response:</p>
-              if (i == proof.length - 1 && lastStepErrors) {
+          {interimDiags.map(diag => {
-                // if the last command contains an error, we only display the errors but not the
+            const severityClass = diag.severity ? {
-                // entered command as it is still present in the command line.
+              [DiagnosticSeverity.Error]: 'error',
-                // TODO: Should not use index as key.
+              [DiagnosticSeverity.Warning]: 'warning',
-                return <div key={`proof-step-${i}`}>
+              [DiagnosticSeverity.Information]: 'information',
-                  <Errors errors={step.errors} typewriterMode={true} />
+              [DiagnosticSeverity.Hint]: 'hint',
+            }[diag.severity] : '';
+
+            return <div>
+              <div className={`${severityClass} ml1 message`}>
+                <p className="mv2">Line {diag.range.start.line}, Character {diag.range.start.character}</p>
+                <pre className="font-code pre-wrap">
+                  {diag.message}
+                </pre>
                 </div>
-              } else {
+            </div>
+          })}
+
+        </div> : proof?.steps.length ?
+          <>
+            {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)} />
+                  <Command proof={proof} i={i} deleteProof={deleteProof(i)} />
-                  <Errors errors={step.errors} typewriterMode={true} />
+                  <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 +540,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) => {}}/>
+                  {/* <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)) &&
-                  {mobile && i == proof.length - 1 &&
+                    <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) => {}}/>
-                    hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+                  }
-                    <Button className="btn btn-help" to="" onClick={activateHiddenHints}>
+                  {mobile && i == proof?.steps.length - 1 &&
-                      Show more help!
+                    <MoreHelpButton />
-                    </Button>
                   }
 
                   {/* 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 +562,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}`}>
@@ -535,11 +585,14 @@ export function TypewriterInterface({props}) {
                 }
               </div>
             }
-          </> : <CircularProgress variant="determinate" value={loadingProgress} />
+          </> : <CircularProgress variant="determinate" value={100*(1 - 1.024 ** (- loadingProgress))} />
+        // note: since we don't know the total number of files,
+        // we use a function which strictly monotonely increases towards `100` as `x → ∞`
+        // The base is chosen at random s.t. we get roughly 91% for `x = 100`.
         }
       </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,82 @@
  *
  * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts`
  */
-import { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
+import type { Range } from 'vscode-languageserver-protocol';
-
+import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api';
-export interface GameHint {
+import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*';
-  text: string;
+import type { Diagnostic } from 'vscode-languageserver-protocol';
-  hidden: boolean;
-}
 
 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;
+  rawText: string;
+  varNames: string[][]; // in Lean: `Array (Name × Name)`
+}
+
+export interface InteractiveGoalWithHints {
+  goal: InteractiveGoal;
   hints: GameHint[];
 }
 
-export interface InteractiveGoals {
+export interface InteractiveGoalsWithHints {
-  goals: InteractiveGoal[];
+  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 { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext } from './context'
-import { goalsToString } from './goals'
+import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
-import { GameHint, InteractiveGoals } from './rpc_api'
+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)
@@ -79,7 +87,7 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   const inputRef = useRef()
 
   // The context storing all information about the current proof
-  const {proof, setProof} = React.useContext(ProofContext)
+  const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
 
   // state to store the last batch of deleted messages
   const {setDeletedChat} = React.useContext(DeletedChatContext)
@@ -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 goalCalls = []
-    let msgCalls = []
+  //   let msgCalls = []
 
-    // For each line of code ask the server for the goals and the messages on this line
+  //   // 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++) {
+  //   for (let i = 0; i < model.getLineCount(); i++) {
-      goalCalls.push(
+  //     goalCalls.push(
-        rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
+  //       rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri}))
-      )
+  //     )
-      msgCalls.push(
+  //     msgCalls.push(
-        getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}).catch((error) => {console.debug("promise broken")})
+  //       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
+  //   // Wait for all these requests to be processed before saving the results
-    Promise.all(goalCalls).then((steps : InteractiveGoals[]) => {
+  //   Promise.all(goalCalls).then((steps : InteractiveGoalsWithHints[]) => {
-      Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
+  //     Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => {
-        let tmpProof : ProofStep[] = []
+  //       let tmpProof : ProofStep[] = []
 
-        let goalCount = 0
+  //       let goalCount = 0
 
-        steps.map((goals, i) => {
+  //       steps.map((goals, i) => {
-          // The first step has an empty command and therefore also no error messages
+  //         // 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
+  //         // 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.
+  //         // 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]) : []
+  //         let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
 
-          // Filter out the 'unsolved goals' message
+  //         // Filter out the 'unsolved goals' message
-          messages = messages.filter((msg) => {
+  //         messages = messages.filter((msg) => {
-            return !("append" in msg.message &&
+  //           return !("append" in msg.message &&
-              "text" in msg.message.append[0] &&
+  //             "text" in msg.message.append[0] &&
-              msg.message.append[0].text === "unsolved goals")
+  //             msg.message.append[0].text === "unsolved goals")
-          })
+  //         })
 
-          if (typeof goals == 'undefined') {
+  //         if (typeof goals == 'undefined') {
-            tmpProof.push({
+  //           tmpProof.push({
-              command: i ? model.getLineContent(i) : '',
+  //             command: i ? model.getLineContent(i) : '',
-              goals: [],
+  //             goals: [],
-              hints: [],
+  //             hints: [],
-              errors: messages
+  //             errors: messages
-            } as ProofStep)
+  //           } as ProofStep)
-            console.debug('goals is undefined')
+  //           console.debug('goals is undefined')
-            return
+  //           return
-          }
+  //         }
 
-          // If the number of goals reduce, show a message
+  //         // If the number of goals reduce, show a message
-          if (goals.goals.length && goalCount > goals.goals.length) {
+  //         if (goals.length && goalCount > goals.length) {
-            messages.unshift({
+  //           messages.unshift({
-              range: {
+  //             range: {
-                start: {
+  //               start: {
-                  line: i-1,
+  //                 line: i-1,
-                  character: 0,
+  //                 character: 0,
-                },
+  //               },
-                end: {
+  //               end: {
-                  line: i-1,
+  //                 line: i-1,
-                  character: 0,
+  //                 character: 0,
-                }},
+  //               }},
-              severity: DiagnosticSeverity.Information,
+  //             severity: DiagnosticSeverity.Information,
-              message: {
+  //             message: {
-              text: 'intermediate goal solved 🎉'
+  //             text: 'intermediate goal solved 🎉'
-              }
+  //             }
-            })
+  //           })
-          }
+  //         }
-          goalCount = goals.goals.length
+  //         goalCount = goals.length
 
-          // with no goals there will be no hints.
+  //         // with no goals there will be no hints.
-          let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : []
+  //         let hints : GameHint[] = goals.length ? goals[0].hints : []
 
-          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+  //         console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
-          console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+  //         console.debug(`Goals: (${i}): `, goalsToString(goals)) //
-          console.debug(`Hints: (${i}): `, hints)
+  //         console.debug(`Hints: (${i}): `, hints)
-          console.debug(`Errors: (${i}): `, messages)
+  //         console.debug(`Errors: (${i}): `, messages)
 
-          tmpProof.push({
+  //         tmpProof.push({
-            // the command of the line above. Note that `getLineContent` starts counting
+  //           // the command of the line above. Note that `getLineContent` starts counting
-            // at `1` instead of `zero`. The first ProofStep will have an empty command.
+  //           // at `1` instead of `zero`. The first ProofStep will have an empty command.
-            command: i ? model.getLineContent(i) : '',
+  //           command: i ? model.getLineContent(i) : '',
-            // TODO: store correct data
+  //           // TODO: store correct data
-            goals: goals.goals,
+  //           goals: goals.map(g => g.goal),
-            // only need the hints of the active goals in chat
+  //           // only need the hints of the active goals in chat
-            hints: hints,
+  //           hints: hints,
-            // errors and messages from the server
+  //           // errors and messages from the server
-            errors: messages
+  //           errors: messages
-          } as ProofStep)
+  //         } as ProofStep)
 
-        })
+  //       })
-        // Save the proof to the context
+  //       // Save the proof to the context
-        setProof(tmpProof)
+  //       setProof(tmpProof)
-      }).catch((error) => {console.debug("promise broken")})
+  //     }).catch((error) => {console.debug("promise broken")})
-    }).catch((error) => {console.debug("promise broken")})
+  //   }).catch((error) => {console.debug("promise broken")})
-  }, [editor, rpcSess, uri, model])
+  // }, [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, setCrashed)
     }
 
     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)) {
+    loadGoals(rpcSess, uri, setProof, setCrashed)
-      setTypewriterInput(proof[proof.length - 1].command)
+  }, [])
+
+  /** 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,14 @@ export function Typewriter({hidden, disabled}: {hidden?: boolean, disabled?: boo
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == uri) {
       setProcessing(false)
-      loadAllGoals()
+
+      console.log('Received lean diagnostics')
+      console.log(params.diagnostics)
+      setInterimDiags(params.diagnostics)
+
+      //loadGoals(rpcSess, uri, setProof)
+
+      // TODO: loadAllGoals()
       if (!hasErrors(params.diagnostics)) {
         //setTypewriterInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
@@ -236,6 +259,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 +338,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 +348,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 +377,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/level.tsx

@@ -16,6 +16,7 @@ import { InfoviewApi } from '@leanprover/infoview'
 import { EditorContext } from '../../../node_modules/lean4-infoview/src/infoview/contexts'
 import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-infoview/src/infoview/editorConnection'
 import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event'
+import { Diagnostic } from 'vscode-languageserver-types'
 
 import { GameIdContext } from '../app'
 import { useAppDispatch, useAppSelector } from '../hooks'
@@ -28,10 +29,10 @@ import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
 import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
-  ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
+  ProofContext, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
-import { GameHint } from './infoview/rpc_api'
+import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
-import { DeletedHints, Hint, Hints, filterHints } from './hints'
+import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints'
 import { PrivacyPolicyPopup } from './popup/privacy_policy'
 import path from 'path';
 
@@ -49,6 +50,7 @@ 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()
@@ -72,7 +74,7 @@ function Level() {
   </WorldLevelIdContext.Provider>
 }
 
-function ChatPanel({lastLevel}) {
+function ChatPanel({lastLevel, visible = true}) {
   const chatRef = useRef<HTMLDivElement>(null)
   const {mobile} = useContext(PreferencesContext)
   const gameId = useContext(GameIdContext)
@@ -83,9 +85,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?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
-  let k = proof.length - 1
-  let withErr = hasInteractiveErrors(proof[k]?.errors) ? 1 : 0
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -98,29 +98,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')
@@ -146,29 +123,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
+  return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
-  // This effectively prevent consequtive hints being shown.
-  let modifiedHints : GameHint[][] = filterHints(proof)
-
-  return <div className="chat-panel">
     <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)} />
+          hint={{text: t, hidden: false, rawText: t, varNames: []}} 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! 🎉
@@ -182,7 +164,7 @@ function ChatPanel({lastLevel}) {
       }
     </div>
     <div className="button-row">
-      {completed && (lastLevel ?
+      {proof?.completed && (lastLevel ?
         <Button to={`/${gameId}`}>
           <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
         </Button> :
@@ -190,16 +172,13 @@ function ChatPanel({lastLevel}) {
           Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
         </Button>)
         }
-      {hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
+      <MoreHelpButton />
-        <Button to="" onClick={activateHiddenHints}>
-          Show more help!
-        </Button>
-      }
     </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})
@@ -229,7 +208,11 @@ 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})
+  const [interimDiags, setInterimDiags] = useState<Array<Diagnostic>>([])
+  const [isCrashed, setIsCrashed] = useState<Boolean>(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>>([])
@@ -356,15 +339,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)}))
     }
@@ -402,7 +385,7 @@ function PlayableLevel({impressum, setImpressum}) {
     <DeletedChatContext.Provider value={{deletedChat, setDeletedChat, showHelp, setShowHelp}}>
       <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
         <InputModeContext.Provider value={{typewriterMode, setTypewriterMode, typewriterInput, setTypewriterInput, lockInputMode, setLockInputMode}}>
-          <ProofContext.Provider value={{proof, setProof}}>
+          <ProofContext.Provider value={{proof, setProof, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
             <EditorContext.Provider value={editorConnection}>
               <MonacoEditorContext.Provider value={editor}>
                 <LevelAppBar
@@ -449,7 +432,7 @@ function IntroductionPanel({gameInfo}) {
     <div className="chat">
       {text?.filter(t => t.trim()).map(((t, i) =>
         <Hint key={`intro-p-${i}`}
-          hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
+          hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
       ))}
     </div>
     <div className={`button-row${mobile ? ' mobile' : ''}`}>
@@ -622,7 +605,9 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
     }
     // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
     setInfoProvider(infoProvider)
-    client.restart()
+
+    // TODO: it looks like we get errors "File Changed" here.
+    client.restart("Lean4Game")
 
     const editorApi = infoProvider.getApi()
 

client/src/css/infoview.css

@@ -41,6 +41,13 @@
 .level-completed {
   font-size: 1.8rem;
   font-weight: 500;
+  padding-left: .5em;
+  padding-right: .5em;
+  padding-top: .2em;
+  padding-bottom: .2em;
+  border-radius: .5em;
+  background-color: #eee;
+
 }
 
 .typewriter {
@@ -188,6 +195,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;
@@ -199,3 +218,10 @@
 .undo-button {
   color: #888;
 }
+
+.crashed_message {
+  color: #D8000C;
+  font-weight: bold;
+  padding-left: .5em;
+  padding-right: .5em;
+}

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);
+} */

doc/create_game.md

@@ -189,8 +189,7 @@ The statement is the exercise of the level. The basics work the same as they wou
 
 #### 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 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
@@ -203,6 +202,28 @@ Statement ...
   sorry
 ```
 
+#### Local `let` definitions
+
+If you want to make a local definition/notation which only holds for this exercise (e.g.
+a function `f : ℤ → ℤ := fun x ↦ 2 * x`) the recommended way is to use a `let`-statement:
+
+```lean
+Statement (a : ℤ) (h : 0 < a) :
+    let f : ℤ → ℤ := fun x ↦ 2 * x
+    0 < f a := by
+  sorry
+```
+
+The game automatically `intros` such `let`-statements, such that you and the player will see
+the following initial proof state:
+
+```
+a: ℤ
+h: 0 < a
+f: ℤ → ℤ := fun x => 2 * x
+⊢ 0 < f a
+```
+
 #### Attributes
 
 You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:

doc/hints.md

@@ -86,4 +86,36 @@ create new assumptions.
 
 You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$`
 
+**Escaping**: Generally, if you add text inside quotes `" "` (e.g. in `Hint`) you need to escape
+backslashes, but if you provide text inside a doc comment
+`/-- -/` (e.g. in the `Statement` description) you do not!
+
 TODO: Write a doc about latex/markdown options available.
+
+### Commutative diagrams
+
+Here is an example of how to write a commutative diagram in KaTeX:
+
+$$
+\begin{CD}
+      A  @>{f}>> B @<{g}<< C    \\
+  @V{h}VV    @V{i}VV   @V{j}VV \\
+      D  @<{k}<< E @>{l}>> F    \\
+  @A{m}AA    @A{n}AA   @V{p}VV \\
+      G  @<{q}<< H @>{r}>> I
+\end{CD}
+$$
+
+```
+$$
+\\begin{CD}
+      A  @>{f}>> B @<{g}<< C    \\\\
+  @V{h}VV    @V{i}VV   @V{j}VV \\\\
+      D  @<{k}<< E @>{l}>> F    \\\\
+  @A{m}AA    @A{n}AA   @V{p}VV \\\\
+      G  @<{q}<< H @>{r}>> I
+\\end{CD}
+$$
+```
+
+See https://www.jmilne.org/not/Mamscd.pdf

package-lock.json

@@ -8753,9 +8753,9 @@
       }
     },
     "node_modules/ip": {
-      "version": "1.1.8",
+      "version": "1.1.9",
-      "resolved": "https://registry.npmjs.org/ip/-/ip-1.1.8.tgz",
+      "resolved": "https://registry.npmjs.org/ip/-/ip-1.1.9.tgz",
-      "integrity": "sha512-PuExPYUiu6qMBQb4l06ecm6T6ujzhmh+MeJcW9wa89PoAz5pvd4zPgN5WJV104mb6S2T1AwNIAaB70JNrLQWhg=="
+      "integrity": "sha512-cyRxvOEpNHNtchU3Ln9KC/auJgup87llfQpQ+t5ghoC/UhL16SWzbueiCsdTnWmqAWl7LadfuwhlqmtOaqMHdQ=="
     },
     "node_modules/ip-anonymize": {
       "version": "0.1.0",
@@ -14341,6 +14341,14 @@
         "node": ">=6"
       }
     },
+    "node_modules/stacktrace-parser/node_modules/type-fest": {
+      "version": "0.7.1",
+      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-0.7.1.tgz",
+      "integrity": "sha512-Ne2YiiGN8bmrmJJEuTWTLJR32nh/JdL1+PSicowtNb0WFpn59GK8/lfD61bVtzguz7b3PBt74nxpv/Pw5po5Rg==",
+      "engines": {
+        "node": ">=8"
+      }
+    },
     "node_modules/statuses": {
       "version": "2.0.1",
       "resolved": "https://registry.npmjs.org/statuses/-/statuses-2.0.1.tgz",
@@ -14902,9 +14910,12 @@
       }
     },
     "node_modules/type-fest": {
-      "version": "0.7.1",
+      "version": "4.10.3",
-      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-0.7.1.tgz",
+      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-4.10.3.tgz",
-      "integrity": "sha512-Ne2YiiGN8bmrmJJEuTWTLJR32nh/JdL1+PSicowtNb0WFpn59GK8/lfD61bVtzguz7b3PBt74nxpv/Pw5po5Rg==",
+      "integrity": "sha512-JLXyjizi072smKGGcZiAJDCNweT8J+AuRxmPZ1aG7TERg4ijx9REl8CNhbr36RV4qXqL1gO1FF9HL8OkVmmrsA==",
+      "dev": true,
+      "optional": true,
+      "peer": true,
       "engines": {
         "node": ">=8"
       }

server/GameServer/Commands.lean

@@ -2,6 +2,9 @@ import GameServer.Helpers
 import GameServer.Inventory
 import GameServer.Options
 import GameServer.SaveData
+import GameServer.Hints
+import GameServer.Tactic.LetIntros
+import I18n
 
 open Lean Meta Elab Command
 
@@ -32,16 +35,17 @@ elab "Level" level:num : command => do
 
 /-- Define the title of the current game/world/level. -/
 elab "Title" t:str : command => do
+  let title ← t.getString.translate
   match ← getCurLayer with
-  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
+  | .Level => modifyCurLevel fun level => pure {level with title := title}
-  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with title := title}
   | .Game => modifyCurGame  fun game => pure {game with
       title := t.getString
-      tile := {game.tile with title := t.getString}}
+      tile := {game.tile with title := title}}
 
 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let intro := t.getString
+  let intro ← t.getString.translate
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
   | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
@@ -49,7 +53,7 @@ elab "Introduction" t:str : command => do
 
 /-- Define the info of the current game. Used for e.g. credits -/
 elab "Info" t:str : command => do
-  let info:= t.getString
+  let info ← t.getString.translate
   match ← getCurLayer with
   | .Level =>
     logError "Can't use `Info` in a level!"
@@ -81,7 +85,7 @@ elab "Image" t:str : command => do
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
-  let conclusion := t.getString
+  let conclusion ← t.getString.translate
   match ← getCurLayer with
   | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
   | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
@@ -94,13 +98,13 @@ elab "Prerequisites" t:str* : command => do
 
 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
-  let caption := t.getString
+  let caption ← t.getString.translate
   modifyCurGame fun game => pure {game with
     tile := {game.tile with short := caption}}
 
 /-- More detailed description what the game is about (2-4 sentences). -/
 elab "CaptionLong" t:str : command => do
-  let caption := t.getString
+  let caption ← t.getString.translate
   modifyCurGame fun game => pure {game with
     tile := {game.tile with long := caption}}
 
@@ -141,6 +145,7 @@ TacticDoc rw "`rw` stands for rewrite, etc. "
  -/
 elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do
   let doc ← parseDocCommentLegacy doc content
+  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Tactic
     name := name.getId
@@ -165,6 +170,7 @@ The theorem/definition to have the same fully qualified name as in mathlib.
 elab doc:docComment ? "TheoremDoc" name:ident "as" displayName:str "in" category:str content:str ? :
     command => do
   let doc ← parseDocCommentLegacy doc content
+  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Lemma
     name := name.getId
@@ -194,6 +200,7 @@ The theorem/definition to have the same fully qualified name as in mathlib.
  -/
 elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do
   let doc ← parseDocCommentLegacy doc template
+  let doc ← doc.translate
   modifyEnv (inventoryTemplateExt.addEntry · {
     type := .Definition
     name := name.getId,
@@ -340,6 +347,9 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   let lvlIdx ← getCurLevelIdx
 
   let docContent ← parseDocComment doc
+  let docContent ← match docContent with
+  | none => pure none
+  | some d => d.translate
 
   -- Save the messages before evaluation of the proof.
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
@@ -355,36 +365,38 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     collectUsedInventory proof
   | _ => throwError "expected `:=`"
 
+  -- extract the `tacticSeq` from `val` in order to add `let_intros` in front.
+  -- TODO: don't understand meta-programming enough to avoid having `let_intros`
+  -- duplicated three times below…
+  let tacticStx : TSyntax `Lean.Parser.Tactic.tacticSeq := match val with
+  | `(Parser.Command.declVal| := by $proof) => proof
+  | _ => panic "expected `:= by`"
+
   -- Add theorem to context.
   match statementName with
   | some name =>
     let env ← getEnv
-
     let fullName := (← getCurrNamespace) ++ name.getId
-
     if env.contains fullName then
       let origType := (env.constants.map₁.find! fullName).type
       -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
       -- in that case.
       logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
-
     else
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $val)
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
-
   | none =>
-    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨tacticStx⟩)})
     elabCommand thmStatement
 
   let msgs := (← get).messages
-
   let mut hints := #[]
   let mut nonHintMsgs := #[]
   for msg in msgs.msgs do
@@ -396,12 +408,41 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
         .nest hidden $
         .compose (.ofGoal text) (.ofGoal goal) := msg.data then
       let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
+
+        let goalDecl ← goal.getDecl
+        let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (·.fvarId)
+
+        -- NOTE: This code about `hintFVarsNames` is duplicated from `RpcHandlers`
+        -- where the variable bijection is constructed, and they
+        -- need to be matching.
+        -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
+        -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
+        -- and we wrap them in `«{}»` here since I don't know how to do it later.
+        let mut hintFVarsNames : Array Expr := #[]
+        for fvar in fvars do
+          let name₁ ← fvar.getUserName
+          hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
+
+        let text ← instantiateMVars (mkMVar text)
+
+        -- Evaluate the text in the `Hint`'s context to get the old variable names.
+        let rawText := (← GameServer.evalHintMessage text) hintFVarsNames
+        let ctx₂ := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+        let rawText : String ← (MessageData.withContext ctx₂ rawText).toString
+
         return {
           goal := ← abstractCtx goal
-          text := ← instantiateMVars (mkMVar text)
+          text := text
+          rawText := rawText
           strict := strict == 1
           hidden := hidden == 1
         }
+
+      -- Note: The current setup for hints is a bit convoluted, but for now we need to
+      -- send the text once through i18n to register it in the env extension.
+      -- This could probably be rewritten once i18n works fully.
+      let _ ← hint.rawText.translate
+
       hints := hints.push hint
     else
       nonHintMsgs := nonHintMsgs.push msg
@@ -440,6 +481,8 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
 
 /-! # Hints -/
 
+open GameServer in
+
 /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
 see hints. The tactic does not affect the goal state.
 -/

server/GameServer/EnvExtensions.lean

@@ -1,7 +1,13 @@
 import GameServer.AbstractCtx
 import GameServer.Graph
+import GameServer.Hints
 
+open GameServer
 
+-- TODO: Is there a better place?
+/-- Keywords that the server should not consider as tactics. -/
+def GameServer.ALLOWED_KEYWORDS : List String :=
+  ["with", "fun", "at", "only", "by", "generalizing"]
 
 /-- The default game name if `Game "MyGame"` is not used. -/
 def defaultGameName: String := "MyGame"
@@ -18,22 +24,6 @@ defined in this file.
 
 open Lean
 
-/-! ## Hints -/
-
-/-- A hint to help the user with a specific goal state -/
-structure GoalHintEntry where
-  goal : AbstractCtxResult
-  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
-  text : Expr
-  /-- If true, then hint should be hidden and only be shown on player's request -/
-  hidden : Bool := false
-  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
-  strict : Bool := false
-
-instance : Repr GoalHintEntry := {
-  reprPrec := fun a n => reprPrec a.text n
-}
-
 /-! ## Inventory (documentation)
 
 The inventory contains documentation that the user can access.

server/GameServer/FileWorker.lean

@@ -3,6 +3,8 @@ import Lean.Server.FileWorker
 import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
+import GameServer.EnvExtensions
+import GameServer.Tactic.LetIntros
 
 namespace MyModule
 
@@ -60,8 +62,8 @@ open Snapshots
 open JsonRpc
 
 /--
-Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
+Game-specific state to be packed on top of the `Server.FileWorker.WorkerState`
-used by the lean server.
+used by the Lean server.
 -/
 structure WorkerState :=
   /--
@@ -84,7 +86,7 @@ structure WorkerState :=
 deriving ToJson, FromJson
 
 /--
-Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
+Pack the our custom `WorkerState` on top of the normal worker monad
 `Server.FileWorker.WorkerM`.
 -/
 abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
@@ -102,16 +104,6 @@ def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
       pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
       data     := s }}
 
-/-- Deprecated! -/
-def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (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 }}
-
 -- TODO: use HashSet for allowed tactics?
 /--
 Find all tactics in syntax object that are forbidden according to a
@@ -131,7 +123,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
     -- 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"]
+    let allowed := GameServer.ALLOWED_KEYWORDS
     -- 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
       -- Treat `simp?` and `simp!` like `simp`
@@ -178,15 +170,20 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
       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!"
+        addMessageByDifficulty info s!"The theorem/definition '{n}' is not available in this game!"
       | 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.
+          match workerState.inventory.find? (· == n.toString) with
-          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+          | none =>
+            -- Theorem is still locked.
+            addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+          | some _ =>
+            -- Theorem is in the inventory, allow it.
+            pure ()
 
 where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
   -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
@@ -262,8 +259,11 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
 
+          -- Always call `let_intros` to get rid `let` statements in the goal.
+          -- This makes the experience for the user much nicer and allows for local
+          -- definitions in the exercise.
           let cmdStx ← `(command|
-            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {let_intros; $(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
       cmdCtx cmdStateRef
   let postNew := (← tacticCacheNew.get).post
@@ -308,7 +308,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 }
 
@@ -322,74 +322,133 @@ where
     uri : String
   deriving ToJson, FromJson
 
-  /-- Checks whether game level has been completed and sends a notification to the client -/
+structure GameDiagnostics where
-  def publishGameCompleted (m : DocumentMeta) (hOut : FS.Stream) (snaps : Array Snapshot) : IO Unit := do
+  diagnostics : List Diagnostic
-    -- check if there is any error or warning
+deriving ToJson, FromJson
-    for snap in snaps do
-      if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
-      then return
-    let param := { uri := m.uri : GameCompletedParams}
-    hOut.writeLspNotification { method := "$/game/completed", param }
 
-  /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
+structure GameParams where
-  private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
+  uri : String
-      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
+  diagnostics : GameDiagnostics
-      : AsyncElabM (Option Snapshot) := do
+deriving ToJson, FromJson
-    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
-    -- 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
-      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.
-    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`. -/
+/-- WIP: publish diagnostics, all intermediate goals and if the game is completed. -/
-  def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
+def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.InitializeParams) (hOut : FS.Stream) :
-      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
+    IO Unit := do
-      : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
+  -- let text := m.text
-    let ctx ← read
+
-    let some headerSnap := snaps[0]? | panic! "empty snapshots"
+  -- -- `snap` is the one snapshot containing the entire proof.
-    if headerSnap.msgLog.hasErrors then
+  -- let mut goals : Array <| InteractiveGoalsWithHints := #[]
-      -- Treat header processing errors as fatal so users aren't swamped with
+  -- for pos in text.positions do
-      -- followup errors
+  --   let source := text.getLineBefore pos
-      publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
+  --   -- iterate over all newlines in the proof and get the goals and hints at each position
-      publishIleanInfoFinal m ctx.hOut #[headerSnap]
+  --   if let goalsAtResult@(_ :: _) := snap.infoTree.goalsAt? text pos then
-      return AsyncList.ofList [headerSnap]
+  --     pure ()
-    else
+  --     let goalAtPos : List <| List InteractiveGoalWithHints ← goalsAtResult.mapM
-      -- This will overwrite existing ilean info for the file since this has a
+  --       fun { ctxInfo := ci, tacticInfo := tacticInfo, useAfter := useAfter, .. } => do
-      -- higher version number.
+  --         -- TODO: What does this function body do?
-      publishIleanInfoUpdate m ctx.hOut snaps
+  --         -- let ciAfter := { ci with mctx := ti.mctxAfter }
-      return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+  --         let ci := if useAfter then
-        IO.sleep startAfterMs
+  --             { ci with mctx := tacticInfo.mctxAfter }
-        AsyncList.unfoldAsync (nextSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
+  --           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
+  for snap in snaps do
+    if snap.diagnostics.any fun d => d.severity? == some .error ∨ d.severity? == some .warning
+    then return
+  let param := { uri := m.uri : GameCompletedParams}
+  hOut.writeLspNotification { method := "$/game/completed", param }
+
+/-- 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
+    publishDiagnostics m lastSnap.diagnostics.toArray ctx.hOut
+    publishProgressDone m ctx.hOut
+    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
+    gameWorkerState initParams
+
+  set { s with snaps := s.snaps.push snap }
+  cancelTk.check
+  -- publishProofState m snap initParams ctx.hOut
+  publishDiagnostics m snap.diagnostics.toArray ctx.hOut
+  publishIleanInfoUpdate m ctx.hOut #[snap]
+  return some snap
+
+-- 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
+    publishProgressAtPos m headerSnap.beginPos ctx.hOut (kind := LeanFileProgressKind.fatalError)
+    publishIleanInfoFinal m ctx.hOut #[headerSnap]
+    return AsyncList.ofList [headerSnap]
+  else
+    publishIleanInfoUpdate m ctx.hOut snaps
+    return AsyncList.ofList snaps.toList ++ AsyncList.delayed (← EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+      IO.sleep startAfterMs
+      AsyncList.unfoldAsync (nextCmdSnap ctx m cancelTk gameWorkerState ctx.initParams) { snaps })
 
 end Elab
 
@@ -439,7 +498,7 @@ def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
         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 s ctx
+    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 }}
@@ -453,6 +512,12 @@ def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
   fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
   fileMap  := default
 
+/-- `gameDir` and `module` were added.
+
+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
@@ -488,7 +553,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let cmdState := Elab.Command.mkState headerEnv {} opts
     let cmdState := { cmdState with infoState := {
       enabled := true
-      trees := #[Elab.InfoTree.context ({
+      trees := #[Elab.InfoTree.context (.commandCtx {
         env     := headerEnv
         fileMap := m.text
         ngen    := { namePrefix := `_worker }
@@ -505,7 +570,7 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     let headerSnap := {
       beginPos := 0
       stx := headerStx
-      mpState := {}
+      mpState := {} -- was `headerParserState`
       cmdState := cmdState
       interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
       tacticCache := (← IO.mkRef {})
@@ -513,49 +578,52 @@ def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWid
     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 gameWorkerState.levelInfo.module
+    (gameDir := gameDir) (module := gameWorkerState.levelInfo.module)
   let cancelTk ← CancelToken.new
-  let ctx :=
+  let ctx := {
-    { hIn  := i
+    hIn  := i
-      hOut := o
+    hOut := o
-      hLog := e
+    hLog := e
-      headerTask
+    headerTask
-      initParams
+    initParams
-      clientHasWidgets
+    clientHasWidgets
-    }
+  }
   let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-    | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | 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,
+  return (ctx, {
-  { doc             := doc
+    doc                := doc
-    initHeaderStx   := headerStx
+    initHeaderStx      := headerStx
     currHeaderStx      := headerStx
     importCachingTask? := none
-    pendingRequests := RBMap.empty
+    pendingRequests    := RBMap.empty
-    rpcSessions     := RBMap.empty
+    rpcSessions        := RBMap.empty
   })
 
 end Initialization
 
 section NotificationHandling
 
+/-- 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
+  let oldDoc := (← StateT.lift get).doc -- needed a lift to our custom `WorkerM`
-  let some newVersion ← pure docId.version?
+  let newVersion := docId.version?.getD 0
-    | throwServerError "Expected version number"
+  if ¬ changes.isEmpty then
-  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
+    -- modification: set the `DependencyBuildMode` from
+    -- `oldDoc.meta.dependencyBuildMode` to `.always`
     updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
@@ -591,39 +659,34 @@ end MessageHandling
 section MainLoop
 
 /--
-Erase finished tasks if there are no errors.
+The main-loop. Copied from `Lean.Server.FileWorker.mainLoop`. Use custom `WorkerM` as well
--/
+as custom `handleNotification`.
-private def 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
-
-/--
-The main-loop.
 -/
+--@[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
-  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
+  -- Erase finished tasks if there are no errors.
-    filterFinishedTasks acc id task) st.pendingRequests
+  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 }
-  -- 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 }
 
   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) =>
@@ -633,6 +696,7 @@ partial def mainLoop : WorkerM Unit := do
   | Message.notification "exit" none =>
     let doc := st.doc
     doc.cancelTk.set
+    doc.cmdSnaps.cancel
     return ()
   | Message.notification method (some params) =>
     -- Custom notification handler
@@ -643,10 +707,15 @@ partial def mainLoop : WorkerM Unit := do
 
 end MainLoop
 
-
+/-- 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
+
+
+  -- BIG MODIFICATION
   let initRequest ← i.readLspRequestAs "initialize" Game.InitializeParams
   o.writeLspResponse {
     id     := initRequest.id
@@ -662,16 +731,16 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
   discard $ i.readLspNotificationAs "initialized" InitializedParams
   let ⟨_, param⟩ ← i.readLspNotificationAs "textDocument/didOpen" DidOpenTextDocumentParams
 
+
   let doc := param.textDocument
-  /- NOTE(WN): `toFileMap` marks line beginnings as immediately following
+  -- modification: using `.always`
-    "\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. -/
   let meta : DocumentMeta := ⟨doc.uri, doc.version, doc.text.toFileMap, .always⟩
   let e := e.withPrefix s!"[{param.textDocument.uri}] "
   let _ ← IO.setStderr e
   try
+
+
+    -- BIG MODIFICATION
     let game ← loadGameData gameDir
     -- TODO: We misuse the `rootUri` field to the gameName
     let rootUri? : Option String := some (toString game.name)
@@ -691,6 +760,8 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
     -- Run the main loop
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
       StateT.run (s := gameWorkerState) <| (mainLoop)
+
+
     return (0 : UInt32)
   catch e =>
     IO.eprintln e
@@ -703,8 +774,12 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
 /--
 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
@@ -712,9 +787,6 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
   try
     let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
     let exitCode ← initAndRunWorker i o e opts gameDir
-    -- 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.
     o.flush
     e.flush
     IO.Process.exit exitCode.toUInt8

server/GameServer/Helpers.lean

@@ -4,8 +4,6 @@ import Lean
 
 open Lean Meta Elab Command
 
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
 /-! ## Doc Comment Parsing -/
 
 /-- Read a doc comment and get its content. Return `""` if no doc comment available. -/
@@ -85,23 +83,6 @@ def getStatementString (name : Name) : CommandElabM String := do
 syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")"
 -- TODO
 
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
-
 /-! ## Loops in Graph-like construct
 
 TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`?

server/GameServer/Hints.lean

@@ -0,0 +1,54 @@
+import GameServer.AbstractCtx
+
+/-!
+This file contains anything related to the `Hint` tactic used to add hints to a game level.
+-/
+
+open Lean Meta Elab
+
+namespace GameServer
+
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
+
+/-- A hint to help the user with a specific goal state -/
+structure GoalHintEntry where
+  goal : AbstractCtxResult
+  /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
+  text : Expr
+  rawText : String
+  /-- If true, then hint should be hidden and only be shown on player's request -/
+  hidden : Bool := false
+  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
+  strict : Bool := false
+
+instance : Repr GoalHintEntry := {
+  reprPrec := fun a n => reprPrec a.text n
+}
+
+/-- For a hint `(hint : GoalHintEntry)` one uses `(← evalHintMessage hint.text) x`
+ where `(x : Array Expr)` contains the names of all the variables that should be inserted
+ in the text.
+
+ TODO: explain better. -/
+unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
+  evalExpr (Array Expr → MessageData)
+    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
+      (mkConst ``MessageData) .default)
+
+@[implemented_by evalHintMessageUnsafe]
+def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
+
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""

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
+-- duplicated with custom `InteractiveGoalCore`
-  text : String
+-- @[inherit_doc Lean.Widget.InteractiveGoalCore.pretty]
-  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
-
 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)
+        |>.filter (· != toString Name.anonymous)
-        |>.map toString
         |> " ".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)
+    type        := (← ppExprTagged type)
-    val?           := (← value?.mapM ppExprTagged)
+    val?        := (← value?.mapM ppExprTagged)
-    isInstance?    := if (← isClass? type).isSome then true else none
+    isInstance? := if (← isClass? type).isSome then true else none
-    isType?        := if (← instantiateMVars type).isSort then true else none
+    isType?     := if (← instantiateMVars type).isSort then true else none
-    isAssumption?  := if (← inferType type).isProp 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/Inventory.lean

@@ -121,7 +121,7 @@ partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : Co
   | .atom _info val =>
     -- ignore syntax elements that do not start with a letter
     -- and ignore some standard keywords
-    let allowed := ["with", "fun", "at", "only", "by"]
+    let allowed := GameServer.ALLOWED_KEYWORDS
     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`
       return {acc with tactics := acc.tactics.insert val}

server/GameServer/RpcHandlers.lean

@@ -1,5 +1,7 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
+import Std.Data.Array.Init.Basic
+import GameServer.Hints
 
 open Lean
 open Server
@@ -7,7 +9,6 @@ open Widget
 open RequestM
 open Meta
 
-
 /-! ## GameGoal -/
 
 namespace GameServer
@@ -103,49 +104,236 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in
   then return some bij
   else return none
 
-unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
-  evalExpr (Array Expr → MessageData)
-    (.forallE default (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr))
-      (mkConst ``MessageData) .default)
-
-@[implemented_by evalHintMessageUnsafe]
-def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pure (fun _ => "")
-
 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
+    let some level ← getLevelByFileName? initParams m.mkInputContext.fileName
-      | throwError "Level not found: {doc.meta.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)
         then
-          let lctx := (← goal.getDecl).lctx
+
-          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          -- NOTE: This code for `hintFVarsNames` is also duplicated in the
+          -- "Statement" command, where `hint.rawText` is created. They need to be matching.
+          -- NOTE: This is a bit a hack of somebody who does not know how meta-programming works.
+          -- All we want here is a list of `userNames` for the `FVarId`s in `hintFVars`...
+          -- and we wrap them in `«{}»` here since I don't know how to do it later.
+          let mut hintFVarsNames : Array Expr := #[]
+          for fvar in hintFVars do
+            let name₁ ← fvar.fvarId!.getUserName
+            hintFVarsNames := hintFVarsNames.push <| Expr.fvar ⟨s!"«\{{name₁}}»"⟩
+
+          let lctx := (← goal.getDecl).lctx -- the player's local context
+          if let some bij ← matchDecls hintFVars lctx.getFVars
+            (strict := hint.strict) (initBij := fvarBij)
           then
             let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
+            -- Evaluate the text in the player's context to get the new variable names.
             let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
             let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}}
             let text ← (MessageData.withContext ctx text).toString
-            return some { text := text, hidden := hint.hidden }
+
+            -- Here we map the goal's variable names to the player's variable names.
+            let mut varNames : Array <| Name × Name := #[]
+            for (fvar₁, fvar₂) in bij.forward.toArray do
+              -- get the `userName` of the fvar in the opened local context of the hint.
+              let name₁ ← fvar₁.getUserName
+              -- get the `userName` in the player's local context.
+              let name₂ := (lctx.get! fvar₂).userName
+              varNames := varNames.push (name₁, name₂)
+
+            return some {
+              text := text,
+              hidden := hint.hidden,
+              rawText := hint.rawText,
+              varNames := varNames }
+
           else return none
         else
           return none
     return hints
 
-open RequestM in
+def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
-def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do
+    Array InteractiveDiagnostic :=
+  a.filter (fun d => match d.message with
+  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
+  | _ => true)
+
+-- 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
+    -- If there is any errors, goals might vanish without being 'solved'
+    -- so showing the message "intermediate goal solved" would be confusing.
+    if (¬ (filterUnsolvedGoal startDiags).any (·.severity? == some .error)) then
+      out := out.push {
+        message := .text "intermediate goal solved! 🎉"
+        range := {
+          start := pos
+          «end» := pos
+          }
+        severity? := Lsp.DiagnosticSeverity.information
+      }
+
+  return out
+
+
+/-- 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
+
+  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 +341,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
+              -- let hints ← findHints goal doc.meta rc.initParams
-              return ← goalToInteractive goal hints
+              return ← goalToInteractive goal
           -- compute the goal diff
           -- let goals ← ciAfter.runMetaM {} (do
           --     try
@@ -163,8 +351,8 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio
           --       -- fail silently, since this is just a bonus feature
           --       return goals
           -- )
-          return {goals}
+          return goals
-        return some <| goals.foldl (· ++ ·) ⟨#[]⟩
+        return some <| ⟨goals.foldl (· ++ ·) #[]⟩
       else
         return none
 
@@ -172,7 +360,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

@@ -1,8 +1,8 @@
 import GameServer.EnvExtensions
+import I18n
 
 open Lean Meta Elab Command
 
-
 /-! ## Copy images -/
 
 open IO.FS System FilePath in
@@ -59,6 +59,9 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name))
 
   IO.FS.writeFile (path / inventoryFileName) (toString (toJson inventory))
 
+  -- write PO file for translation
+  I18n.createPOTemplate
+
 open GameData
 
 def loadData (f : System.FilePath) (α : Type) [FromJson α] : IO α := do

server/GameServer/Structures.lean

@@ -0,0 +1,102 @@
+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
+  /-- The text with the variable names already inserted.
+
+  Note: This is in theory superfluous and will be completely replaced by `rawText`. We just left
+  it in for debugging for now. -/
+  text : String
+  /-- Flag whether the hint should be hidden initially. -/
+  hidden : Bool
+  /-- The text with the variables not inserted yet. -/
+  rawText : String
+  /-- The assignment of variable names in the `rawText` to the ones the player used. -/
+  varNames : Array <| Name × Name
+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/Tactic/LetIntros.lean

@@ -0,0 +1,65 @@
+import Lean.Elab.Binders
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Intro
+
+/-!
+# `let_intros` Tactic
+
+`let_intros` is a weaker form of `intros` aimed to only introduce `let` statements,
+but not for example `∀`-binders.
+-/
+
+namespace GameServer
+
+open Lean Meta Elab Parser Tactic
+
+/--
+Copied from `Lean.Meta.getIntrosSize`.
+-/
+private partial def getLetIntrosSize : Expr → Nat
+  -- | .forallE _ _ b _ => getLetIntrosSize b + 1
+  | .letE _ _ _ b _  => getLetIntrosSize b + 1
+  | .mdata _ b       => getLetIntrosSize b
+  | e                =>
+    if let some (_, _, _, b) := e.letFun? then
+      getLetIntrosSize b + 1
+    else
+      0
+
+/--
+Copied and from `Lean.MVarId.intros`.
+-/
+def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
+  let type ← mvarId.getType
+  let type ← instantiateMVars type
+  let n := getLetIntrosSize type
+  if n == 0 then
+    return (#[], mvarId)
+  else
+    -- `introNP` preserves the binder names
+    mvarId.introNP n
+
+/--
+`let_intros` introduces all `let` statements that are preceeding the proof. Concretely
+it does a subset of what `intros` does.
+
+If names are provided, it will introduce as many `let` statements as there are names.
+-/
+syntax (name := letIntros) "let_intros" : tactic
+-- (ppSpace colGt (ident <|> hole))*
+
+#check letIntros
+
+@[tactic letIntros] def evalLetIntros : Tactic := fun stx => do
+  match stx with
+  | `(tactic| let_intros) => liftMetaTactic fun mvarId => do
+    let (_, mvarId) ← mvarId.letIntros
+    return [mvarId]
+  -- | `(tactic| let_intros $ids*) => do
+  --   let fvars ← liftMetaTacticAux fun mvarId => do
+  --     let (fvars, mvarId) ← mvarId.introN ids.size (ids.map getNameOfIdent').toList
+  --     return (fvars, [mvarId])
+  --   withMainContext do
+  --     for stx in ids, fvar in fvars do
+  --       Term.addLocalVarInfo stx (mkFVar fvar)
+  | _ => throwUnsupportedSyntax

server/lake-manifest.json

@@ -4,10 +4,19 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hhu-adam/lean-i18n.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
+   "name": "i18n",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lakefile.lean

@@ -4,9 +4,11 @@ open Lake DSL
 package GameServer
 
 -- Using this assumes that each dependency has a tag of the form `v4.X.0`.
-def leanVersion : String := s!"v{Lean.versionString}"
+-- def leanVersion : String := s!"v{Lean.versionString}"
+def leanVersion := "v4.6.0" -- TODO
 
 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
+require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
 
 lean_lib GameServer
 

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.1

server/test/let_intros.lean

@@ -0,0 +1,17 @@
+import GameServer.Tactic.LetIntros
+
+set_option linter.unusedVariables false in
+
+example (f : Nat) :
+    let f := fun x ↦ x + 1
+    let g : Nat → Nat := fun y ↦ y
+    ∀ x : Nat, x ≤ f x := by
+  let_intros
+  /-
+  f✝ : Nat
+  f : Nat → Nat := fun x => x + 1
+  g : Nat → Nat := fun y => y
+  ⊢ ∀ (x : Nat), x ≤ f x
+  -/
+  intro x
+  exact Nat.le_succ x

tsconfig.json

@@ -11,6 +11,10 @@
     "downlevelIteration": true,
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
+    "lib": [
+      "ES2021.String",
+      "DOM"
+    ]
   },
   "exclude": ["server", "relay"]
 }