diff --git a/client/package.json b/client/package.json index f922949c..687cb4ca 100644 --- a/client/package.json +++ b/client/package.json @@ -11,7 +11,7 @@ "@fortawesome/free-regular-svg-icons": "^7.2.0", "@fortawesome/free-solid-svg-icons": "^7.2.0", "@fortawesome/react-fontawesome": "^3.2.0", - "@leanprover/infoview": "^0.4.3", + "@leanprover/infoview-api": "^0.13.0", "@mui/material": "^5.11.1", "@reduxjs/toolkit": "^1.9.1", "@tanstack/query-core": "^5.90.20", @@ -20,9 +20,10 @@ "i18next": "^25.8.18", "i18next-http-backend": "^3.0.2", "jotai": "^2.13.1", + "jotai-effect": "^2.2.3", "jotai-location": "^0.6.2", "jotai-tanstack-query": "^0.11.0", - "lean4monaco": "^1.1.9", + "lean4monaco": "^1.1.14", "monaco-editor-wrapper": "^5.3.1", "react": "^18.2.0", "react-country-flag": "^3.1.0", @@ -34,8 +35,7 @@ "react-split": "^2.0.14", "rehype-katex": "^7.0.1", "remark-gfm": "^4.0.1", - "remark-math": "^6.0.0", - "vscode-lean4": "github:leanprover/vscode-lean4#de0062c" + "remark-math": "^6.0.0" }, "devDependencies": { "@codingame/esbuild-import-meta-url-plugin": "^1.0.3", diff --git a/client/src/components/infoview/rpc_api.ts b/client/src/api/rpc_api.ts similarity index 58% rename from client/src/components/infoview/rpc_api.ts rename to client/src/api/rpc_api.ts index aebdd8be..52081799 100644 --- a/client/src/components/infoview/rpc_api.ts +++ b/client/src/api/rpc_api.ts @@ -1,32 +1,6 @@ -/** - * @fileOverview Defines the interface for the communication with the server. - * - * This file is based on `vscode-lean4/vscode-lean4/src/rpcApi.ts` - */ -import type { Range } from 'vscode-languageserver-protocol'; -import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api'; -import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*'; +import { CodeWithInfos, ContextInfo, FVarId, InteractiveDiagnostic, InteractiveGoalCore, MVarId, TermInfo } from '@leanprover/infoview-api' -export interface InteractiveHypothesisBundle { - /** The pretty names of the variables in the bundle. Anonymous names are rendered - * as `"[anonymous]"` whereas inaccessible ones have a `โœ` appended at the end. - * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */ - names: string[]; - fvarIds?: FVarId[]; - type: CodeWithInfos; - val?: CodeWithInfos; - isInstance?: boolean; - isType?: boolean; - isInserted?: boolean; - isRemoved?: boolean; - isAssumption?: boolean; -} -export interface InteractiveGoalCore { - hyps: InteractiveHypothesisBundle[]; - type: CodeWithInfos; - ctx?: ContextInfo; -} export interface InteractiveGoal extends InteractiveGoalCore { userName?: string; diff --git a/client/src/app.tsx b/client/src/app.tsx index f8086fdf..66ac7b12 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -9,6 +9,17 @@ import '@fontsource/roboto/700.css'; import './css/reset.css'; import './css/app.css'; +import './css/error_page.css'; +import "./css/infoview.css" +import "./css/landing_page.css" +import './css/layout.css'; +import './css/level.css'; +import "./css/popup.css" +import "./css/tab_bar.css" +import "./css/typewriter.css" +import "./css/welcome.css" +import "./css/world_tree.css" + import i18n from './i18n'; import { Popup } from './components/popup/popup'; import { leanMonacoAtom, leanMonacoOptionsAtom } from './store/editor-atoms'; @@ -17,7 +28,6 @@ import { preferencesAtom } from './store/preferences-atoms'; function App({ children }: { children?: React.ReactNode }) { - const infoviewRef = useRef(null) const [leanMonaco, setLeanMonaco] = useAtom(leanMonacoAtom) const [leanMonacoOptions] = useAtom(leanMonacoOptionsAtom) const [preferences] = useAtom(preferencesAtom) @@ -30,7 +40,6 @@ function App({ children }: { children?: React.ReactNode }) { useEffect(() => { const _leanMonaco = new LeanMonaco() setLeanMonaco(_leanMonaco) - _leanMonaco.setInfoviewElement(infoviewRef.current!) ;(async () => { await _leanMonaco.start(leanMonacoOptions) @@ -45,12 +54,12 @@ function App({ children }: { children?: React.ReactNode }) { }, [leanMonacoOptions, setLeanMonaco]) return ( -
+ <> {children} -
+ ) } diff --git a/client/src/components/chat/ChatPanel.tsx b/client/src/components/chat/ChatPanel.tsx new file mode 100644 index 00000000..492a40e2 --- /dev/null +++ b/client/src/components/chat/ChatPanel.tsx @@ -0,0 +1,134 @@ +import * as React from 'react' +import { useTranslation } from 'react-i18next' +import { useGameTranslation } from '../../utils/translation' +import { useEffect, useRef } from 'react' +import { useAtom } from 'jotai' +import { mobileAtom } from '../../store/preferences-atoms' +import { gameIdAtom, levelIdAtom } from '../../store/location-atoms' +import { levelInfoAtom } from '../../store/query-atoms' +import { deletedChatAtom, helpAtom, selectedStepAtom } from '../../store/chat-atoms' +import { proofAtom } from '../../store/editor-atoms' +import { DeletedHints, filterHints, Hint, Hints, MoreHelpButton } from '../hints' +import Markdown from 'react-markdown' +import { faArrowRight, faHome } from '@fortawesome/free-solid-svg-icons' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { Button } from '../button' + +/** Appears on the left of playable levels */ +export function ChatPanel({lastLevel, visible = true}: {lastLevel: boolean, visible: boolean}) { + let { t } = useTranslation() + const { t : gT } = useGameTranslation() + const chatRef = useRef(null) + const [mobile] = useAtom(mobileAtom) + const [gameId, navigateToGame] = useAtom(gameIdAtom) + const [levelId, navigateToLevel] = useAtom(levelIdAtom) + const [{ data: levelInfo }] = useAtom(levelInfoAtom) + const [help] = useAtom(helpAtom) + const [proof] = useAtom(proofAtom) + const [deletedChat] = useAtom(deletedChatAtom) + const [selectedStep, setSelectedStep] = useAtom(selectedStepAtom) + + let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0 + + function toggleSelection(line: number) { + return (ev: any) => { + console.debug('toggled selection') + if (selectedStep == line) { + setSelectedStep(undefined) + } else { + setSelectedStep(line) + } + } + } + + useEffect(() => { + // TODO: For some reason this is always called twice + console.debug('scroll chat') + if (!mobile) { + chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) + } + }, [proof, help]) + + // Scroll to element if selection changes + useEffect(() => { + if (typeof selectedStep !== 'undefined') { + Array.from(chatRef.current!.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { + elem.scrollIntoView({block: "center"}) + }) + } + }, [selectedStep]) + + // useEffect(() => { + // // // Scroll to top when loading a new level + // // // TODO: Thats the wrong behaviour probably + // // chatRef.current!.scrollTo(0,0) + // }, [gameId, worldId, levelId]) + + let introText: Array = gT(levelInfo?.introduction ?? "").split(/\n(\s*\n)+/) + + const focusRef = useRef() + useEffect(() => { + if (proof?.completed) { + focusRef.current?.focus() + } + }, [!!proof?.completed]) + + return
+
+ {introText?.filter(it => it.trim()).map(((it, i) => + // Show the level's intro text as hints, too + + ))} + {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 + } + })} + + {/* {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)) { + // TODO: Should not use index as key. + return + } + })} */} + + {proof?.completed && + <> +
+ {t("Level completed! ๐ŸŽ‰")} +
+ {levelInfo?.conclusion?.trim() && +
+ {gT(levelInfo?.conclusion ?? "")} +
+ } + + } +
+
+ {proof?.completed && (lastLevel ? + : + ) + } + +
+
+} + +//FIXME: implement +function lastStepHasErrors(x: any) {return false} + +//FIXME: implement +function isLastStepWithErrors(x: any, y: any) {return false} diff --git a/client/src/components/chat/IntroPanel.tsx b/client/src/components/chat/IntroPanel.tsx new file mode 100644 index 00000000..fada2984 --- /dev/null +++ b/client/src/components/chat/IntroPanel.tsx @@ -0,0 +1,52 @@ +import { useTranslation } from "react-i18next" +import { useGameTranslation } from "../../utils/translation" +import { useAtom } from "jotai" +import { gameIdAtom, levelIdAtom, worldIdAtom } from "../../store/location-atoms" +import { gameInfoAtom } from "../../store/query-atoms" +import { readWorldIntroAtom } from "../../store/progress-atoms" +import { mobileAtom } from "../../store/preferences-atoms" +import { useEffect, useRef } from "react" +import React from "react" +import { Hint } from "../hints" +import { FontAwesomeIcon } from "@fortawesome/react-fontawesome" +import { faArrowRight, faHome } from "@fortawesome/free-solid-svg-icons" +import { Button } from "../button" + +/** Appears on the left side of the intro of a world */ +export function IntroPanel() { + let { t } = useTranslation() + const { t : gT } = useGameTranslation() + const [gameId, navigateToGame] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [, navigateToLevel] = useAtom(levelIdAtom) + const [, readWorldIntro] = useAtom(readWorldIntroAtom) + + const [mobile] = useAtom(mobileAtom) + + let text: Array = gT(gameInfo?.worlds?.nodes[worldId ?? ""]?.introduction ?? "").split(/\n(\s*\n)+/) + + const focusRef = useRef() + useEffect(() => { + focusRef.current?.focus() + }, []) + + return
+
+ {text?.filter(t => t.trim()).map(((t, i) => + + ))} +
+
+ {gameInfo?.worldSize?.[worldId ?? ""] == 0 ? + : + + } +
+
+} diff --git a/client/src/components/editor/ExerciseStatement.tsx b/client/src/components/editor/ExerciseStatement.tsx new file mode 100644 index 00000000..bd32ea30 --- /dev/null +++ b/client/src/components/editor/ExerciseStatement.tsx @@ -0,0 +1,39 @@ +import React from "react" +import { useTranslation } from "react-i18next" +import { useGameTranslation } from "../../utils/translation" +import { useAtom } from "jotai" +import { gameIdAtom } from "../../store/location-atoms" +import { levelInfoAtom } from "../../store/query-atoms" +import { Markdown } from "../markdown" + +/** The mathematical formulation of the statement, supporting e.g. Latex + * It takes three forms, depending on the precence of name and description: + * - Theorem xyz: description + * - Theorem xyz + * - Exercises: description + * + * If `showLeanStatement` is true, it will additionally display the lean code. + */ +export function ExerciseStatement({ showLeanStatement = false }) { + const { t : gT } = useGameTranslation() + const { t } = useTranslation() + const [gameId] = useAtom(gameIdAtom) + const [{ data: levelInfo }] = useAtom(levelInfoAtom) + + if (!(levelInfo?.descrText || levelInfo?.descrFormat)) { return <> } + return <> +
+ {levelInfo?.descrText ? + + {(levelInfo?.displayName ? `**${t("Theorem")}** \`${levelInfo?.displayName}\`: ` : '') + t(levelInfo?.descrText, {ns: gameId})} + : levelInfo?.displayName && + + {(levelInfo?.displayName ? `**${t("Theorem")}** \`${levelInfo?.displayName}\`: ` : '') + gT(levelInfo?.descrText ?? "")} + + } + {levelInfo?.descrFormat && showLeanStatement && +

{levelInfo?.descrFormat}

+ } +
+ +} diff --git a/client/src/components/editor/GameEditor.tsx b/client/src/components/editor/GameEditor.tsx new file mode 100644 index 00000000..77888b0f --- /dev/null +++ b/client/src/components/editor/GameEditor.tsx @@ -0,0 +1,26 @@ +import { useAtom } from "jotai" +import { leanMonacoAtom, typewriterModeAtom } from "../../store/editor-atoms" +import React, { useEffect, useLayoutEffect, useRef } from "react" +import { ExerciseStatement } from "./ExerciseStatement" +import { Typewriter } from "./typewriter/Typewriter" + +/** + * Note: It is important that the `div` with `codeViewRef` is + * always present, or the monaco editor cannot start. + */ +export function GameEditor({ codeviewRef } : { codeviewRef: React.MutableRefObject }) { + const infoviewRef = useRef(null) + const [leanMonaco] = useAtom(leanMonacoAtom) + const [typewriterMode] = useAtom(typewriterModeAtom) + + useLayoutEffect(() => { + leanMonaco?.setInfoviewElement(infoviewRef.current!) + }) + + return <> + +
+
+ {typewriterMode && } + +} diff --git a/client/src/components/editor/messages/Error.tsx b/client/src/components/editor/messages/Error.tsx new file mode 100644 index 00000000..9fc67482 --- /dev/null +++ b/client/src/components/editor/messages/Error.tsx @@ -0,0 +1,47 @@ +// TODO: Should not use index as key. +import React from "react"; + +import { InteractiveDiagnostic, MsgEmbed, TaggedText, TaggedText_stripTags } from "@leanprover/infoview-api"; +import { DiagnosticSeverity } from "vscode-languageserver-types"; + +/** A list of messages (info/warning/error) that are produced after this command */ +export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) { + return
+ {errors.map((err, i) => ())} +
+} + +/** A list of messages (info/warning/error) that are produced after this command */ +function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : 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: TaggedText; + 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 + } + + const messageString = TaggedText_stripTags(message); + + return (messageString.trim().length > 0 && ( +
+ {!typewriterMode &&

{title}

} + 
+      
{messageString}

+
+
+ )) +} diff --git a/client/src/components/editor/types.ts b/client/src/components/editor/types.ts new file mode 100644 index 00000000..fd45bb1b --- /dev/null +++ b/client/src/components/editor/types.ts @@ -0,0 +1,6 @@ +export interface GameHint { + text: string; + hidden: boolean; + rawText: string; + varNames: string[][]; // in Lean: `Array (Name ร— Name)` +} diff --git a/client/src/components/editor/typewriter/Typewriter.tsx b/client/src/components/editor/typewriter/Typewriter.tsx new file mode 100644 index 00000000..ec570950 --- /dev/null +++ b/client/src/components/editor/typewriter/Typewriter.tsx @@ -0,0 +1,38 @@ +import React, { useRef } from "react"; +import { useAtom } from "jotai"; +import { gameInfoAtom } from "../../../store/query-atoms"; +import { gameIdAtom, worldIdAtom } from "../../../store/location-atoms"; +import path from "node:path"; +import { proofAtom } from "../../../store/editor-atoms"; +import { ExerciseStatement } from "../ExerciseStatement"; +import { ProofStep } from "./proof_step/ProofStep"; +import { TypewriterCommandLine } from "./TypewriterCommandline"; +import { LoadingIcon } from "../../utils"; +import { CircularProgress } from "@mui/material"; + +/** + * Der Typewriter bestehend aus Eingabezeile, Beweisschritten, Aufgabenstellung und Hintergrundbild + */ +export function Typewriter() { + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [gameId] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [proof] = useAtom(proofAtom) + + const proofPanelRef = useRef(null) + + let image = gameInfo?.worlds?.nodes[worldId!]?.image + + return
+
+ {image && } +
+
+ + {proof ? proof.steps.map((step, i) => ) + :
} +
+
+ +
+} diff --git a/client/src/components/editor/typewriter/TypewriterCommandline.tsx b/client/src/components/editor/typewriter/TypewriterCommandline.tsx new file mode 100644 index 00000000..ffd1ef23 --- /dev/null +++ b/client/src/components/editor/typewriter/TypewriterCommandline.tsx @@ -0,0 +1,165 @@ +import React, { FormEvent, useEffect, useRef, useState } from "react"; +import "../../../css/typewriter.css" +import { useTranslation } from "react-i18next"; +import { FontAwesomeIcon } from "@fortawesome/react-fontawesome"; +import { faWandMagicSparkles } from "@fortawesome/free-solid-svg-icons"; +import { useAtom } from "jotai"; +import * as monaco from 'monaco-editor' +import { typewriterContentAtom, codeAtom, modelAtom, appendCodeLineAtom } from "../../../store/editor-atoms"; +import { twMerge } from "tailwind-merge"; +import { deletedChatAtom } from "../../../store/chat-atoms"; +import { oneLineEditorAtom } from "./typewriter-atoms"; + +/** The input field */ +export function TypewriterCommandLine() { + let { t } = useTranslation() + const [isProcessing, setProcessing] = useState(false) + const [oneLineEditor, setOneLineEditor] = useAtom(oneLineEditorAtom) + const [model] = useAtom(modelAtom) + const [code] = useAtom(codeAtom) + const [, appendLine] = useAtom(appendCodeLineAtom) + const [, setDeletedChatAtom] = useAtom(deletedChatAtom) + const [typewriter, setTypewriter] = useAtom(typewriterContentAtom) + const oneLineEditorRef = useRef(null) + const inputRef = useRef(null) + + /** Handle keyboard events */ + function handleKeyDown(event: KeyboardEvent) { + if (event.key == "Enter" || event.key == "NumpadEnter") { + event.preventDefault() + handleSubmit() + } + } + + /** Wrapper to set the typewriter to processing. */ + function handleSubmit(ev?: FormEvent) { + ev?.preventDefault() + setProcessing(true) + try { handleSubmitAux(ev) } finally { setProcessing(false) } + } + + /** Process the entered command */ + async function handleSubmitAux(ev?: FormEvent) { + const content = typewriter.trimEnd() + if (content.length == 0) return + + // Add typewriter content to the editor + appendLine(content) + + // TODO: Desired logic is to only reset this after a new *error-free* command has been entered + setDeletedChatAtom([]) + + // Clear typewriter + oneLineEditor?.getModel()?.setValue('') + } + + // start the editor used in the typewriter command line + useEffect(() => { + // Guard: only create once + if (oneLineEditorRef.current) { + console.log("Editor already exists, skipping initialization") + return + } + + // Guard: wait for DOM element + if (!inputRef.current) { + console.log("inputRef.current is not ready yet") + return + } + + const editorConfig: monaco.editor.IStandaloneEditorConstructionOptions = { + value: typewriter, + language: "lean4", + quickSuggestions: false, + unicodeHighlight: { + ambiguousCharacters: false, + }, + automaticLayout: true, + minimap: { + enabled: false + }, + lineNumbers: 'off', + tabSize: 2, + wordWrap: 'on', + glyphMargin: false, + folding: false, + lineDecorationsWidth: 0, + lineNumbersMinChars: 0, + 'semanticHighlighting.enabled': true, + overviewRulerLanes: 0, + hideCursorInOverviewRuler: true, + padding: { + top: 0, + bottom: 0, + }, + scrollbar: { + verticalScrollbarSize: 3 + }, + scrollBeyondLastLine: false, + overviewRulerBorder: false, + theme: 'Visual Studio Light', + contextmenu: false + } + + console.log("Creating Monaco editor instance...") + const myEditor = monaco.editor.create(inputRef.current, editorConfig) + + const layoutInput = () => { + const lineHeight = myEditor.getOption(monaco.editor.EditorOption.lineHeight) + const height = Math.min(myEditor.getContentHeight(), lineHeight + 2, window.innerHeight / 3) + if (inputRef.current) { + inputRef.current.style.height = `${height}px` + myEditor.layout({ + width: inputRef.current.clientWidth, + height + }) + } + } + + myEditor.onDidContentSizeChange(layoutInput) + layoutInput() + + const changeDisposable = myEditor.getModel()?.onDidChangeContent(() => { + const value = myEditor.getValue() + setTypewriter(value) + + // Prevent newlines (single-line behavior) + const newValue = value.replace(/[\n\r]/g, '') + if (value !== newValue) { + myEditor.setValue(newValue) + } + }) + + oneLineEditorRef.current = myEditor + setOneLineEditor(myEditor) + console.log("Editor initialized successfully") + + return () => { + console.log("Cleaning up editor...") + changeDisposable?.dispose() + myEditor.dispose() + oneLineEditorRef.current = null + setOneLineEditor(null) + } + }, [setTypewriter, setOneLineEditor]) + + // Handle keyboard events (i.e. "Enter") + useEffect(() => { + document.addEventListener('keydown', handleKeyDown) + return () => { + document.removeEventListener('keydown', handleKeyDown) + } + }, [handleKeyDown]) + + // do not display if the proof is completed (with potential warnings still present) + return
+
+
+
+
+ + +
+} diff --git a/client/src/components/editor/typewriter/proof_step/Command.tsx b/client/src/components/editor/typewriter/proof_step/Command.tsx new file mode 100644 index 00000000..58646a70 --- /dev/null +++ b/client/src/components/editor/typewriter/proof_step/Command.tsx @@ -0,0 +1,48 @@ +import { useTranslation } from "react-i18next" +import { GameHint, ProofState } from "../../../../api/rpc_api" +import React from "react" +import { Button } from "@mui/material" +import { FontAwesomeIcon } from "@fortawesome/react-fontawesome" +import { faDeleteLeft } from "@fortawesome/free-solid-svg-icons" +import { filterHints } from "../../../hints" +import { deletedChatAtom, helpAtom } from "../../../../store/chat-atoms" +import { useAtom } from "jotai" +import { editor } from 'monaco-editor' +import { codeAtom, deleteCodeFromLineAtom, lastProofStepHasErrorsAtom } from "../../../../store/editor-atoms" + +//FIXME: implement +function isLastStepWithErrors(x: any, y: any) { + return false +} + +/** The display of a single entered lean command */ +export function Command({ proof, i }: { proof: ProofState, i: number }) { + let {t} = useTranslation() + const [lastProofStepHasErrors,] = useAtom(lastProofStepHasErrorsAtom) + const [, setDeletedChat] = useAtom(deletedChatAtom) + const [help, setHelp] = useAtom(helpAtom) + const [, setCode] = useAtom(codeAtom) + const [, deleteCodeFromLine] = useAtom(deleteCodeFromLineAtom) + + // The first step will always have an empty command + if (!proof.steps[i]?.command) { return <> } + + //if (isLastStepWithErrors(proof, i)) + if (lastProofStepHasErrors){ + // 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
+ {t("Failed command")}: {proof.steps[i].command} +
+ } else { + return
+
{proof.steps[i].command}
+ +
+ } +} diff --git a/client/src/components/editor/typewriter/proof_step/Goal.tsx b/client/src/components/editor/typewriter/proof_step/Goal.tsx new file mode 100644 index 00000000..c1e9fdbf --- /dev/null +++ b/client/src/components/editor/typewriter/proof_step/Goal.tsx @@ -0,0 +1,54 @@ +import { useAtom } from "jotai"; +import React from "react"; +import { typewriterModeAtom } from "../../../../store/editor-atoms"; +import { gameInfoAtom } from "../../../../store/query-atoms"; +import { mobileAtom } from "../../../../store/preferences-atoms"; +import { useTranslation } from "react-i18next"; +import { InteractiveGoal, ProofState } from "../../../../api/rpc_api"; +import { Hyp } from "./Hyp"; +import { InteractiveHypothesisBundle, TaggedText_stripTags } from "@leanprover/infoview-api"; + + +export function Goal({goal} : { goal: InteractiveGoal}) { + const { t} = useTranslation() + const [mobile] = useAtom(mobileAtom) + const [typewriterMode] = useAtom(typewriterModeAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + + function unbundleHyps (hyps: InteractiveHypothesisBundle[]) : InteractiveHypothesisBundle[] { + return hyps.flatMap(hyp => ( + gameInfo?.settings?.unbundleHyps ? hyp.names.map(name => {return {...hyp, names: [name]}}) : [hyp] + )) + } + + const objectHyps = unbundleHyps(goal.hyps.filter(hyp => !(hyp as any).isAssumption)) + const assumptionHyps = unbundleHyps(goal.hyps.filter(hyp => (hyp as any).isAssumption)) + + return ( + <> +
+ {objectHyps.length > 0 && +
{t("Objects")}:
+ {objectHyps.map((h, i) => )}
} + {assumptionHyps.length > 0 && +
{t("Assumptions")}:
+ {assumptionHyps.map((h, i) => { + h = {...h, val: undefined} // JE: never show value of assumptions (proof irrelevance) + return })}
} + +
+ { (!mobile && typewriterMode) && +
+ + + + +
+ } +
+ {(mobile || !typewriterMode) &&
{t("Goal")}:
} + {TaggedText_stripTags(goal.type)} +
+ + ) +} diff --git a/client/src/components/editor/typewriter/proof_step/GoalsTab.tsx b/client/src/components/editor/typewriter/proof_step/GoalsTab.tsx new file mode 100644 index 00000000..dd7b2a01 --- /dev/null +++ b/client/src/components/editor/typewriter/proof_step/GoalsTab.tsx @@ -0,0 +1,35 @@ +import { useTranslation } from "react-i18next" +import { InteractiveGoalsWithHints } from "../../../../api/rpc_api" +import { useAtom } from "jotai" +import { mobileAtom } from "../../../../store/preferences-atoms" +import React from "react" +import { Goal } from "./Goal" + +/** The tabs of goals that lean ahs after the command of this step has been processed */ +export function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { + let { t } = useTranslation() + const [mobile] = useAtom(mobileAtom) + const [selectedGoal, setSelectedGoal] = React.useState(0) + + if (proofStep.goals.length == 0) { + return <> + } + + const goal = proofStep.goals[selectedGoal]?.goal + + if (!goal) return + + return
+
+ {proofStep.goals.map((goal, i) => ( + // TODO: Should not use index as key. +
{ onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}> + {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")} +
+ ))} +
+
+ +
+
+} diff --git a/client/src/components/editor/typewriter/proof_step/Hyp.tsx b/client/src/components/editor/typewriter/proof_step/Hyp.tsx new file mode 100644 index 00000000..9b2ef967 --- /dev/null +++ b/client/src/components/editor/typewriter/proof_step/Hyp.tsx @@ -0,0 +1,38 @@ +import { InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from "@leanprover/infoview-api" +import React from "react" +import {useAppendTypewriterInput} from "../useAppendTypewriterInput" + +interface HypProps { + hyp: InteractiveHypothesisBundle + mvarId?: MVarId +} + +function isInaccessibleName(h: string): boolean { + return h.indexOf('โœ') >= 0; +} + +export function Hyp({ hyp: h, mvarId }: HypProps) { + const namecls: string = 'mr1 hyp-name ' + + (h.isInserted ? 'inserted-text ' : '') + + (h.isRemoved ? 'removed-text ' : '') + + const appendTypewriterInput = useAppendTypewriterInput() + + const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) => + { + appendTypewriterInput(ev.shiftKey, n, (h as any).isAssumption ?? false, (h as any).isAssumption ?? false) + ev.stopPropagation() + } } + >{n} + ) + return
+ {names} + :  + {TaggedText_stripTags(h.type)} + {h.val && ` := ${h.val}`} +
+} diff --git a/client/src/components/editor/typewriter/proof_step/ProofStep.tsx b/client/src/components/editor/typewriter/proof_step/ProofStep.tsx new file mode 100644 index 00000000..5d88050d --- /dev/null +++ b/client/src/components/editor/typewriter/proof_step/ProofStep.tsx @@ -0,0 +1,87 @@ +import React from "react"; +import { editor } from 'monaco-editor' +import { InteractiveGoalsWithHints } from "../../../../api/rpc_api"; +import { useAtom } from "jotai"; +import { helpAtom, selectedStepAtom } from "../../../../store/chat-atoms"; +import { twMerge } from "tailwind-merge"; +import { Command } from "./Command"; +import { proofAtom } from "../../../../store/editor-atoms"; +import { Errors } from "../../messages/Error"; +import { mobileAtom } from "../../../../store/preferences-atoms"; +import { gameInfoAtom, levelInfoAtom } from "../../../../store/query-atoms"; +import { useGameTranslation } from "../../../../utils/translation"; +import { filterHints, Hint, Hints } from "../../../hints"; +import { i } from "@tanstack/query-core/build/legacy/hydration-BlEVG2Lp"; +import { GoalsTabs } from "./GoalsTab"; +import { GameHint } from "../../types"; + +export function ProofStep({step, idx}: {step:InteractiveGoalsWithHints, idx: number}) { + const {t : gT} = useGameTranslation() + const [selectedStep, setSelectedStep] = useAtom(selectedStepAtom) + const [proof] = useAtom(proofAtom) + const [help] = useAtom(helpAtom) + const [mobile] = useAtom(mobileAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [{ data: levelInfo }] = useAtom(levelInfoAtom) + let introText: Array = gT(levelInfo?.introduction ?? "").split(/\n(\s*\n)+/) + + function toggleSelectStep(line: number) { + if (mobile) {return} + setSelectedStep(selectedStep != line ? line : undefined) + } + + // TODO: this should be an atom + let filteredHints: GameHint[] = proof ? filterHints(step.goals[0]?.hints, proof.steps[idx-1]?.goals[0]?.hints) : [] + + if (!proof) return + + return ( +
+ + + {mobile && idx == 0 && gameInfo?.introduction && + introText?.filter(it => it.trim()).map(((it, i) => + // Show the level's intro text as hints, too + + )) + } + {mobile && + + } + setDisableInput(n > 0) : (n) => {}} + /> +
+ ) +} + + +{/* + + + {!(isLastStepWithErrors(proof, i)) && + setDisableInput(n > 0) : (n) => {}}/> + } + {mobile && i == proof?.steps.length - 1 && + + } + + Show a message that there are no goals left + {!step.goals.length && ( +
+ {proof?.completed ? +

Level completed! ๐ŸŽ‰

: +

+ no goals left
+ This probably means you solved the level with warnings or Lean encountered a parsing error. +

+ } +
+ )} +
*/} diff --git a/client/src/components/editor/typewriter/typewriter-atoms.ts b/client/src/components/editor/typewriter/typewriter-atoms.ts new file mode 100644 index 00000000..a3edad1b --- /dev/null +++ b/client/src/components/editor/typewriter/typewriter-atoms.ts @@ -0,0 +1,5 @@ +import { atom } from "jotai"; +import { editor } from 'monaco-editor' + +/** The editor powering the typewriter (single line) input */ +export const oneLineEditorAtom = atom(null) diff --git a/client/src/components/editor/typewriter/useAppendTypewriterInput.ts b/client/src/components/editor/typewriter/useAppendTypewriterInput.ts new file mode 100644 index 00000000..f8686385 --- /dev/null +++ b/client/src/components/editor/typewriter/useAppendTypewriterInput.ts @@ -0,0 +1,86 @@ +import { useAtom } from "jotai" +import { typewriterAtom, typewriterContentAtom } from "../../../store/editor-atoms" +import { preferencesAtom } from "../../../store/preferences-atoms" + +// FIXME: implement +// Step 1: Copy over from infoview/context +// Step 2: Auto-import the used atoms +// Step 3: Copy SUFFIX and PREFIX OVERRIDES into function scpe +// Step 4: Reformulate parameters to adhere to old implementation +// Step 5: Relocate useAtoms into enclosing scope of function to stop infinite re-renders +export function useAppendTypewriterInput() { + const [typewriterContent] = useAtom(typewriterContentAtom) + const [, setTypewriter] = useAtom(typewriterAtom) + const [{ isSuggestionsMobileMode }] = useAtom(preferencesAtom) + + const SUFFIX_OVERRIDES: Record = { + "induction": "generalizing", + "left": ".left", + "rewrite": "โ†", + "right": ".right", + "rw": "โ†", + } + + const PREFIX_OVERRIDES: Record = { + "by_cases": "by_cases this :", + "contrapose": "contrapose!", + "have": "have :", + "obtain": "obtain โŸจโŸฉ :=", + "rewrite": "rw []", + "rw": "rw []", + "simp": "simp only []", + } + + return (shiftKey: boolean, suffix: string, isTheorem: boolean, isAssumption: boolean) => { + //return (shiftKey: boolean, suffix: string, isTheorem: boolean, isAssumption: boolean) => { + if (!isSuggestionsMobileMode && !shiftKey) { + return false + } + // Automagically detect and adjust punctuation for mobile keyboardless usage + let _typewriter = typewriterContent.trim() + + if (!typewriterContent.length) { + _typewriter = Object.hasOwn(PREFIX_OVERRIDES, suffix) ? PREFIX_OVERRIDES[suffix] : isTheorem ? `rw [${suffix}]` : suffix + setTypewriter(_typewriter + " ") + return true + } + + suffix = !isAssumption && Object.hasOwn(SUFFIX_OVERRIDES, suffix) ? SUFFIX_OVERRIDES[suffix] : suffix + + if (suffix === "โ„•") { + if (/ \d$/.test(_typewriter)) { + suffix = ((+_typewriter.slice(-2) + 1) % 10).toString() + _typewriter = _typewriter.slice(0, -2) + } else { + suffix = "0" + } + suffix = " " + suffix + } else if (suffix === "โˆˆ" && _typewriter.endsWith("โˆˆ")) { + suffix = " {} " + } else if (isAssumption && /^apply |^symm|^push_neg/.test(_typewriter)) { + suffix = " at " + suffix + } else if (suffix === "have") { + suffix = _typewriter === "have :" ? "=" : " :=" + } else if (/[\]}]$/.test(_typewriter)) { + if (isAssumption) { + suffix = " at " + suffix + } else { + const closing = _typewriter.slice(-1) + _typewriter = _typewriter.slice(0, -1) + if (suffix === "โ†") { + const imbalance = (_typewriter.match(/\(/)?.length ?? 0) - (_typewriter.match(/\)/)?.length ?? 0) + suffix = /[[,({]$/.test(_typewriter) ? "โ†" : /\([^)]*$/.test(_typewriter) ? ")" : " (" + } else { + if (!/[[,({]$/.test(_typewriter)) { + suffix = (isTheorem && !_typewriter.endsWith("โ†") && closing === "]" ? ", " : /^[แถœ.]/.test(suffix) ? "" : " ") + suffix + } + } + suffix = suffix + closing + } + } else if (!/^[แถœ.]/.test(suffix)) { + suffix = " " + suffix + } + setTypewriter(`${_typewriter}${suffix} `.trimStart()) + return true + } + } diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index 6ef2ad72..204f9450 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -1,7 +1,5 @@ -import { GameHint, InteractiveGoalsWithHints } from "./infoview/rpc_api"; import * as React from 'react'; import { Markdown } from './markdown'; -import { lastStepHasErrors } from "./infoview/goals"; import { Button } from "./button"; import { useGameTranslation } from "../utils/translation"; import { useTranslation } from "react-i18next"; @@ -9,6 +7,11 @@ import { useAtom } from "jotai"; import { gameIdAtom } from "../store/location-atoms"; import { deletedChatAtom, helpAtom } from "../store/chat-atoms"; import { proofAtom } from "../store/editor-atoms"; +import { GameHint, InteractiveGoalsWithHints } from './infoview/types'; + +//FIXME: implement +function lastStepHasErrors(x: any) {return false} + /** Plug-in the variable names in a hint. We do this client-side to prepare * for i18n in the future. i.e. one should be able translate the `rawText` diff --git a/client/src/components/infoview/infos.tsx b/client/src/components/infoview/infos.tsx deleted file mode 100644 index 54470092..00000000 --- a/client/src/components/infoview/infos.tsx +++ /dev/null @@ -1,135 +0,0 @@ -/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/infos.tsx */ - -import * as React from 'react'; -import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentContentChangeEvent } from 'vscode-languageserver-protocol'; - -import { EditorContext } from '../../../../node_modules/vscode-lean4/lean4-infoview/src/infoview/contexts'; -import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useEvent, useEventResult } from '../../../../node_modules/vscode-lean4/lean4-infoview/src/infoview/util'; -import { Info, InfoProps } from './info'; -import { useTranslation } from 'react-i18next'; - -/** Manages and displays pinned infos, as well as info for the current location. */ -export function Infos() { - let { t } = useTranslation() - const ec = React.useContext(EditorContext); - - // Update pins when the document changes. In particular, when edits are made - // earlier in the text such that a pin has to move up or down. - const [pinnedPositions, setPinnedPositions] = React.useState>>([]) - useClientNotificationEffect( - 'textDocument/didChange', - (params: DidChangeTextDocumentParams) => { - setPinnedPositions((prevPins) => { - if (prevPins.length === 0) return prevPins; - - let changed: boolean = false; - const newPins = prevPins.map(pin => { - if (pin.uri !== params.textDocument.uri) return pin; - // NOTE(WN): It's important to make a clone here, otherwise this - // actually mutates the pin. React state updates must be pure. - // See https://github.com/facebook/react/issues/12856 - const newPin: Keyed = { ...pin }; - for (const chg of params.contentChanges) { - if (!TextDocumentContentChangeEvent.isIncremental(chg)) { - changed = true; - return null; - } - if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.start)) continue; - // We can assume chg.range.start < pin - - // If the pinned position is replaced with new text, just delete the pin. - if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.end)) { - changed = true; - return null; - } - - const oldPin = { ...newPin }; - - // How many lines before the pin position were added by the change. - // Can be negative when more lines are removed than added. - let additionalLines = 0; - let lastLineLen = chg.range.start.character; - for (const c of chg.text) - if (c === '\n') { - additionalLines++; - lastLineLen = 0; - } else lastLineLen++; - - // Subtract lines that were already present - additionalLines -= (chg.range.end.line - chg.range.start.line) - newPin.line += additionalLines; - - if (oldPin.line < chg.range.end.line) { - // Should never execute by the <= check above. - throw new Error('unreachable code reached') - } else if (oldPin.line === chg.range.end.line) { - newPin.character = lastLineLen + (oldPin.character - chg.range.end.character); - } - } - if (!DocumentPosition.isEqual(newPin, pin)) changed = true; - - // NOTE(WN): We maintain the `key` when a pin is moved around to maintain - // its component identity and minimise flickering. - return newPin; - }); - - if (changed) return newPins.filter(p => p !== null) as Keyed[]; - return prevPins; - }); - }, - [] - ); - - // Remove pins for closed documents - useClientNotificationEffect( - 'textDocument/didClose', - (params: DidCloseTextDocumentParams) => { - setPinnedPositions(pinnedPositions => pinnedPositions.filter(p => p.uri !== params.textDocument.uri)); - }, - [] - ); - - const curPos: DocumentPosition | undefined = - useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) - - // Update pins on UI actions - const pinKey = React.useRef(0); - const isPinned = (pinnedPositions: DocumentPosition[], pos: DocumentPosition) => { - return pinnedPositions.some(p => DocumentPosition.isEqual(p, pos)); - } - const pin = React.useCallback((pos: DocumentPosition) => { - setPinnedPositions(pinnedPositions => { - if (isPinned(pinnedPositions, pos)) return pinnedPositions; - pinKey.current += 1; - return [ ...pinnedPositions, { ...pos, key: pinKey.current.toString() } ]; - }); - }, []); - const unpin = React.useCallback((pos: DocumentPosition) => { - setPinnedPositions(pinnedPositions => { - if (!isPinned(pinnedPositions, pos)) return pinnedPositions; - return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, pos)); - }); - }, []); - - // Toggle pin at current position when the editor requests it - useEvent(ec.events.requestedAction, act => { - if (act.kind !== 'togglePin') return - if (!curPos) return - setPinnedPositions(pinnedPositions => { - if (isPinned(pinnedPositions, curPos)) { - return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, curPos)); - } else { - pinKey.current += 1; - return [ ...pinnedPositions, { ...curPos, key: pinKey.current.toString() } ]; - } - }); - }, [curPos?.uri, curPos?.line, curPos?.character]); - - const infoProps: Keyed[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key })); - if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' }); - - return
- {infoProps.map (ps => )} - {!curPos &&

{t("Click somewhere in the Lean file to enable the infoview.")}

} -
; -} diff --git a/client/src/components/inventory/inventory_item.tsx b/client/src/components/inventory/inventory_item.tsx index 7c7f8c4c..31f29fbe 100644 --- a/client/src/components/inventory/inventory_item.tsx +++ b/client/src/components/inventory/inventory_item.tsx @@ -2,11 +2,13 @@ import { faBan, faCheck, faClipboard, faLock, faReply } from "@fortawesome/free- import { FontAwesomeIcon } from "@fortawesome/react-fontawesome" import React, { useState } from "react" import { useTranslation } from "react-i18next" -import { useAppendTypewriterInput } from "../infoview/context" import { InventoryTile } from "../../store/api" import { useAtom } from "jotai" import { selectedDocTileAtom } from "../../store/inventory-atoms" import { levelIdAtom } from "../../store/location-atoms" +import { typewriterAtom, typewriterContentAtom } from "../../store/editor-atoms" +import { preferencesAtom } from "../../store/preferences-atoms" +import { useAppendTypewriterInput } from "../editor/typewriter/useAppendTypewriterInput" export function InventoryItem({tile, isTheorem, recent=false, enableAll=false} : { tile: InventoryTile, @@ -17,6 +19,9 @@ export function InventoryItem({tile, isTheorem, recent=false, enableAll=false} : const { t } = useTranslation() const [, setDoc] = useAtom(selectedDocTileAtom) const [levelId] = useAtom(levelIdAtom) + const [typewriterContent,] = useAtom(typewriterContentAtom) + const [, setTypewriter] = useAtom(typewriterAtom) + const [{ isSuggestionsMobileMode }] = useAtom(preferencesAtom) const insertable: boolean = (levelId ?? 0) > 0 && (enableAll || !(tile.locked || tile.disabled)) @@ -31,6 +36,7 @@ export function InventoryItem({tile, isTheorem, recent=false, enableAll=false} : const [inserted, setInserted] = useState(false) const appendTypewriterInput = useAppendTypewriterInput() + const handleClick = (ev: any) => {setDoc(tile)} const insertItemName = (ev: any) => { diff --git a/client/src/components/inventory/inventory_panel.tsx b/client/src/components/inventory/inventory_panel.tsx index 2095362e..ed6c5e6d 100644 --- a/client/src/components/inventory/inventory_panel.tsx +++ b/client/src/components/inventory/inventory_panel.tsx @@ -36,16 +36,11 @@ export function InventoryPanel({levelInfo, visible = true} : { } }, [levelInfo]) - return
- {doc ? - - : -
- - - -
- } + return
+ + + + {doc && }
} diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index 1f1e7d7a..3a62c3cb 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -61,7 +61,7 @@ function Tile({tileWithName}: {tileWithName: GameTileWithName}) { if (preferences.useFlags && langOpt?.flag) { return } else { - return {lang} + return {lang} } })} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx deleted file mode 100644 index 5f201405..00000000 --- a/client/src/components/level.tsx +++ /dev/null @@ -1,626 +0,0 @@ -import * as React from 'react' -import { useEffect, useState, useRef } from 'react' -import Split from 'react-split' -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons' -import { CircularProgress } from '@mui/material' -import type { Location } from 'vscode-languageserver-protocol' -import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco' -import { setupMonacoClient } from 'lean4monaco/dist/monacoleanclient' -import type { EditorApi, InfoviewApi } from '@leanprover/infoview-api' -import { EditorContext } from '../../../node_modules/vscode-lean4/lean4-infoview/src/infoview/contexts' -import { EditorConnection, EditorEvents } from '../../../node_modules/vscode-lean4/lean4-infoview/src/infoview/editorConnection' -import { EventEmitter } from '../../../node_modules/vscode-lean4/lean4-infoview/src/infoview/event' -import { Button } from './button' -import { Markdown } from './markdown' -import { MonacoEditorContext } from './infoview/context' -import { DualEditor } from './infoview/main' -import { DeletedHints, Hint, Hints, MoreHelpButton, filterHints } from './hints' -import path from 'path'; - -import '@fontsource/roboto/300.css' -import '@fontsource/roboto/400.css' -import '@fontsource/roboto/500.css' -import '@fontsource/roboto/700.css' -import '../css/level.css' -import { LevelAppBar } from './app_bar' -import { isLastStepWithErrors, lastStepHasErrors } from './infoview/goals' -import { useTranslation } from 'react-i18next' -import { useGameTranslation } from '../utils/translation' -import { InventoryPanel } from './inventory/inventory_panel' -import { useAtom } from 'jotai' -import { codeAtom, leanMonacoAtom, lockEditorModeAtom, proofAtom, selectionsAtom, typewriterModeAtom } from '../store/editor-atoms' -import { gameIdAtom, levelIdAtom, worldIdAtom } from '../store/location-atoms' -import { gameInfoAtom, levelInfoAtom } from '../store/query-atoms' -import { deletedChatAtom, helpAtom, selectedStepAtom } from '../store/chat-atoms' -import { inventoryOverviewAtom } from '../store/inventory-atoms' -import { mobileAtom } from '../store/preferences-atoms' -import { readWorldIntroAtom } from '../store/progress-atoms' - -const reconfigureLeanMonacoClient = async (leanMonaco: LeanMonaco, options: LeanMonacoOptions) => { - const maybeLeanMonaco = leanMonaco as unknown as { - clientProvider?: { - getClients?: () => Array<{ getClientFolder?: () => unknown; stop?: () => Promise }> - stopClient?: (folder: unknown) => Promise - setupClient?: unknown - } - getWebSocketOptions?: (options: LeanMonacoOptions) => unknown - } - if (!maybeLeanMonaco.clientProvider || !maybeLeanMonaco.getWebSocketOptions) { - return - } - maybeLeanMonaco.clientProvider.setupClient = setupMonacoClient( - maybeLeanMonaco.getWebSocketOptions(options) as any - ) - const clients = maybeLeanMonaco.clientProvider.getClients?.() ?? [] - for (const client of clients) { - const folder = client?.getClientFolder?.() - if (folder && maybeLeanMonaco.clientProvider.stopClient) { - await maybeLeanMonaco.clientProvider.stopClient(folder) - } else { - await client?.stop?.() - } - } -} - -function Level() { - const { t: gT, i18n } = useGameTranslation() - const [gameId] = useAtom(gameIdAtom) - const [worldId] = useAtom(worldIdAtom) - const [levelId] = useAtom(levelIdAtom) - const [{ data: gameInfo }] = useAtom(gameInfoAtom) - - // Load the namespace of the game - i18n.loadNamespaces(gameId ?? "").catch(err => { - console.warn(`translations for ${gameId} do not exist.`) - }) - - // set the window title - useEffect(() => { - if (gameInfo?.title) { - window.document.title = gT(gameInfo.title) - } - }, [gameInfo?.title, i18n.language]) - - - if (levelId == 0) return - return -} - -function ChatPanel({lastLevel, visible = true}: {lastLevel: boolean, visible: boolean}) { - let { t } = useTranslation() - const { t : gT } = useGameTranslation() - const chatRef = useRef(null) - const [mobile] = useAtom(mobileAtom) - const [gameId, navigateToGame] = useAtom(gameIdAtom) - const [levelId, navigateToLevel] = useAtom(levelIdAtom) - const [{ data: levelInfo }] = useAtom(levelInfoAtom) - const [help] = useAtom(helpAtom) - const [proof] = useAtom(proofAtom) - const [deletedChat] = useAtom(deletedChatAtom) - const [selectedStep, setSelectedStep] = useAtom(selectedStepAtom) - - let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0 - - function toggleSelection(line: number) { - return (ev: any) => { - console.debug('toggled selection') - if (selectedStep == line) { - setSelectedStep(undefined) - } else { - setSelectedStep(line) - } - } - } - - useEffect(() => { - // TODO: For some reason this is always called twice - console.debug('scroll chat') - if (!mobile) { - chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) - } - }, [proof, help]) - - // Scroll to element if selection changes - useEffect(() => { - if (typeof selectedStep !== 'undefined') { - Array.from(chatRef.current!.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { - elem.scrollIntoView({block: "center"}) - }) - } - }, [selectedStep]) - - // useEffect(() => { - // // // Scroll to top when loading a new level - // // // TODO: Thats the wrong behaviour probably - // // chatRef.current!.scrollTo(0,0) - // }, [gameId, worldId, levelId]) - - let introText: Array = gT(levelInfo?.introduction ?? "").split(/\n(\s*\n)+/) - - const focusRef = useRef() - useEffect(() => { - if (proof?.completed) { - focusRef.current?.focus() - } - }, [!!proof?.completed]) - - return
-
- {introText?.filter(it => it.trim()).map(((it, i) => - // Show the level's intro text as hints, too - - ))} - {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 - } - })} - - {/* {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)) { - // TODO: Should not use index as key. - return - } - })} */} - - {proof?.completed && - <> -
- {t("Level completed! ๐ŸŽ‰")} -
- {levelInfo?.conclusion?.trim() && -
- {gT(levelInfo?.conclusion ?? "")} -
- } - - } -
-
- {proof?.completed && (lastLevel ? - : - ) - } - -
-
-} - - -function ExercisePanel({codeviewRef, infoviewRef, visible=true}: {codeviewRef: React.MutableRefObject, infoviewRef: React.MutableRefObject, visible?: boolean}) { - return
-
-
- -
-
-} - -function PlayableLevel() { - let { t } = useTranslation() - const { t : gT } = useGameTranslation() - const codeviewRef = useRef(null) - const infoviewRef = useRef(null) - const [leanMonaco] = useAtom(leanMonacoAtom) - const [gameId] = useAtom(gameIdAtom) - const [worldId] = useAtom(worldIdAtom) - const [levelId] = useAtom(levelIdAtom) - const [typewriterMode, setTypewriterMode] = useAtom(typewriterModeAtom) - const [mobile] = useAtom(mobileAtom) - const [code, setCode] = useAtom(codeAtom) - const [{ data: gameInfo }] = useAtom(gameInfoAtom) - const [{ data: levelInfo, isLoading: levelInfoIsLoading }] = useAtom(levelInfoAtom) - // Only for mobile layout - const [pageNumber, setPageNumber] = useState(0) - // set to true to prevent switching between typewriter and editor - const [lockEditorMode] = useAtom(lockEditorModeAtom) - const [, setTypewriterInput] = useState("") - const lastLevel = worldId && (levelId !== undefined) && levelId >= (gameInfo?.worldSize?.[worldId] ?? 0) - - // When clicking on an inventory item, the inventory is overlayed by the item's doc. - // If this state is set to a pair `(name, type)` then the according doc will be open. - // Set `inventoryDoc` to `null` to close the doc - const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string} | null>(null) - function closeInventoryDoc () {setInventoryDoc(null)} - - const [leanMonacoEditor, setLeanMonacoEditor] = useState(null) - const [editorConnection, setEditorConnection] = useState(null) - - // Start the editor - useEffect(() => { - if (leanMonaco) { - const leanMonacoEditor = new LeanMonacoEditor() - const uriStr = `file:///${worldId}/${levelId}.lean` - - ;(async () => { - await leanMonaco!.whenReady - console.debug('[demo]: starting editor') - await leanMonacoEditor.start(codeviewRef.current!, uriStr, code ?? "") - console.debug('[demo]: editor started') - setLeanMonacoEditor(leanMonacoEditor) - - // TODO: old stuff from here on - - const infoProvider = leanMonaco.infoProvider as { - editorApi: EditorApi - webviewPanel?: { api: InfoviewApi, visible: boolean } - sendConfig?: () => Promise - sendPosition?: () => Promise - } | undefined - - if (!infoProvider?.editorApi) { - console.warn('Lean infoview is not ready yet.') - return - } - - const editorEvents: EditorEvents = { - initialize: new EventEmitter(), - gotServerNotification: new EventEmitter(), - sentClientNotification: new EventEmitter(), - serverRestarted: new EventEmitter(), - serverStopped: new EventEmitter(), - changedCursorLocation: new EventEmitter(), - changedInfoviewConfig: new EventEmitter(), - runTestScript: new EventEmitter(), - requestedAction: new EventEmitter(), - } - - const infoviewApi: InfoviewApi = { - initialize: async l => editorEvents.initialize.fire(l), - gotServerNotification: async (method, params) => { - editorEvents.gotServerNotification.fire([method, params]) - }, - sentClientNotification: async (method, params) => { - editorEvents.sentClientNotification.fire([method, params]) - }, - serverRestarted: async r => editorEvents.serverRestarted.fire(r), - serverStopped: async serverStoppedReason => { - editorEvents.serverStopped.fire(serverStoppedReason) - }, - changedCursorLocation: async loc => editorEvents.changedCursorLocation.fire(loc), - changedInfoviewConfig: async conf => editorEvents.changedInfoviewConfig.fire(conf), - requestedAction: async action => editorEvents.requestedAction.fire(action), - runTestScript: async script => new Function(script)(), - getInfoviewHtml: async () => document.body.innerHTML, - } - - infoProvider.webviewPanel = { - api: infoviewApi, - visible: true, - } - - const editorConnection = new EditorConnection(infoProvider.editorApi, editorEvents) - setEditorConnection(editorConnection) - - const model = leanMonacoEditor.editor?.getModel() - const fireCursorLocation = () => { - const selection = leanMonacoEditor.editor?.getSelection() - const position = leanMonacoEditor.editor?.getPosition() - if (!selection || !model) { - if (!position || !model) { - return - } - const loc: Location = { - uri: model.uri.toString(), - range: { - start: { - line: position.lineNumber - 1, - character: position.column - 1, - }, - end: { - line: position.lineNumber - 1, - character: position.column - 1, - }, - }, - } - editorEvents.changedCursorLocation.fire(loc) - return - } - const loc: Location = { - uri: model.uri.toString(), - range: { - start: { - line: selection.startLineNumber - 1, - character: selection.startColumn - 1, - }, - end: { - line: selection.endLineNumber - 1, - character: selection.endColumn - 1, - }, - }, - } - editorEvents.changedCursorLocation.fire(loc) - } - - fireCursorLocation() - leanMonacoEditor.editor?.onDidChangeCursorSelection(() => { - fireCursorLocation() - }) - - await infoProvider.sendConfig?.() - await infoProvider.sendPosition?.() - - })() - - return () => { - leanMonacoEditor.dispose() - } - } - }, [leanMonaco, worldId, levelId]) - - // Persist editor text into progress whenever the model changes. - useEffect(() => { - const editor = leanMonacoEditor?.editor - if (!editor) { - return - } - - setCode(editor.getValue()) - const disposable = editor.onDidChangeModelContent(() => { - setCode(editor.getValue()) - }) - - return () => { - disposable.dispose() - } - }, [leanMonacoEditor?.editor, setCode]) - - // /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside - // * `TypewriterInterface`. - // */ - // const handleUndo = () => { - // const endPos = leanMonacoEditor?.editor.getModel().getFullModelRange().getEndPosition() - // let range - // console.log(endPos?.column) - // if (endPos?.column === 1) { - // range = monaco.Selection.fromPositions( - // new monaco.Position(endPos.lineNumber - 1, 1), - // endPos - // ) - // } else { - // range = monaco.Selection.fromPositions( - // new monaco.Position(endPos.lineNumber, 1), - // endPos - // ) - // } - // leanMonacoEditor?.editor.executeEdits("undo-button", [{ - // range, - // text: "", - // forceMoveMarkers: false - // }]); - // } - - // Select and highlight proof steps and corresponding hints - // TODO: with the new design, there is no difference between the introduction and - // a hint at the beginning of the proof... - const [selectedStep, setSelectedStep] = useState() - - - useEffect (() => { - // Lock editor mode - if (levelInfo?.template) { - const model = leanMonacoEditor?.editor?.getModel() - - if (model) { - let code = model.getLinesContent() - - // console.log(`insert. code: ${code}`) - // console.log(`insert. join: ${code.join('')}`) - // console.log(`insert. trim: ${code.join('').trim()}`) - // console.log(`insert. length: ${code.join('').trim().length}`) - // console.log(`insert. range: ${editor.getModel().getFullModelRange()}`) - - - // TODO: It does seem that the template is always indented by spaces. - // This is a hack, assuming there are exactly two. - if (!code.join("").trim().length) { - console.debug(`inserting template:\n${levelInfo?.template}`) - // TODO: This does not work! HERE - // Probably overwritten by a query to the server - leanMonacoEditor?.editor.executeEdits("template-writer", [{ - range: model.getFullModelRange(), - text: levelInfo?.template + `\n`, - forceMoveMarkers: true - }]) - } else { - console.debug(`not inserting template.`) - } - } - } else { - } - }, [levelInfo, levelId, worldId, gameId, leanMonacoEditor?.editor]) - - - useEffect(() => { - // TODO: That's a problem if the saved proof contains an error - // Reset command line input when loading a new level - setTypewriterInput("") - - }, [gameId, worldId, levelId]) - - useEffect(() => { - const editor = leanMonacoEditor?.editor; - const selection = editor?.getSelection(); - if (!typewriterMode && editor && selection) { - // Delete last input attempt from command line - editor.executeEdits("typewriter", [{ - range: selection, - text: "", - forceMoveMarkers: false - }]); - leanMonacoEditor?.editor.focus() - } - }, [typewriterMode]) - - // useEffect(() => { - // // Forget whether hidden hints are displayed for steps that don't exist yet - // if (proof?.steps.length) { - // console.debug(Array.from(help)) - // setHelp([...new Set(Array.from(help).filter(i => (i < proof?.steps.length)))]) - // } - // }, [proof]) - - // // save showed help in store - // useEffect(() => { - // if (proof?.steps.length) { - // console.debug(`showHelp:\n ${showHelp}`) - // setHelp(Array.from(showHelp)) - // } - // }, [showHelp]) - - // Effect when command line mode gets enabled - useEffect(() => { - const model = leanMonacoEditor?.editor?.getModel() - if (model&& (typewriterMode)) { - let code = model.getLinesContent().filter(line => line.trim()) - leanMonacoEditor?.editor.executeEdits("typewriter", [{ - range: model.getFullModelRange(), - text: code.length ? code.join('\n') + '\n' : '', - forceMoveMarkers: true - }]); - - // let endPos = editor.getModel().getFullModelRange().getEndPosition() - // if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") { - // editor.executeEdits("typewriter", [{ - // range: monaco.Selection.fromPositions(endPos, endPos), - // text: "\n", - // forceMoveMarkers: true - // }]); - // } - // let endPos = editor.getModel().getFullModelRange().getEndPosition() - // let currPos = editor.getPosition() - // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) { - // // This is not a position that would naturally occur from Typewriter, reset: - // editor.setSelection(monaco.Selection.fromPositions(endPos, endPos)) - // } - } - }, [leanMonacoEditor, leanMonacoEditor?.editor, typewriterMode, lockEditorMode]) - - return <> -
- - - - {mobile? - // TODO: This is copied from the `Split` component below... - <> -
- - -
- - : - - - - - - } - - - -} - -function IntroductionPanel() { - let { t } = useTranslation() - const { t : gT } = useGameTranslation() - const [gameId, navigateToGame] = useAtom(gameIdAtom) - const [worldId] = useAtom(worldIdAtom) - const [{ data: gameInfo }] = useAtom(gameInfoAtom) - const [, navigateToLevel] = useAtom(levelIdAtom) - const [, readWorldIntro] = useAtom(readWorldIntroAtom) - - const [mobile] = useAtom(mobileAtom) - - let text: Array = gT(gameInfo?.worlds?.nodes[worldId ?? ""]?.introduction ?? "").split(/\n(\s*\n)+/) - - const focusRef = useRef() - useEffect(() => { - focusRef.current?.focus() - }, []) - - return
-
- {text?.filter(t => t.trim()).map(((t, i) => - - ))} -
-
- {gameInfo?.worldSize?.[worldId ?? ""] == 0 ? - : - - } -
-
-} - -export default Level - -/** The site with the introduction text of a world */ -function Introduction() { - let { t } = useTranslation() - - const [gameId] = useAtom(gameIdAtom) - const [worldId] = useAtom(worldIdAtom) - - const [mobile] = useAtom(mobileAtom) - - const [{ data: inventory }] = useAtom(inventoryOverviewAtom) - - const [{ data: gameInfo, isLoading: isLoadingGameInfo }] = useAtom(gameInfoAtom) - - - let image: string = worldId ? gameInfo?.worlds?.nodes[worldId]?.image ?? "" : "" - - return <> - - {isLoadingGameInfo ? -
- : mobile ? - - : - - -
- {image && gameId && - - } - -
- - - } - - -} -function useGetGameInfoQuery(arg0: { game: string | undefined }) { - throw new Error('Function not implemented.') -} diff --git a/client/src/components/level/ExercisePanel.tsx b/client/src/components/level/ExercisePanel.tsx new file mode 100644 index 00000000..905d5865 --- /dev/null +++ b/client/src/components/level/ExercisePanel.tsx @@ -0,0 +1,9 @@ +import React from "react" +import { GameEditor } from "../editor/GameEditor" + +/** The center-piece of a playable level */ +export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject, visible?: boolean}) { + return
+ +
+} diff --git a/client/src/components/level/IntroLevel.tsx b/client/src/components/level/IntroLevel.tsx new file mode 100644 index 00000000..5744dbeb --- /dev/null +++ b/client/src/components/level/IntroLevel.tsx @@ -0,0 +1,50 @@ +import { useAtom } from "jotai" +import { useTranslation } from "react-i18next" +import { gameIdAtom, worldIdAtom } from "../../store/location-atoms" +import { mobileAtom } from "../../store/preferences-atoms" +import { inventoryOverviewAtom } from "../../store/inventory-atoms" +import { gameInfoAtom } from "../../store/query-atoms" +import { CircularProgress } from "@mui/material" +import { LevelAppBar } from "../app_bar" +import React from "react" +import { IntroPanel } from "../chat/IntroPanel" +import Split from "react-split" +import path from 'path' +import { InventoryPanel } from "../inventory/inventory_panel" + + +/** The site with the introduction text of a world */ +export function IntroLevel() { + let { t } = useTranslation() + + const [gameId] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + + const [mobile] = useAtom(mobileAtom) + + const [{ data: gameInfo, isLoading: isLoadingGameInfo }] = useAtom(gameInfoAtom) + + + let image: string = worldId ? gameInfo?.worlds?.nodes[worldId]?.image ?? "" : "" + + return <> + + {isLoadingGameInfo ? +
+ : mobile ? + + : + + +
+ {image && gameId && + + } + +
+ + + } + + +} diff --git a/client/src/components/level/Level.tsx b/client/src/components/level/Level.tsx new file mode 100644 index 00000000..0c9f1b10 --- /dev/null +++ b/client/src/components/level/Level.tsx @@ -0,0 +1,40 @@ +import * as React from 'react' +import { useEffect } from 'react' + +import '@fontsource/roboto/300.css' +import '@fontsource/roboto/400.css' +import '@fontsource/roboto/500.css' +import '@fontsource/roboto/700.css' +import '../../css/level.css' +import { useGameTranslation } from '../../utils/translation' +import { useAtom } from 'jotai' +import { gameIdAtom, levelIdAtom, worldIdAtom } from '../../store/location-atoms' +import { gameInfoAtom } from '../../store/query-atoms' +import { PlayableLevel } from './PlayableLevel' +import { IntroLevel } from './IntroLevel' + +export default function Level() { + const { t: gT, i18n } = useGameTranslation() + const [gameId] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [levelId] = useAtom(levelIdAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + + // Load the namespace of the game + i18n.loadNamespaces(gameId ?? "").catch(err => { + console.warn(`translations for ${gameId} do not exist.`) + }) + + // set the window title + useEffect(() => { + if (gameInfo?.title) { + window.document.title = gT(gameInfo.title) + } + }, [gameInfo?.title, i18n.language]) + + return ( + levelId == 0 ? + : + + ) +} diff --git a/client/src/components/level/PlayableLevel.tsx b/client/src/components/level/PlayableLevel.tsx new file mode 100644 index 00000000..96ba34cd --- /dev/null +++ b/client/src/components/level/PlayableLevel.tsx @@ -0,0 +1,254 @@ +import { useTranslation } from "react-i18next" +import { useGameTranslation } from "../../utils/translation" +import { useEffect, useRef, useState } from "react" +import { useAtom } from "jotai" +import { clientAtom, codeStorageAtom, rpcSessionAtom, editorAtom, leanMonacoAtom, lockEditorModeAtom, modelAtom, typewriterModeAtom, uriAtom } from "../../store/editor-atoms" +import { gameIdAtom, levelIdAtom, worldIdAtom } from "../../store/location-atoms" +import { mobileAtom } from "../../store/preferences-atoms" +import { gameInfoAtom, levelInfoAtom } from "../../store/query-atoms" +import { LeanMonacoEditor, RpcSessionAtPos } from "lean4monaco" +import { RpcConnectParams } from "@leanprover/infoview-api" +import { CircularProgress } from "@mui/material" +import { LevelAppBar } from "../app_bar" +import React from "react" +import { ExercisePanel } from "./ExercisePanel" +import { InventoryPanel } from "../inventory/inventory_panel" +import { ChatPanel } from "../chat/ChatPanel" +import Split from 'react-split' + +export function PlayableLevel() { + let { t } = useTranslation() + const { t : gT } = useGameTranslation() + const codeviewRef = useRef(null) + const [leanMonaco] = useAtom(leanMonacoAtom) + const [gameId] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [levelId] = useAtom(levelIdAtom) + const [typewriterMode, setTypewriterMode] = useAtom(typewriterModeAtom) + const [mobile] = useAtom(mobileAtom) + const [code, setCode] = useAtom(codeStorageAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [{ data: levelInfo, isLoading: levelInfoIsLoading }] = useAtom(levelInfoAtom) + // Only for mobile layout + const [pageNumber, setPageNumber] = useState(0) + // set to true to prevent switching between typewriter and editor + const [lockEditorMode] = useAtom(lockEditorModeAtom) + const [, setTypewriterInput] = useState("") + const lastLevel = worldId && (levelId !== undefined) && levelId >= (gameInfo?.worldSize?.[worldId] ?? 0) + + // When clicking on an inventory item, the inventory is overlayed by the item's doc. + // If this state is set to a pair `(name, type)` then the according doc will be open. + // Set `inventoryDoc` to `null` to close the doc + const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string} | null>(null) + function closeInventoryDoc () {setInventoryDoc(null)} + + const [editor, setEditor] = useAtom(editorAtom) + const [model] = useAtom(modelAtom) + const [client, setClient] = useAtom(clientAtom) + const [uri] = useAtom(uriAtom) + const [rpcSess, setRpcSess] = useAtom(rpcSessionAtom) + + // Start the editor, following lean4monaco demo + useEffect(() => { + if (leanMonaco) { + const leanMonacoEditor = new LeanMonacoEditor() + const uriStr = `file:///${worldId}/${levelId}.lean` + + ;(async () => { + await leanMonaco!.whenReady + console.debug('[lean4game]: starting editor') + await leanMonacoEditor.start(codeviewRef.current!, uriStr, code ?? "") + console.debug('[lean4game]: editor started') + setEditor(leanMonacoEditor.editor) + })() + + return () => { + leanMonacoEditor.dispose() + } + } + }, [leanMonaco, worldId, levelId]) + + // Persist editor text into progress whenever the model changes. + useEffect(() => { + if (!editor) return + + setCode(editor.getValue()) + const disposable = editor.onDidChangeModelContent(() => { + setCode(editor.getValue()) + }) + + return () => { + disposable.dispose() + } + }, [editor, setCode]) + + // wait until the client exists + // TODO: it didn't work to define an atom `get(editorAtom)?.clientProvider?.getClients()?.[0]` + // is there a way to tell atoms to fully reevaluate until they get a non-null result? + useEffect(() => { + const updateClient = () => { + const clients = leanMonaco?.clientProvider?.getClients() + const firstClient = clients?.[0] ?? null + if (firstClient) { + setClient(firstClient) + return true + } + return false + } + updateClient() + const interval = setInterval(() => { + // try to get `client` until successful + if (updateClient()) { + clearInterval(interval) + } + }, 500) + return () => clearInterval(interval) + }, [leanMonaco?.clientProvider]) + + // Start RPC session + useEffect(() => { + function updateRpcSession() { + if (rpcSess) return true + if (!client || !uri) return false + console.debug('rpc session connecting...') + client.sendRequest('$/lean/rpc/connect', {uri: uri.toString()} as RpcConnectParams).then(result => { + const sessionId = result.sessionId + console.debug(`rpc session id: ${sessionId}`) + const _rpcSess = new RpcSessionAtPos(client, sessionId, uri.toString()) + setRpcSess(_rpcSess) + }).catch((err) => { + console.debug("rpc connect failed: ", err) + }) + } + updateRpcSession() + const interval = setInterval(() => { + // try to get `rpcSess` until successful + if (updateRpcSession()) { + clearInterval(interval) + } + }, 500) + return () => clearInterval(interval) + }, [client, uri, rpcSess]) + + // Select and highlight proof steps and corresponding hints + // TODO: with the new design, there is no difference between the introduction and + // a hint at the beginning of the proof... + const [selectedStep, setSelectedStep] = useState() + + useEffect (() => { + // Lock editor mode + if (levelInfo?.template) { + + if (model) { + let code = model.getLinesContent() + + // TODO: It does seem that the template is always indented by spaces. + // This is a hack, assuming there are exactly two. + if (!code.join("").trim().length) { + console.debug(`inserting template:\n${levelInfo?.template}`) + // TODO: This does not work! HERE + // Probably overwritten by a query to the server + // DOC: REMOVED editor here + editor?.executeEdits("template-writer", [{ + range: model.getFullModelRange(), + text: levelInfo?.template + `\n`, + forceMoveMarkers: true + }]) + } else { + console.debug(`not inserting template.`) + } + } + } else { + } + }, [levelInfo, levelId, worldId, gameId, editor]) + + + useEffect(() => { + // TODO: That's a problem if the saved proof contains an error + // Reset command line input when loading a new level + setTypewriterInput("") + + }, [gameId, worldId, levelId]) + + useEffect(() => { + const selection = editor?.getSelection(); + if (!typewriterMode && editor && selection) { + // Delete last input attempt from command line + editor.executeEdits("typewriter", [{ + range: selection, + text: "", + forceMoveMarkers: false + }]); + editor?.focus() // leanMonacoEditor?.editor.focus() + } + }, [typewriterMode]) + + // useEffect(() => { + // // Forget whether hidden hints are displayed for steps that don't exist yet + // if (proof?.steps.length) { + // console.debug(Array.from(help)) + // setHelp([...new Set(Array.from(help).filter(i => (i < proof?.steps.length)))]) + // } + // }, [proof]) + + // // save showed help in store + // useEffect(() => { + // if (proof?.steps.length) { + // console.debug(`showHelp:\n ${showHelp}`) + // setHelp(Array.from(showHelp)) + // } + // }, [showHelp]) + + // Effect when command line mode gets enabled + useEffect(() => { + if (model && (typewriterMode)) { + let code = model.getLinesContent().filter(line => line.trim()) + // REMOVED .editor call + editor?.executeEdits("typewriter", [{ + range: model.getFullModelRange(), + text: code.length ? code.join('\n') + '\n' : '', + forceMoveMarkers: true + }]); + + // let endPos = editor.getModel().getFullModelRange().getEndPosition() + // if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") { + // editor.executeEdits("typewriter", [{ + // range: monaco.Selection.fromPositions(endPos, endPos), + // text: "\n", + // forceMoveMarkers: true + // }]); + // } + // let endPos = editor.getModel().getFullModelRange().getEndPosition() + // let currPos = editor.getPosition() + // if (currPos.column != 1 || (currPos.lineNumber != endPos.lineNumber && currPos.lineNumber != endPos.lineNumber - 1)) { + // // This is not a position that would naturally occur from Typewriter, reset: + // editor.setSelection(monaco.Selection.fromPositions(endPos, endPos)) + // } + } + }, [editor, typewriterMode, lockEditorMode]) // TODO: typewriterMode too? + + return <> + { levelInfoIsLoading &&
} + + {mobile? + // TODO: This is copied from the `Split` component below... + <> +
+ + +
+ + : + + + + + + } + +} diff --git a/client/src/components/main/DualEditor.tsx b/client/src/components/main/DualEditor.tsx new file mode 100644 index 00000000..645c4d91 --- /dev/null +++ b/client/src/components/main/DualEditor.tsx @@ -0,0 +1,183 @@ +import { useAtom } from "jotai" +import { editorConnectionAtom, infoviewConfigAtom, leanFileProgressAtom, lspDiagnosticsAtom, proofAtom, rpcSessionsAtom, serverVersionAtom, typewriterModeAtom } from "../../store/editor-atoms" +import React from "react" +import { ExerciseStatement } from "../infoview/ExerciseStatement" +import { gameIdAtom, levelIdAtom, worldIdAtom } from "../../store/location-atoms" +import { gameInfoAtom, levelInfoAtom } from "../../store/query-atoms" +import { completedAtom, progressAtom } from "../../store/progress-atoms" +import { inventoryAtom } from "../../store/inventory-atoms" +import { TypewriterInterfaceWrapper } from "./TypewriterInterfaceWrapper" +import { Main } from "./Main" +import { useClientNotificationEffect, useEvent, useEventResult, useServerNotificationState } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/util" +import type { Diagnostic, DidCloseTextDocumentParams, DocumentUri, PublishDiagnosticsParams } from 'vscode-languageserver-protocol'; +import { LeanFileProgressParams, LeanFileProgressProcessingInfo, RpcCallParams, defaultInfoviewConfig } from '@leanprover/infoview-api'; +import { ServerVersion } from 'lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/serverVersion' +import { RpcSessionAtPos, RpcSessions } from 'lean4monaco/dist/vscode-lean4/lean4-infoview-api/src/rpcSessions' +import { RpcReleaseParams } from "lean4monaco/dist/vscode-lean4/lean4-infoview-api/src/lspTypes" + + + +/** 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({ codeviewRef } : { codeviewRef: any }) { + const [typewriterMode] = useAtom(typewriterModeAtom) + const ec = useAtom(editorConnectionAtom)//React.useContext(EditorContext) + const showTypewriter = Boolean(ec) && typewriterMode + return <> +
+ +
+
+ {ec ? + : + // TODO: Style this if relevant. + <> + } + +} + +/** The part of the two editors that needs the editor connection first */ +function DualEditorMain() { + const [editorConnection,] = useAtom(editorConnectionAtom)//React.useContext(EditorContext) + const [rpcSessions, setRpcSessions] = useAtom(rpcSessionsAtom) + const [, setServerVersion] = useAtom(serverVersionAtom) + const [, setInfoviewConfig] = useAtom(infoviewConfigAtom) + const [, setLspDiagnostics] = useAtom(lspDiagnosticsAtom) + const [, setLeanFileProgressAtom] = useAtom(leanFileProgressAtom) + const [gameId] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [levelId] = useAtom(levelIdAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [{ data: levelInfo }] = useAtom(levelInfoAtom) + + const [, setCompleted] = useAtom(completedAtom) + + const [, addToInventory] = useAtom(inventoryAtom) + const [typewriterMode, setTypewriterMode] = useAtom(typewriterModeAtom) + + const [proof] = useAtom(proofAtom) + + // REPLACES WithRpcSessions + // Initialize RpcSessions when editorConnection is available + React.useEffect(() => { + if (!editorConnection) { + console.log("[DualEditorMain] No editor connection available during RPC sesssion creation.") + return; + } + + const sessions = new RpcSessions({ + createRpcSession: (uri: DocumentUri) => editorConnection.api.createRpcSession(uri), + closeRpcSession: (uri: DocumentUri) => editorConnection.api.closeRpcSession(uri), + call: (params: RpcCallParams) => editorConnection.api.sendClientRequest(params.textDocument.uri, '$/lean/rpc/call', params), + release: (params: RpcReleaseParams) => editorConnection.api.sendClientNotification(params.uri, '$/lean/rpc/release', params), + }); + + setRpcSessions(sessions); + + // Clean up the sessions on unmount + return () => sessions.dispose(); + }, [editorConnection, setRpcSessions]); + + React.useEffect(() => { + if (proof?.completed) { + console.log(`[DualEditorMain] Start proof-completion procedure`) + setCompleted(true) + + // On completion, add the names of all new items to the local storage + let newTiles = [ + ...levelInfo?.tactics ?? [], + ...levelInfo?.lemmas ?? [], + ...levelInfo?.definitions ?? [] + ].filter((tile) => tile.new).map((tile) => tile.name) + + // Add the proven statement to the local storage as well. + if (levelInfo?.statementName != null) { + newTiles.push(levelInfo?.statementName) + } + addToInventory(newTiles) + } + }, [proof, levelInfo]) + + // REPLACES the ConfigContext + /* Set up updates to the global infoview state on editor events. */ + React.useEffect(() => { + if (!editorConnection) { + console.log("[DualEditorMain] No editor connection available during InfoviewConfig creation.") + return; + } + + // The value for the messageOrder had to be copied from @leanprovers definition. + // This is needed, because EditorConnection is imported from lean4monaco where the + // the definition for the InfoViewConfig does not contain messageOrder. + // This is a symptom of several dependency crashed that need to be addressed at some point. + const unsubscribe = editorConnection.events.changedInfoviewConfig.on((config) => { + setInfoviewConfig({...config, messageOrder: 'Sort by proximity to text cursor'}) + }); + + // Clean up the subscription on unmount + return () => unsubscribe?.dispose(); + }, [editorConnection, setInfoviewConfig]); + + // REPLACES the VersionContext + // Update the server version whenever the server restarts + React.useEffect(() => { + if (!editorConnection) return; + + const unsubscribeServer = editorConnection.events.serverRestarted.on((result) => { + const serverVersion = new ServerVersion(result.serverInfo?.version ?? '') + console.log(`[DualEditorMain] Setting server session after restart: ${serverVersion}`) + setServerVersion(serverVersion); + }); + + return () => unsubscribeServer?.dispose(); + }, [editorConnection, setServerVersion]); + + // Handle closing sessions for closed files + useClientNotificationEffect( + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + const [rpcSessions] = useAtom(rpcSessionsAtom); + rpcSessions?.closeSessionForFile(params.textDocument.uri); + }, + [], + ); + + // REPLACES the WithLspDiagnosticsContext + // Update the LSP diagnostics whenever the notification is received + useServerNotificationState( + 'textDocument/publishDiagnostics', + new Map(), + async (params: PublishDiagnosticsParams) => (diags) => { + const newDiags = new Map(diags); + newDiags.set(params.uri, params.diagnostics); + setLspDiagnostics(newDiags); + return newDiags; + }, + [] + ); + + // REPLACES the ProgressContext + const [allProgress, _1] = useServerNotificationState( + '$/lean/fileProgress', + new Map(), + async (params: LeanFileProgressParams) => (allProgress) => { + const newProgress = new Map(allProgress); + newProgress.set(params.textDocument.uri, params.processing); + setLeanFileProgressAtom(newProgress) + return newProgress + }, []) + + // Handle server restart + useEvent(editorConnection!.events.serverRestarted, () => { + rpcSessions?.closeAllSessions(); + }); + + return <> + {(typewriterMode) ? + + : +
+ } + +} diff --git a/client/src/components/main/Main.tsx b/client/src/components/main/Main.tsx new file mode 100644 index 00000000..3a652dd1 --- /dev/null +++ b/client/src/components/main/Main.tsx @@ -0,0 +1,215 @@ +// TODO: This is only used in `EditorInterface` + +import { useTranslation } from "react-i18next"; +import { useGameTranslation } from "../../utils/translation"; +import { crashedAtom, editorConnectionAtom, editorAtom, lockEditorModeAtom, proofAtom, serverVersionAtom, typewriterModeAtom } from "../../store/editor-atoms"; +import { useAtom } from "jotai"; +import React from "react"; +import { gameIdAtom, levelIdAtom, worldIdAtom } from "../../store/location-atoms"; +import { gameInfoAtom, levelInfoAtom } from "../../store/query-atoms"; +import { helpAtom, selectedStepAtom } from "../../store/chat-atoms"; +import { useRpcSessionAtPos } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/rpcSessions"; +import { lastStepHasErrors, loadGoals } from "../../../../infoview/goals"; +import { DocumentPosition } from "../editor/editor/util"; +import { useServerNotificationEffect, useServerNotificationState, useEventResult, useClientNotificationEffect } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/util"; +import { defaultInfoviewConfig, LeanFileProgressParams, LeanFileProgressProcessingInfo } from "@leanprover/infoview-api"; +import type { DidCloseTextDocumentParams, DocumentUri } from 'vscode-languageserver-protocol' +import { ServerVersion } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/serverVersion"; +import { Hints } from "../hints"; + +// TODO: This is only used in `EditorInterface` +// while `TypewriterInterface` has this copy-pasted in. +export function Main() { + let { t } = useTranslation() + const { t: gT } = useGameTranslation() + const [lockEditorMode] = useAtom(lockEditorModeAtom) + const [editorConnection,] = useAtom(editorConnectionAtom)//React.useContext(EditorContext); + const [gameId] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [levelId] = useAtom(levelIdAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [{ data: levelInfo }] = useAtom(levelInfoAtom) + const [help, setHelp] = useAtom(helpAtom) + + const [typewriterMode] = useAtom(typewriterModeAtom) + + const [proof, setProof] = useAtom(proofAtom) + const [, setCrashed] = useAtom(crashedAtom) + const [selectedStep, setSelectedStep] = useAtom(selectedStepAtom) + const [editor,] = useAtom(editorAtom)//React.useContext(MonacoEditorContext) + const [, setServerVersion] = useAtom(serverVersionAtom) + const model = editor?.getModel() + const uri = model?.uri.toString() + const rpcSess = useRpcSessionAtPos({ uri: uri ?? '', line: 0, character: 0 }) + + React.useEffect(() => { + if (!uri || !worldId || !levelId) { + return + } + loadGoals(rpcSess, uri, worldId, levelId, setProof, setCrashed) + }, [rpcSess, uri, worldId, levelId, setProof, setCrashed]) + + function toggleSelection(line: number) { + return (ev: any) => { + console.debug('toggled selection') + if (selectedStep == line) { + setSelectedStep(undefined) + } else { + setSelectedStep(line) + } + } + } + //console.debug(`template: ${props.data?.template}`) + + // React.useEffect (() => { + // if (props.data.template) { + // let code: string = selectCode(gameId, worldId, levelId)(store.getState()) + // if (!code.length) { + // //models.push(monaco.editor.createModel(code, 'lean4', uri)) + // } + // } + // }, [props.data.template]) + + /* Set up updates to the global infoview state on editor events. */ + // config is not used + //const config = useEventResult(editorConnection!.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); + }, + [] + ); + + // curUri is not used + //const curUri = useEventResult(editorConnection.events.changedCursorLocation, loc => loc?.uri); + + const curPos: DocumentPosition | undefined = + useEventResult( + editorConnection!.events.changedCursorLocation, + loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) + + React.useEffect(() => { + if (typewriterMode) { + return + } + if (!uri) { + return + } + loadGoals(rpcSess, uri, worldId!, levelId!, setProof, setCrashed) + }, [typewriterMode, lockEditorMode, uri, worldId, levelId, rpcSess, setProof, setCrashed]) + + useServerNotificationEffect('textDocument/publishDiagnostics', (params: any) => { + if (typewriterMode) { + return + } + if (!uri || params?.uri !== uri) { + return + } + loadGoals(rpcSess, uri, worldId!, levelId!, setProof, setCrashed) + }, [typewriterMode, lockEditorMode, uri, worldId, levelId, rpcSess, setProof, setCrashed]) + + const hintLine = (() => { + const isEditorMode = !(typewriterMode) + const curLine = Number.isFinite(curPos?.line) + ? curPos?.line + : (Number.isFinite((curPos as any)?._line) ? (curPos as any)._line : undefined) + const curChar = Number.isFinite(curPos?.character) + ? curPos?.character + : (Number.isFinite((curPos as any)?._character) ? (curPos as any)._character : undefined) + if (isEditorMode && Number.isFinite(curLine)) { + const baseLine = curLine + return (curChar === 0 && baseLine > 0) ? baseLine - 1 : baseLine + } + if (Number.isFinite(selectedStep)) { + return selectedStep + } + if (!proof?.steps?.length) { + return 0 + } + const lastIndex = proof.steps.length - 1 + return lastStepHasErrors(proof) ? Math.max(0, lastIndex - 1) : lastIndex + })() + + const clampedHintLine = Math.max(0, Math.min(Number.isFinite(hintLine) ? hintLine : 0, (proof?.steps?.length ?? 1) - 1)) + + const hintStepIndex = (() => { + if (Number.isFinite(selectedStep)) { + return selectedStep + } + if (!proof?.steps?.length) { + return 0 + } + const maxIndex = proof.steps.length - 1 + return Math.min(clampedHintLine + 1, maxIndex) + })() + + const hintsToShow = (() => { + if (!proof?.steps?.length) { + return undefined + } + return proof.steps[hintStepIndex!]?.goals?.[0]?.hints + })() + + // Effect when the cursor changes in the editor + React.useEffect(() => { + // TODO: this is a bit of a hack and will yield unexpected behaviour if lines + // are indented. + const newPos = curPos!.line + (curPos?.character == 0 ? 0 : 1) + + if (Number.isFinite(newPos)) { + // scroll the chat along + setSelectedStep(newPos) + } + }, [curPos]) + + useClientNotificationEffect( + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + if (editorConnection!.events.changedCursorLocation.current && + editorConnection!.events.changedCursorLocation.current.uri === params.textDocument.uri) { + editorConnection!.events.changedCursorLocation.fire(undefined) + } + }, + [] + ); + + // serverVersion has to be given to what was former the version context + const serverVersion = useEventResult(editorConnection!.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) + + console.log(`server version: ${serverVersion}`) + + setServerVersion(serverVersion!) + + const serverStoppedResult = useEventResult(editorConnection!.events.serverStopped); + // NB: the cursor may temporarily become `undefined` when a file is closed. In this case + // it's important not to reconstruct the `WithBlah` wrappers below since they contain state + // that we want to persist. + let ret + if (serverStoppedResult) { + ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

+ } else { + ret =
+
+ {proof?.completedWithWarnings && +
+ {proof?.completed ? t("Level completed! ๐ŸŽ‰") : t("Level completed with warnings ๐ŸŽญ")} +
+ } + {/* */} +
+ {hintsToShow && ( + + )} + {/* */} +
+ } + + return ret +} diff --git a/client/src/components/main/TypewriterInterface.tsx b/client/src/components/main/TypewriterInterface.tsx new file mode 100644 index 00000000..5082c4d9 --- /dev/null +++ b/client/src/components/main/TypewriterInterface.tsx @@ -0,0 +1,340 @@ +import path from 'path'; +import React from "react" +import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' + +import { useAtom } from "jotai" +import { useTranslation } from "react-i18next" +import { gameIdAtom, levelIdAtom, worldIdAtom } from "../../store/location-atoms" +import { gameInfoAtom } from "../../store/query-atoms" +import { deletedChatAtom, helpAtom, selectedStepAtom } from "../../store/chat-atoms" +import { mobileAtom } from "../../store/preferences-atoms" +import { crashedAtom, editorConnectionAtom, interimDiagsAtom, editorAtom, proofAtom, rpcSessionAtPosAtom, typewriterContentAtom } from "../../store/editor-atoms" +import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from "../../../../infoview/goals" +import { filterHints, Hint, Hints, MoreHelpButton } from "../hints" +import { GameHint } from "../infoview/types" +import { ExerciseStatement } from "../infoview/ExerciseStatement" +import { useRpcSessionAtPos } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/rpcSessions" +import { useServerNotificationEffect } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/util" +import { DiagnosticSeverity } from 'vscode-languageclient'; +import { getInteractiveDiagsAt, hasInteractiveErrors } from "../../../../infoview/typewriter" +import { Button } from '../button'; +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { faArrowRight, faDeleteLeft, faHome } from "@fortawesome/free-solid-svg-icons" +import { InteractiveGoalsWithHints, ProofState } from "../../api/rpc_api" +import { Errors } from '../infoview/messages/Error' +import { CircularProgress } from '@mui/material'; +import { Typewriter } from '../infoview/typewriter'; +import { IconProp } from '@fortawesome/fontawesome-svg-core'; + + +/** The interface in command line mode */ +export function TypewriterInterface() { + let { t } = useTranslation() + const [editorConnection, _] = useAtom(editorConnectionAtom)//React.useContext(EditorContext) + const [gameId, navigateToGame] = useAtom(gameIdAtom) + const [worldId] = useAtom(worldIdAtom) + const [levelId, navigateToLevel] = useAtom(levelIdAtom) + const [{ data: gameInfo }] = useAtom(gameInfoAtom) + const [help, setHelp] = useAtom(helpAtom) + + const [editor] = useAtom(editorAtom)//React.useContext(MonacoEditorContext) + const model = editor?.getModel() + const uri = model?.uri.toString() ?? '' + + const worldSize = gameInfo?.worldSize?.[worldId ?? ""] ?? 0 + + const fallbackUri = `file:///${worldId}/${levelId}.lean` + const effectiveUri = uri || fallbackUri + let image: string | undefined = gameInfo?.worlds?.nodes[worldId!]?.image + + + const [disableInput, setDisableInput] = React.useState(false) + const [loadingProgress, setLoadingProgress] = React.useState(0) + const [, setDeletedChat] = useAtom(deletedChatAtom) + const [mobile] = useAtom(mobileAtom) + const [proof, setProof ] = useAtom(proofAtom) + const [crashed, setCrashed ] = useAtom(crashedAtom) + const [interimDiags ] = useAtom(interimDiagsAtom) + + const [, setTypewriter] = useAtom(typewriterContentAtom) + const [selectedStep, setSelectedStep] = useAtom(selectedStepAtom) + + const proofPanelRef = React.useRef(null) + // const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; + // const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); + + const rpcSess = useRpcSessionAtPos({uri: effectiveUri, line: 0, character: 0}) + const [rpcSession, setRpcSession] = useAtom(rpcSessionAtPosAtom) + + // Set the RPC session in the atom + React.useEffect(() => { + setRpcSession(rpcSess); + }, [rpcSess, setRpcSession]); + + React.useEffect(() => { + if (!effectiveUri) { + return + } + setCrashed(false) + loadGoals(rpcSess, effectiveUri, worldId!, levelId!, setProof, setCrashed) + }, [rpcSess, effectiveUri, worldId, levelId, setProof, setCrashed]) + + /** 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: any) => { + let deletedChat: Array = [] + 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 + deletedChat = [...deletedChat, ...filteredHints.filter(hint => (!hint.hidden || help.has(line + i)))] + }) + setDeletedChat(deletedChat) + + // delete showHelp for deleted steps + setHelp(new Set(Array.from(help).filter(i => i < line - 1))) + + editor!.executeEdits("typewriter", [{ + range: monaco.Selection.fromPositions( + { lineNumber: line, column: 1 }, + editor!.getModel()?.getFullModelRange().getEndPosition() + ), + text: '', + forceMoveMarkers: false + }]) + setSelectedStep(undefined) + setTypewriter(proof?.steps[line].command ?? "") + // Reload proof on deleting + loadGoals(rpcSess, uri, worldId!, levelId!, setProof, setCrashed) + ev.stopPropagation() + } + } + + function toggleSelectStep(line: number) { + return (ev: any) => { + if (mobile) {return} + if (selectedStep == line) { + setSelectedStep(undefined) + console.debug(`unselected step`) + } else { + setSelectedStep(line) + console.debug(`step ${line} selected`) + } + } + } + + // Scroll to the end of the proof if it is updated. + React.useEffect(() => { + if (proof?.steps?.length && proof?.steps?.length > 1) { + proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0) + } else { + proofPanelRef.current?.scrollTo(0,0) + } + // also reenable the commandline when the proof changes + + // BUG: If selecting 2nd goal on a intermediate proofstep and then delete proof to there, + // the commandline is not displaying disabled even though it should. + setDisableInput(false) + }, [proof]) + + // Scroll to element if selection changes + React.useEffect(() => { + if (typeof selectedStep !== 'undefined') { + Array.from(proofPanelRef.current!.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { + elem.scrollIntoView({ block: "center" }) + }) + } + }, [selectedStep]) + + // TODO: superfluous, can be replaced with `withErr` from above + let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false + + + useServerNotificationEffect("$/game/loading", (params : any) => { + if (params.kind == "loadConstants") { + setLoadingProgress(params.counter/100*50) + } else if (params.kind == "finalizeExtensions") { + setLoadingProgress(50 + params.counter/150*50) + } else { + console.error(`Unknown loading kind: ${params.kind}`) + } + }) + + let introText: Array = t(gameInfo?.introduction ?? "", {ns: gameId}).split(/\n(\s*\n)+/) + + return
+
+
+ {image && + + } + +
+
+ {/*
+ +
*/} +
+
+ + {((crashed && (interimDiags.length > 0 || proof!.steps.length > 0))) ?
+

{t("Crashed! Go to editor mode and fix your proof! Last server response:")}

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

{t("Line")} {diag.range.start.line}, {t("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) + + // 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. + // return
+ // + //
+ // } else { + return
+ + + {mobile && i == 0 && gameInfo?.introduction && + introText?.filter(it => it.trim()).map(((it, i) => + // Show the level's intro text as hints, too + + )) + } + {mobile && + + } + {/* setDisableInput(n > 0) : (n) => {}}/> */} + {!(isLastStepWithErrors(proof, i)) && + setDisableInput(n! > 0) : (n) => {}}/> + } + {mobile && i == proof?.steps.length - 1 && + + } + + {/* Show a message that there are no goals left */} + {/* {!step.goals.length && ( +
+ {proof?.completed ? +

Level completed! ๐ŸŽ‰

: +

+ no goals left
+ This probably means you solved the level with warnings or Lean encountered a parsing error. +

+ } +
+ )} */} +
+ } + //} + )} + {proof?.diagnostics.length > 0 && +
+ +
+ } + {mobile && proof?.completed && +
+ {levelId! >= worldSize ? + + : + + } +
+ } + : + + // + // 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`. + } +
+
+ +
+} + +/** The display of a single entered lean command */ +function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, deleteProof: any }) { + let {t} = useTranslation() + + // The first step will always have an empty command + if (!proof?.steps[i]?.command) { return <> } + + if (isLastStepWithErrors(proof, i)) { + // 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
+ {t("Failed command")}: {proof?.steps[i].command} +
+ } else { + return
+
{proof?.steps[i].command}
+ +
+ } +} + +const goalFilter = { + reverse: false, + showType: true, + showInstance: true, + showHiddenAssumption: true, + showLetValue: true +} + + +/** The tabs of goals that lean ahs after the command of this step has been processed */ +function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { + let { t } = useTranslation() + const [mobile] = useAtom(mobileAtom) + const [selectedGoal, setSelectedGoal] = React.useState(0) + + if (proofStep.goals.length == 0) { + return <> + } + + return
+
+ {proofStep.goals.map((goal, i) => ( + // TODO: Should not use index as key. +
{ onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}> + {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")} +
+ ))} +
+
+ +
+
+} diff --git a/client/src/components/main/TypewriterInterfaceWrapper.tsx b/client/src/components/main/TypewriterInterfaceWrapper.tsx new file mode 100644 index 00000000..82160337 --- /dev/null +++ b/client/src/components/main/TypewriterInterfaceWrapper.tsx @@ -0,0 +1,38 @@ +import React from "react"; +import { TypewriterInterface } from "./TypewriterInterface"; +import { useClientNotificationEffect, useEventResult } from "lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/util"; +import { ServerVersion } from 'lean4monaco/dist/vscode-lean4/lean4-infoview/src/infoview/serverVersion'; +import type { DidCloseTextDocumentParams, DocumentUri } from 'vscode-languageserver-protocol'; +import { useAtom } from "jotai"; +import { editorConnectionAtom } from "../../store/editor-atoms"; + +// Splitting up Typewriter into two parts is a HACK +export function TypewriterInterfaceWrapper() { + const [editorConnection, _] = useAtom(editorConnectionAtom)//React.useContext(EditorContext) + + useClientNotificationEffect( + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + if (editorConnection!.events.changedCursorLocation.current && + editorConnection!.events.changedCursorLocation.current.uri === params.textDocument.uri) { + editorConnection!.events.changedCursorLocation.fire(undefined) + } + }, [] + ) + + const serverVersion = + useEventResult(editorConnection!.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) + const serverStoppedResult = useEventResult(editorConnection!.events.serverStopped); + // NB: the cursor may temporarily become `undefined` when a file is closed. In this case + // it's important not to reconstruct the `WithBlah` wrappers below since they contain state + // that we want to persist. + + if (serverStoppedResult) { + return
+

{serverStoppedResult.message}

+

{serverStoppedResult.reason}

+
+ } + + return +} diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index b244aff1..a163216c 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -38,7 +38,7 @@ function IntroductionPanel({setPageNumber}: {setPageNumber: (val: number) => voi // let text: Array = introduction.split(/\n(\s*\n)+/) let text: Array = gameInfo?.introduction ? [gT(gameInfo.introduction)] : [] - return
+ return
{text?.map(((t, i) => t.trim() ? diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index f30252b3..51d0cba2 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -340,13 +340,17 @@ export function WorldTreePanel() { let dx = bounds ? s*(bounds.x2 - bounds.x1) + 2*padding : 100 - return
+ return ( +
- - {svgElements} - -
+
+ + {svgElements} + +
+
+ ) } diff --git a/client/src/css/app.css b/client/src/css/app.css index cb07ab61..a3480d93 100644 --- a/client/src/css/app.css +++ b/client/src/css/app.css @@ -13,7 +13,6 @@ html { --ff-primary: Roboto; } - /* General styling */ body { @@ -92,22 +91,8 @@ em { /* App Bar */ -#root { - height: 100%; -} - -.app { - height: 100%; - display: flex; - flex-direction: column; -} - .app-bar { - flex: 0; background: var(--clr-primary); - display: flex; - position: relative; - flex-direction: row; justify-content: space-between; align-items: center; padding: 1.1em; @@ -130,14 +115,6 @@ em { /* margin: 0 1em; */ } -.app-content { - height: 100%; - flex: 1; - min-height: 0; - display: flex; -} - - .markdown li ul, .markdown li ol { margin:0 1.5em; } diff --git a/client/src/css/infoview.css b/client/src/css/infoview.css index 5453b3a3..784c87d2 100644 --- a/client/src/css/infoview.css +++ b/client/src/css/infoview.css @@ -126,14 +126,12 @@ .typewriter .typewriter-input { flex: 0 0 auto; - width: 100%; align-self: flex-start; margin-top: 0; } .typewriter-input .monaco-editor, .typewriter-input .monaco-editor-background { - height: 100%; margin-top: 0; } @@ -211,10 +209,6 @@ scroll-behavior: smooth; } -.typewriter-interface .content .tmp-pusher { - flex: 1; -} - .exercise .command { background-color: #bbb; padding: .5em; @@ -293,3 +287,11 @@ stroke: var(--clr-dark-gray); stroke-width: 2; } + +.exercise-statement { + padding-left: .5em; + padding-right: .5em; + padding-top: 1em; + padding-bottom: 1em; + margin: 0; +} diff --git a/client/src/css/inventory.css b/client/src/css/inventory.css index ed4d2657..7c157342 100644 --- a/client/src/css/inventory.css +++ b/client/src/css/inventory.css @@ -1,16 +1,12 @@ -.inventory-panel { - position: relative; -} .inventory-panel .documentation { position: absolute; display: block; top: 0; left: 0; - width: 100%; - height: 100%; z-index: 10; background-color: white; + padding: 1em; } .documentation .nav-button { @@ -26,6 +22,14 @@ font-size: .7rem; } +.inventory-list { + display: flex; + flex-direction: column; + gap: 0; + flex-wrap : wrap; + padding: 0 1em; +} + .inventory h2, .inventory-panel .documentation h2, .inventory-panel .documentation h1 { font-size: 1.5em; margin-top: 1em; @@ -48,16 +52,6 @@ height: 100%; } -.inventory-list { - flex: 1; - display: flex; - flex-direction: column; - gap: 0; - min-height: 0; - overflow-y: auto; - padding-left: 1rem; - padding-right: 1rem; -} .inventory .item { background: #fff; diff --git a/client/src/css/layout.css b/client/src/css/layout.css new file mode 100644 index 00000000..cd1f7c48 --- /dev/null +++ b/client/src/css/layout.css @@ -0,0 +1,92 @@ +html, body { + height: 100%; + margin: 0; +} + +#root { + height: 100vh; + width: 100vw; + box-sizing: border-box; + display: flex; + flex-direction: column; +} + +.app-bar { + flex-shrink: 0; + background: var(--clr-primary); + display: flex; + position: relative; + flex-direction: row; + justify-content: space-between; + align-items: center; + padding: 1.1em; + filter: drop-shadow(0 0 5px rgba(0,0,0,0.5)); + z-index: 20; +} + +.app-content { + flex: 1; + min-height: 0; + position: relative; +} + +.level, .welcome { + display: flex; + height: 100%; +} + +.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel, .chat-panel, .panel { + display: flex; + min-height: 0; + flex-direction: column; + position: relative; + overflow-y: hidden; +} + +/* World Tree Panel */ + +.world-tree { + flex: 1; + min-height: 0; + overflow-y: auto; +} + +.world-selection { + max-width: 100%; + display: block; + margin: auto; +} + +/* Exercise Panel */ +.exercise { + gap: 8px; +} + +.codeview { + flex: 1; +} + +.infoview { + flex: 1; + display: flex; + border: 1px solid green; + padding-top: 1em; + padding-bottom: 0; + padding-top: 0em; +} + +.infoview iframe { + width: 100%; + height: 100%; +} + +/* Inventory Panel */ + +.tab-bar { + flex-shrink: 0; +} + +.inventory-list { + flex: 1; + overflow-y: auto; +} diff --git a/client/src/css/level.css b/client/src/css/level.css index b084fa7d..6e197035 100644 --- a/client/src/css/level.css +++ b/client/src/css/level.css @@ -1,5 +1,4 @@ .level-mobile { - height: 100%; flex: 1; min-height: 0; /* display: flex; */ @@ -24,32 +23,6 @@ background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg=='); } -.inventory-panel, .exercise-panel, .doc-panel, .introduction-panel { - height: 100%; - width: 100%; - overflow: auto; - position: relative; -} - -.infoview { - padding-top: 1em; - padding-bottom: 0; -} - -.infoview, .exercise-statement { - padding-left: .5em; - padding-right: .5em; -} - -.exercise-statement { - padding-top: 1em; - padding-bottom: 1em; -} - -.exercise-statement p { - margin: 0; -} - .exercise-statement .lean-code { color: rgba(0, 32, 90, 0.87); font-size: 12px; /* TODO: is the monaco font-size hardcoded? */ @@ -59,22 +32,6 @@ padding: 1em; } -.infoview { - padding-top: 0em; -} - -.exercise { - flex: 1 1 auto; - display: flex; - flex-flow: column; -} - -.codeview { - flex: 1 1 auto; - min-height: 192px; - -} - .exercise h4 { margin-top: 0; margin-bottom: 0; @@ -192,7 +149,6 @@ td code { } */ .exercise { - height: 100%; } .chat { @@ -208,7 +164,6 @@ td code { overflow: hidden; display: flex; flex-direction: column; - } .chat-panel .button-row { @@ -217,6 +172,7 @@ td code { margin-right: .5em; min-height: 2.5em; border-top: 0.1em solid #aaa; + flex-shrink: 0; } .chat-panel .btn { @@ -249,7 +205,6 @@ td code { .typewriter-interface { display: flex; flex-flow: column; - height: 100%; } .typewriter { @@ -340,41 +295,6 @@ td code { width: 1.8rem; } -.tmp-pusher { - align-items: center; - display: flex; - justify-content: center; -} - -.typewriter-interface .content, .world-image-container.empty { - background-color: #eee; -} - -.world-image-container { - display: flex; - flex-direction: column; - min-height: 0px; /* somehow this has a desired affect, but why? */ - overflow: hidden; -} - -.world-image-container img.contain { - object-fit: contain; -} - -.world-image-container.center { - justify-content: center; -} - - -.world-image-container img.cover { - height: 100%; - object-fit: cover; -} - -.typewriter-interface .proof { - background-color: #fff; -} - .toggle-width { min-width: 40px; text-align: center; diff --git a/client/src/css/typewriter.css b/client/src/css/typewriter.css new file mode 100644 index 00000000..f9191533 --- /dev/null +++ b/client/src/css/typewriter.css @@ -0,0 +1,66 @@ +.centered-spinner { + display: flex; + justify-content: center; + width: 100%; + margin-top: -1.5rem; +} + +.typewriter-canvas { + position: absolute; + width: 100%; + height: 100%; + display: flex; + flex-direction: column; + background-color: white; +} + +.typewriter-info { + flex: 1; + display: flex; + flex-direction: column; + min-height: 0; + position: relative; + overflow-y: auto; +} + +.typewriter-input { + width: 100%; + flex: 1; + border: 1px solid; + align-self: flex-start; + margin-top: 0; +} + +.pusher { + flex: 1; + min-height: 0; + display: block; +} + +.typewriter-canvas .typewriter-info { + background-color: #eee; +} + +.world-image { + position: absolute; + max-height: 100%; + width: 100%; +} + +.world-image.contain { + object-fit: contain; +} + +.world-image.cover { + height: 100%; + object-fit: cover; +} + +.typewriter-info .proof { + background-color: #fff; + border-radius: 8px 8px 0 0; +} + +.proof { + z-index: 1; +} diff --git a/client/src/css/welcome.css b/client/src/css/welcome.css index cf87e69c..056adc05 100644 --- a/client/src/css/welcome.css +++ b/client/src/css/welcome.css @@ -3,25 +3,7 @@ fill: var(--clr-primary) } */ -.welcome { - height: 100%; - flex: 1; - min-height: 0; - display: flex; -} - -.welcome.mobile .column { - width: 100%; -} - -.app-content { - height: 100% -} - -.welcome .column { - height: 100%; - overflow: auto; - position: relative; +.panel { scroll-behavior: smooth; } diff --git a/client/src/css/world_tree.css b/client/src/css/world_tree.css index ab13154a..91ae99dd 100644 --- a/client/src/css/world_tree.css +++ b/client/src/css/world_tree.css @@ -44,14 +44,6 @@ svg .disabled { cursor: default; } -.world-selection { - display: block; - margin-left: auto; - margin-right: auto; - margin-top: 2em; - max-width: 100%; -} - .world-selection-menu { right: 1em; top: 1em; diff --git a/client/src/index.tsx b/client/src/index.tsx index 690307a4..e6ec33e1 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -4,7 +4,7 @@ import App from './app' import { Provider } from 'react-redux' import Welcome from './components/welcome' import LandingPage from './components/landing_page' -import Level from './components/level' +import Level from './components/level/Level' import './i18n'; import { useAtom } from 'jotai' import { gameIdAtom, hashSegmentsAtom, levelIdAtom, pathSegmentsAtom, redirectAtom, worldIdAtom } from './store/location-atoms' diff --git a/client/src/store/chat-atoms.ts b/client/src/store/chat-atoms.ts index 78ebcf51..22416b20 100644 --- a/client/src/store/chat-atoms.ts +++ b/client/src/store/chat-atoms.ts @@ -1,6 +1,6 @@ import { atom } from "jotai" import { levelProgressAtom, progressAtom, defaultLevelProgress } from "./progress-atoms" -import { GameHint } from "../components/infoview/rpc_api" +import { GameHint } from "../api/rpc_api" /** User read the game introduction. Only relevant on mobile */ export const readGameIntroAtom = atom( diff --git a/client/src/store/editor-atoms.ts b/client/src/store/editor-atoms.ts index f0cbae24..02d180ac 100644 --- a/client/src/store/editor-atoms.ts +++ b/client/src/store/editor-atoms.ts @@ -1,11 +1,220 @@ +import { editor } from 'monaco-editor' import { atom } from "jotai"; -import { LeanMonaco, LeanMonacoOptions } from 'lean4monaco' -import { gameIdAtom } from "./location-atoms"; +import { atomEffect } from 'jotai-effect'; +import { LeanMonaco, LeanMonacoOptions, RpcSessionAtPos, LeanClient} from 'lean4monaco' +import { gameIdAtom, levelIdAtom, worldIdAtom } from "./location-atoms"; import { levelProgressAtom, progressAtom } from "./progress-atoms"; import { Selection } from "./progress-types"; import { levelInfoAtom } from "./query-atoms"; -import { ProofState } from "../components/infoview/rpc_api"; -import { Diagnostic } from 'vscode-languageserver-types' +import { Diagnostic, DiagnosticSeverity, DocumentUri } from 'vscode-languageserver-types' +import { preferencesAtom } from './preferences-atoms'; +import { ProofState } from '../api/rpc_api'; + +import { defaultInfoviewConfig, InfoviewConfig, LeanFileProgressProcessingInfo } from '@leanprover/infoview-api'; +import { atomWithQuery } from 'jotai-tanstack-query'; +import { oneLineEditorAtom } from '../components/editor/typewriter/typewriter-atoms'; +import { deletedChatAtom, helpAtom, selectedStepAtom } from './chat-atoms'; +import { filterHints } from '../components/hints'; + +/** The unique leanMonaco instance for the entire application */ +export const leanMonacoAtom = atom(null) + +/** The active client. lean4game only uses one client simultaneously */ +export const clientAtom = atom() +// get => { +// const clients = get(leanMonacoAtom)?.clientProvider?.getClients() ?? [] +// return clients?.[0] +// }) + +/** The current (multiline) editor */ +export const editorAtom = atom(null) + +/** The model of the current editor */ +export const modelAtom = atom(get => get(editorAtom)?.getModel() ?? undefined) + +/** The URI of the currently opened file */ +export const uriAtom = atom(get => get(modelAtom)?.uri) + +/** The currently used RPC session */ +export const rpcSessionAtom = atom() + +/** The code of the current level as stored in local storage. + * + * The setter must not be used directly, expect inside the + * listener which listens to changes of the editor's content. + * This is because the editor won't update leading to inconsistent state. + * + * Instead, use `codeAtom` to set the editor's content and the code + * in storage. +*/ +export const codeStorageAtom = atom( + get => { + const levelProgress = get(levelProgressAtom) + return levelProgress?.code + }, + (get, set, val: string) => { + const levelProgress = get(levelProgressAtom) + if (levelProgress == null) return + set(levelProgressAtom, { ...levelProgress, code: val }) + } +) + +/** + * The code of the current level as stored in local storage. + * + * Can be used to manually update the editor's content which + * in turn keeps the code in local storage up to date. +*/ +export const codeAtom = atom( + get => get(codeStorageAtom), + (get, set, val: string) => { + const model = get(modelAtom) + model?.setValue(val) + } +) + +/** Appends a new line of code at the end of the current code */ +export const appendCodeLineAtom = atom(null, (get, set, line: string) => { + const code = get(codeAtom) + + const oldCode = code?.trimEnd() ?? '' + const newCode = oldCode.length > 0 ? `${oldCode}\n${line}\n` : `${line}\n` + set(codeAtom, newCode) +}) + +/** Delete all code starting at line `line` */ +export const deleteCodeFromLineAtom = atom(null, (get, set, line: number) => { + const code = get(codeAtom) + if (code == undefined) return + + set(selectedStepAtom, undefined) + set(typewriterContentAtom, "") + + const help = get(helpAtom) + const proof = get(proofAtom) + if (proof) { + const newDeletedChat = proof.steps.slice(line).flatMap((step, i) => { + let filteredHints = filterHints(step.goals[0]?.hints, proof.steps[i-1]?.goals[0]?.hints) + return filteredHints.filter(hint => (!hint.hidden || help.has(line + i))) + }) + set(deletedChatAtom, newDeletedChat) + } + + // delete the info about displayed help where the lines were deleted + const newHelp = new Set(Array.from(help).filter(i => i < line - 1)) + set(helpAtom, newHelp) + + const lines = code.split("\n") + const newCode = lines.slice(0, line).join("\n") + set(codeAtom, newCode) +}) + +/** The analysed proof, received over RPC */ +export const proofQueryAtom = atomWithQuery((get) => { + const worldId = get(worldIdAtom) + const levelId = get(levelIdAtom) + const code = get(codeStorageAtom) + const rpcSess = get(rpcSessionAtom) + return { + queryKey: ['proof', worldId, levelId, rpcSess?.sessionId, code], + queryFn: async () => { + if (!rpcSess) return undefined + const res = await rpcSess.client.sendRequest( + '$/lean/rpc/call', + { + method: "Game.getProofState", + params: { + textDocument: {uri: rpcSess.uri}, + position: {line: 0, character: 0}, + worldId, + levelId, + }, + textDocument: {uri: rpcSess.uri}, + position: {line: 0, character: 0}, + sessionId: rpcSess.sessionId + } + ).catch((err) => { + console.warn(err) + return null + }) + return res + }, + enabled: rpcSess?.sessionId != undefined && code != undefined && worldId != undefined && levelId != undefined + } +}) + +/** + * 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 "" as command + */ +export const proofAtom = atom(get => get(proofQueryAtom).data) + + + + + + +/* + * FIXME: everything below here is not curated yet! + */ + + + + + + +/* +I went up the dependency graph starting from the former +info.tsx -> infos.ts -> main.tsx -> level.tsx -> index.tsx and extracted +contexts by their respective atoms. Some of the atoms do not belong here +and have been put here temporarly during my refactoring attempts. +*/ + +export const leanFileProgressAtom = atom>(new Map()) + +export const lspDiagnosticsAtom = atom>(new Map()); + +// export const serverVersionAtom = atom(new ServerVersion('')) + +export const infoviewConfigAtom = atom(defaultInfoviewConfig) + +// export const editorConnectionAtom = atom(null) + + + +// export const rpcSessionsAtom = atom(null) + +// export const rpcSessionAtPosAtom = atom(null) + +export const isProcessingAtom = atom(false) + +export const typewriterContentAtom = atom("") + +export const typewriterAtom = atom( + (get) => {get(typewriterContentAtom)}, + (get, set, val: string) => { + const oneLineEditor = get(oneLineEditorAtom) + const { isSuggestionsMobileMode } = get(preferencesAtom) + + if (!oneLineEditor) { + console.log("[TypewriterAtom] oneLineEditor is False") + return + } + + console.log(`[TypewriterAtom] Set value in oneLineEditor to ${val}`) + oneLineEditor.setValue(val) + oneLineEditor.setPosition({ + column: val.length + 1, + lineNumber: 1 + }) + + if (!isSuggestionsMobileMode) { + oneLineEditor.focus() + } + } +) /** Options for the LeanMonaco instance */ export const leanMonacoOptionsAtom = atom(get => { @@ -23,22 +232,28 @@ export const leanMonacoOptionsAtom = atom(get => { } }}) -/** The unique leanMonaco instance for the entire application */ -export const leanMonacoAtom = atom(null) +export const leanMonacoEditorModelAtom = atom( + (get) => { + const editor = get(editorAtom) + return editor?.getModel() + } +) -export const codeAtom = atom( - get => { - const levelProgress = get(levelProgressAtom) - return levelProgress?.code - }, - (get, set, val: string) => { - const levelProgress = get(levelProgressAtom) - if (levelProgress == null) return - set(levelProgressAtom, { ...levelProgress, code: val }) +export const leanMonacoEditorUriAtom = atom( + (get) => { + const model = get(leanMonacoEditorModelAtom) + return model?.uri.toString() ?? '' } ) -export const typewriterContentAtom = atom("") +export const haseditorAtom = atom( + (get) => { + const editor = get(editorAtom) + console.log(`haseditorAtom: editor state is ${editor}`) + const model = get(leanMonacoEditorModelAtom) + console.log(`haseditorAtom: model state is ${model}`) + return Boolean(editor && model) + }) export const selectionsAtom = atom( get => { @@ -77,15 +292,87 @@ export const typewriterModeAtom = atom( } ) -/** 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 "" as command - */ -export const proofAtom = atom() +export const restoreErrorCommandEffect = atomEffect( + (get, set) => { + const errorCommand = get(lastProofStepErrorCommandAtom) + if (errorCommand) { + set(typewriterContentAtom, errorCommand) + } + } +) + +export const lastProofStepHasErrorsAtom = atom( + (get) => { + const proof = get(proofAtom) + if (!proof?.steps.length) { + return false + } + let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics] + return diags.some( + (d) => (d.severity == DiagnosticSeverity.Error) + ) + } +) + +export const lastProofStepErrorCommandAtom = atom( + (get) => { + const proof = get(proofAtom) + const hasErrors = get(lastProofStepHasErrorsAtom) + if (!hasErrors || !proof?.steps) { + return null + } + return proof.steps[proof.steps.length - 1].command + } +) /** TODO: Workaround to capture a crash of the gameserver. */ export const interimDiagsAtom = atom>([]) /** TODO: Workaround to capture a crash of the gameserver. */ export const crashedAtom = atom(false) + +export const syncTypewriterToEditorEffect = atomEffect( + (get, set) => { + const oneLineEditor = get(oneLineEditorAtom) + const typewriter = get(typewriterContentAtom) + const { isSuggestionsMobileMode } = get(preferencesAtom) + + if (!oneLineEditor) { + console.log("oneLineEditor is False") + return + } + + if (oneLineEditor.getValue() !== typewriter) { + console.log(`Set value in oneLineEditor to ${typewriter}`) + oneLineEditor.setValue(typewriter) + oneLineEditor.setPosition({ + column: typewriter.length + 1, + lineNumber: 1 + }) + } + + if (!isSuggestionsMobileMode) { + oneLineEditor.focus() + } + } +) + +export const syncEditorPositionEffect = atomEffect( + (get, set) => { + const oneLineEditor = get(oneLineEditorAtom) + const editor = get(editorAtom) + const hasEditor = get(haseditorAtom) + const { isSuggestionsMobileMode } = get(preferencesAtom) + + if (!oneLineEditor || !hasEditor || !editor) return + + oneLineEditor.setPosition({ + column: editor.getValue().length + 1, + lineNumber: 1 + }) + + if (!isSuggestionsMobileMode) { + oneLineEditor.focus() + } + } +) diff --git a/client/src/store/inventory-atoms.ts b/client/src/store/inventory-atoms.ts index 31ab9746..ba4c2926 100644 --- a/client/src/store/inventory-atoms.ts +++ b/client/src/store/inventory-atoms.ts @@ -2,9 +2,9 @@ import { Atom, atom } from "jotai"; import { Doc, InventoryOverview, InventoryTile } from "./api"; import { gameIdAtom, levelIdAtom, worldIdAtom } from "./location-atoms"; import { atomWithQuery } from "jotai-tanstack-query"; -import { atomFamily } from "jotai/utils"; import { progressAtom } from "./progress-atoms"; import { preferencesAtom } from "./preferences-atoms"; +import { atomFamily } from "jotai-family"; /** Valid inventory tabs */ export enum InventoryTab { diff --git a/client/src/store/query-atoms.ts b/client/src/store/query-atoms.ts index 4814bfb6..2ec51c5a 100644 --- a/client/src/store/query-atoms.ts +++ b/client/src/store/query-atoms.ts @@ -1,9 +1,9 @@ import { atomWithQuery } from 'jotai-tanstack-query' import { gameIdAtom, levelIdAtom, worldIdAtom } from './location-atoms' import { Doc, GameInfo, InventoryOverview, LevelInfo } from './api' -import { atomFamily } from 'jotai/utils' import { atom } from 'jotai' import { InventoryTab } from './inventory-atoms' +import { atomFamily } from 'jotai-family' /** The info about all games */ export const gameInfoAtomFamily = atomFamily((gameId: string) => atomWithQuery(() => { diff --git a/client/src/store/world-tree-atoms.ts b/client/src/store/world-tree-atoms.ts index 0a035d8b..4f29144b 100644 --- a/client/src/store/world-tree-atoms.ts +++ b/client/src/store/world-tree-atoms.ts @@ -1,7 +1,7 @@ import { atom } from "jotai" -import { atomFamily } from "jotai/utils" import { progressAtom } from "./progress-atoms" import { gameInfoAtom, gameInfoAtomFamily } from "./query-atoms" +import { atomFamily } from "jotai-family" /** World progress family */ export const worldProgressAtomFamily = atomFamily((worldId: string) => atom(get => { diff --git a/client/tsconfig.json b/client/tsconfig.json index 5f4853f4..bf580571 100644 --- a/client/tsconfig.json +++ b/client/tsconfig.json @@ -20,6 +20,6 @@ }, "include": [ "./src/", - "./src/config.json", + "./src/config.json", "../infoview", "../infoview", "../infoview", ] } diff --git a/cypress/TestGame/.i18n/en/Game.pot b/cypress/TestGame/.i18n/en/Game.pot index 1eebca96..28928425 100644 --- a/cypress/TestGame/.i18n/en/Game.pot +++ b/cypress/TestGame/.i18n/en/Game.pot @@ -1,7 +1,7 @@ msgid "" msgstr "Project-Id-Version: Game v4.29.1\n" "Report-Msgid-Bugs-To: \n" -"POT-Creation-Date: 2026-04-23\n" +"POT-Creation-Date: 2026-04-24\n" "Last-Translator: \n" "Language-Team: none\n" "Language: en\n" diff --git a/client/src/components/infoview/context.ts b/infoview/context.ts similarity index 96% rename from client/src/components/infoview/context.ts rename to infoview/context.ts index c3556e7b..83324cd9 100644 --- a/client/src/components/infoview/context.ts +++ b/infoview/context.ts @@ -5,9 +5,9 @@ import * as React from 'react'; import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { InteractiveDiagnostic } from '@leanprover/infoview-api'; import { InteractiveTermGoal,InteractiveGoalsWithHints } from './rpc_api'; -import { Preferences, preferencesAtom } from '../../store/preferences-atoms'; +import { Preferences, preferencesAtom } from '../client/src/store/preferences-atoms'; import { useAtom } from 'jotai'; -import { typewriterContentAtom } from '../../store/editor-atoms'; +import { typewriterContentAtom } from '../client/src/store/editor-atoms'; export const MonacoEditorContext = React.createContext( null as any) diff --git a/client/src/components/infoview/goals.tsx b/infoview/goals.tsx similarity index 98% rename from client/src/components/infoview/goals.tsx rename to infoview/goals.tsx index 862f8d3f..c1023e82 100644 --- a/client/src/components/infoview/goals.tsx +++ b/infoview/goals.tsx @@ -16,10 +16,10 @@ import { DocumentPosition } from '../../../../node_modules/vscode-lean4/lean4-in import { DiagnosticSeverity } from 'vscode-languageserver-protocol'; import { useTranslation } from 'react-i18next'; import { useAtom } from 'jotai'; -import { gameIdAtom } from '../../store/location-atoms'; -import { typewriterModeAtom } from '../../store/editor-atoms'; -import { gameInfoAtom } from '../../store/query-atoms'; -import { mobileAtom } from '../../store/preferences-atoms'; +import { gameIdAtom } from '../client/src/store/location-atoms'; +import { typewriterModeAtom } from '../client/src/store/editor-atoms'; +import { gameInfoAtom } from '../client/src/store/query-atoms'; +import { mobileAtom } from '../client/src/store/preferences-atoms'; /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ function isInaccessibleName(h: string): boolean { diff --git a/client/src/components/infoview/info.tsx b/infoview/info.tsx similarity index 99% rename from client/src/components/infoview/info.tsx rename to infoview/info.tsx index e1198fb0..32158a63 100644 --- a/client/src/components/infoview/info.tsx +++ b/infoview/info.tsx @@ -18,8 +18,8 @@ import { InteractiveTermGoal, InteractiveGoals, ProofState } from './rpc_api' import { MonacoEditorContext, InfoStatus } from './context' import { useTranslation } from 'react-i18next' import { useAtom } from 'jotai' -import { levelIdAtom, worldIdAtom } from '../../store/location-atoms' -import { proofAtom, typewriterModeAtom } from '../../store/editor-atoms' +import { levelIdAtom, worldIdAtom } from '../client/src/store/location-atoms' +import { proofAtom, typewriterModeAtom } from '../client/src/store/editor-atoms' // TODO: All about pinning could probably be removed type InfoKind = 'cursor' | 'pin' diff --git a/client/src/components/infoview/main.tsx b/infoview/main.tsx similarity index 93% rename from client/src/components/infoview/main.tsx rename to infoview/main.tsx index b5e9fff7..6b7c34e5 100644 --- a/client/src/components/infoview/main.tsx +++ b/infoview/main.tsx @@ -19,30 +19,30 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faDeleteLeft, faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' -import { Markdown } from '../markdown'; +import { Markdown } from '../client/src/components/markdown'; import { Infos } from './infos'; import { Errors, WithLspDiagnosticsContext } from './messages'; import { Goal, isLastStepWithErrors, lastStepHasErrors, loadGoals } from './goals'; import { MonacoEditorContext } from './context'; import { Typewriter, getInteractiveDiagsAt, hasInteractiveErrors } from './typewriter'; -import { Button } from '../button'; +import { Button } from '../client/src/components/button'; import { CircularProgress } from '@mui/material'; import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api'; -import { Hint, Hints, MoreHelpButton, filterHints } from '../hints'; +import { Hint, Hints, MoreHelpButton, filterHints } from '../client/src/components/hints'; import { DocumentPosition } from '../../../../node_modules/vscode-lean4/lean4-infoview/src/infoview/util'; import { DiagnosticSeverity } from 'vscode-languageclient'; import { useTranslation } from 'react-i18next'; import path from 'path'; -import { useGameTranslation } from '../../utils/translation'; +import { useGameTranslation } from '../client/src/utils/translation'; import { useAtom } from 'jotai'; -import { gameIdAtom, levelIdAtom, worldIdAtom } from '../../store/location-atoms'; -import { completedAtom } from '../../store/progress-atoms'; -import { gameInfoAtom, levelInfoAtom } from '../../store/query-atoms'; -import { crashedAtom, interimDiagsAtom, lockEditorModeAtom, proofAtom, typewriterContentAtom, typewriterModeAtom } from '../../store/editor-atoms'; -import { inventoryAtom } from '../../store/inventory-atoms'; -import { mobileAtom } from '../../store/preferences-atoms'; -import { deletedChatAtom, helpAtom, selectedStepAtom } from '../../store/chat-atoms'; +import { gameIdAtom, levelIdAtom, worldIdAtom } from '../client/src/store/location-atoms'; +import { completedAtom } from '../client/src/store/progress-atoms'; +import { gameInfoAtom, levelInfoAtom } from '../client/src/store/query-atoms'; +import { crashedAtom, interimDiagsAtom, lockEditorModeAtom, proofAtom, typewriterContentAtom, typewriterModeAtom } from '../client/src/store/editor-atoms'; +import { inventoryAtom } from '../client/src/store/inventory-atoms'; +import { mobileAtom } from '../client/src/store/preferences-atoms'; +import { deletedChatAtom, helpAtom, selectedStepAtom } from '../client/src/store/chat-atoms'; /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is * always present, or the monaco editor cannot start. @@ -130,38 +130,6 @@ function DualEditorMain() { } -/** The mathematical formulation of the statement, supporting e.g. Latex - * It takes three forms, depending on the precence of name and description: - * - Theorem xyz: description - * - Theorem xyz - * - Exercises: description - * - * If `showLeanStatement` is true, it will additionally display the lean code. - */ -function ExerciseStatement({ showLeanStatement = false }) { - const { t : gT } = useGameTranslation() - const { t } = useTranslation() - const [gameId] = useAtom(gameIdAtom) - const [{ data: levelInfo }] = useAtom(levelInfoAtom) - - if (!(levelInfo?.descrText || levelInfo?.descrFormat)) { return <> } - return <> -
- {levelInfo?.descrText ? - - {(levelInfo?.displayName ? `**${t("Theorem")}** \`${levelInfo?.displayName}\`: ` : '') + t(levelInfo?.descrText, {ns: gameId})} - : levelInfo?.displayName && - - {(levelInfo?.displayName ? `**${t("Theorem")}** \`${levelInfo?.displayName}\`: ` : '') + gT(levelInfo?.descrText ?? "")} - - } - {levelInfo?.descrFormat && showLeanStatement && -

{levelInfo?.descrFormat}

- } -
- -} - // TODO: This is only used in `EditorInterface` // while `TypewriterInterface` has this copy-pasted in. export function Main() { diff --git a/client/src/components/infoview/messages.tsx b/infoview/messages.tsx similarity index 99% rename from client/src/components/infoview/messages.tsx rename to infoview/messages.tsx index 882cf22b..f384dcd5 100644 --- a/client/src/components/infoview/messages.tsx +++ b/infoview/messages.tsx @@ -12,7 +12,7 @@ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/vscode- import { useTranslation } from 'react-i18next' import { useAtom } from 'jotai' -import { typewriterModeAtom } from '../../store/editor-atoms' +import { typewriterModeAtom } from '../client/src/store/editor-atoms' interface MessageViewProps { uri: DocumentUri; diff --git a/client/src/components/infoview/typewriter.tsx b/infoview/typewriter.tsx similarity index 80% rename from client/src/components/infoview/typewriter.tsx rename to infoview/typewriter.tsx index 64db45fb..6438833a 100644 --- a/client/src/components/infoview/typewriter.tsx +++ b/infoview/typewriter.tsx @@ -13,10 +13,10 @@ import { lastStepHasErrors, loadGoals } from './goals' import { ProofState } from './rpc_api' import { useTranslation } from 'react-i18next' import { useAtom } from 'jotai' -import { levelIdAtom, worldIdAtom } from '../../store/location-atoms' -import { preferencesAtom } from '../../store/preferences-atoms' -import { crashedAtom, interimDiagsAtom, proofAtom, typewriterContentAtom } from '../../store/editor-atoms' -import { deletedChatAtom } from '../../store/chat-atoms' +import { levelIdAtom, worldIdAtom } from '../client/src/store/location-atoms' +import { preferencesAtom } from '../client/src/store/preferences-atoms' +import { crashedAtom, interimDiagsAtom, proofAtom, typewriterContentAtom } from '../client/src/store/editor-atoms' +import { deletedChatAtom } from '../client/src/store/chat-atoms' export interface GameDiagnosticsParams { uri: DocumentUri; @@ -140,72 +140,6 @@ export function Typewriter({disabled}: {disabled?: boolean}) { // }, [uri]); - useEffect(() => { - if (oneLineEditorRef.current) { - return - } - const myEditor = monaco.editor.create(inputRef.current!, { - value: typewriter, - language: "lean4", - quickSuggestions: false, - // lightbulb: { - // enabled: true - // }, - unicodeHighlight: { - ambiguousCharacters: false, - }, - automaticLayout: true, - minimap: { - enabled: false - }, - lineNumbers: 'off', - tabSize: 2, - wordWrap: 'on', - glyphMargin: false, - folding: false, - lineDecorationsWidth: 0, - lineNumbersMinChars: 0, - 'semanticHighlighting.enabled': true, - overviewRulerLanes: 0, - hideCursorInOverviewRuler: true, - padding: { - top: 0, - bottom: 0, - }, - scrollbar: { - verticalScrollbarSize: 3 - }, - scrollBeyondLastLine: false, - overviewRulerBorder: false, - theme: 'vs-code-theme-converted', - contextmenu: false - }) - - const layoutInput = () => { - const lineHeight = myEditor.getOption(monaco.editor.EditorOption.lineHeight) - const height = Math.min(myEditor.getContentHeight(), lineHeight + 2, window.innerHeight / 3) - inputRef.current.style.height = `${height}px` - myEditor.layout({ - width: inputRef.current.clientWidth, - height - }) - } - myEditor.onDidContentSizeChange(layoutInput) - layoutInput() - - oneLineEditorRef.current = myEditor - setOneLineEditor(myEditor) - - // const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor) - - return () => { - // abbrevRewriter.dispose() - myEditor.dispose() - oneLineEditorRef.current = null - setOneLineEditor(undefined) - } - }, []) - useEffect(() => { if (!oneLineEditor) return // Ensure that our one-line editor can only have a single line diff --git a/package-lock.json b/package-lock.json index c1641174..d5af61c4 100644 --- a/package-lock.json +++ b/package-lock.json @@ -11,6 +11,10 @@ "client", "relay" ], + "dependencies": { + "jotai-family": "^1.0.2", + "tailwind-merge": "^3.6.0" + }, "devDependencies": { "concurrently": "^9.2.1", "cypress": "^15.12.0", @@ -29,7 +33,7 @@ "@fortawesome/free-regular-svg-icons": "^7.2.0", "@fortawesome/free-solid-svg-icons": "^7.2.0", "@fortawesome/react-fontawesome": "^3.2.0", - "@leanprover/infoview": "^0.4.3", + "@leanprover/infoview-api": "^0.13.0", "@mui/material": "^5.11.1", "@reduxjs/toolkit": "^1.9.1", "@tanstack/query-core": "^5.90.20", @@ -38,9 +42,10 @@ "i18next": "^25.8.18", "i18next-http-backend": "^3.0.2", "jotai": "^2.13.1", + "jotai-effect": "^2.2.3", "jotai-location": "^0.6.2", "jotai-tanstack-query": "^0.11.0", - "lean4monaco": "^1.1.9", + "lean4monaco": "^1.1.14", "monaco-editor-wrapper": "^5.3.1", "react": "^18.2.0", "react-country-flag": "^3.1.0", @@ -52,8 +57,7 @@ "react-split": "^2.0.14", "rehype-katex": "^7.0.1", "remark-gfm": "^4.0.1", - "remark-math": "^6.0.0", - "vscode-lean4": "github:leanprover/vscode-lean4#de0062c" + "remark-math": "^6.0.0" }, "devDependencies": { "@codingame/esbuild-import-meta-url-plugin": "^1.0.3", @@ -1675,24 +1679,11 @@ "tslib": "2" } }, - "node_modules/@leanprover/infoview": { - "version": "0.4.4", - "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.4.tgz", - "integrity": "sha512-OxHffFaHcEudLyBEWpicOl7TfXuTYxW5Sz1RkHdUINWJpQsQn60YDF5fNRKmSb0d/fm7p+LVeBvM273jvfR5wQ==", - "dependencies": { - "@leanprover/infoview-api": "~0.2.1", - "@vscode/codicons": "^0.0.32", - "es-module-shims": "^1.6.2", - "marked": "^4.2.2", - "react-fast-compare": "^3.2.0", - "tachyons": "^4.12.0", - "vscode-languageserver-protocol": "^3.17.2" - } - }, "node_modules/@leanprover/infoview-api": { - "version": "0.2.1", - "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.2.1.tgz", - "integrity": "sha512-4sYdwOhUsa5wfvo/ZsCbcm8fBWcrATciZq0sWfmi5NRbIyZ+c2QjTm6D9CeYPCNvz9yvD1KBp/2+hKEZ8SOHkA==" + "version": "0.13.0", + "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.13.0.tgz", + "integrity": "sha512-WmRqGyXNG7a6mmI7B7xjzRHiyZc7I+D7MrBTlwbMo7n2TA3ts8yTSWZhbio3mOOEMCVMf0jzTnnS8TVJgqkoBA==", + "license": "Apache-2.0" }, "node_modules/@leanprover/unicode-input": { "version": "0.1.9", @@ -2507,9 +2498,6 @@ "arm" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2524,9 +2512,6 @@ "arm" ], "dev": true, - "libc": [ - "musl" - ], "license": "MIT", "optional": true, "os": [ @@ -2541,9 +2526,6 @@ "arm64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2558,9 +2540,6 @@ "arm64" ], "dev": true, - "libc": [ - "musl" - ], "license": "MIT", "optional": true, "os": [ @@ -2575,9 +2554,6 @@ "loong64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2592,9 +2568,6 @@ "loong64" ], "dev": true, - "libc": [ - "musl" - ], "license": "MIT", "optional": true, "os": [ @@ -2609,9 +2582,6 @@ "ppc64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2626,9 +2596,6 @@ "ppc64" ], "dev": true, - "libc": [ - "musl" - ], "license": "MIT", "optional": true, "os": [ @@ -2643,9 +2610,6 @@ "riscv64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2660,9 +2624,6 @@ "riscv64" ], "dev": true, - "libc": [ - "musl" - ], "license": "MIT", "optional": true, "os": [ @@ -2677,9 +2638,6 @@ "s390x" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2694,9 +2652,6 @@ "x64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "MIT", "optional": true, "os": [ @@ -2711,9 +2666,6 @@ "x64" ], "dev": true, - "libc": [ - "musl" - ], "license": "MIT", "optional": true, "os": [ @@ -3185,9 +3137,6 @@ "arm64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "Apache-2.0 AND MIT", "optional": true, "os": [ @@ -3205,9 +3154,6 @@ "arm64" ], "dev": true, - "libc": [ - "musl" - ], "license": "Apache-2.0 AND MIT", "optional": true, "os": [ @@ -3225,9 +3171,6 @@ "x64" ], "dev": true, - "libc": [ - "glibc" - ], "license": "Apache-2.0 AND MIT", "optional": true, "os": [ @@ -3245,9 +3188,6 @@ "x64" ], "dev": true, - "libc": [ - "musl" - ], "license": "Apache-2.0 AND MIT", "optional": true, "os": [ @@ -3983,9 +3923,9 @@ "dev": true }, "node_modules/axios": { - "version": "1.15.1", - "resolved": "https://registry.npmjs.org/axios/-/axios-1.15.1.tgz", - "integrity": "sha512-WOG+Jj8ZOvR0a3rAn+Tuf1UQJRxw5venr6DgdbJzngJE3qG7X0kL83CZGpdHMxEm+ZK3seAbvFsw4FfOfP9vxg==", + "version": "1.15.2", + "resolved": "https://registry.npmjs.org/axios/-/axios-1.15.2.tgz", + "integrity": "sha512-wLrXxPtcrPTsNlJmKjkPnNPK2Ihe0hn0wGSaTEiHRPxwjvJwT3hKmXF4dpqxmPO9SoNb2FsYXj/xEo0gHN+D5A==", "dev": true, "license": "MIT", "dependencies": { @@ -7574,9 +7514,9 @@ } }, "node_modules/jotai": { - "version": "2.13.1", - "resolved": "https://registry.npmjs.org/jotai/-/jotai-2.13.1.tgz", - "integrity": "sha512-cRsw6kFeGC9Z/D3egVKrTXRweycZ4z/k7i2MrfCzPYsL9SIWcPXTyqv258/+Ay8VUEcihNiE/coBLE6Kic6b8A==", + "version": "2.19.1", + "resolved": "https://registry.npmjs.org/jotai/-/jotai-2.19.1.tgz", + "integrity": "sha512-sqm9lVZiqBHZH8aSRk32DSiZDHY3yUIlulXYn9GQj7/LvoUdYXSMti7ZPJGo+6zjzKFt5a25k/I6iBCi43PJcw==", "license": "MIT", "engines": { "node": ">=12.20.0" @@ -7602,6 +7542,30 @@ } } }, + "node_modules/jotai-effect": { + "version": "2.2.3", + "resolved": "https://registry.npmjs.org/jotai-effect/-/jotai-effect-2.2.3.tgz", + "integrity": "sha512-MKw5eUydU6aL+fGtrMbdWLB+KFHc4R1AfQcCnXYpvc2AN+tiE/qS0yZwuL2HEBQoEm6quGPb5M1Uib6viK2Eeg==", + "license": "MIT", + "engines": { + "node": ">=12.20.0" + }, + "peerDependencies": { + "jotai": ">=2.16.0" + } + }, + "node_modules/jotai-family": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/jotai-family/-/jotai-family-1.0.2.tgz", + "integrity": "sha512-U1aTMGxmsmz2Z8gaJD1/ljmMnsmG4/dqrcsfwGbjWV7p6boB9Vy3+75YwUpwPj7GbLNJk9O8rl1VNi8d7+6Rxw==", + "license": "MIT", + "engines": { + "node": ">=12.20.0" + }, + "peerDependencies": { + "jotai": ">=2.9.0" + } + }, "node_modules/jotai-location": { "version": "0.6.2", "resolved": "https://registry.npmjs.org/jotai-location/-/jotai-location-0.6.2.tgz", @@ -7778,9 +7742,9 @@ "link": true }, "node_modules/lean4monaco": { - "version": "1.1.9", - "resolved": "https://registry.npmjs.org/lean4monaco/-/lean4monaco-1.1.9.tgz", - "integrity": "sha512-oCnCA4HlRaJJhPvs6uLZrdKGXcrqEU1Q9MadzRQJXfhKJY7oLfaM/qJbU9pWxmYmLTHj7c5524EanjAkN/USag==", + "version": "1.1.14", + "resolved": "https://registry.npmjs.org/lean4monaco/-/lean4monaco-1.1.14.tgz", + "integrity": "sha512-VryKJReDZsBQWFJAKUkR/6s2V6O+lPmabvI6hgvGld/6XuaYb2y20UPz/qHbAGfGwAvqgIDiATthnUD1WJefOw==", "license": "Apache-2.0", "dependencies": { "@leanprover/infoview": "~0.8.5", @@ -8142,17 +8106,6 @@ "url": "https://github.com/sponsors/wooorm" } }, - "node_modules/marked": { - "version": "4.3.0", - "resolved": "https://registry.npmjs.org/marked/-/marked-4.3.0.tgz", - "integrity": "sha512-PRsaiG84bK+AMvxziE/lCFss8juXjNaWzVbN5tXAm4XjeaS9NAHhop+PjQxz2A9h8Q4M/xGmzP8vqNwy6JeK0A==", - "bin": { - "marked": "bin/marked.js" - }, - "engines": { - "node": ">= 12" - } - }, "node_modules/math-intrinsics": { "version": "1.1.0", "resolved": "https://registry.npmjs.org/math-intrinsics/-/math-intrinsics-1.1.0.tgz", @@ -11406,6 +11359,16 @@ "resolved": "https://registry.npmjs.org/tachyons/-/tachyons-4.12.0.tgz", "integrity": "sha512-2nA2IrYFy3raCM9fxJ2KODRGHVSZNTW3BR0YnlGsLUf1DA3pk3YfWZ/DdfbnZK6zLZS+jUenlUGJsKcA5fUiZg==" }, + "node_modules/tailwind-merge": { + "version": "3.6.0", + "resolved": "https://registry.npmjs.org/tailwind-merge/-/tailwind-merge-3.6.0.tgz", + "integrity": "sha512-uxL7qAVQriqRQPAyK3pj66VqskWqoZ37PW94jwOTwNfq/z9oyu1V+eqrZqtR2+fCiXdYOZe/Modt8GtvqNzu+w==", + "license": "MIT", + "funding": { + "type": "github", + "url": "https://github.com/sponsors/dcastil" + } + }, "node_modules/teex": { "version": "1.0.1", "resolved": "https://registry.npmjs.org/teex/-/teex-1.0.1.tgz", @@ -12548,10 +12511,6 @@ "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.5.tgz", "integrity": "sha512-Ld1VelNuX9pdF39h2Hgaeb5hEZM2Z3jUrrMgWQAu82jMtZp7p3vJT3BzToKtZI7NgQssZje5o0zryOrhQvzQAg==" }, - "node_modules/vscode-lean4": { - "name": "@leanprover/vscode-lean4-repo", - "resolved": "git+ssh://git@github.com/leanprover/vscode-lean4.git#de0062c9e108270c8dbf649a77538f433721154e" - }, "node_modules/vscode-oniguruma": { "version": "1.7.0", "resolved": "https://registry.npmjs.org/vscode-oniguruma/-/vscode-oniguruma-1.7.0.tgz", diff --git a/package.json b/package.json index 2d3acb54..cb6d7fe0 100644 --- a/package.json +++ b/package.json @@ -44,5 +44,9 @@ "last 1 firefox version", "last 1 safari version" ] + }, + "dependencies": { + "jotai-family": "^1.0.2", + "tailwind-merge": "^3.6.0" } } diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index 2697ef17..48da831a 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -354,8 +354,6 @@ def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Optio end GameServer - - @[server_rpc_method] def Game.getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Widget.InteractiveGoals)) := FileWorker.getInteractiveGoals p