From be039b5de3d0d6c0be9629aabd953b87ace4fcb2 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 12 Jul 2023 17:55:29 +0200 Subject: [PATCH] display all proof steps in command line modus --- .../src/components/infoview/command_line.tsx | 123 +++++++++- client/src/components/infoview/context.ts | 47 ++-- client/src/components/infoview/goals.tsx | 9 +- client/src/components/infoview/main.tsx | 227 +++++++++++++----- client/src/components/infoview/messages.tsx | 38 +++ client/src/components/level.css | 12 + client/src/components/level.tsx | 43 ++-- 7 files changed, 384 insertions(+), 115 deletions(-) diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx index 1c88a9b..aa963e9 100644 --- a/client/src/components/infoview/command_line.tsx +++ b/client/src/components/infoview/command_line.tsx @@ -13,8 +13,13 @@ import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json' import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json' import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json' import languageConfig from 'lean4/language-configuration.json'; +import { InteractiveDiagnostic, getInteractiveDiagnostics } from '@leanprover/infoview-api'; +import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +import { useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; -import { InputModeContext, MonacoEditorContext } from './context' +import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context' +import { goalsToString } from './goals' +import { InteractiveGoals } from './rpc_api' /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */ @@ -58,10 +63,14 @@ config.autoClosingPairs = config.autoClosingPairs.map( ) monaco.languages.setLanguageConfiguration('lean4cmd', config); +/** The input field */ export function CommandLine() { /** Reference to the hidden multi-line editor */ const editor = React.useContext(MonacoEditorContext) + const model = editor.getModel() + const uri = model.uri.toString() + const [oneLineEditor, setOneLineEditor] = useState(null) const [processing, setProcessing] = useState(false) @@ -69,26 +78,108 @@ export function CommandLine() { const inputRef = useRef() + // The context storing all information about the current proof + const {proof, setProof} = React.useContext(ProofContext) + + // TODO: does the position matter at all? + const rpcSess = useRpcSessionAtPos({uri: uri, line: 1, character: 1}) + + /** Load all goals an messages of the current proof (line-by-line) and save + * the retrieved information into context (`ProofContext`) + */ + const loadAllGoals = React.useCallback(() => { + let goalCalls = [] + let msgCalls = [] + + // For each line of code ask the server for the goals and the messages on this line + for (let i = 0; i < model.getLineCount(); i++) { + goalCalls.push( + rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp({line: i, character: 0, uri: uri})) + ) + msgCalls.push( + getInteractiveDiagnostics(rpcSess, {start: i, end: i+1}) + ) + } + + // Wait for all these requests to be processed before saving the results + Promise.all(goalCalls).then((steps : InteractiveGoals[]) => { + Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => { + let tmpProof : ProofStep[] = [] + + steps.map((goals, i) => { + // The first step has an empty command and therefore also no error messages + let messages = i ? 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") + }) + + // TODO: Check what happens if the code gets into a bad state and no goals are available + if (!goals) { + tmpProof.push({ + command: i ? model.getLineContent(i) : '', + goals: [], + hints: [], + errors: messages + } as ProofStep) + } else { + + console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '') + console.debug(`Goals: (${i}): `, goalsToString(goals)) // + console.debug(`Hints: (${i}): `, goals.goals[0]?.hints) + console.debug(`Errors: (${i}): `, messages) + + // with no goals there will be no hints + let hints = goals.goals.length ? goals.goals[0].hints : [] + + tmpProof.push({ + // the command of the line above. Note that `getLineContent` starts counting + // at `1` instead of `zero`. The first ProofStep will have an empty command. + command: i ? model.getLineContent(i) : '', + // TODO: store correct data + goals: goals.goals || [], + // only need the hints of the active goals in chat + hints: hints, + // errors and messages from the server + errors: messages + } as ProofStep) + } + }) + // Save the proof to the context + setProof(tmpProof) + }) + }) + }, [commandLineInput, editor]) + // Run the command const runCommand = React.useCallback(() => { - if (processing) return; + if (processing) {return} const pos = editor.getPosition() - editor.executeEdits("command-line", [{ - range: monaco.Selection.fromPositions( - pos, - editor.getModel().getFullModelRange().getEndPosition() - ), - text: commandLineInput + "\n", - forceMoveMarkers: false - }]); + if (commandLineInput) { + setProcessing(true) + editor.executeEdits("command-line", [{ + range: monaco.Selection.fromPositions( + pos, + editor.getModel().getFullModelRange().getEndPosition() + ), + text: commandLineInput + "\n", + forceMoveMarkers: false + }]) + } + editor.setPosition(pos) - setProcessing(true) }, [commandLineInput, editor]) useEffect(() => { if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) { oneLineEditor.setValue(commandLineInput) } + + // TODO: Is this the right place to load the goals once initially? + loadAllGoals() }, [commandLineInput]) // React when answer from the server comes back @@ -118,6 +209,7 @@ export function CommandLine() { enabled: false }, lineNumbers: 'off', + tabSize: 2, glyphMargin: false, folding: false, lineDecorationsWidth: 0, @@ -146,7 +238,7 @@ export function CommandLine() { // Ensure that our one-line editor can only have a single line const l = oneLineEditor.getModel().onDidChangeContent((e) => { const value = oneLineEditor.getValue() - setCommandLineInput(value) + setCommandLineInput(value.trim()) const newValue = value.replace(/[\n\r]/g, '') if (value != newValue) { oneLineEditor.setValue(newValue) @@ -161,14 +253,17 @@ export function CommandLine() { const l = oneLineEditor.onKeyUp((ev) => { if (ev.code === "Enter") { runCommand() + loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one } }) return () => { l.dispose() } }, [oneLineEditor, runCommand]) + /** Process the entered command */ const handleSubmit : React.FormEventHandler = (ev) => { ev.preventDefault() runCommand() + loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one } return
@@ -176,7 +271,9 @@ export function CommandLine() {
- +
} diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 9332a35..4432ebc 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -4,39 +4,54 @@ import * as React from 'react'; import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api'; -import { InteractiveGoals } from './rpc_api'; +import { InteractiveGoal, InteractiveGoals } from './rpc_api'; export const MonacoEditorContext = React.createContext( null as any) -// TODO: Is this still used? -export const HintContext = React.createContext<{ - showHiddenHints : boolean, - setShowHiddenHints: React.Dispatch> -}>({ - showHiddenHints: true, - setShowHiddenHints: () => {}, -}); - export type InfoStatus = 'updating' | 'error' | 'ready'; +/** One step of the proof */ export type ProofStep = { - // TODO: Add correct types + /** The command in this step */ command : string - goals: string - hints: string - errors: string + /** List of goals *after* this command */ + goals: InteractiveGoal[] // TODO: Add correct type + /** Story relevant messages */ + hints: any // TODO: Add correct type + /** Errors and warnings */ + errors: any // TODO: Add correct type } +/** The context storing the proof step-by-step for the command line mode */ export const ProofContext = React.createContext<{ - // The first entry will always have an empty/undefined command + /** The proof consists of multiple steps that are processed one after the other. + * In particular multi-line terms like `match`-statements will not be supported. + * + * Note that the first step will always have `null` as command + */ proof: ProofStep[], setProof: React.Dispatch>> }>({ proof: [], - setProof: () => {} + setProof: () => {} // TODO: implement me }) + + + + + + +// TODO: Is this still used? +export const HintContext = React.createContext<{ + showHiddenHints : boolean, + setShowHiddenHints: React.Dispatch> +}>({ + showHiddenHints: true, + setShowHiddenHints: () => {}, +}); + export interface ProofStateProps { // pos: DocumentPosition; status: InfoStatus; diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index 0a95825..7b5e9e5 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -2,8 +2,7 @@ * @fileOverview * * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx -*/ - + */ import * as React from 'react' import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api' import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; @@ -13,7 +12,6 @@ import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/ import { InputModeContext } from './context'; import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpc_api'; - /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ function isInaccessibleName(h: string): boolean { return h.indexOf('✝') >= 0; @@ -140,6 +138,9 @@ interface ProofDisplayProps { export const Goal = React.memo((props: GoalProps) => { const { goal, filter, showHints, commandLine } = props + // TODO: Apparently `goal` can be `undefined` + if (!goal) {return <>} + const filteredList = getFilteredHypotheses(goal.hyps, filter); const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; const locs = React.useContext(LocationsContext) @@ -182,6 +183,8 @@ export const Goal = React.memo((props: GoalProps) => { export const MainAssumptions = React.memo((props: GoalProps2) => { const { goals, filter } = props + + const goal = goals[0] const filteredList = getFilteredHypotheses(goal.hyps, filter); const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index a03a0c2..e1621c7 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -21,11 +21,77 @@ import { levelCompleted, selectCompleted } from '../../state/progress'; import Markdown from '../markdown'; import { Infos } from './infos'; -import { AllMessages, WithLspDiagnosticsContext } from './messages'; +import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; -import { InputModeContext, ProofStateContext } from './context'; +import { InputModeContext, ProofContext, ProofStateContext, ProofStep } from './context'; import { CommandLine } from './command_line'; +import { InteractiveDiagnostic } from '@leanprover/infoview/*'; +/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is + * always present, or the monaco editor cannot start. + */ +export function DualEditor({level, codeviewRef, levelId, worldId, commandLineMode}) { + const ec = React.useContext(EditorContext) +// const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext) + +// return
+// +//
{data?.descrFormat}
+//
+// {ec &&
} + +//
+// } + + return <> +
+ +
+
+ {ec && } + +} + +/* The part of the two editors that can needs the editor connection first */ +function DualEditorMain({worldId, levelId, level, commandLineMode}) { + const ec = React.useContext(EditorContext) + const gameId = React.useContext(GameIdContext) + + /* Set up updates to the global infoview state on editor events. */ + const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; + + const [allProgress, _1] = useServerNotificationState( + '$/lean/fileProgress', + new Map(), + async (params: LeanFileProgressParams) => (allProgress) => { + const newProgress = new Map(allProgress); + return newProgress.set(params.textDocument.uri, params.processing); + }, []) + const serverVersion = useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) + + return <> + + + + + + {/* We need the editor to always there and hidden because + the command line edits its content */} + { // TODO: Is there any possibility that the editor connection takes a while + // and we should show a circular progress here? + } + {commandLineMode ? + + : +
+ } + + + + + + +} // The mathematical formulation of the statement, supporting e.g. Latex // It takes three forms, depending on the precence of name and description: @@ -106,43 +172,101 @@ export function Main(props: {world: string, level: number}) {
} - return ( - - - - - - {ret} - - - - - - ); + return ret } -// `codeviewRef`: the codeViewRef. Used to edit the editor's content even if not visible -export function EditorInterface({data, codeviewRef, hidden, worldId, levelId, editorConnection}) { +const goalFilter = { + reverse: false, + showType: true, + showInstance: true, + showHiddenAssumption: true, + showLetValue: true +} - const { commandLineMode, setCommandLineMode } = React.useContext(InputModeContext) +/** The display of a single entered lean command */ +function Command({command} : {command: string}) { + // The first step will always have an empty command + if (!command) {return <>} + return
+ {command} +
+} - return
- -
{data?.descrFormat}
-
- {editorConnection &&
} +// const MessageView = React.memo(({uri, diag}: MessageViewProps) => { +// const ec = React.useContext(EditorContext); +// const fname = escapeHtml(basename(uri)); +// const {line, character} = diag.range.start; +// const loc: Location = { uri, range: diag.range }; +// const text = TaggedText_stripTags(diag.message); +// const severityClass = diag.severity ? { +// [DiagnosticSeverity.Error]: 'error', +// [DiagnosticSeverity.Warning]: 'warning', +// [DiagnosticSeverity.Information]: 'information', +// [DiagnosticSeverity.Hint]: 'hint', +// }[diag.severity] : ''; +// const title = `Line ${line+1}, Character ${character}`; + +// // Hide "unsolved goals" messages +// let message; +// if ("append" in diag.message && "text" in diag.message.append[0] && +// diag.message?.append[0].text === "unsolved goals") { +// message = diag.message.append[0] +// } else { +// message = diag.message +// } + +// const { commandLineMode } = React.useContext(InputModeContext) + +// return ( +// //
+// // {title} +// // +// // { e.preventDefault(); void ec.revealLocation(loc); }} +// // title="reveal file location"> +// // {e.preventDefault(); void ec.copyToComment(text)}} +// // title="copy message to comment"> +// // {e.preventDefault(); void ec.api.copyToClipboard(text)}} +// // title="copy message to clipboard"> +// // +// // +//
+// {!commandLineMode &&

{title}

} +// 
+//               
+//
+//
+// //
+// ) +// }, fastIsEqual) + +/** The tabs of goals that lean ahs after the command of this step has been processed */ +function GoalsTab({proofStep} : {proofStep: ProofStep}) { + const [selectedGoal, setSelectedGoal] = React.useState(0) + return
+
+ {proofStep.goals.map((goal, i) => ( +
{ setSelectedGoal(i) }}> + {i ? `Goal ${i+1}` : "Active Goal"} +
+ ))} +
+
+ +
} +/** The interface in command line mode */ export function CommandLineInterface(props: {world: string, level: number, data: LevelInfo}) { - const ec = React.useContext(EditorContext); + const ec = React.useContext(EditorContext) const gameId = React.useContext(GameIdContext) - - const proofStateContext = React.useContext(ProofStateContext) - - const [selectedGoal, setSelectedGoal] = React.useState(0) + const {proof} = React.useContext(ProofContext) const dispatch = useAppDispatch() @@ -187,8 +311,6 @@ export function CommandLineInterface(props: {world: string, level: number, data: [] ); - const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true } - const serverVersion = useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) const serverStoppedResult = useEventResult(ec.events.serverStopped); @@ -206,39 +328,28 @@ export function CommandLineInterface(props: {world: string, level: number, data: {/* {completed &&
Level completed! 🎉
} */}
- + {/* */}
-
- {proofStateContext.proofState.goals?.goals.map((goal, i) => -
{ setSelectedGoal(i) }}> - {i ? `Goal ${i+1}` : "Active Goal"} -
)} -
-
- {proofStateContext.proofState.goals?.goals?.length && - + {proof.map((step, i) => { + if (i == proof.length - 1 && step.errors.length) { + // if the last command contains an error, we should not display it + // as it will be overwritten by the next entered command + return
+ +
+ } + else { + return
+ + + +
} -
+ })}
} - return <> - {/* */} - - - - - - {ret} - - - - - - - - + return ret } diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx index 46550f7..f010fd1 100644 --- a/client/src/components/infoview/messages.tsx +++ b/client/src/components/infoview/messages.tsx @@ -17,6 +17,44 @@ interface MessageViewProps { diag: InteractiveDiagnostic; } +/** A list of messages (info/warning/error) that are produced after this command */ +function Error({error, commandLineMode} : {error : InteractiveDiagnostic, commandLineMode : boolean}) { + // The first step will always have an empty command + + const severityClass = error.severity ? { + [DiagnosticSeverity.Error]: 'error', + [DiagnosticSeverity.Warning]: 'warning', + [DiagnosticSeverity.Information]: 'information', + [DiagnosticSeverity.Hint]: 'hint', + }[error.severity] : ''; + + const {line, character} = error.range.start; + const title = `Line ${line+1}, Character ${character}`; + + // Hide "unsolved goals" messages + let message; + if ("append" in error.message && "text" in error.message.append[0] && + error.message?.append[0].text === "unsolved goals") { + message = error.message.append[0] + } else { + message = error.message + } + + return
+ {!commandLineMode &&

{title}

} + 
+      
+
+
+} + +/** A list of messages (info/warning/error) that are produced after this command */ +export function Errors ({errors, commandLineMode} : {errors : InteractiveDiagnostic[], commandLineMode : boolean}) { + return
+ {errors.map((err) => ())} +
+} + const MessageView = React.memo(({uri, diag}: MessageViewProps) => { const ec = React.useContext(EditorContext); const fname = escapeHtml(basename(uri)); diff --git a/client/src/components/level.css b/client/src/components/level.css index 7494e0b..0c8f0b0 100644 --- a/client/src/components/level.css +++ b/client/src/components/level.css @@ -211,3 +211,15 @@ td code { overflow-y: scroll; padding: 1em; } + +/* TODO: Create a nice style and move this to a better place */ + +.exercise .command { + background-color: rgb(167, 167, 167); +} + +.exercise .step { + background-color: #ffeb91; + margin-top: 5px; + margin-bottom: 5px; +} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 5bb09bc..1ea3583 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -6,7 +6,7 @@ import '@fontsource/roboto/300.css'; import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; -import { InfoviewApi } from '@leanprover/infoview' +import { InfoviewApi, defaultInfoviewConfig } from '@leanprover/infoview' import { Link, useParams } from 'react-router-dom'; import { Box, CircularProgress, FormControlLabel, FormGroup, Switch, IconButton } from '@mui/material'; import MuiDrawer from '@mui/material/Drawer'; @@ -28,7 +28,6 @@ import type { Location } from 'vscode-languageserver-protocol'; import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons' import { styled, useTheme, Theme, CSSObject } from '@mui/material/styles'; -import { DocumentPosition } from '../../../node_modules/lean4-infoview/src/infoview/util'; import { GameIdContext } from '../app'; import { ConnectionContext, useLeanClient } from '../connection'; @@ -38,7 +37,7 @@ import Markdown from './markdown'; import {Inventory, Documentation} from './inventory'; import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'; import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress'; -import { EditorInterface, CommandLineInterface } from './infoview/main' +import { DualEditor } from './infoview/main' import { Hints } from './hints'; import { HintContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStateProps, ProofStep } from './infoview/context'; @@ -62,6 +61,10 @@ function PlayableLevel({worldId, levelId}) { const chatPanelRef = useRef(null) const gameId = React.useContext(GameIdContext) + + // The state variables for the `ProofContext` + const [proof, setProof] = useState>([]) + const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) @@ -71,7 +74,6 @@ function PlayableLevel({worldId, levelId}) { const [showHiddenHints, setShowHiddenHints] = useState(false) - const [proof, setProof] = useState>([]) const [proofState, setProofState] = React.useState({ status: 'updating', @@ -79,7 +81,7 @@ function PlayableLevel({worldId, levelId}) { goals: undefined, termGoal: undefined, error: undefined, -}) + }) const theme = useTheme(); @@ -182,6 +184,9 @@ function PlayableLevel({worldId, levelId}) { const levelTitle = <>{levelId && `Level ${levelId}`}{level?.data?.title && `: ${level?.data?.title}`} + // TODO: with the new design, there is no difference between the introduction and + // a hint at the beginning of the proof... + return <>
@@ -197,9 +202,9 @@ function PlayableLevel({worldId, levelId}) { {level?.data?.introduction} } - {proofState.goals?.goals.length && - - } + {proof.map((step, i) => { + return + })} {completed && <>
@@ -216,10 +221,6 @@ function PlayableLevel({worldId, levelId}) { Next } } - - {/* { hints.map(hint =>
{hint.text}
) } */} - {/* TODO: Remove this debugging message: */} - {showHiddenHints &&

Hidden Hints are displayed

}
- -
- {/* We need the editor to always there and hidden because - the command line edits its content */} -
- + +
+ +
+