bump to v4.6.1

This reverts commit 381930e547.

client/src/components/hints.tsx

@@ -91,12 +91,14 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
   const {proof, setProof} = React.useContext(ProofContext)
   const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
 
-  let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected
+  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}
+    if (!(proof?.steps.length)) {return}
 
     // state must not be mutated, therefore we need to clone the set
     let tmp = new Set(showHelp)
@@ -109,7 +111,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>

client/src/components/infoview/context.ts

@@ -4,6 +4,7 @@
 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';
 
@@ -33,9 +34,19 @@ 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},
-  setProof: () => {}
+  proof: {steps: [], diagnostics: [], completed: false, completedWithWarnings: false},
+  setProof: () => {},
+  interimDiags: [],
+  setInterimDiags: () => {},
+  crashed: false,
+  setCrashed: () => {}
 })
 
 

client/src/components/infoview/goals.tsx

@@ -345,96 +345,29 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
 })
 
 export function loadGoals(
-    rpcSess: RpcSessionAtPos,
-    uri: string,
-    setProof: React.Dispatch<React.SetStateAction<ProofState>>) {
-  console.info('sending rpc request to load the proof state')
+  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) => {
+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)
-
-
-
-
-      // 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)
-
-
-
+      setCrashed(false)
+    } else {
+      console.warn('received undefined proof state!')
+      setCrashed(true)
+      // setProof(undefined)
     }
-  )
+  }
+).catch((error) => {
+  setCrashed(true)
+  console.warn(error)
+})
 }
 
 

client/src/components/infoview/info.tsx

@@ -293,7 +293,9 @@ 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))
+        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)

client/src/components/infoview/main.tsx

@@ -36,6 +36,7 @@ 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.
@@ -67,7 +68,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
@@ -232,16 +233,16 @@ 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 &&
+      {proof?.completedWithWarnings &&
         <div className="level-completed">
-          {proof.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
+          {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
         </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>
   }
@@ -266,11 +267,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>
@@ -398,7 +399,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 } = React.useContext(ProofContext)
+  const { proof, setProof, crashed, setCrashed, interimDiags } = React.useContext(ProofContext)
   const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)
 
@@ -414,7 +415,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
@@ -431,9 +432,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)
+      loadGoals(rpcSess, uri, setProof, setCrashed)
       ev.stopPropagation()
     }
   }
@@ -453,7 +454,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)
@@ -475,7 +476,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) => {
@@ -495,12 +496,33 @@ export function TypewriterInterface({props}) {
       </div>
       <div className='proof' ref={proofPanelRef}>
         <ExerciseStatement data={props.data} />
-        {proof.steps.length ?
+        {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.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.
@@ -521,18 +543,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 />
@@ -545,12 +567,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}`}>
@@ -563,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 disabled={disableInput || !proof.steps.length}/>
+    <Typewriter disabled={disableInput || !proof?.steps.length}/>
     </RpcContext.Provider>
   </div>
 }

client/src/components/infoview/typewriter.tsx

@@ -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} = 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)
@@ -210,7 +210,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
       }])
       setTypewriterInput('')
       // Load proof after executing edits
-      loadGoals(rpcSess, uri, setProof)
+      loadGoals(rpcSess, uri, setProof, setCrashed)
     }
 
     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)
+    loadGoals(rpcSess, uri, setProof, setCrashed)
   }, [])
 
   /** 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,6 +238,11 @@ 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()
@@ -254,13 +259,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(() => {
@@ -344,7 +349,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" />
@@ -376,10 +381,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)
   }
 }

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'
@@ -84,7 +85,7 @@ function ChatPanel({lastLevel, visible = true}) {
   const {selectedStep, setSelectedStep} = useContext(SelectionContext)
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
 
-  let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)
+  let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
 
   function toggleSelection(line: number) {
     return (ev) => {
@@ -127,29 +128,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}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
+          hint={{text: t, hidden: false, rawText: t, varNames: []}} 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! 🎉
@@ -163,7 +164,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> :
@@ -208,6 +209,10 @@ 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>>([])
@@ -334,15 +339,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)}))
     }
@@ -380,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
@@ -427,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' : ''}`}>

client/src/css/infoview.css

@@ -218,3 +218,10 @@
 .undo-button {
   color: #888;
 }
+
+.crashed_message {
+  color: #D8000C;
+  font-weight: bold;
+  padding-left: .5em;
+  padding-right: .5em;
+}

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

server/GameServer/Commands.lean

@@ -3,6 +3,7 @@ import GameServer.Inventory
 import GameServer.Options
 import GameServer.SaveData
 import GameServer.Hints
+import GameServer.Tactic.LetIntros
 import I18n
 
 open Lean Meta Elab Command
@@ -364,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

server/GameServer/FileWorker.lean

@@ -4,6 +4,7 @@ import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
 import GameServer.EnvExtensions
+import GameServer.Tactic.LetIntros
 
 namespace MyModule
 
@@ -258,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
@@ -424,7 +428,7 @@ private def nextCmdSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : Can
 
   set { s with snaps := s.snaps.push snap }
   cancelTk.check
-  publishProofState m snap initParams ctx.hOut
+  -- publishProofState m snap initParams ctx.hOut
   publishDiagnostics m snap.diagnostics.toArray ctx.hOut
   publishIleanInfoUpdate m ctx.hOut #[snap]
   return some snap

server/GameServer/RpcHandlers.lean

@@ -155,6 +155,12 @@ def findHints (goal : MVarId) (m : DocumentMeta) (initParams : Lsp.InitializePar
           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)
@@ -182,21 +188,20 @@ def completionDiagnostics (goalCount : Nat) (prevGoalCount : Nat) (completed : B
     else
       pure ()
   else if goalCount < prevGoalCount then
-    out := out.push {
-      message := .text "intermediate goal solved! 🎉"
-      range := {
-        start := pos
-        «end» := pos
-        }
-      severity? := Lsp.DiagnosticSeverity.information
-    }
+    -- 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
 
-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.
@@ -206,9 +211,6 @@ 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

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/lakefile.lean

@@ -4,7 +4,8 @@ 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

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.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

@@ -12,7 +12,8 @@
     "experimentalDecorators": true,
     "allowSyntheticDefaultImports": true,
     "lib": [
-      "ES2021.String"
+      "ES2021.String",
+      "DOM"
     ]
   },
   "exclude": ["server", "relay"]