fixes for v4.6.0-rc1

bump to v4.6.0-rc1
2024-02-14 16:22:10 +01:00 · 2024-02-14 15:04:32 +01:00
30 changed files with 299 additions and 602 deletions
@@ -1,8 +1,6 @@
 name: Build
 run-name: Build the project
-on:
-  workflow_dispatch:
-  push:
+on: [push]
 jobs:
  build:
    runs-on: ubuntu-latest
@@ -5,33 +5,15 @@ 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>{getHintText(hint)}</Markdown>
+    <Markdown>{hint.text}</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>{getHintText(hint)}</Markdown>
+    <Markdown>{hint.text}</Markdown>
  </div>
 }

@@ -49,7 +31,7 @@ export function Hints({hints, showHidden, step, selected, toggleSelection, lastL

 export function DeletedHint({hint} : {hint: GameHint}) {
  return <div className="message information deleted-hint">
-    <Markdown>{getHintText(hint)}</Markdown>
+    <Markdown>{hint.text}</Markdown>
  </div>
 }

@@ -91,14 +73,12 @@ 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
+  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected

  const activateHiddenHints = (ev) => {
    // If the last step (`k`) has errors, we want the hidden hints from the
    // second-to-last step to be affected
-    if (!(proof?.steps.length)) {return}
+    if (!(proof.steps.length)) {return}

    // state must not be mutated, therefore we need to clone the set
    let tmp = new Set(showHelp)
@@ -111,7 +91,7 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
    console.debug(`help: ${Array.from(tmp.values())}`)
  }

-  if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
+  if (hasHiddenHints(proof.steps[k]) && !showHelp.has(k)) {
    return <Button to="" onClick={activateHiddenHints}>
      Show more help!
    </Button>
@@ -4,7 +4,6 @@
 import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { InteractiveDiagnostic } from '@leanprover/infoview-api';
-import { Diagnostic } from 'vscode-languageserver-types'
 import { GameHint, InteractiveGoal, InteractiveTermGoal,InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { PreferencesState } from '../../state/preferences';

@@ -34,19 +33,9 @@ export const ProofContext = React.createContext<{
   */
  proof: ProofState,
  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: {steps: [], diagnostics: [], completed: false, completedWithWarnings: false},
-  setProof: () => {},
-  interimDiags: [],
-  setInterimDiags: () => {},
-  crashed: false,
-  setCrashed: () => {}
+  proof: {steps: [], diagnostics: [], completed: false},
+  setProof: () => {}
 })


@@ -268,7 +268,7 @@ interface GoalsProps {

 export function Goals({ goals, filter }: GoalsProps) {
    if (goals.goals.length === 0) {
-        return <></>
+        return <>No goals</>
    } else {
        return <>
          {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
@@ -345,29 +345,96 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
 })

 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: RpcSessionAtPos,
+    uri: string,
+    setProof: React.Dispatch<React.SetStateAction<ProofState>>) {
+  console.info('sending rpc request to load the proof state')

-rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then(
-  (proof : ProofState) => {
-    if (typeof proof !== 'undefined') {
+  rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then(
+    (proof : ProofState) => {
      console.info(`received a proof state!`)
      console.log(proof)
      setProof(proof)
-      setCrashed(false)
-    } else {
-      console.warn('received undefined proof state!')
-      setCrashed(true)
-      // setProof(undefined)
+
+
+
+
+      // let tmpProof : ProofStep[] = []
+
+      // let goalCount = 0
+
+      // steps.map((goals, i) => {
+      //   // The first step has an empty command and therefore also no error messages
+      //   // Usually there is a newline at the end of the editors content, so we need to
+      //   // display diagnostics from potentally two lines in the last step.
+      //   let messages = i ? (i == steps.length - 1 ? diagnostics.slice(i-1).flat() : diagnostics[i-1]) : []
+
+      //   // Filter out the 'unsolved goals' message
+      //   messages = messages.filter((msg) => {
+      //     return !("append" in msg.message &&
+      //       "text" in msg.message.append[0] &&
+      //       msg.message.append[0].text === "unsolved goals")
+      //   })
+
+      //   if (typeof goals == 'undefined') {
+      //     tmpProof.push({
+      //       command: i ? model.getLineContent(i) : '',
+      //       goals: [],
+      //       hints: [],
+      //       errors: messages
+      //     } as ProofStep)
+      //     console.debug('goals is undefined')
+      //     return
+      //   }
+
+      //   // If the number of goals reduce, show a message
+      //   if (goals.length && goalCount > goals.length) {
+      //     messages.unshift({
+      //       range: {
+      //         start: {
+      //           line: i-1,
+      //           character: 0,
+      //         },
+      //         end: {
+      //           line: i-1,
+      //           character: 0,
+      //         }},
+      //       severity: DiagnosticSeverity.Information,
+      //       message: {
+      //       text: 'intermediate goal solved 🎉'
+      //       }
+      //     })
+      //   }
+      //   goalCount = goals.length
+
+      //   // with no goals there will be no hints.
+      //   let hints : GameHint[] = goals.length ? goals[0].hints : []
+
+      //   console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+      //   console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+      //   console.debug(`Hints: (${i}): `, hints)
+      //   console.debug(`Errors: (${i}): `, messages)
+
+      //   tmpProof.push({
+      //     // the command of the line above. Note that `getLineContent` starts counting
+      //     // at `1` instead of `zero`. The first ProofStep will have an empty command.
+      //     command: i ? model.getLineContent(i) : '',
+      //     // TODO: store correct data
+      //     goals: goals.map(g => g.goal),
+      //     // only need the hints of the active goals in chat
+      //     hints: hints,
+      //     // errors and messages from the server
+      //     errors: messages
+      //   } as ProofStep)
+
+      // })
+      // // Save the proof to the context
+      // setProof(tmpProof)
+
+
+
    }
-  }
-).catch((error) => {
-  setCrashed(true)
-  console.warn(error)
-})
+  )
 }


@@ -293,9 +293,7 @@ function InfoAux(props: InfoProps) {
    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 proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos))
        const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos))
        const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
        const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound)
@@ -36,7 +36,6 @@ import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { store } from '../../state/store';
 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.
@@ -68,7 +67,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
  const dispatch = useAppDispatch()

  React.useEffect(() => {
-    if (proof?.completed) {
+    if (proof.completed) {
      dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))

      // On completion, add the names of all new items to the local storage
@@ -233,16 +232,12 @@ 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">
-      {proof?.completedWithWarnings &&
-        <div className="level-completed">
-          {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
-        </div>
-      }
+      {proof.completed && <div className="level-completed">Level completed! 🎉</div>}
      <Infos />
-      <Hints hints={proof?.steps[curPos?.line]?.goals[0]?.hints}
+      <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}/>
+        lastLevel={curPos?.line == proof.steps.length - 1}/>
      <MoreHelpButton selected={curPos?.line}/>
    </div>
  }
@@ -267,11 +262,11 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
    // If the last step has errors, we display the command in a different style
    // indicating that it will be removed on the next try.
    return <div className="failed-command">
-      <i>Failed command</i>: {proof?.steps[i].command}
+      <i>Failed command</i>: {proof.steps[i].command}
    </div>
  } else {
    return <div className="command">
-      <div className="command-text">{proof?.steps[i].command}</div>
+      <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>
@@ -399,7 +394,7 @@ 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, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext)
+  const { proof, setProof } = React.useContext(ProofContext)
  const { setTypewriterInput } = React.useContext(InputModeContext)
  const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)

@@ -415,7 +410,7 @@ export function TypewriterInterface({props}) {
  function deleteProof(line: number) {
    return (ev) => {
      let deletedChat: Array<GameHint> = []
-      proof?.steps.slice(line).map((step, 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
@@ -432,9 +427,9 @@ export function TypewriterInterface({props}) {
        forceMoveMarkers: false
      }])
      setSelectedStep(undefined)
-      setTypewriterInput(proof?.steps[line].command)
+      setTypewriterInput(proof.steps[line].command)
      // Reload proof on deleting
-      loadGoals(rpcSess, uri, setProof, setCrashed)
+      loadGoals(rpcSess, uri, setProof)
      ev.stopPropagation()
    }
  }
@@ -454,7 +449,7 @@ export function TypewriterInterface({props}) {

   // Scroll to the end of the proof if it is updated.
   React.useEffect(() => {
-    if (proof?.steps.length > 1) {
+    if (proof.steps.length > 1) {
      proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
    } else {
      proofPanelRef.current?.scrollTo(0,0)
@@ -476,7 +471,7 @@ export function TypewriterInterface({props}) {
  }, [selectedStep])

  // TODO: superfluous, can be replaced with `withErr` from above
-  let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
+  let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false


  useServerNotificationEffect("$/game/loading", (params : any) => {
@@ -496,33 +491,12 @@ export function TypewriterInterface({props}) {
      </div>
      <div className='proof' ref={proofPanelRef}>
        <ExerciseStatement data={props.data} />
-        {crashed ? <div>
-          <p className="crashed_message">Crashed! Go to editor mode and fix your proof!
-          Last server response:</p>
-          {interimDiags.map(diag => {
-            const severityClass = diag.severity ? {
-              [DiagnosticSeverity.Error]: 'error',
-              [DiagnosticSeverity.Warning]: 'warning',
-              [DiagnosticSeverity.Information]: 'information',
-              [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>
-            </div>
-          })}
-
-        </div> : proof?.steps.length ?
+        {proof.steps.length ?
          <>
-            {proof?.steps.map((step, i) => {
+            {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 (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.
@@ -543,18 +517,18 @@ export function TypewriterInterface({props}) {
                      hints={filteredHints} showHidden={showHelp.has(i)} step={i}
                      selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
                  }
-                  {/* <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) => {}}/> */}
+                  {/* <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
                  {!(isLastStepWithErrors(proof, i)) &&
-                    <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+                    <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
                  }
-                  {mobile && i == proof?.steps.length - 1 &&
+                  {mobile && i == proof.steps.length - 1 &&
                    <MoreHelpButton />
                  }

                  {/* Show a message that there are no goals left */}
                  {/* {!step.goals.length && (
                    <div className="message information">
-                      {proof?.completed ?
+                      {proof.completed ?
                        <p>Level completed! 🎉</p> :
                        <p>
                          <b>no goals left</b><br />
@@ -567,12 +541,12 @@ export function TypewriterInterface({props}) {
              }
            //}
            )}
-            {proof?.diagnostics.length > 0 &&
+            {proof.diagnostics.length > 0 &&
              <div key={`proof-step-remaining`} className="step step-remaining">
-                <Errors errors={proof?.diagnostics} typewriterMode={true} />
+                <Errors errors={proof.diagnostics} typewriterMode={true} />
              </div>
            }
-            {mobile && proof?.completed &&
+            {mobile && proof.completed &&
              <div className="button-row mobile">
                {props.level >= props.worldSize ?
                  <Button to={`/${gameId}`}>
@@ -585,14 +559,11 @@ export function TypewriterInterface({props}) {
                }
              </div>
            }
-          </> : <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`.
+          </> : <CircularProgress variant="determinate" value={loadingProgress} />
        }
      </div>
    </div>
-    <Typewriter disabled={disableInput || !proof?.steps.length}/>
+    <Typewriter disabled={disableInput || !proof.steps.length}/>
    </RpcContext.Provider>
  </div>
 }
@@ -49,8 +49,6 @@ export interface InteractiveTermGoal extends InteractiveGoalCore {
 export interface GameHint {
  text: string;
  hidden: boolean;
-  rawText: string;
-  varNames: string[][]; // in Lean: `Array (Name × Name)`
 }

 export interface InteractiveGoalWithHints {
@@ -87,7 +87,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
  const inputRef = useRef()

  // The context storing all information about the current proof
-  const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
+  const {proof, setProof} = React.useContext(ProofContext)

  // state to store the last batch of deleted messages
  const {setDeletedChat} = React.useContext(DeletedChatContext)
@@ -210,7 +210,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
      }])
      setTypewriterInput('')
      // Load proof after executing edits
-      loadGoals(rpcSess, uri, setProof, setCrashed)
+      loadGoals(rpcSess, uri, setProof)
    }

    editor.setPosition(pos)
@@ -224,13 +224,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {

  /* Load proof on start/switching to typewriter */
  useEffect(() => {
-    loadGoals(rpcSess, uri, setProof, setCrashed)
+    loadGoals(rpcSess, uri, setProof)
  }, [])

  /** If the last step has an error, add the command to the typewriter. */
  useEffect(() => {
    if (lastStepHasErrors(proof)) {
-      setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
+      setTypewriterInput(proof.steps[proof.steps.length - 1].command)
    }
  }, [proof])

@@ -238,11 +238,6 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
  useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
    if (params.uri == uri) {
      setProcessing(false)
-
-      console.log('Received lean diagnostics')
-      console.log(params.diagnostics)
-      setInterimDiags(params.diagnostics)
-
      //loadGoals(rpcSess, uri, setProof)

      // TODO: loadAllGoals()
@@ -259,13 +254,13 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
    // 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)
+  // 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]);
+  }, [uri]);


  useEffect(() => {
@@ -349,7 +344,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
  }

  // do not display if the proof is completed (with potential warnings still present)
-  return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
+  return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
      <form onSubmit={handleSubmit}>
        <div className="typewriter-input-wrapper">
          <div ref={inputRef} className="typewriter-input" />
@@ -381,10 +376,10 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
 export function getInteractiveDiagsAt (proof: ProofState, k : number) {
  if (k == 0) {
    return []
-  } else if (k >= proof?.steps.length-1) {
+  } 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)
+    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)
+    return proof.diagnostics.filter(msg => msg.range.start.line == k-1)
  }
 }
@@ -16,7 +16,6 @@ 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'
@@ -85,7 +84,7 @@ function ChatPanel({lastLevel, visible = true}) {
  const {selectedStep, setSelectedStep} = useContext(SelectionContext)
  const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))

-  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
+  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)

  function toggleSelection(line: number) {
    return (ev) => {
@@ -128,29 +127,29 @@ function ChatPanel({lastLevel, visible = true}) {
      {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, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
+          hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
      ))}
-      {proof?.steps.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}/>
+          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?.steps.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?.steps.length - 1}/>
+            selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/>
        }
      })} */}
      <DeletedHints hints={deletedChat}/>
-      {proof?.completed &&
+      {proof.completed &&
        <>
          <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
            Level completed! 🎉
@@ -164,7 +163,7 @@ function ChatPanel({lastLevel, visible = true}) {
      }
    </div>
    <div className="button-row">
-      {proof?.completed && (lastLevel ?
+      {proof.completed && (lastLevel ?
        <Button to={`/${gameId}`}>
          <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
        </Button> :
@@ -209,10 +208,6 @@ function PlayableLevel({impressum, setImpressum}) {

  // The state variables for the `ProofContext`
  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>>([])
@@ -339,15 +334,15 @@ function PlayableLevel({impressum, setImpressum}) {

  useEffect(() => {
    // Forget whether hidden hints are displayed for steps that don't exist yet
-    if (proof?.steps.length) {
+    if (proof.steps.length) {
      console.debug(Array.from(showHelp))
-      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof?.steps.length))))
+      setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length))))
    }
  }, [proof])

  // save showed help in store
  useEffect(() => {
-    if (proof?.steps.length) {
+    if (proof.steps.length) {
      console.debug(`showHelp:\n ${showHelp}`)
      dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
    }
@@ -385,7 +380,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, interimDiags, setInterimDiags, crashed: isCrashed, setCrashed: setIsCrashed}}>
+          <ProofContext.Provider value={{proof, setProof}}>
            <EditorContext.Provider value={editorConnection}>
              <MonacoEditorContext.Provider value={editor}>
                <LevelAppBar
@@ -432,7 +427,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, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
+          hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} />
      ))}
    </div>
    <div className={`button-row${mobile ? ' mobile' : ''}`}>
@@ -41,13 +41,6 @@
 .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 {
@@ -218,10 +211,3 @@
 .undo-button {
  color: #888;
 }
-
-.crashed_message {
-  color: #D8000C;
-  font-weight: bold;
-  padding-left: .5em;
-  padding-right: .5em;
-}
@@ -370,6 +370,6 @@ td code  {
 }

 /* DEBUG */
-/* .proof .step {
+.proof .step {
  border: 2px solid rgb(0, 123, 255);
-} */
+}
@@ -189,7 +189,8 @@ 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
@@ -202,28 +203,6 @@ 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:
@@ -86,36 +86,4 @@ 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
@@ -2,15 +2,6 @@

 Here are some issues experienced by users.

- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
-  ```
-  cd [THE PROJECT]
-  rm -rf .lake/
-  lake update -R
-  lake build
-  ```
-  If you experience problems related to Lean or lake, you should first try to reset it this way.
-
 # VSCode Dev-Container
 * If you don't get the pop-up, you might have disabled them, and you can reenable it by
  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
@@ -8753,9 +8753,9 @@
      }
    },
    "node_modules/ip": {
-      "version": "1.1.9",
-      "resolved": "https://registry.npmjs.org/ip/-/ip-1.1.9.tgz",
-      "integrity": "sha512-cyRxvOEpNHNtchU3Ln9KC/auJgup87llfQpQ+t5ghoC/UhL16SWzbueiCsdTnWmqAWl7LadfuwhlqmtOaqMHdQ=="
+      "version": "1.1.8",
+      "resolved": "https://registry.npmjs.org/ip/-/ip-1.1.8.tgz",
+      "integrity": "sha512-PuExPYUiu6qMBQb4l06ecm6T6ujzhmh+MeJcW9wa89PoAz5pvd4zPgN5WJV104mb6S2T1AwNIAaB70JNrLQWhg=="
    },
    "node_modules/ip-anonymize": {
      "version": "0.1.0",
@@ -14341,14 +14341,6 @@
        "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",
@@ -14910,12 +14902,9 @@
      }
    },
    "node_modules/type-fest": {
-      "version": "4.10.3",
-      "resolved": "https://registry.npmjs.org/type-fest/-/type-fest-4.10.3.tgz",
-      "integrity": "sha512-JLXyjizi072smKGGcZiAJDCNweT8J+AuRxmPZ1aG7TERg4ijx9REl8CNhbr36RV4qXqL1gO1FF9HL8OkVmmrsA==",
-      "dev": true,
-      "optional": true,
-      "peer": true,
+      "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"
      }
@@ -2,9 +2,6 @@ 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

@@ -35,17 +32,16 @@ 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 := title}
-  | .World => modifyCurWorld  fun world => pure {world with title := title}
+  | .Level => modifyCurLevel fun level => pure {level with title := t.getString}
+  | .World => modifyCurWorld  fun world => pure {world with title := t.getString}
  | .Game => modifyCurGame  fun game => pure {game with
      title := t.getString
-      tile := {game.tile with title := title}}
+      tile := {game.tile with title := t.getString}}

 /-- Define the introduction of the current game/world/level. -/
 elab "Introduction" t:str : command => do
-  let intro ← t.getString.translate
+  let intro := t.getString
  match ← getCurLayer with
  | .Level => modifyCurLevel fun level => pure {level with introduction := intro}
  | .World => modifyCurWorld  fun world => pure {world with introduction := intro}
@@ -53,7 +49,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.translate
+  let info:= t.getString
  match ← getCurLayer with
  | .Level =>
    logError "Can't use `Info` in a level!"
@@ -85,7 +81,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.translate
+  let conclusion := t.getString
  match ← getCurLayer with
  | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion}
  | .World => modifyCurWorld  fun world => pure {world with conclusion := conclusion}
@@ -98,13 +94,13 @@ elab "Prerequisites" t:str* : command => do

 /-- Short caption for the game (1 sentence) -/
 elab "CaptionShort" t:str : command => do
-  let caption ← t.getString.translate
+  let caption := t.getString
  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.translate
+  let caption := t.getString
  modifyCurGame fun game => pure {game with
    tile := {game.tile with long := caption}}

@@ -145,7 +141,6 @@ 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
@@ -170,7 +165,6 @@ 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
@@ -200,7 +194,6 @@ 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,
@@ -347,9 +340,6 @@ 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 := {} })
@@ -365,38 +355,36 @@ 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 := by {let_intros; $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
      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 := by {let_intros; $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $val)
      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 := by {let_intros; $(⟨tacticStx⟩)})
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
    elabCommand thmStatement

  let msgs := (← get).messages
+
  let mut hints := #[]
  let mut nonHintMsgs := #[]
  for msg in msgs.msgs do
@@ -408,41 +396,12 @@ 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 := text
-          rawText := rawText
+          text := ← instantiateMVars (mkMVar text)
          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
@@ -481,8 +440,6 @@ 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.
 -/
@@ -1,13 +1,7 @@
 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"
@@ -24,6 +18,22 @@ 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.
@@ -4,7 +4,6 @@ import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
 import GameServer.EnvExtensions
-import GameServer.Tactic.LetIntros

 namespace MyModule

@@ -123,7 +122,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 := GameServer.ALLOWED_KEYWORDS
+    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
    -- Ignore syntax elements that do not start with a letter or are listed above.
    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then
      -- Treat `simp?` and `simp!` like `simp`
@@ -170,20 +169,15 @@ 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!"The theorem/definition '{n}' is not available in this game!"
+        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
      | some thm =>
        -- Theorem is introduced at some point in the game.
        if thm.disabled then
          -- Theorem is disabled in this level.
          addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
        else if thm.locked then
-          match workerState.inventory.find? (· == n.toString) with
-          | 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 ()
+          -- Theorem is still locked.
+          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"

 where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
  -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
@@ -259,11 +253,8 @@ 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 {let_intros; $(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
          Elab.Command.elabCommandTopLevel cmdStx)
      cmdCtx cmdStateRef
  let postNew := (← tacticCacheNew.get).post
@@ -395,60 +386,60 @@ def publishProofState (m : DocumentMeta) (snap : Snapshot) (initParams : Lsp.Ini

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

@@ -4,6 +4,8 @@ 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. -/
@@ -83,6 +85,23 @@ 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)`?
@@ -1,54 +0,0 @@
-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⟩ ""
@@ -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 := GameServer.ALLOWED_KEYWORDS
+    let allowed := ["with", "fun", "at", "only", "by"]
    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}
@@ -1,7 +1,6 @@
 import GameServer.EnvExtensions
 import GameServer.InteractiveGoal
 import Std.Data.Array.Init.Basic
-import GameServer.Hints

 open Lean
 open Server
@@ -104,6 +103,14 @@ 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) (m : DocumentMeta) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
@@ -114,53 +121,19 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
      openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
        if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
        then
-
-          -- 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)
+          let lctx := (← goal.getDecl).lctx
+          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
-
-            -- 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 }
-
+            return some { text := text, hidden := hint.hidden }
          else return none
        else
          return none
    return hints

-def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
-    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)
@@ -188,20 +161,21 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
    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
-      }
-
+    out := out.push {
+      message := .text "intermediate goal solved! 🎉"
+      range := {
+        start := pos
+        «end» := pos
+        }
+      severity? := Lsp.DiagnosticSeverity.information
+    }
  return out

+def filterUnsolvedGoal (a : Array InteractiveDiagnostic) :
+    Array InteractiveDiagnostic :=
+  a.filter (fun d => match d.message with
+  | .append ⟨(.text x) :: _⟩ => x != "unsolved goals"
+  | _ => true)

 /-- Request that returns the goals at the end of each line of the tactic proof
 plus the diagnostics (i.e. warnings/errors) for the proof.
@@ -211,6 +185,9 @@ def getProofState (_ : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Proo
  let rc ← readThe RequestContext
  let text := doc.meta.text

+  -- BUG: trimming here is a problem, since the snap might already be evaluated before
+  -- the trimming and then the positions don't match anymore :((
+
  withWaitFindSnap
    doc
    -- TODO (Alex): I couldn't find a good condition to find the correct snap. So we are looking
@@ -1,8 +1,8 @@
 import GameServer.EnvExtensions
-import I18n

 open Lean Meta Elab Command

+
 /-! ## Copy images -/

 open IO.FS System FilePath in
@@ -59,9 +59,6 @@ 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
@@ -54,17 +54,8 @@ 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. -/
@@ -1,65 +0,0 @@
-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
@@ -4,19 +4,10 @@
 [{"url": "https://github.com/leanprover/std4.git",
   "type": "git",
   "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
   "name": "std",
   "manifestFile": "lake-manifest.json",
-   "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",
+   "inputRev": "v4.6.0-rc1",
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "GameServer",
@@ -4,11 +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 := "v4.6.0" -- TODO
+def leanVersion : String := s!"v{Lean.versionString}"

 require std from git "https://github.com/leanprover/std4.git" @ leanVersion
-require i18n from git "https://github.com/hhu-adam/lean-i18n.git" @ leanVersion
+
+-- require importGraph from git "https://github.com/leanprover-community/import-graph" @ leanVersion

 lean_lib GameServer

@@ -1 +1 @@
-leanprover/lean4:v4.6.1
+leanprover/lean4:v4.6.0-rc1
@@ -1,17 +0,0 @@
-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
@@ -11,10 +11,6 @@
    "downlevelIteration": true,
    "experimentalDecorators": true,
    "allowSyntheticDefaultImports": true,
-    "lib": [
-      "ES2021.String",
-      "DOM"
-    ]
  },
  "exclude": ["server", "relay"]
 }
Author	SHA1	Message	Date
Jon Eugster	ce739078b9	fixes for v4.6.0-rc1	2024-02-14 16:22:10 +01:00
Jon Eugster	a671bfa15f	bump to v4.6.0-rc1	2024-02-14 15:04:32 +01:00