From 47297e419450b8259d3880778548ceee57cfa8fe Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 11 Mar 2024 17:33:06 +0100 Subject: [PATCH] temporary fix to improve message on server crash --- client/src/components/infoview/context.ts | 15 ++- client/src/components/infoview/goals.tsx | 105 ++++-------------- client/src/components/infoview/info.tsx | 4 +- client/src/components/infoview/main.tsx | 33 +++++- client/src/components/infoview/typewriter.tsx | 23 ++-- client/src/components/level.tsx | 7 +- client/src/css/infoview.css | 7 ++ server/GameServer/FileWorker.lean | 2 +- server/GameServer/RpcHandlers.lean | 3 - 9 files changed, 92 insertions(+), 107 deletions(-) diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index a3d0399..a413191 100644 --- a/client/src/components/infoview/context.ts +++ b/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> + /** TODO: Workaround to capture a crash of the gameserver. */ + interimDiags: Diagnostic[], + setInterimDiags: React.Dispatch>> + /** TODO: Workaround to capture a crash of the gameserver. */ + crashed: Boolean, + setCrashed: React.Dispatch> }>({ - proof: {steps: [], diagnostics: [], completed: false}, - setProof: () => {} + proof: {steps: [], diagnostics: [], completed: false, completedWithWarnings: false}, + setProof: () => {}, + interimDiags: [], + setInterimDiags: () => {}, + crashed: false, + setCrashed: () => {} }) diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index bb56ad5..9a742aa 100644 --- a/client/src/components/infoview/goals.tsx +++ b/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>) { - 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: RpcSessionAtPos, + uri: string, + setProof: React.Dispatch>, + setCrashed: React.Dispatch>) { +console.info('sending rpc request to load the proof state') + +rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then( + (proof : ProofState) => { + if (typeof proof !== 'undefined') { console.info(`received a proof state!`) console.log(proof) setProof(proof) - - - - - // 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) +}) } diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 9a9f880..9189b8d 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -293,7 +293,9 @@ function InfoAux(props: InfoProps) { type InfoRequestResult = Omit const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise((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) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index decf9ec..691c1e0 100644 --- a/client/src/components/infoview/main.tsx +++ b/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. @@ -398,7 +399,7 @@ export function TypewriterInterface({props}) { const [loadingProgress, setLoadingProgress] = React.useState(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) @@ -433,7 +434,7 @@ export function TypewriterInterface({props}) { setSelectedStep(undefined) setTypewriterInput(proof?.steps[line].command) // Reload proof on deleting - loadGoals(rpcSess, uri, setProof) + loadGoals(rpcSess, uri, setProof, setCrashed) ev.stopPropagation() } } @@ -495,7 +496,28 @@ export function TypewriterInterface({props}) {
- {proof?.steps.length ? + {crashed ?
+

Crashed! Go to editor mode and fix your proof! + Last server response:

+ {interimDiags.map(diag => { + const severityClass = diag.severity ? { + [DiagnosticSeverity.Error]: 'error', + [DiagnosticSeverity.Warning]: 'warning', + [DiagnosticSeverity.Information]: 'information', + [DiagnosticSeverity.Hint]: 'hint', + }[diag.severity] : ''; + + return
+
+

Line {diag.range.start.line}, Character {diag.range.start.character}

+ 
+                  {diag.message}
+
+
+
+ })} + +
: proof?.steps.length ? <> {proof?.steps.map((step, i) => { let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) @@ -563,7 +585,10 @@ export function TypewriterInterface({props}) { }
} - : + : + // 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`. } diff --git a/client/src/components/infoview/typewriter.tsx b/client/src/components/infoview/typewriter.tsx index 2b50a69..4ed05cd 100644 --- a/client/src/components/infoview/typewriter.tsx +++ b/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,7 +224,7 @@ 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. */ @@ -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(() => { diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index ae3c9bd..633c659 100644 --- a/client/src/components/level.tsx +++ b/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' @@ -208,6 +209,10 @@ function PlayableLevel({impressum, setImpressum}) { // The state variables for the `ProofContext` const [proof, setProof] = useState({steps: [], diagnostics: [], completed: false, completedWithWarnings: false}) + const [interimDiags, setInterimDiags] = useState>([]) + const [isCrashed, setIsCrashed] = useState(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>([]) @@ -380,7 +385,7 @@ function PlayableLevel({impressum, setImpressum}) { - +