From bd7dc02e702766cb26d4f6845fcf1ee9ffdec8f4 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 13 Jul 2023 17:31:58 +0200 Subject: [PATCH] lots of stuff --- client/src/components/hints.tsx | 8 +- .../src/components/infoview/command_line.tsx | 47 ++++++++-- client/src/components/infoview/context.ts | 8 +- client/src/components/infoview/goals.tsx | 2 - client/src/components/infoview/info.tsx | 1 - client/src/components/infoview/infoview.css | 20 +++- client/src/components/infoview/main.tsx | 94 +++++++++++++------ client/src/components/landing_page.css | 2 +- client/src/components/level.css | 10 +- client/src/components/level.tsx | 8 +- server/GameServer/FileWorker.lean | 16 ++-- 11 files changed, 151 insertions(+), 65 deletions(-) diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index 90918f1..d08e494 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -3,7 +3,11 @@ import * as React from 'react'; import Markdown from './markdown'; export function Hint({hint} : {hint: GameHint}) { - return
{hint.text}
+ return
{hint.text}
+} + +export function AdditionalHint({hint} : {hint: GameHint}) { + return
{hint.text}
} export function Hints({hints, showHidden} : {hints: GameHint[], showHidden: boolean}) { @@ -13,6 +17,6 @@ export function Hints({hints, showHidden} : {hints: GameHint[], showHidden: bool return <> {openHints.map(hint => )} - {showHidden && hiddenHints.map(hint => )} + {showHidden && hiddenHints.map(hint => )} } diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx index aa963e9..dffd9a0 100644 --- a/client/src/components/infoview/command_line.tsx +++ b/client/src/components/infoview/command_line.tsx @@ -14,9 +14,9 @@ import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown. 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 { Diagnostic } from 'vscode-languageserver-types'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; - import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context' import { goalsToString } from './goals' import { InteractiveGoals } from './rpc_api' @@ -106,9 +106,13 @@ export function CommandLine() { Promise.all(msgCalls).then((diagnostics : [InteractiveDiagnostic[]]) => { let tmpProof : ProofStep[] = [] + let goalCount = 0 + steps.map((goals, i) => { // The first step has an empty command and therefore also no error messages - let messages = i ? diagnostics[i-1] : [] + // 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) => { @@ -117,6 +121,26 @@ export function CommandLine() { msg.message.append[0].text === "unsolved goals") }) + // If the number of goals reduce, show a message + if (goals.goals.length && goalCount > goals.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.goals.length + // TODO: Check what happens if the code gets into a bad state and no goals are available if (!goals) { tmpProof.push({ @@ -177,20 +201,18 @@ export function CommandLine() { 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 useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => { if (params.uri == editor.getModel().uri.toString()) { setProcessing(false) - if (!hasErrorsOrWarnings(params.diagnostics)) { + if (!hasErrors(params.diagnostics)) { setCommandLineInput("") editor.setPosition(editor.getModel().getFullModelRange().getEndPosition()) } } + loadAllGoals() // TODO: instead of loading all goals every time, we could only load the last one }, []); useEffect(() => { @@ -253,7 +275,6 @@ 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() } @@ -263,7 +284,6 @@ export function CommandLine() { 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
@@ -280,10 +300,17 @@ export function CommandLine() { /** Checks whether the diagnostics contain any errors or warnings to check whether the level has been completed.*/ -function hasErrorsOrWarnings(diags) { +export function hasErrors(diags: Diagnostic[]) { return diags.some( (d) => !d.message.startsWith("unsolved goals") && - (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning) + (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning + ) +} + +// TODO: Didn't manage to unify this with the one above +export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) { + return diags.some( + (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning ) } diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 4432ebc..719b022 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -20,7 +20,7 @@ export type ProofStep = { /** Story relevant messages */ hints: any // TODO: Add correct type /** Errors and warnings */ - errors: any // TODO: Add correct type + errors: InteractiveDiagnostic[] // TODO: Add correct type } /** The context storing the proof step-by-step for the command line mode */ @@ -37,12 +37,6 @@ export const ProofContext = React.createContext<{ setProof: () => {} // TODO: implement me }) - - - - - - // TODO: Is this still used? export const HintContext = React.createContext<{ showHiddenHints : boolean, diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index 7b5e9e5..7cd67c8 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -183,8 +183,6 @@ 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/info.tsx b/client/src/components/infoview/info.tsx index 1b87255..9085eeb 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -128,7 +128,6 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
{ goals && goals.goals.length > 0 && <> - }
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css index 9aa5fd2..8def2d8 100644 --- a/client/src/components/infoview/infoview.css +++ b/client/src/components/infoview/infoview.css @@ -4,8 +4,9 @@ padding: 5px 10px; border-radius: 3px 3px 3px 3px; } -.message.info { +.message.information, .message.info { /* color: #059; */ + color: #000; background-color: #DDF6FF; } .message.warning { @@ -139,3 +140,20 @@ .commandline-interface .content .tmp-pusher { flex: 1; } + +.undo-button { + border: 1px solid #bbb; + display: block; + padding-left: .3rem; + padding-right: .5rem; + float: right; + border-radius: .5rem; + background-color: #fff; + color: #888; +} + +.undo-button:hover { + border: 1px solid #888; + background-color: #ffdcc7; + cursor: pointer; +} diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index e1621c7..7a8fa23 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -14,6 +14,10 @@ import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '. import { WithRpcSessions } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; import { ServerVersion } from '../../../../node_modules/lean4-infoview/src/infoview/serverVersion'; +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faDeleteLeft, faHome, faArrowRight, faArrowLeft, faRotateLeft } from '@fortawesome/free-solid-svg-icons' +import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' + import { GameIdContext } from '../../app'; import { useAppDispatch, useAppSelector } from '../../hooks'; import { LevelInfo } from '../../state/api'; @@ -23,9 +27,10 @@ import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; -import { InputModeContext, ProofContext, ProofStateContext, ProofStep } from './context'; -import { CommandLine } from './command_line'; +import { InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStep } from './context'; +import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; +import { Button } from '../button'; /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is * always present, or the monaco editor cannot start. @@ -184,11 +189,14 @@ const goalFilter = { } /** The display of a single entered lean command */ -function Command({command} : {command: string}) { +function Command({command, deleteProof} : {command: string, deleteProof: any}) { // The first step will always have an empty command if (!command) {return <>} return
{command} +
+ +
} @@ -247,6 +255,8 @@ function Command({command} : {command: string}) { function GoalsTab({proofStep} : {proofStep: ProofStep}) { const [selectedGoal, setSelectedGoal] = React.useState(0) + if (!proofStep.goals.length) {return <>} + return
{proofStep.goals.map((goal, i) => ( @@ -265,6 +275,8 @@ function GoalsTab({proofStep} : {proofStep: ProofStep}) { export function CommandLineInterface(props: {world: string, level: number, data: LevelInfo}) { const ec = React.useContext(EditorContext) + const editor = React.useContext(MonacoEditorContext) + const gameId = React.useContext(GameIdContext) const {proof} = React.useContext(ProofContext) @@ -283,33 +295,47 @@ export function CommandLineInterface(props: {world: string, level: number, data: [] ); + /** Delete all proof lines starting from a given line. + * Note that the first line (i.e. deleting everything) is `1`! + */ + function deleteProof(line: number) { + return (ev) => { + editor.executeEdits("command-line", [{ + range: monaco.Selection.fromPositions( + {lineNumber: line, column: 1}, + editor.getModel().getFullModelRange().getEndPosition() + ), + text: '', + forceMoveMarkers: false + }]) + } + } + const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) - /* Set up updates to the global infoview state on editor events. */ + /* Set up updates to the global infoview seither you solved the level with warnings or your last command contains a syntax error Lean can't parseate 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); - }, - [] - ); + '$/lean/fileProgress', + new Map(), + async (params: LeanFileProgressParams) => (allProgress) => { + const newProgress = new Map(allProgress); + return newProgress.set(params.textDocument.uri, params.processing); + }, [] + ) const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); useClientNotificationEffect( - 'textDocument/didClose', - (params: DidCloseTextDocumentParams) => { - if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { - ec.events.changedCursorLocation.fire(undefined) - } - }, - [] - ); + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + if (ec.events.changedCursorLocation.current && + ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { + ec.events.changedCursorLocation.fire(undefined) + } + }, [] + ) const serverVersion = useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) @@ -331,7 +357,7 @@ export function CommandLineInterface(props: {world: string, level: number, data: {/* */}
{proof.map((step, i) => { - if (i == proof.length - 1 && step.errors.length) { + if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) { // if the last command contains an error, we should not display it // as it will be overwritten by the next entered command return
@@ -339,11 +365,25 @@ export function CommandLineInterface(props: {world: string, level: number, data:
} else { - return
- - - -
+ return <> +
+ + + +
+ {/* Show a message that there are no goals left */} + {!step.goals.length && ( +
+ {completed ? +

Level completed! 🎉

: +

+ no goals left
+ This probably means you solved the level with warnings +

+ } +
+ )} + } })}
diff --git a/client/src/components/landing_page.css b/client/src/components/landing_page.css index 325e556..a42f184 100644 --- a/client/src/components/landing_page.css +++ b/client/src/components/landing_page.css @@ -91,7 +91,7 @@ div.image { .info { margin-top: 5px; margin-bottom: 15px; - width: calc(100% - 20px); + /* width: calc(100% - 20px); */ border-collapse: collapse; } diff --git a/client/src/components/level.css b/client/src/components/level.css index 0c8f0b0..d62f284 100644 --- a/client/src/components/level.css +++ b/client/src/components/level.css @@ -215,11 +215,17 @@ td code { /* TODO: Create a nice style and move this to a better place */ .exercise .command { - background-color: rgb(167, 167, 167); + /* background-color: rgb(167, 167, 167); */ + border: 1px solid #bbb; + background-color: #eee; + padding: .5rem; + border-radius: .5rem; + margin-top: 1rem; } .exercise .step { - background-color: #ffeb91; + /* background-color: #e6f0f4; */ margin-top: 5px; margin-bottom: 5px; + /* border: 3px dotted rgb(88, 131, 24); */ } diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 1ea3583..dd8ea40 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -198,7 +198,7 @@ function PlayableLevel({worldId, levelId}) {
{level?.data?.introduction && -
+
{level?.data?.introduction}
} @@ -207,11 +207,11 @@ function PlayableLevel({worldId, levelId}) { })} {completed && <> -
+
Level completed! 🎉
{level?.data?.conclusion?.trim() && -
+
{level?.data?.conclusion}
} @@ -266,7 +266,7 @@ function Introduction({worldId}) {
-
+
{gameInfo.data?.worlds.nodes[worldId].introduction} diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 3ce7328..c02b23d 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -75,12 +75,12 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) 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` match levelParams.tactics.find? (fun t => t.name.toString == val) with - | none => addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!" + | none => addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!" | some tac => if tac.locked then - addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!" + addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!" else if tac.disabled then - addErrorMessage info s!"The tactic '{val}' is disabled in this level!" + addWarningMessage info s!"The tactic '{val}' is disabled in this level!" | .ident info rawVal val preresolved => let ns ← try resolveGlobalConst (mkIdent val) @@ -90,17 +90,17 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) | return () -- not a theroem -> ignore let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions match lemmasAndDefs.find? (fun l => l.name == n) with - | none => addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!" + | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!" | some lem => if lem.locked then - addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!" + addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!" else if lem.disabled then - addErrorMessage info s!"The lemma/definition '{n}' is disabled in this level!" -where addErrorMessage (info : SourceInfo) (s : MessageData) := + addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!" +where addWarningMessage (info : SourceInfo) (s : MessageData) := modify fun st => { st with messages := st.messages.add { fileName := inputCtx.fileName - severity := MessageSeverity.error + severity := MessageSeverity.warning pos := inputCtx.fileMap.toPosition (info.getPos?.getD 0) data := s }