phc
/
lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

wip

Browse Source
dev
Jon Eugster 2 years ago
parent 3a885245ae
commit 64ad36dd4f
20 changed files with 10609 additions and 13338 deletions
Show Stats Download Patch File Download Diff File

81
client/src/components/infoview/rpc_api.ts → client/src/components/editor/Defs.ts
Unescape Escape View File

@ -1,67 +1,72 @@
/** /**
* @fileOverview Defines the interface for the communication with the server. * @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 { Range } from 'vscode-languageserver-protocol'
// import type { ContextInfo, FVarId, CodeWithInfos, MVarId } from '@leanprover/infoview-api'; import type {
// import { InteractiveDiagnostic, TermInfo } from '@leanprover/infoview/*'; CodeWithInfos,
import type { Diagnostic } from 'vscode-languageserver-protocol'; ContextInfo,
FVarId,
InteractiveDiagnostic,
MVarId,
TermInfo
} from '@leanprover/infoview-api'
import type { Diagnostic } from 'vscode-languageserver-protocol'
export interface InteractiveHypothesisBundle { export interface InteractiveHypothesisBundle {
/** The pretty names of the variables in the bundle. Anonymous names are rendered /** The pretty names of the variables in the bundle. Anonymous names are rendered
* as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end. * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
* Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */ * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
names: string[]; names: string[]
fvarIds?: any // FVarId[]; fvarIds?: FVarId[]
type: any // CodeWithInfos; type: CodeWithInfos
val?: any // CodeWithInfos; val?: CodeWithInfos
isInstance?: boolean; isInstance?: boolean
isType?: boolean; isType?: boolean
isInserted?: boolean; isInserted?: boolean
isRemoved?: boolean; isRemoved?: boolean
isAssumption?: boolean; isAssumption?: boolean
} }
export interface InteractiveGoalCore { export interface InteractiveGoalCore {
hyps: InteractiveHypothesisBundle[]; hyps: InteractiveHypothesisBundle[]
type: any // CodeWithInfos; type: CodeWithInfos
ctx?: any // ContextInfo; ctx?: ContextInfo
} }
export interface InteractiveGoal extends InteractiveGoalCore { export interface InteractiveGoal extends InteractiveGoalCore {
userName?: string; userName?: string
goalPrefix?: string; goalPrefix?: string
mvarId?: any // MVarId; mvarId?: MVarId
isInserted?: boolean; isInserted?: boolean
isRemoved?: boolean; isRemoved?: boolean
} }
export interface InteractiveGoals extends InteractiveGoalCore { export interface InteractiveGoals extends InteractiveGoalCore {
goals: InteractiveGoals[]; goals: InteractiveGoals[]
} }
export interface InteractiveTermGoal extends InteractiveGoalCore { export interface InteractiveTermGoal extends InteractiveGoalCore {
range?: Range; range?: Range
term?: any //TermInfo; term?: TermInfo
} }
export interface GameHint { export interface GameHint {
text: string; text: string
hidden: boolean; hidden: boolean
rawText: string; rawText: string
varNames?: string[][]; // in Lean: `Array (Name × Name)` varNames?: string[][] // in Lean: `Array (Name × Name)`
} }
export interface InteractiveGoalWithHints { export interface InteractiveGoalWithHints {
goal: InteractiveGoal; goal: InteractiveGoal
hints: GameHint[]; hints: GameHint[]
} }
export interface InteractiveGoalsWithHints { export interface InteractiveGoalsWithHints {
goals: InteractiveGoalWithHints[]; goals: InteractiveGoalWithHints[]
command: string; command: string
diags: any //InteractiveDiagnostic[]; diags: InteractiveDiagnostic[]
} }
/** /**
@ -74,11 +79,11 @@ export interface ProofState {
* *
* In particular `step[i]` is the proof step at the beginning of line `i` in vscode. * In particular `step[i]` is the proof step at the beginning of line `i` in vscode.
*/ */
steps: InteractiveGoalsWithHints[]; steps: InteractiveGoalsWithHints[]
/** The remaining diagnostics that are not in the steps. Usually this should only /** The remaining diagnostics that are not in the steps. Usually this should only
* be the "unsolved goals" message, I believe. * be the "unsolved goals" message, I believe.
*/ */
diagnostics : any // InteractiveDiagnostic[]; diagnostics : InteractiveDiagnostic[]
completed : Boolean; completed : Boolean
completedWithWarnings : Boolean; completedWithWarnings : Boolean
} }

27
client/src/components/editor/Editor.tsx
Unescape Escape View File

@ -2,7 +2,7 @@ import * as React from 'react';
import Split from 'react-split' import Split from 'react-split'
import { useContext, useEffect, useRef, useState } from 'react' import { useContext, useEffect, useRef, useState } from 'react'
import { useTranslation } from "react-i18next" import { useTranslation } from "react-i18next"
import { GameIdContext } from '../../state/context'; import { GameIdContext, MonacoEditorContext } from '../../state/context';
import { useLoadLevelQuery } from '../../state/api'; import { useLoadLevelQuery } from '../../state/api';
import { Markdown } from '../utils'; import { Markdown } from '../utils';
import * as monaco from 'monaco-editor' import * as monaco from 'monaco-editor'
@ -11,6 +11,7 @@ import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'
import '../../css/editor.css' import '../../css/editor.css'
import { useSelector } from 'react-redux'; import { useSelector } from 'react-redux';
import { selectTypewriterMode } from '../../state/progress'; import { selectTypewriterMode } from '../../state/progress';
import { Typewriter } from './Typewriter';
export function Editor() { export function Editor() {
let { t } = useTranslation() let { t } = useTranslation()
@ -37,7 +38,12 @@ export function Editor() {
window.location.host + `/websocket/${gameId}` window.location.host + `/websocket/${gameId}`
console.log(`[LeanGame] socket url: ${socketUrl}`) console.log(`[LeanGame] socket url: ${socketUrl}`)
var _options: LeanMonacoOptions = { var _options: LeanMonacoOptions = {
websocket: {url: socketUrl}, websocket: {
url: socketUrl,
// @ts-ignore
difficulty: 1,
inventory: []
},
// Restrict monaco's extend (e.g. context menu) to the editor itself // Restrict monaco's extend (e.g. context menu) to the editor itself
htmlElement: editorRef.current ?? undefined, htmlElement: editorRef.current ?? undefined,
vscode: { vscode: {
@ -69,7 +75,8 @@ export function Editor() {
_leanMonaco.setInfoviewElement(infoviewRef.current!) _leanMonaco.setInfoviewElement(infoviewRef.current!)
;(async () => { ;(async () => {
await _leanMonaco.start(options) await _leanMonaco.start(options)
await leanMonacoEditor.start(editorRef.current!, `${gameId}/${worldId}/Level_${levelId}.lean`, code) console.warn('gameId', gameId)
await leanMonacoEditor.start(editorRef.current!, `/${worldId}/L_${levelId}.lean`, code)
setEditor(leanMonacoEditor.editor) setEditor(leanMonacoEditor.editor)
setLeanMonaco(_leanMonaco) setLeanMonaco(_leanMonaco)
@ -85,9 +92,13 @@ export function Editor() {
} }
}, [options, infoviewRef, editorRef, gameId, worldId, levelId]) }, [options, infoviewRef, editorRef, gameId, worldId, levelId])
return <Split direction='vertical' minSize={200} sizes={[50, 50]} return <MonacoEditorContext.Provider value={editor}>
className={`editor-wrapper ${typewriterMode ? 'hidden' : ''}`} > <div className="editor-wrapper"><Split direction='vertical' minSize={200} sizes={[50, 50]}
<div ref={editorRef} id="editor" /> className={`editor-split ${typewriterMode ? 'hidden' : ''}`} >
<div ref={infoviewRef} id="infoview" /> <div ref={editorRef} id="editor" />
</Split> <div ref={infoviewRef} id="infoview" />
</Split>
{typewriterMode && <Typewriter />}
</div>
</MonacoEditorContext.Provider>
} }

443
client/src/components/editor/Typewriter.tsx
Unescape Escape View File

@ -0,0 +1,443 @@
import * as React from 'react'
import { useContext } from 'react'
import { useRef, useState, useEffect } from 'react'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faArrowRight, faHome, faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
import { useTranslation } from 'react-i18next'
import * as monaco from 'monaco-editor'
import { ChatContext, GameIdContext, InputModeContext, MonacoEditorContext, PageContext, PreferencesContext, ProofContext } from '../../state/context';
import { RpcContext, WithRpcSessions, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
import '../../css/infoview.css'
import { useGetGameInfoQuery } from '../../state/api'
import { GameHint } from './Defs'
import { MoreHelpButton, filterHints } from '../chat'
import { isLastStepWithErrors, lastStepHasErrors, loadGoals } from '../infoview/goals'
import { getInteractiveDiagsAt, hasInteractiveErrors } from '../infoview/typewriter'
import { Errors } from '../infoview/messages'
import { Button, Markdown } from '../utils'
import { Command, GoalsTabs } from '../infoview/main'
import { CircularProgress } from '@mui/material'
/** The input field */
export function TypewriterInput({disabled}: {disabled?: boolean}) {
let { t } = useTranslation()
/** Reference to the hidden multi-line editor */
// const editor = React.useContext(MonacoEditorContext)
// const model = editor.getModel()
// const uri = model.uri.toString()
const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
const [processing, setProcessing] = useState(false)
// const {typewriterInput, setTypewriterInput} = React.useContext(InputModeContext)
const inputRef = useRef()
// // The context storing all information about the current proof
const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
// // state to store the last batch of deleted messages
// const {setDeletedChat} = React.useContext(DeletedChatContext)
// const rpcSess = React.useContext(RpcContext)
// // Run the command
// const runCommand = React.useCallback(() => {
// if (processing) {return}
// // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
// setDeletedChat([])
// const pos = editor.getPosition()
// if (typewriterInput) {
// setProcessing(true)
// editor.executeEdits("typewriter", [{
// range: monaco.Selection.fromPositions(
// pos,
// editor.getModel().getFullModelRange().getEndPosition()
// ),
// text: typewriterInput.trim() + "\n",
// forceMoveMarkers: false
// }])
// setTypewriterInput('')
// // Load proof after executing edits
// loadGoals(rpcSess, uri, setProof, setCrashed)
// }
// editor.setPosition(pos)
// }, [typewriterInput, editor])
// useEffect(() => {
// if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
// oneLineEditor.setValue(typewriterInput)
// }
// }, [typewriterInput])
// /* Load proof on start/switching to typewriter */
// useEffect(() => {
// loadGoals(rpcSess, uri, setProof, setCrashed)
// }, [])
// /** If the last step has an error, add the command to the typewriter. */
// useEffect(() => {
// if (lastStepHasErrors(proof)) {
// setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
// }
// }, [proof])
// // React when answer from the server comes back
// useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
// if (params.uri == uri) {
// setProcessing(false)
// console.log('Received lean diagnostics')
// console.log(params.diagnostics)
// setInterimDiags(params.diagnostics)
// //loadGoals(rpcSess, uri, setProof)
// // TODO: loadAllGoals()
// if (!hasErrors(params.diagnostics)) {
// //setTypewriterInput("")
// editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
// }
// } else {
// // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
// // console.debug(params)
// }
// // TODO: This is the wrong place apparently. Where do wee need to load them?
// // TODO: instead of loading all goals every time, we could only load the last one
// // loadAllGoals()
// }, [uri]);
// // // React when answer from the server comes back
// // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
// // console.log('Received game diagnostics')
// // console.log(`diag. uri : ${params.uri}`)
// // console.log(params.diagnostics)
// // }, [uri]);
// useEffect(() => {
// const myEditor = monaco.editor.create(inputRef.current!, {
// value: typewriterInput,
// language: "lean4cmd",
// quickSuggestions: false,
// lightbulb: {
// enabled: true
// },
// unicodeHighlight: {
// ambiguousCharacters: false,
// },
// automaticLayout: true,
// minimap: {
// enabled: false
// },
// lineNumbers: 'off',
// tabSize: 2,
// glyphMargin: false,
// folding: false,
// lineDecorationsWidth: 0,
// lineNumbersMinChars: 0,
// 'semanticHighlighting.enabled': true,
// overviewRulerLanes: 0,
// hideCursorInOverviewRuler: true,
// scrollbar: {
// vertical: 'hidden',
// horizontalScrollbarSize: 3
// },
// overviewRulerBorder: false,
// theme: 'vs-code-theme-converted',
// contextmenu: false
// })
// setOneLineEditor(myEditor)
// const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
// return () => {abbrevRewriter.dispose(); myEditor.dispose()}
// }, [])
// useEffect(() => {
// if (!oneLineEditor) return
// // Ensure that our one-line editor can only have a single line
// const l = oneLineEditor.getModel().onDidChangeContent((e) => {
// const value = oneLineEditor.getValue()
// setTypewriterInput(value)
// const newValue = value.replace(/[\n\r]/g, '')
// if (value != newValue) {
// oneLineEditor.setValue(newValue)
// }
// })
// return () => { l.dispose() }
// }, [oneLineEditor, setTypewriterInput])
// useEffect(() => {
// if (!oneLineEditor) return
// // Run command when pressing enter
// const l = oneLineEditor.onKeyUp((ev) => {
// if (ev.code === "Enter") {
// runCommand()
// }
// })
// return () => { l.dispose() }
// }, [oneLineEditor, runCommand])
// // BUG: Causes `file closed` error
// //TODO: Intention is to run once when loading, does that work?
// useEffect(() => {
// console.debug(`time to update: ${uri} \n ${rpcSess}`)
// console.debug(rpcSess)
// // console.debug('LOAD ALL GOALS')
// // TODO: loadAllGoals()
// }, [rpcSess])
/** Process the entered command */
const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
// ev.preventDefault()
// runCommand()
}
// do not display if the proof is completed (with potential warnings still present)
return <div className={`typewriter-cmd${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
<form onSubmit={handleSubmit}>
<div className="typewriter-input-wrapper">
<div ref={inputRef} className="typewriter-input" />
</div>
<button type="submit" disabled={processing} className="btn btn-inverted">
<FontAwesomeIcon icon={faWandMagicSparkles} />&nbsp;{t("Execute")}
</button>
</form>
</div>
}
export function TypewriterInterFace() {
let { t } = useTranslation()
const {gameId, worldId, levelId} = useContext(GameIdContext)
const editor = useContext(MonacoEditorContext)
const model = editor.getModel()
const uri = model.uri.toString()
const gameInfo = useGetGameInfoQuery({game: gameId})
let image: string = gameInfo.data?.worlds.nodes[worldId].image
const [disableInput, setDisableInput] = useState<boolean>(false)
const [loadingProgress, setLoadingProgress] = useState<number>(0)
const { selectedStep, setSelectedStep, setDeletedChat, showHelp, setShowHelp } = useContext(ChatContext)
const {mobile} = useContext(PreferencesContext)
const { proof, setProof, crashed, setCrashed, interimDiags } = useContext(ProofContext)
const { setTypewriterInput } = useContext(PageContext)
const proofPanelRef = React.useRef<HTMLDivElement>(null)
// const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
// const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri);
const rpcSess = useRpcSessionAtPos({uri: uri, line: 0, character: 0})
/** 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) => {
let deletedChat: Array<GameHint> = []
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 || showHelp.has(line + i)))]
})
setDeletedChat(deletedChat)
// delete showHelp for deleted steps
setShowHelp(new Set(Array.from(showHelp).filter(i => i < line - 1)))
editor.executeEdits("typewriter", [{
range: monaco.Selection.fromPositions(
{ lineNumber: line, column: 1 },
editor.getModel().getFullModelRange().getEndPosition()
),
text: '',
forceMoveMarkers: false
}])
setSelectedStep(null)
setTypewriterInput(proof?.steps[line].command)
// Reload proof on deleting
loadGoals(rpcSess, uri, setProof, setCrashed)
ev.stopPropagation()
}
}
function toggleSelectStep(line: number) {
return (ev) => {
if (mobile) {return}
if (selectedStep == line) {
setSelectedStep(null)
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 > 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}`)
}
})
return <div className="typewriter-interface">
<RpcContext.Provider value={rpcSess}>
<div className="content">
{/* <div className='world-image-container empty'>
{image &&
<img className="contain" src={path.join("data", gameId, image)} alt="" />
}
</div> */}
{/* <div className="tmp-pusher">
<div className="world-image-container empty">
</div>
</div> */}
<div className='proof' ref={proofPanelRef}>
{/* <ExerciseStatement /> */}
{crashed ? <div>
<p className="crashed_message">{t("Crashed! Go to editor mode and fix your proof! Last server response:")}</p>
{interimDiags.map(diag => {
const severityClass = diag.severity ? {
[DiagnosticSeverity.Error]: 'error',
[DiagnosticSeverity.Warning]: 'warning',
[DiagnosticSeverity.Information]: 'information',
[DiagnosticSeverity.Hint]: 'hint',
}[diag.severity] : '';
return <div key={diag.message} >
<div className={`${severityClass} ml1 message`}>
<p className="mv2">{t("Line")}&nbsp;{diag.range.start.line}, {t("Character")}&nbsp;{diag.range.start.character}</p>
<pre className="font-code pre-wrap">
{diag.message}as React
</pre>
</div>
</div>
})}
</div> : 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 <div key={`proof-step-${i}`} className={`step step-${i}`}>
// <Errors errors={step.diags} typewriterMode={true} />
// </div>
// } else {
return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
{i > 0 && <>
<Command proof={proof} i={i} deleteProof={deleteProof(i)} />
<Errors errors={step.diags} typewriterMode={true} />
</>}
{mobile && i == 0 && props.data?.introduction &&
<div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
<Markdown>{props.data?.introduction}</Markdown>
</div>
}
{mobile &&
<Hints key={`hints-${i}`}
hints={filteredHints.map(hint => ({hint: hint, step: i}))} />
}
{/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
{!(isLastStepWithErrors(proof, i)) &&
<GoalsTabs goals={step.goals} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
}
{mobile && i == proof?.steps.length - 1 &&
<MoreHelpButton />
}
{/* Show a message that there are no goals left */}
{/* {!step.goals.length && (
<div className="message information">
{proof?.completed ?
<p>Level completed! 🎉</p> :
<p>
<b>no goals left</b><br />
<i>This probably means you solved the level with warnings or Lean encountered a parsing error.</i>
</p>
}
</div>
)} */}
</div>
}
//}
)}
{proof?.diagnostics.length > 0 &&
<div key={`proof-step-remaining`} className="step step-remaining">
<Errors errors={proof?.diagnostics} typewriterMode={true} />
</div>
}
{mobile && proof?.completed &&
<div className="button-row mobile">
{props.level >= props.worldSize ?
<Button to={`/${gameId}`}>
<FontAwesomeIcon icon={faHome} />&nbsp;{t("Home")}
</Button>
:
<Button to={`/${gameId}/world/${props.world}/level/${props.level + 1}`}>
Next&nbsp;<FontAwesomeIcon icon={faArrowRight} />
</Button>
}
</div>
}
</> : <CircularProgress variant="determinate" value={100*(1 - 1.024 ** (- loadingProgress))} />
// note: since we don't know the total number of files,
// we use a function which strictly monotonely increases towards `100` as `x → ∞`
// The base is chosen at random s.t. we get roughly 91% for `x = 100`.
}
</div>
</div>
{/* <Typewriter disabled={disableInput || !proof?.steps.length}/> */}
<TypewriterInput />
</RpcContext.Provider>
</div>
}

764
client/src/components/infoview/goals.tsx
Unescape Escape View File

@ -1,382 +1,382 @@
// /** /**
// * @fileOverview * @fileOverview
// * *
// * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx * Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx
// */ */
// import * as React from 'react' import * as React from 'react'
// // import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api' // import { InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
// // import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; // import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
// // import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; // import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
// // import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' // import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
// // import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; // import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips';
// import { PageContext } from '../../state/context'; import { PageContext } from '../../state/context';
// import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api'; import { InteractiveGoal, InteractiveGoals, InteractiveGoalsWithHints, InteractiveHypothesisBundle, ProofState } from './rpc_api';
// // import { RpcSessionAtPos } from '@leanprover/infoview/*'; // import { RpcSessionAtPos } from '@leanprover/infoview/*';
// // import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; // import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
// import { DiagnosticSeverity } from 'vscode-languageserver-protocol'; import { DiagnosticSeverity } from 'vscode-languageserver-protocol';
// import { useTranslation } from 'react-i18next'; import { useTranslation } from 'react-i18next';
// /** Returns true if `h` is inaccessible according to Lean's default name rendering. */ /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
// function isInaccessibleName(h: string): boolean { function isInaccessibleName(h: string): boolean {
// return h.indexOf('✝') >= 0; return h.indexOf('✝') >= 0;
// } }
// // function goalToString(g: InteractiveGoal): string { function goalToString(g: InteractiveGoal): string {
// // let ret = '' let ret = ''
// // if (g.userName) { if (g.userName) {
// // ret += `case ${g.userName}\n` ret += `case ${g.userName}\n`
// // } }
// // for (const h of g.hyps) { for (const h of g.hyps) {
// // const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ') const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ')
// // ret += `${names} : ${TaggedText_stripTags(h.type)}` ret += `${names} : ${TaggedText_stripTags(h.type)}`
// // if (h.val) { if (h.val) {
// // ret += ` := ${TaggedText_stripTags(h.val)}` ret += ` := ${TaggedText_stripTags(h.val)}`
// // } }
// // ret += '\n' ret += '\n'
// // } }
// // ret += `⊢ ${TaggedText_stripTags(g.type)}` ret += `⊢ ${TaggedText_stripTags(g.type)}`
// // return ret return ret
// // } }
// // export function goalsToString(goals: InteractiveGoals): string { export function goalsToString(goals: InteractiveGoals): string {
// // return goals.goals.map(g => goalToString(g)).join('\n\n') return goals.goals.map(g => goalToString(g)).join('\n\n')
// // } }
// // export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string { export function goalsWithHintsToString(goals: InteractiveGoalsWithHints): string {
// // return goals.goals.map(g => goalToString(g.goal)).join('\n\n') return goals.goals.map(g => goalToString(g.goal)).join('\n\n')
// // } }
// interface GoalFilterState { interface GoalFilterState {
// /** If true reverse the list of hypotheses, if false present the order received from LSP. */ /** If true reverse the list of hypotheses, if false present the order received from LSP. */
// reverse: boolean, reverse: boolean,
// /** If true show hypotheses that have isType=True, otherwise hide them. */ /** If true show hypotheses that have isType=True, otherwise hide them. */
// showType: boolean, showType: boolean,
// /** If true show hypotheses that have isInstance=True, otherwise hide them. */ /** If true show hypotheses that have isInstance=True, otherwise hide them. */
// showInstance: boolean, showInstance: boolean,
// /** If true show hypotheses that contain a dagger in the name, otherwise hide them. */ /** If true show hypotheses that contain a dagger in the name, otherwise hide them. */
// showHiddenAssumption: boolean showHiddenAssumption: boolean
// /** If true show the bodies of let-values, otherwise hide them. */ /** If true show the bodies of let-values, otherwise hide them. */
// showLetValue: boolean; showLetValue: boolean;
// } }
// function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] { function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] {
// return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => { return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => {
// if (h.isInstance && !filter.showInstance) return acc if (h.isInstance && !filter.showInstance) return acc
// if (h.isType && !filter.showType) return acc if (h.isType && !filter.showType) return acc
// const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n)) const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n))
// const hNew: InteractiveHypothesisBundle = filter.showLetValue ? { ...h, names } : { ...h, names, val: undefined } const hNew: InteractiveHypothesisBundle = filter.showLetValue ? { ...h, names } : { ...h, names, val: undefined }
// if (names.length !== 0) acc.push(hNew) if (names.length !== 0) acc.push(hNew)
// return acc return acc
// }, []) }, [])
// } }
// interface HypProps { interface HypProps {
// hyp: InteractiveHypothesisBundle hyp: InteractiveHypothesisBundle
// mvarId?: any // MVarId mvarId?: any // MVarId
// } }
// function Hyp({ hyp: h, mvarId }: HypProps) { function Hyp({ hyp: h, mvarId }: HypProps) {
// const locs = React.useContext(LocationsContext) const locs = React.useContext(LocationsContext)
// const namecls: string = 'mr1 ' + const namecls: string = 'mr1 ' +
// (h.isInserted ? 'inserted-text ' : '') + (h.isInserted ? 'inserted-text ' : '') +
// (h.isRemoved ? 'removed-text ' : '') (h.isRemoved ? 'removed-text ' : '')
// const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) => const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
// <span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}> <span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}>
// <SelectableLocation <SelectableLocation
// locs={locs} locs={locs}
// loc={mvarId && h.fvarIds && h.fvarIds.length > i ? loc={mvarId && h.fvarIds && h.fvarIds.length > i ?
// { mvarId, loc: { hyp: h.fvarIds[i] }} : { mvarId, loc: { hyp: h.fvarIds[i] }} :
// undefined undefined
// } }
// alwaysHighlight={false} alwaysHighlight={false}
// >{n}</SelectableLocation> >{n}</SelectableLocation>
// </span>) </span>)
// const typeLocs: Locations | undefined = React.useMemo(() => const typeLocs: Locations | undefined = React.useMemo(() =>
// locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
// { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} : { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} :
// undefined, undefined,
// [locs, mvarId, h.fvarIds]) [locs, mvarId, h.fvarIds])
// const valLocs: Locations | undefined = React.useMemo(() => const valLocs: Locations | undefined = React.useMemo(() =>
// h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
// { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} : { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} :
// undefined, undefined,
// [h.val, locs, mvarId, h.fvarIds]) [h.val, locs, mvarId, h.fvarIds])
// return <div> return <div>
// <strong className="goal-hyp">{names}</strong> <strong className="goal-hyp">{names}</strong>
// :&nbsp; :&nbsp;
// <LocationsContext.Provider value={typeLocs}> <LocationsContext.Provider value={typeLocs}>
// <InteractiveCode fmt={h.type} /> <InteractiveCode fmt={h.type} />
// </LocationsContext.Provider> </LocationsContext.Provider>
// {h.val && {h.val &&
// <LocationsContext.Provider value={valLocs}> <LocationsContext.Provider value={valLocs}>
// &nbsp;:=&nbsp;<InteractiveCode fmt={h.val} /> &nbsp;:=&nbsp;<InteractiveCode fmt={h.val} />
// </LocationsContext.Provider>} </LocationsContext.Provider>}
// </div> </div>
// } }
// interface GoalProps2 { interface GoalProps2 {
// goals: InteractiveGoal[] goals: InteractiveGoal[]
// filter: GoalFilterState filter: GoalFilterState
// } }
// interface GoalProps { interface GoalProps {
// goal: InteractiveGoal goal: InteractiveGoal
// filter: GoalFilterState filter: GoalFilterState
// showHints?: boolean showHints?: boolean
// typewriter: boolean typewriter: boolean
// unbundle?: boolean /** unbundle `x y : Nat` into `x : Nat` and `y : Nat` */ unbundle?: boolean /** unbundle `x y : Nat` into `x : Nat` and `y : Nat` */
// } }
// /** /**
// * Displays the hypotheses, target type and optional case label of a goal according to the * Displays the hypotheses, target type and optional case label of a goal according to the
// * provided `filter`. */ * provided `filter`. */
// export const Goal = React.memo((props: GoalProps) => { export const Goal = React.memo((props: GoalProps) => {
// const { goal, filter, showHints, typewriter, unbundle } = props const { goal, filter, showHints, typewriter, unbundle } = props
// let { t } = useTranslation() let { t } = useTranslation()
// // TODO: Apparently `goal` can be `undefined` // TODO: Apparently `goal` can be `undefined`
// if (!goal) {return <></>} if (!goal) {return <></>}
// const filteredList = getFilteredHypotheses(goal.hyps, filter); const filteredList = getFilteredHypotheses(goal.hyps, filter);
// const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
// const locs = React.useContext(LocationsContext) const locs = React.useContext(LocationsContext)
// const goalLocs = React.useMemo(() => const goalLocs = React.useMemo(() =>
// locs && goal.mvarId ? locs && goal.mvarId ?
// { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
// undefined, undefined,
// [locs, goal.mvarId]) [locs, goal.mvarId])
// const goalLi = <div key={'goal'} className="goal"> const goalLi = <div key={'goal'} className="goal">
// {/* <div className="goal-title">{t("Goal")}:</div> */} {/* <div className="goal-title">{t("Goal")}:</div> */}
// <LocationsContext.Provider value={goalLocs}> <LocationsContext.Provider value={goalLocs}>
// <InteractiveCode fmt={goal.type} /> <InteractiveCode fmt={goal.type} />
// </LocationsContext.Provider> </LocationsContext.Provider>
// </div> </div>
// // let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent ' // let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
// // if (props.goal.isInserted) cn += 'b--inserted ' // if (props.goal.isInserted) cn += 'b--inserted '
// // if (props.goal.isRemoved) cn += 'b--removed ' // if (props.goal.isRemoved) cn += 'b--removed '
// function unbundleHyps (hyps: InteractiveHypothesisBundle[]) : InteractiveHypothesisBundle[] { function unbundleHyps (hyps: InteractiveHypothesisBundle[]) : InteractiveHypothesisBundle[] {
// return hyps.flatMap(hyp => ( return hyps.flatMap(hyp => (
// unbundle ? hyp.names.map(name => {return {...hyp, names: [name]}}) : [hyp] unbundle ? hyp.names.map(name => {return {...hyp, names: [name]}}) : [hyp]
// )) ))
// } }
// // const hints = <Hints hints={goal.hints} key={goal.mvarId} /> // const hints = <Hints hints={goal.hints} key={goal.mvarId} />
// const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption)) const objectHyps = unbundleHyps(hyps.filter(hyp => !hyp.isAssumption))
// const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption)) const assumptionHyps = unbundleHyps(hyps.filter(hyp => hyp.isAssumption))
// return <> return <>
// {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */} {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
// {filter.reverse && goalLi} {filter.reverse && goalLi}
// <div className="hypotheses"> <div className="hypotheses">
// {! typewriter && objectHyps.length > 0 && {! typewriter && objectHyps.length > 0 &&
// <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div> <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
// {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
// {!typewriter && assumptionHyps.length > 0 && {!typewriter && assumptionHyps.length > 0 &&
// <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div> <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
// {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
// </div> </div>
// {!filter.reverse && <> {!filter.reverse && <>
// <div className='goal-sign'> <div className='goal-sign'>
// <svg width="100%" height="100%"> <svg width="100%" height="100%">
// <line x1="0%" y1="0%" x2="0%" y2="100%" /> <line x1="0%" y1="0%" x2="0%" y2="100%" />
// <line x1="0%" y1="50%" x2="100%" y2="50%" /> <line x1="0%" y1="50%" x2="100%" y2="50%" />
// </svg> </svg>
// </div> </div>
// {goalLi} {goalLi}
// </>} </>}
// {/* {showHints && hints} */} {/* {showHints && hints} */}
// </> </>
// }) })
// export const MainAssumptions = React.memo((props: GoalProps2) => { export const MainAssumptions = React.memo((props: GoalProps2) => {
// let { t } = useTranslation() let { t } = useTranslation()
// const { goals, filter } = props const { goals, filter } = props
// const goal = goals[0] const goal = goals[0]
// const filteredList = getFilteredHypotheses(goal.hyps, filter); const filteredList = getFilteredHypotheses(goal.hyps, filter);
// const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
// const locs = React.useContext(LocationsContext) const locs = React.useContext(LocationsContext)
// const goalLocs = React.useMemo(() => const goalLocs = React.useMemo(() =>
// locs && goal.mvarId ? locs && goal.mvarId ?
// { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
// undefined, undefined,
// [locs, goal.mvarId]) [locs, goal.mvarId])
// const goalLi = <div key={'goal'}> const goalLi = <div key={'goal'}>
// <div className="goal-title">{t("Goal") + ":"}</div> <div className="goal-title">{t("Goal") + ":"}</div>
// <LocationsContext.Provider value={goalLocs}> <LocationsContext.Provider value={goalLocs}>
// <InteractiveCode fmt={goal.type} /> <InteractiveCode fmt={goal.type} />
// </LocationsContext.Provider> </LocationsContext.Provider>
// </div> </div>
// const objectHyps = hyps.filter(hyp => !hyp.isAssumption) const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
// const assumptionHyps = hyps.filter(hyp => hyp.isAssumption) const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
// return <div id="main-assumptions"> return <div id="main-assumptions">
// <div className="goals-section-title">{t("Current Goal")}</div> <div className="goals-section-title">{t("Current Goal")}</div>
// {filter.reverse && goalLi} {filter.reverse && goalLi}
// { objectHyps.length > 0 && { objectHyps.length > 0 &&
// <div className="hyp-group"><div className="hyp-group-title">{t("Objects") + ":"}</div> <div className="hyp-group"><div className="hyp-group-title">{t("Objects") + ":"}</div>
// {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> } {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
// { assumptionHyps.length > 0 && { assumptionHyps.length > 0 &&
// <div className="hyp-group"> <div className="hyp-group">
// <div className="hyp-group-title">{t("Assumptions") + ":"}</div> <div className="hyp-group-title">{t("Assumptions") + ":"}</div>
// {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)} {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
// </div> } </div> }
// </div> </div>
// }) })
// export const OtherGoals = React.memo((props: GoalProps2) => { export const OtherGoals = React.memo((props: GoalProps2) => {
// let { t } = useTranslation() let { t } = useTranslation()
// const { goals, filter } = props const { goals, filter } = props
// return <> return <>
// {goals && goals.length > 1 && {goals && goals.length > 1 &&
// <div id="other-goals" className="other-goals"> <div id="other-goals" className="other-goals">
// <div className="goals-section-title">{t("Further Goals")}</div> <div className="goals-section-title">{t("Further Goals")}</div>
// {goals.slice(1).map((goal, i) => {goals.slice(1).map((goal, i) =>
// <details key={i}> <details key={i}>
// <summary> <summary>
// <InteractiveCode fmt={goal.type} /> <InteractiveCode fmt={goal.type} />
// </summary> </summary>
// <Goal typewriter={false} filter={filter} goal={goal} /> <Goal typewriter={false} filter={filter} goal={goal} />
// </details>)} </details>)}
// </div>} </div>}
// </> </>
// }) })
// interface GoalsProps { interface GoalsProps {
// goals: InteractiveGoalsWithHints goals: InteractiveGoalsWithHints
// filter: GoalFilterState filter: GoalFilterState
// } }
// export function Goals({ goals, filter }: GoalsProps) { export function Goals({ goals, filter }: GoalsProps) {
// if (goals.goals.length === 0) { if (goals.goals.length === 0) {
// return <></> return <></>
// } else { } else {
// return <> return <>
// {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)} {goals.goals.map((g, i) => <Goal typewriter={false} key={i} goal={g.goal} filter={filter} />)}
// </> </>
// } }
// } }
// interface FilteredGoalsProps { interface FilteredGoalsProps {
// /** Components to render in the header. */ /** Components to render in the header. */
// headerChildren: React.ReactNode headerChildren: React.ReactNode
// /** /**
// * When this is `undefined`, the component will not appear at all but will remember its state * When this is `undefined`, the component will not appear at all but will remember its state
// * by virtue of still being mounted in the React tree. When it does appear again, the filter * by virtue of still being mounted in the React tree. When it does appear again, the filter
// * settings and collapsed state will be as before. */ * settings and collapsed state will be as before. */
// goals?: InteractiveGoalsWithHints goals?: InteractiveGoalsWithHints
// } }
// /** /**
// * Display goals together with a header containing the provided children as well as buttons * Display goals together with a header containing the provided children as well as buttons
// * to control how the goals are displayed. * to control how the goals are displayed.
// */ */
// export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => { export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => {
// const ec = React.useContext(EditorContext) const ec = React.useContext(EditorContext)
// const copyToCommentButton = const copyToCommentButton =
// <a className="link pointer mh2 dim codicon codicon-quote" <a className="link pointer mh2 dim codicon codicon-quote"
// data-id="copy-goal-to-comment" data-id="copy-goal-to-comment"
// onClick={e => { onClick={e => {
// e.preventDefault(); e.preventDefault();
// if (goals) void ec.copyToComment(goalsWithHintsToString(goals)) if (goals) void ec.copyToComment(goalsWithHintsToString(goals))
// }} }}
// title="copy state to comment" /> title="copy state to comment" />
// const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>( const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
// { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }); { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true });
// const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down '); const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down ');
// const sortButton = const sortButton =
// <a className={sortClasses} title="reverse list" <a className={sortClasses} title="reverse list"
// onClick={_ => setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} /> onClick={_ => setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} />
// const mkFilterButton = (filterFn: React.SetStateAction<GoalFilterState>, filledFn: (_: GoalFilterState) => boolean, name: string) => const mkFilterButton = (filterFn: React.SetStateAction<GoalFilterState>, filledFn: (_: GoalFilterState) => boolean, name: string) =>
// <a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}> <a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}>
// <span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}>&nbsp;</span> <span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}>&nbsp;</span>
// <span className='tooltip-menu-text '>{name}</span> <span className='tooltip-menu-text '>{name}</span>
// </a> </a>
// const filterMenu = <span> const filterMenu = <span>
// {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')} {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')}
// <br/> <br/>
// {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')} {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')}
// <br/> <br/>
// {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')} {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')}
// <br/> <br/>
// {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')} {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')}
// </span> </span>
// const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue
// const filterButton = const filterButton =
// <WithTooltipOnHover mkTooltipContent={() => filterMenu}> <WithTooltipOnHover mkTooltipContent={() => filterMenu}>
// <a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/> <a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
// </WithTooltipOnHover> </WithTooltipOnHover>
// return <div style={{display: goals !== undefined ? 'block' : 'none'}}> return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
// <details open> <details open>
// <summary className='mv2 pointer'> <summary className='mv2 pointer'>
// {headerChildren} {headerChildren}
// <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span> <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span>
// </summary> </summary>
// <div className='ml1'> <div className='ml1'>
// {goals && <Goals goals={goals} filter={goalFilters}></Goals>} {goals && <Goals goals={goals} filter={goalFilters}></Goals>}
// </div> </div>
// </details> </details>
// </div> </div>
// }) })
// export function loadGoals( export function loadGoals(
// rpcSess: RpcSessionAtPos, rpcSess: RpcSessionAtPos,
// uri: string, uri: string,
// setProof: React.Dispatch<React.SetStateAction<ProofState>>, setProof: React.Dispatch<React.SetStateAction<ProofState>>,
// setCrashed: React.Dispatch<React.SetStateAction<Boolean>>) { setCrashed: React.Dispatch<React.SetStateAction<Boolean>>) {
// console.info('sending rpc request to load the proof state') console.info('sending rpc request to load the proof state')
// rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then( rpcSess.call('Game.getProofState', DocumentPosition.toTdpp({line: 0, character: 0, uri: uri})).then(
// (proof : ProofState) => { (proof : ProofState) => {
// if (typeof proof !== 'undefined') { if (typeof proof !== 'undefined') {
// console.info(`received a proof state!`) console.info(`received a proof state!`)
// console.log(proof) console.log(proof)
// setProof(proof) setProof(proof)
// setCrashed(false) setCrashed(false)
// } else { } else {
// console.warn('received undefined proof state!') console.warn('received undefined proof state!')
// setCrashed(true) setCrashed(true)
// // setProof(undefined) // setProof(undefined)
// } }
// } }
// ).catch((error) => { ).catch((error) => {
// setCrashed(true) setCrashed(true)
// console.warn(error) console.warn(error)
// }) })
// } }
// export function lastStepHasErrors (proof : ProofState): boolean { export function lastStepHasErrors (proof : ProofState): boolean {
// if (!proof?.steps.length) {return false} if (!proof?.steps.length) {return false}
// let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics] let diags = [...proof.steps[proof.steps.length - 1].diags, ...proof.diagnostics]
// return diags.some( return diags.some(
// (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
// ) )
// } }
// export function isLastStepWithErrors (proof : ProofState, i: number): boolean { export function isLastStepWithErrors (proof : ProofState, i: number): boolean {
// if (!proof?.steps.length) {return false} if (!proof?.steps.length) {return false}
// return (i == proof.steps.length - 1) && lastStepHasErrors(proof) return (i == proof.steps.length - 1) && lastStepHasErrors(proof)
// } }

884
client/src/components/infoview/info.tsx
Unescape Escape View File

@ -1,442 +1,442 @@
// /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */ /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */
// import * as React from 'react' import * as React from 'react'
// import { CircularProgress } from '@mui/material' import { CircularProgress } from '@mui/material'
// import type { Location, Diagnostic } from 'vscode-languageserver-protocol' import type { Location, Diagnostic } from 'vscode-languageserver-protocol'
// import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError, import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
// RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api' RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api'
// import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound, import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
// mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util' mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util'
// import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts' import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'
// import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget' import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget'
// import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'
// import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation' import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'
// import { AllMessages, lspDiagToInteractive } from './messages' import { AllMessages, lspDiagToInteractive } from './messages'
// // import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals' // import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals'
// import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api' import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api'
// import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from '../../state/context' import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from '../../state/context'
// import { useTranslation } from 'react-i18next' import { useTranslation } from 'react-i18next'
// import { GoalsTabs } from './main' import { GoalsTabs } from './main'
// // TODO: All about pinning could probably be removed // TODO: All about pinning could probably be removed
// type InfoKind = 'cursor' | 'pin' type InfoKind = 'cursor' | 'pin'
// interface InfoPinnable { interface InfoPinnable {
// kind: InfoKind kind: InfoKind
// /** Takes an argument for caching reasons, but should only ever (un)pin itself. */ /** Takes an argument for caching reasons, but should only ever (un)pin itself. */
// onPin: (pos: DocumentPosition) => void onPin: (pos: DocumentPosition) => void
// } }
// interface InfoStatusBarProps extends InfoPinnable, PausableProps { interface InfoStatusBarProps extends InfoPinnable, PausableProps {
// pos: DocumentPosition pos: DocumentPosition
// status: InfoStatus status: InfoStatus
// triggerUpdate: () => Promise<void> triggerUpdate: () => Promise<void>
// } }
// const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
// const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props
// const ec = React.useContext(EditorContext) const ec = React.useContext(EditorContext)
// const statusColTable: {[T in InfoStatus]: string} = { const statusColTable: {[T in InfoStatus]: string} = {
// 'updating': 'gold ', 'updating': 'gold ',
// 'error': 'dark-red ', 'error': 'dark-red ',
// 'ready': '', 'ready': '',
// } }
// const statusColor = statusColTable[status] const statusColor = statusColTable[status]
// const locationString = `${basename(pos.uri)}:${pos.line+1}:${pos.character}` const locationString = `${basename(pos.uri)}:${pos.line+1}:${pos.character}`
// const isPinned = kind === 'pin' const isPinned = kind === 'pin'
// return ( return (
// <summary style={{transition: 'color 0.5s ease'}} className={'mv2 pointer ' + statusColor}> <summary style={{transition: 'color 0.5s ease'}} className={'mv2 pointer ' + statusColor}>
// {locationString} {locationString}
// {isPinned && !isPaused && ' (pinned)'} {isPinned && !isPaused && ' (pinned)'}
// {!isPinned && isPaused && ' (paused)'} {!isPinned && isPaused && ' (paused)'}
// {isPinned && isPaused && ' (pinned and paused)'} {isPinned && isPaused && ' (pinned and paused)'}
// <span className='fr'> <span className='fr'>
// {isPinned && {isPinned &&
// <a className='link pointer mh2 dim codicon codicon-go-to-file' <a className='link pointer mh2 dim codicon codicon-go-to-file'
// data-id='reveal-file-location' data-id='reveal-file-location'
// onClick={e => { e.preventDefault(); void ec.revealPosition(pos); }} onClick={e => { e.preventDefault(); void ec.revealPosition(pos); }}
// title='reveal file location' />} title='reveal file location' />}
// <a className={'link pointer mh2 dim codicon ' + (isPinned ? 'codicon-pinned ' : 'codicon-pin ')} <a className={'link pointer mh2 dim codicon ' + (isPinned ? 'codicon-pinned ' : 'codicon-pin ')}
// data-id='toggle-pinned' data-id='toggle-pinned'
// onClick={e => { e.preventDefault(); onPin(pos); }} onClick={e => { e.preventDefault(); onPin(pos); }}
// title={isPinned ? 'unpin' : 'pin'} /> title={isPinned ? 'unpin' : 'pin'} />
// <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue ' : 'codicon-debug-pause ')} <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue ' : 'codicon-debug-pause ')}
// data-id='toggle-paused' data-id='toggle-paused'
// onClick={e => { e.preventDefault(); setPaused(!isPaused) }} onClick={e => { e.preventDefault(); setPaused(!isPaused) }}
// title={isPaused ? 'continue updating' : 'pause updating'} /> title={isPaused ? 'continue updating' : 'pause updating'} />
// <a className='link pointer mh2 dim codicon codicon-refresh' <a className='link pointer mh2 dim codicon codicon-refresh'
// data-id='update' data-id='update'
// onClick={e => { e.preventDefault(); void triggerUpdate() }} onClick={e => { e.preventDefault(); void triggerUpdate() }}
// title='update'/> title='update'/>
// </span> </span>
// </summary> </summary>
// ) )
// }) })
// interface InfoDisplayContentProps extends PausableProps { interface InfoDisplayContentProps extends PausableProps {
// pos: DocumentPosition pos: DocumentPosition
// messages: InteractiveDiagnostic[] messages: InteractiveDiagnostic[]
// goals?: InteractiveGoals goals?: InteractiveGoals
// termGoal?: InteractiveTermGoal termGoal?: InteractiveTermGoal
// error?: string error?: string
// userWidgets: UserWidgetInstance[] userWidgets: UserWidgetInstance[]
// triggerUpdate: () => Promise<void> triggerUpdate: () => Promise<void>
// proofString? : string proofString? : string
// } }
// const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
// let { t } = useTranslation() let { t } = useTranslation()
// const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proofString} = props
// const hasWidget = userWidgets.length > 0 const hasWidget = userWidgets.length > 0
// const hasError = !!error const hasError = !!error
// const hasMessages = messages.length !== 0 const hasMessages = messages.length !== 0
// const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget
// const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([]) const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([])
// React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character]) React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character])
// const locs: Locations = React.useMemo(() => ({ const locs: Locations = React.useMemo(() => ({
// isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)), isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)),
// setSelected: (l, act) => setSelectedLocs(ls => { setSelected: (l, act) => setSelectedLocs(ls => {
// // We ensure that `selectedLocs` maintains its reference identity if the selection // We ensure that `selectedLocs` maintains its reference identity if the selection
// // status of `l` didn't change. // status of `l` didn't change.
// const newLocs = ls.filter(v => !GoalsLocation.isEqual(v, l)) const newLocs = ls.filter(v => !GoalsLocation.isEqual(v, l))
// const wasSelected = newLocs.length !== ls.length const wasSelected = newLocs.length !== ls.length
// const isSelected = typeof act === 'function' ? act(wasSelected) : act const isSelected = typeof act === 'function' ? act(wasSelected) : act
// if (isSelected) newLocs.push(l) if (isSelected) newLocs.push(l)
// return wasSelected === isSelected ? ls : newLocs return wasSelected === isSelected ? ls : newLocs
// }), }),
// subexprTemplate: undefined subexprTemplate: undefined
// }), [selectedLocs]) }), [selectedLocs])
// const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true } const goalFilter = { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }
// /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
// return <> return <>
// {hasError && {hasError &&
// <div className='error' key='errors'> <div className='error' key='errors'>
// Error updating:{' '}{error}. Error updating:{' '}{error}.
// <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.</a> <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.</a>
// </div>} </div>}
// <AllMessages /> {/* TODO: Move error messages to Chat instead */} <AllMessages /> {/* TODO: Move error messages to Chat instead */}
// <LocationsContext.Provider value={locs}> <LocationsContext.Provider value={locs}>
// <div className="goals-section"> <div className="goals-section">
// { goals && goals.goals.length > 0 && <> { goals && goals.goals.length > 0 && <>
// <GoalsTabs goals={goals.goals.map(goal => ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/> <GoalsTabs goals={goals.goals.map(goal => ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/>
// {/* <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} /> {/* <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
// <OtherGoals filter={goalFilter} goals={goals.goals} /> */} <OtherGoals filter={goalFilter} goals={goals.goals} /> */}
// </>} </>}
// </div> </div>
// {/* <div> {/* <div>
// { goals && (goals.goals.length > 0 { goals && (goals.goals.length > 0
// ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /> ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
// : <div className="goals-section-title">{t("No Goals")}</div> : <div className="goals-section-title">{t("No Goals")}</div>
// )} )}
// </div> */} </div> */}
// </LocationsContext.Provider> </LocationsContext.Provider>
// {/* {userWidgets.map(widget => {/* {userWidgets.map(widget =>
// <details key={`widget::${widget.id}::${widget.range?.toString()}`} open> <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
// <summary className='mv2 pointer'>{widget.name}</summary> <summary className='mv2 pointer'>{widget.name}</summary>
// <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []} <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
// termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/> termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
// </details> </details>
// )} */} )} */}
// {/* {nothingToShow && ( {/* {nothingToShow && (
// isPaused ? isPaused ?
// /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * / /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * /
// <span>Updating is paused.{' '} <span>Updating is paused.{' '}
// <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>Refresh</a> <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>Refresh</a>
// {' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a> {' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a>
// {' '}to see information. {' '}to see information.
// </span> : </span> :
// <><CircularProgress /><div>{t("Loading goal…")}</div></>)} */} <><CircularProgress /><div>{t("Loading goal…")}</div></>)} */}
// {/* <LocationsContext.Provider value={locs}> {/* <LocationsContext.Provider value={locs}>
// {goals && goals.goals.length > 1 && <div className="goals-section other-goals"> {goals && goals.goals.length > 1 && <div className="goals-section other-goals">
// <div className="goals-section-title">Weitere Goals</div> <div className="goals-section-title">Weitere Goals</div>
// {goals.goals.slice(1).map((goal, i) => {goals.goals.slice(1).map((goal, i) =>
// <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)} <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal typewriter={false} filter={goalFilter} goal={goal} /></details>)}
// </div>} </div>}
// </LocationsContext.Provider> */} </LocationsContext.Provider> */}
// </> </>
// }) })
// interface InfoDisplayProps { interface InfoDisplayProps {
// pos: DocumentPosition, pos: DocumentPosition,
// status: InfoStatus, status: InfoStatus,
// messages: InteractiveDiagnostic[], messages: InteractiveDiagnostic[],
// proof?: ProofState, proof?: ProofState,
// goals?: InteractiveGoals, goals?: InteractiveGoals,
// termGoal?: InteractiveTermGoal, termGoal?: InteractiveTermGoal,
// error?: string, error?: string,
// userWidgets: UserWidgetInstance[], userWidgets: UserWidgetInstance[],
// rpcSess: RpcSessionAtPos, rpcSess: RpcSessionAtPos,
// triggerUpdate: () => Promise<void>, triggerUpdate: () => Promise<void>,
// } }
// /** Displays goal state and messages. Can be paused. */ /** Displays goal state and messages. Can be paused. */
// function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) { function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
// // Used to update the paused state *just once* if it is paused, // Used to update the paused state *just once* if it is paused,
// // but a display update is triggered // but a display update is triggered
// const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false) const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false)
// const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0) const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0)
// if (shouldRefresh) { if (shouldRefresh) {
// propsRef.current = props0 propsRef.current = props0
// setShouldRefresh(false) setShouldRefresh(false)
// } }
// const triggerDisplayUpdate = async () => { const triggerDisplayUpdate = async () => {
// await props0.triggerUpdate() await props0.triggerUpdate()
// setShouldRefresh(true) setShouldRefresh(true)
// } }
// const {kind, goals, rpcSess} = props const {kind, goals, rpcSess} = props
// const ec = React.useContext(EditorContext) const ec = React.useContext(EditorContext)
// // If we are the cursor infoview, then we should subscribe to // If we are the cursor infoview, then we should subscribe to
// // some commands from the editor extension // some commands from the editor extension
// const isCursor = kind === 'cursor' const isCursor = kind === 'cursor'
// useEvent(ec.events.requestedAction, act => { useEvent(ec.events.requestedAction, act => {
// if (!isCursor) return if (!isCursor) return
// if (act.kind !== 'copyToComment') return if (act.kind !== 'copyToComment') return
// if (goals) void ec.copyToComment(goalsToString(goals)) if (goals) void ec.copyToComment(goalsToString(goals))
// }, [goals]) }, [goals])
// useEvent(ec.events.requestedAction, act => { useEvent(ec.events.requestedAction, act => {
// if (!isCursor) return if (!isCursor) return
// if (act.kind !== 'togglePaused') return if (act.kind !== 'togglePaused') return
// setPaused(isPaused => !isPaused) setPaused(isPaused => !isPaused)
// }) })
// const editor = React.useContext(MonacoEditorContext) const editor = React.useContext(MonacoEditorContext)
// return ( return (
// <RpcContext.Provider value={rpcSess}> <RpcContext.Provider value={rpcSess}>
// {/* <details open> */} {/* <details open> */}
// {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */} {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
// <div className="vscode-light"> <div className="vscode-light">
// <InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> <InfoDisplayContent {...props} proofString={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
// </div> </div>
// {/* </details> */} {/* </details> */}
// </RpcContext.Provider> </RpcContext.Provider>
// ) )
// } }
// /** /**
// * Note: in the cursor view, we have to keep the cursor position as part of the component state * Note: in the cursor view, we have to keep the cursor position as part of the component state
// * to avoid flickering when the cursor moved. Otherwise, the component is re-initialised and the * to avoid flickering when the cursor moved. Otherwise, the component is re-initialised and the
// * goal states reset to `undefined` on cursor moves. * goal states reset to `undefined` on cursor moves.
// */ */
// export type InfoProps = InfoPinnable & { pos?: DocumentPosition } export type InfoProps = InfoPinnable & { pos?: DocumentPosition }
// /** Fetches info from the server and renders an {@link InfoDisplay}. */ /** Fetches info from the server and renders an {@link InfoDisplay}. */
// export function Info(props: InfoProps) { export function Info(props: InfoProps) {
// if (props.kind === 'cursor') return <InfoAtCursor {...props} /> if (props.kind === 'cursor') return <InfoAtCursor {...props} />
// else return <InfoAux {...props} pos={props.pos} /> else return <InfoAux {...props} pos={props.pos} />
// } }
// function InfoAtCursor(props: InfoProps) { function InfoAtCursor(props: InfoProps) {
// const ec = React.useContext(EditorContext) const ec = React.useContext(EditorContext)
// // eslint-disable-next-line @typescript-eslint/no-non-null-assertion // eslint-disable-next-line @typescript-eslint/no-non-null-assertion
// const [curLoc, setCurLoc] = React.useState<Location>(ec.events.changedCursorLocation.current!) const [curLoc, setCurLoc] = React.useState<Location>(ec.events.changedCursorLocation.current!)
// useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), []) useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), [])
// const pos = { uri: curLoc.uri, ...curLoc.range.start } const pos = { uri: curLoc.uri, ...curLoc.range.start }
// return <InfoAux {...props} pos={pos} /> return <InfoAux {...props} pos={pos} />
// } }
// function useIsProcessingAt(p: DocumentPosition): boolean { function useIsProcessingAt(p: DocumentPosition): boolean {
// const allProgress = React.useContext(ProgressContext) const allProgress = React.useContext(ProgressContext)
// const processing = allProgress.get(p.uri) const processing = allProgress.get(p.uri)
// if (!processing) return false if (!processing) return false
// return processing.some(i => RangeHelpers.contains(i.range, p)) return processing.some(i => RangeHelpers.contains(i.range, p))
// } }
// function InfoAux(props: InfoProps) { function InfoAux(props: InfoProps) {
// const { setProof } = React.useContext(ProofContext) const { setProof } = React.useContext(ProofContext)
// const config = React.useContext(ConfigContext) const config = React.useContext(ConfigContext)
// // eslint-disable-next-line @typescript-eslint/no-non-null-assertion // eslint-disable-next-line @typescript-eslint/no-non-null-assertion
// const pos = props.pos! const pos = props.pos!
// const rpcSess = useRpcSessionAtPos(pos) const rpcSess = useRpcSessionAtPos(pos)
// // Compute the LSP diagnostics at this info's position. We try to ensure that if these remain // Compute the LSP diagnostics at this info's position. We try to ensure that if these remain
// // the same, then so does the identity of `lspDiagsHere` so that it can be used as a dep. // the same, then so does the identity of `lspDiagsHere` so that it can be used as a dep.
// const lspDiags = React.useContext(LspDiagnosticsContext) const lspDiags = React.useContext(LspDiagnosticsContext)
// const [lspDiagsHere, setLspDiagsHere] = React.useState<Diagnostic[]>([]) const [lspDiagsHere, setLspDiagsHere] = React.useState<Diagnostic[]>([])
// React.useEffect(() => { React.useEffect(() => {
// // Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b // Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b
// setLspDiagsHere(diags0 => { setLspDiagsHere(diags0 => {
// const diagPred = (d: Diagnostic) => const diagPred = (d: Diagnostic) =>
// RangeHelpers.contains(d.range, pos, config.allErrorsOnLine) RangeHelpers.contains(d.range, pos, config.allErrorsOnLine)
// const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred) const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred)
// if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0 if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0
// return newDiags return newDiags
// }) })
// }, [lspDiags, pos.uri, pos.line, pos.character, config.allErrorsOnLine]) }, [lspDiags, pos.uri, pos.line, pos.character, config.allErrorsOnLine])
// const serverIsProcessing = useIsProcessingAt(pos) const serverIsProcessing = useIsProcessingAt(pos)
// // This is a virtual dep of the info-requesting function. It is bumped whenever the Lean server // This is a virtual dep of the info-requesting function. It is bumped whenever the Lean server
// // indicates that another request should be made. Bumping it dirties the dep state of // indicates that another request should be made. Bumping it dirties the dep state of
// // `useAsyncWithTrigger` below, causing the `useEffect` lower down in this component to // `useAsyncWithTrigger` below, causing the `useEffect` lower down in this component to
// // make the request. We cannot simply call `triggerUpdateCore` because `useAsyncWithTrigger` // make the request. We cannot simply call `triggerUpdateCore` because `useAsyncWithTrigger`
// // does not support reentrancy like that. // does not support reentrancy like that.
// const [updaterTick, setUpdaterTick] = React.useState<number>(0) const [updaterTick, setUpdaterTick] = React.useState<number>(0)
// // For atomicity, we use a single update function that fetches all the info at `pos` at once. // For atomicity, we use a single update function that fetches all the info at `pos` at once.
// // Besides what the server replies with, we also include the inputs (deps) in this type so // Besides what the server replies with, we also include the inputs (deps) in this type so
// // that the displayed state cannot ever get out of sync by showing an old reply together // that the displayed state cannot ever get out of sync by showing an old reply together
// // with e.g. a new `pos`. // with e.g. a new `pos`.
// type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'> type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
// const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => { const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => {
// const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos)).catch((error) => { const proofReq = rpcSess.call('Game.getProofState', DocumentPosition.toTdpp(pos)).catch((error) => {
// console.warn(error) console.warn(error)
// }) })
// const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos)) const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos))
// const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos)) const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
// const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound) const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound)
// const messagesReq = getInteractiveDiagnostics(rpcSess, {start: pos.line, end: pos.line+1}) const messagesReq = getInteractiveDiagnostics(rpcSess, {start: pos.line, end: pos.line+1})
// // fall back to non-interactive diagnostics when lake fails // fall back to non-interactive diagnostics when lake fails
// // (see https://github.com/leanprover/vscode-lean4/issues/90) // (see https://github.com/leanprover/vscode-lean4/issues/90)
// .then(diags => diags.length === 0 ? lspDiagsHere.map(lspDiagToInteractive) : diags) .then(diags => diags.length === 0 ? lspDiagsHere.map(lspDiagToInteractive) : diags)
// // While `lake print-paths` is running, the output of Lake is shown as // While `lake print-paths` is running, the output of Lake is shown as
// // info diagnostics on line 1. However, all RPC requests block until // info diagnostics on line 1. However, all RPC requests block until
// // Lake is finished, so we don't see these diagnostics while Lake is // Lake is finished, so we don't see these diagnostics while Lake is
// // building. Therefore we show the LSP diagnostics on line 1 if the // building. Therefore we show the LSP diagnostics on line 1 if the
// // server does not respond within half a second. // server does not respond within half a second.
// if (pos.line === 0 && lspDiagsHere.length) { if (pos.line === 0 && lspDiagsHere.length) {
// setTimeout(() => resolve({ setTimeout(() => resolve({
// pos, pos,
// status: 'updating', status: 'updating',
// messages: lspDiagsHere.map(lspDiagToInteractive), messages: lspDiagsHere.map(lspDiagToInteractive),
// proof: undefined, proof: undefined,
// goals: undefined, goals: undefined,
// termGoal: undefined, termGoal: undefined,
// error: undefined, error: undefined,
// userWidgets: [], userWidgets: [],
// rpcSess rpcSess
// }), 500) }), 500)
// } }
// // NB: it is important to await await reqs at once, otherwise // NB: it is important to await await reqs at once, otherwise
// // if both throw then one exception becomes unhandled. // if both throw then one exception becomes unhandled.
// Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then( Promise.all([proofReq, goalsReq, termGoalReq, widgetsReq, messagesReq]).then(
// ([proof, goals, termGoal, userWidgets, messages]) => resolve({ ([proof, goals, termGoal, userWidgets, messages]) => resolve({
// pos, pos,
// status: 'ready', status: 'ready',
// messages, messages,
// proof : proof as any, proof : proof as any,
// goals: goals as any, goals: goals as any,
// termGoal, termGoal,
// error: undefined, error: undefined,
// userWidgets: userWidgets?.widgets ?? [], userWidgets: userWidgets?.widgets ?? [],
// rpcSess rpcSess
// }), }),
// ex => { ex => {
// if (ex?.code === RpcErrorCode.ContentModified || if (ex?.code === RpcErrorCode.ContentModified ||
// ex?.code === RpcErrorCode.RpcNeedsReconnect) { ex?.code === RpcErrorCode.RpcNeedsReconnect) {
// // Document has been changed since we made the request, or we need to reconnect // Document has been changed since we made the request, or we need to reconnect
// // to the RPC sessions. Try again. // to the RPC sessions. Try again.
// setUpdaterTick(t => t + 1) setUpdaterTick(t => t + 1)
// reject('retry') reject('retry')
// } }
// let errorString = '' let errorString = ''
// if (typeof ex === 'string') { if (typeof ex === 'string') {
// errorString = ex errorString = ex
// } else if (isRpcError(ex)) { } else if (isRpcError(ex)) {
// errorString = mapRpcError(ex).message errorString = mapRpcError(ex).message
// } else if (ex instanceof Error) { } else if (ex instanceof Error) {
// errorString = ex.toString() errorString = ex.toString()
// } else { } else {
// errorString = `Unrecognized error: ${JSON.stringify(ex)}` errorString = `Unrecognized error: ${JSON.stringify(ex)}`
// } }
// resolve({ resolve({
// pos, pos,
// status: 'error', status: 'error',
// messages: lspDiagsHere.map(lspDiagToInteractive), messages: lspDiagsHere.map(lspDiagToInteractive),
// proof: undefined, proof: undefined,
// goals: undefined, goals: undefined,
// termGoal: undefined, termGoal: undefined,
// error: `Error fetching goals: ${errorString}`, error: `Error fetching goals: ${errorString}`,
// userWidgets: [], userWidgets: [],
// rpcSess rpcSess
// }) })
// } }
// ) )
// }), [updaterTick, pos.uri, pos.line, pos.character, rpcSess, serverIsProcessing, lspDiagsHere]) }), [updaterTick, pos.uri, pos.line, pos.character, rpcSess, serverIsProcessing, lspDiagsHere])
// // We use a timeout to debounce info requests. Whenever a request is already scheduled // We use a timeout to debounce info requests. Whenever a request is already scheduled
// // but something happens that warrants a request for newer info, we cancel the old request // but something happens that warrants a request for newer info, we cancel the old request
// // and schedule just the new one. // and schedule just the new one.
// const updaterTimeout = React.useRef<number>() const updaterTimeout = React.useRef<number>()
// const clearUpdaterTimeout = () => { const clearUpdaterTimeout = () => {
// if (updaterTimeout.current) { if (updaterTimeout.current) {
// window.clearTimeout(updaterTimeout.current) window.clearTimeout(updaterTimeout.current)
// updaterTimeout.current = undefined updaterTimeout.current = undefined
// } }
// } }
// const triggerUpdate = React.useCallback(() => new Promise<void>(resolve => { const triggerUpdate = React.useCallback(() => new Promise<void>(resolve => {
// clearUpdaterTimeout() clearUpdaterTimeout()
// const tm = window.setTimeout(() => { const tm = window.setTimeout(() => {
// void triggerUpdateCore().then(resolve) void triggerUpdateCore().then(resolve)
// updaterTimeout.current = undefined updaterTimeout.current = undefined
// }, config.debounceTime) }, config.debounceTime)
// // Hack: even if the request is cancelled, the promise should resolve so that no `await` // Hack: even if the request is cancelled, the promise should resolve so that no `await`
// // is left waiting forever. We ensure this happens in a simple way. // is left waiting forever. We ensure this happens in a simple way.
// window.setTimeout(resolve, config.debounceTime) window.setTimeout(resolve, config.debounceTime)
// updaterTimeout.current = tm updaterTimeout.current = tm
// }), [triggerUpdateCore, config.debounceTime]) }), [triggerUpdateCore, config.debounceTime])
// const [displayProps, setDisplayProps] = React.useState<InfoDisplayProps>({ const [displayProps, setDisplayProps] = React.useState<InfoDisplayProps>({
// pos, pos,
// status: 'updating', status: 'updating',
// messages: [], messages: [],
// proof: undefined, proof: undefined,
// goals: undefined, goals: undefined,
// termGoal: undefined, termGoal: undefined,
// error: undefined, error: undefined,
// userWidgets: [], userWidgets: [],
// rpcSess, rpcSess,
// triggerUpdate triggerUpdate
// }) })
// // Propagates changes in the state of async info requests to the display props, // Propagates changes in the state of async info requests to the display props,
// // and re-requests info if needed. // and re-requests info if needed.
// // This effect triggers new requests for info whenever need. It also propagates changes // This effect triggers new requests for info whenever need. It also propagates changes
// // in the state of the `useAsyncWithTrigger` to the displayed props. // in the state of the `useAsyncWithTrigger` to the displayed props.
// React.useEffect(() => { React.useEffect(() => {
// if (state.state === 'notStarted') if (state.state === 'notStarted')
// void triggerUpdate() void triggerUpdate()
// else if (state.state === 'loading') { else if (state.state === 'loading') {
// setDisplayProps(dp => ({ ...dp, status: 'updating' })) setDisplayProps(dp => ({ ...dp, status: 'updating' }))
// } }
// else if (state.state === 'resolved') { else if (state.state === 'resolved') {
// // if (state.value.goals?.goals?.length) { // if (state.value.goals?.goals?.length) {
// // hintContext.setHints(state.value.goals.goals[0].hints) // hintContext.setHints(state.value.goals.goals[0].hints)
// // } // }
// setDisplayProps({ ...state.value, triggerUpdate }) setDisplayProps({ ...state.value, triggerUpdate })
// // Update the game's proof state // Update the game's proof state
// console.info('updating proof from editor mode.') console.info('updating proof from editor mode.')
// setProof(state.value.proof) setProof(state.value.proof)
// } else if (state.state === 'rejected' && state.error !== 'retry') { } else if (state.state === 'rejected' && state.error !== 'retry') {
// // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception. // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception.
// console.warn('Unreachable code reached with error: ', state.error) console.warn('Unreachable code reached with error: ', state.error)
// } }
// }, [state]) }, [state])
// return <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} /> return <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} />
// } }

266
client/src/components/infoview/infos.tsx
Unescape Escape View File

@ -1,133 +1,133 @@
// /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/infos.tsx */ /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/infos.tsx */
// import * as React from 'react'; import * as React from 'react';
// import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentContentChangeEvent } from 'vscode-languageserver-protocol'; import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentContentChangeEvent } from 'vscode-languageserver-protocol';
// import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
// import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util';
// import { Info, InfoProps } from './info'; import { Info, InfoProps } from './info';
// import { useTranslation } from 'react-i18next'; import { useTranslation } from 'react-i18next';
// /** Manages and displays pinned infos, as well as info for the current location. */ /** Manages and displays pinned infos, as well as info for the current location. */
// export function Infos() { export function Infos() {
// let { t } = useTranslation() let { t } = useTranslation()
// const ec = React.useContext(EditorContext); const ec = React.useContext(EditorContext);
// // Update pins when the document changes. In particular, when edits are made // 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. // earlier in the text such that a pin has to move up or down.
// const [pinnedPositions, setPinnedPositions] = useClientNotificationState( const [pinnedPositions, setPinnedPositions] = useClientNotificationState(
// 'textDocument/didChange', 'textDocument/didChange',
// new Array<Keyed<DocumentPosition>>(), new Array<Keyed<DocumentPosition>>(),
// (pinnedPositions, params: DidChangeTextDocumentParams) => { (pinnedPositions, params: DidChangeTextDocumentParams) => {
// if (pinnedPositions.length === 0) return pinnedPositions; if (pinnedPositions.length === 0) return pinnedPositions;
// let changed: boolean = false; let changed: boolean = false;
// const newPins = pinnedPositions.map(pin => { const newPins = pinnedPositions.map(pin => {
// if (pin.uri !== params.textDocument.uri) return pin; if (pin.uri !== params.textDocument.uri) return pin;
// // NOTE(WN): It's important to make a clone here, otherwise this // NOTE(WN): It's important to make a clone here, otherwise this
// // actually mutates the pin. React state updates must be pure. // actually mutates the pin. React state updates must be pure.
// // See https://github.com/facebook/react/issues/12856 // See https://github.com/facebook/react/issues/12856
// const newPin: Keyed<DocumentPosition> = { ...pin }; const newPin: Keyed<DocumentPosition> = { ...pin };
// for (const chg of params.contentChanges) { for (const chg of params.contentChanges) {
// if (!TextDocumentContentChangeEvent.isIncremental(chg)) { if (!TextDocumentContentChangeEvent.isIncremental(chg)) {
// changed = true; changed = true;
// return null; return null;
// } }
// if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.start)) continue; if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.start)) continue;
// // We can assume chg.range.start < pin // We can assume chg.range.start < pin
// // If the pinned position is replaced with new text, just delete the pin. // If the pinned position is replaced with new text, just delete the pin.
// if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.end)) { if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.end)) {
// changed = true; changed = true;
// return null; return null;
// } }
// const oldPin = { ...newPin }; const oldPin = { ...newPin };
// // How many lines before the pin position were added by the change. // How many lines before the pin position were added by the change.
// // Can be negative when more lines are removed than added. // Can be negative when more lines are removed than added.
// let additionalLines = 0; let additionalLines = 0;
// let lastLineLen = chg.range.start.character; let lastLineLen = chg.range.start.character;
// for (const c of chg.text) for (const c of chg.text)
// if (c === '\n') { if (c === '\n') {
// additionalLines++; additionalLines++;
// lastLineLen = 0; lastLineLen = 0;
// } else lastLineLen++; } else lastLineLen++;
// // Subtract lines that were already present // Subtract lines that were already present
// additionalLines -= (chg.range.end.line - chg.range.start.line) additionalLines -= (chg.range.end.line - chg.range.start.line)
// newPin.line += additionalLines; newPin.line += additionalLines;
// if (oldPin.line < chg.range.end.line) { if (oldPin.line < chg.range.end.line) {
// // Should never execute by the <= check above. // Should never execute by the <= check above.
// throw new Error('unreachable code reached') throw new Error('unreachable code reached')
// } else if (oldPin.line === chg.range.end.line) { } else if (oldPin.line === chg.range.end.line) {
// newPin.character = lastLineLen + (oldPin.character - chg.range.end.character); newPin.character = lastLineLen + (oldPin.character - chg.range.end.character);
// } }
// } }
// if (!DocumentPosition.isEqual(newPin, pin)) changed = true; if (!DocumentPosition.isEqual(newPin, pin)) changed = true;
// // NOTE(WN): We maintain the `key` when a pin is moved around to maintain // NOTE(WN): We maintain the `key` when a pin is moved around to maintain
// // its component identity and minimise flickering. // its component identity and minimise flickering.
// return newPin; return newPin;
// }); });
// if (changed) return newPins.filter(p => p !== null) as Keyed<DocumentPosition>[]; if (changed) return newPins.filter(p => p !== null) as Keyed<DocumentPosition>[];
// return pinnedPositions; return pinnedPositions;
// }, },
// [] []
// ); );
// // Remove pins for closed documents // Remove pins for closed documents
// useClientNotificationEffect( useClientNotificationEffect(
// 'textDocument/didClose', 'textDocument/didClose',
// (params: DidCloseTextDocumentParams) => { (params: DidCloseTextDocumentParams) => {
// setPinnedPositions(pinnedPositions => pinnedPositions.filter(p => p.uri !== params.textDocument.uri)); setPinnedPositions(pinnedPositions => pinnedPositions.filter(p => p.uri !== params.textDocument.uri));
// }, },
// [] []
// ); );
// const curPos: DocumentPosition | undefined = const curPos: DocumentPosition | undefined =
// useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined)
// // Update pins on UI actions // Update pins on UI actions
// const pinKey = React.useRef<number>(0); const pinKey = React.useRef<number>(0);
// const isPinned = (pinnedPositions: DocumentPosition[], pos: DocumentPosition) => { const isPinned = (pinnedPositions: DocumentPosition[], pos: DocumentPosition) => {
// return pinnedPositions.some(p => DocumentPosition.isEqual(p, pos)); return pinnedPositions.some(p => DocumentPosition.isEqual(p, pos));
// } }
// const pin = React.useCallback((pos: DocumentPosition) => { const pin = React.useCallback((pos: DocumentPosition) => {
// setPinnedPositions(pinnedPositions => { setPinnedPositions(pinnedPositions => {
// if (isPinned(pinnedPositions, pos)) return pinnedPositions; if (isPinned(pinnedPositions, pos)) return pinnedPositions;
// pinKey.current += 1; pinKey.current += 1;
// return [ ...pinnedPositions, { ...pos, key: pinKey.current.toString() } ]; return [ ...pinnedPositions, { ...pos, key: pinKey.current.toString() } ];
// }); });
// }, []); }, []);
// const unpin = React.useCallback((pos: DocumentPosition) => { const unpin = React.useCallback((pos: DocumentPosition) => {
// setPinnedPositions(pinnedPositions => { setPinnedPositions(pinnedPositions => {
// if (!isPinned(pinnedPositions, pos)) return pinnedPositions; if (!isPinned(pinnedPositions, pos)) return pinnedPositions;
// return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, pos)); return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, pos));
// }); });
// }, []); }, []);
// // Toggle pin at current position when the editor requests it // Toggle pin at current position when the editor requests it
// useEvent(ec.events.requestedAction, act => { useEvent(ec.events.requestedAction, act => {
// if (act.kind !== 'togglePin') return if (act.kind !== 'togglePin') return
// if (!curPos) return if (!curPos) return
// setPinnedPositions(pinnedPositions => { setPinnedPositions(pinnedPositions => {
// if (isPinned(pinnedPositions, curPos)) { if (isPinned(pinnedPositions, curPos)) {
// return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, curPos)); return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, curPos));
// } else { } else {
// pinKey.current += 1; pinKey.current += 1;
// return [ ...pinnedPositions, { ...curPos, key: pinKey.current.toString() } ]; return [ ...pinnedPositions, { ...curPos, key: pinKey.current.toString() } ];
// } }
// }); });
// }, [curPos?.uri, curPos?.line, curPos?.character]); }, [curPos?.uri, curPos?.line, curPos?.character]);
// const infoProps: Keyed<InfoProps>[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key })); const infoProps: Keyed<InfoProps>[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key }));
// if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' }); if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' });
// return <div> return <div>
// {infoProps.map (ps => <Info {...ps} />)} {infoProps.map (ps => <Info {...ps} />)}
// {!curPos && <p>{t("Click somewhere in the Lean file to enable the infoview.")}</p> } {!curPos && <p>{t("Click somewhere in the Lean file to enable the infoview.")}</p> }
// </div>; </div>;
// } }

1052
client/src/components/infoview/main.tsx
View File

File diff suppressed because it is too large Load Diff

480
client/src/components/infoview/messages.tsx
Unescape Escape View File

@ -1,240 +1,240 @@
// import * as React from 'react' import * as React from 'react'
// import fastIsEqual from 'react-fast-compare' import fastIsEqual from 'react-fast-compare'
// import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol' import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol'
// import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api' import { LeanDiagnostic, RpcErrorCode, getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api'
// import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util' import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'
// import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts' import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'
// import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing' import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing'
// import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer' import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer'
// import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'
// import { PageContext } from '../../state/context' import { PageContext } from '../../state/context'
// import { useTranslation } from 'react-i18next' import { useTranslation } from 'react-i18next'
// interface MessageViewProps { interface MessageViewProps {
// uri: DocumentUri; uri: DocumentUri;
// diag: InteractiveDiagnostic; diag: InteractiveDiagnostic;
// } }
// /** A list of messages (info/warning/error) that are produced after this command */ /** A list of messages (info/warning/error) that are produced after this command */
// function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) { function Error({error, typewriterMode} : {error : InteractiveDiagnostic, typewriterMode : boolean}) {
// // The first step will always have an empty command // The first step will always have an empty command
// const severityClass = error.severity ? { const severityClass = error.severity ? {
// [DiagnosticSeverity.Error]: 'error', [DiagnosticSeverity.Error]: 'error',
// [DiagnosticSeverity.Warning]: 'warning', [DiagnosticSeverity.Warning]: 'warning',
// [DiagnosticSeverity.Information]: 'information', [DiagnosticSeverity.Information]: 'information',
// [DiagnosticSeverity.Hint]: 'hint', [DiagnosticSeverity.Hint]: 'hint',
// }[error.severity] : ''; }[error.severity] : '';
// const {line, character} = error.range.start; const {line, character} = error.range.start;
// const title = `Line ${line+1}, Character ${character}`; const title = `Line ${line+1}, Character ${character}`;
// // Hide "unsolved goals" messages // Hide "unsolved goals" messages
// let message; let message;
// if ("append" in error.message && "text" in error.message.append[0] && if ("append" in error.message && "text" in error.message.append[0] &&
// error.message?.append[0].text === "unsolved goals") { error.message?.append[0].text === "unsolved goals") {
// message = error.message.append[0] message = error.message.append[0]
// } else { } else {
// message = error.message message = error.message
// } }
// return <div className={severityClass + ' ml1 message'}> return <div className={severityClass + ' ml1 message'}>
// {!typewriterMode && <p className="mv2">{title}</p>} {!typewriterMode && <p className="mv2">{title}</p>}
// <pre className="font-code pre-wrap"> <pre className="font-code pre-wrap">
// <InteractiveMessage fmt={message} /> <InteractiveMessage fmt={message} />
// </pre> </pre>
// </div> </div>
// } }
// // TODO: Should not use index as key. // TODO: Should not use index as key.
// /** A list of messages (info/warning/error) that are produced after this command */ /** A list of messages (info/warning/error) that are produced after this command */
// export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) { export function Errors ({errors, typewriterMode} : {errors : InteractiveDiagnostic[], typewriterMode : boolean}) {
// return <div> return <div>
// {errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))} {errors.map((err, i) => (<Error key={`error-${i}`} error={err} typewriterMode={typewriterMode}/>))}
// </div> </div>
// } }
// const MessageView = React.memo(({uri, diag}: MessageViewProps) => { const MessageView = React.memo(({uri, diag}: MessageViewProps) => {
// const ec = React.useContext(EditorContext); const ec = React.useContext(EditorContext);
// const fname = escapeHtml(basename(uri)); const fname = escapeHtml(basename(uri));
// const {line, character} = diag.range.start; const {line, character} = diag.range.start;
// const loc: Location = { uri, range: diag.range }; const loc: Location = { uri, range: diag.range };
// const text = TaggedText_stripTags(diag.message); const text = TaggedText_stripTags(diag.message);
// const severityClass = diag.severity ? { const severityClass = diag.severity ? {
// [DiagnosticSeverity.Error]: 'error', [DiagnosticSeverity.Error]: 'error',
// [DiagnosticSeverity.Warning]: 'warning', [DiagnosticSeverity.Warning]: 'warning',
// [DiagnosticSeverity.Information]: 'information', [DiagnosticSeverity.Information]: 'information',
// [DiagnosticSeverity.Hint]: 'hint', [DiagnosticSeverity.Hint]: 'hint',
// }[diag.severity] : ''; }[diag.severity] : '';
// const title = `Line ${line+1}, Character ${character}`; const title = `Line ${line+1}, Character ${character}`;
// // Hide "unsolved goals" messages // Hide "unsolved goals" messages
// let message; let message;
// if ("append" in diag.message && "text" in diag.message.append[0] && if ("append" in diag.message && "text" in diag.message.append[0] &&
// diag.message?.append[0].text === "unsolved goals") { diag.message?.append[0].text === "unsolved goals") {
// message = diag.message.append[0] message = diag.message.append[0]
// } else { } else {
// message = diag.message message = diag.message
// } }
// const { typewriterMode, lockEditorMode } = React.useContext(PageContext) const { typewriterMode, lockEditorMode } = React.useContext(PageContext)
// return ( return (
// // <details open> // <details open>
// // <summary className={severityClass + ' mv2 pointer'}>{title} // <summary className={severityClass + ' mv2 pointer'}>{title}
// // <span className="fr"> // <span className="fr">
// // <a className="link pointer mh2 dim codicon codicon-go-to-file" // <a className="link pointer mh2 dim codicon codicon-go-to-file"
// // onClick={e => { e.preventDefault(); void ec.revealLocation(loc); }} // onClick={e => { e.preventDefault(); void ec.revealLocation(loc); }}
// // title="reveal file location"></a> // title="reveal file location"></a>
// // <a className="link pointer mh2 dim codicon codicon-quote" // <a className="link pointer mh2 dim codicon codicon-quote"
// // data-id="copy-to-comment" // data-id="copy-to-comment"
// // onClick={e => {e.preventDefault(); void ec.copyToComment(text)}} // onClick={e => {e.preventDefault(); void ec.copyToComment(text)}}
// // title="copy message to comment"></a> // title="copy message to comment"></a>
// // <a className="link pointer mh2 dim codicon codicon-clippy" // <a className="link pointer mh2 dim codicon codicon-clippy"
// // onClick={e => {e.preventDefault(); void ec.api.copyToClipboard(text)}} // onClick={e => {e.preventDefault(); void ec.api.copyToClipboard(text)}}
// // title="copy message to clipboard"></a> // title="copy message to clipboard"></a>
// // </span> // </span>
// // </summary> // </summary>
// <div className={severityClass + ' ml1 message'}> <div className={severityClass + ' ml1 message'}>
// {!(typewriterMode && !lockEditorMode) && <p className="mv2">{title}</p>} {!(typewriterMode && !lockEditorMode) && <p className="mv2">{title}</p>}
// <pre className="font-code pre-wrap"> <pre className="font-code pre-wrap">
// <InteractiveMessage fmt={message} /> <InteractiveMessage fmt={message} />
// </pre> </pre>
// </div> </div>
// // </details> // </details>
// ) )
// }, fastIsEqual) }, fastIsEqual)
// function mkMessageViewProps(uri: DocumentUri, messages: InteractiveDiagnostic[]): MessageViewProps[] { function mkMessageViewProps(uri: DocumentUri, messages: InteractiveDiagnostic[]): MessageViewProps[] {
// const views: MessageViewProps[] = messages const views: MessageViewProps[] = messages
// .sort((msga, msgb) => { .sort((msga, msgb) => {
// const a = msga.fullRange?.end || msga.range.end; const a = msga.fullRange?.end || msga.range.end;
// const b = msgb.fullRange?.end || msgb.range.end; const b = msgb.fullRange?.end || msgb.range.end;
// return a.line === b.line ? a.character - b.character : a.line - b.line return a.line === b.line ? a.character - b.character : a.line - b.line
// }).map(m => { }).map(m => {
// return { uri, diag: m }; return { uri, diag: m };
// }); });
// return addUniqueKeys(views, v => DocumentPosition.toString({uri: v.uri, ...v.diag.range.start})); return addUniqueKeys(views, v => DocumentPosition.toString({uri: v.uri, ...v.diag.range.start}));
// } }
// /** Shows the given messages assuming they are for the given file. */ /** Shows the given messages assuming they are for the given file. */
// export const MessagesList = React.memo(({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) => { export const MessagesList = React.memo(({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) => {
// const should_hide = messages.length === 0; const should_hide = messages.length === 0;
// if (should_hide) { return <></> } if (should_hide) { return <></> }
// return ( return (
// <div> <div>
// {mkMessageViewProps(uri, messages).map(m => <MessageView {...m} />)} {mkMessageViewProps(uri, messages).map(m => <MessageView {...m} />)}
// </div> </div>
// ); );
// }) })
// function lazy<T>(f: () => T): () => T { function lazy<T>(f: () => T): () => T {
// let state: {t: T} | undefined let state: {t: T} | undefined
// return () => { return () => {
// if (!state) state = {t: f()} if (!state) state = {t: f()}
// return state.t return state.t
// } }
// } }
// /** Displays all messages for the specified file. Can be paused. */ /** Displays all messages for the specified file. Can be paused. */
// export function AllMessages() { export function AllMessages() {
// const ec = React.useContext(EditorContext); const ec = React.useContext(EditorContext);
// const sv = React.useContext(VersionContext); const sv = React.useContext(VersionContext);
// const curPos: DocumentPosition | undefined = const curPos: DocumentPosition | undefined =
// useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined)
// const rs0 = useRpcSessionAtPos({ uri: curPos.uri, line: 0, character: 0 }); const rs0 = useRpcSessionAtPos({ uri: curPos.uri, line: 0, character: 0 });
// const dc = React.useContext(LspDiagnosticsContext); const dc = React.useContext(LspDiagnosticsContext);
// const config = React.useContext(ConfigContext); const config = React.useContext(ConfigContext);
// const diags0 = dc.get(curPos.uri) || []; const diags0 = dc.get(curPos.uri) || [];
// const iDiags0 = React.useMemo(() => lazy(async () => { const iDiags0 = React.useMemo(() => lazy(async () => {
// try { try {
// const diags = await getInteractiveDiagnostics(rs0); const diags = await getInteractiveDiagnostics(rs0);
// if (diags.length > 0) { if (diags.length > 0) {
// return diags return diags
// } }
// } catch (err: any) { } catch (err: any) {
// if (err?.code === RpcErrorCode.ContentModified) { if (err?.code === RpcErrorCode.ContentModified) {
// // Document has been changed since we made the request. This can happen // Document has been changed since we made the request. This can happen
// // while typing quickly. When the server catches up on next edit, it will // while typing quickly. When the server catches up on next edit, it will
// // send new diagnostics to which the infoview responds by calling // send new diagnostics to which the infoview responds by calling
// // `getInteractiveDiagnostics` again. // `getInteractiveDiagnostics` again.
// } else { } else {
// console.log('getInteractiveDiagnostics error ', err) console.log('getInteractiveDiagnostics error ', err)
// } }
// } }
// return diags0.map(d => ({ ...(d as LeanDiagnostic), message: { text: d.message } })); return diags0.map(d => ({ ...(d as LeanDiagnostic), message: { text: d.message } }));
// }), [sv, rs0, curPos.uri, diags0]); }), [sv, rs0, curPos.uri, diags0]);
// const [{ isPaused, setPaused }, [uri, rs, diags, iDiags], _] = usePausableState(false, [curPos.uri, rs0, diags0, iDiags0]); const [{ isPaused, setPaused }, [uri, rs, diags, iDiags], _] = usePausableState(false, [curPos.uri, rs0, diags0, iDiags0]);
// // Fetch interactive diagnostics when we're entering the paused state // Fetch interactive diagnostics when we're entering the paused state
// // (if they haven't already been fetched before) // (if they haven't already been fetched before)
// React.useEffect(() => { if (isPaused) { void iDiags() } }, [iDiags, isPaused]); React.useEffect(() => { if (isPaused) { void iDiags() } }, [iDiags, isPaused]);
// const setOpenRef = React.useRef<React.Dispatch<React.SetStateAction<boolean>>>(); const setOpenRef = React.useRef<React.Dispatch<React.SetStateAction<boolean>>>();
// useEvent(ec.events.requestedAction, act => { useEvent(ec.events.requestedAction, act => {
// if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) { if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) {
// setOpenRef.current(t => !t); setOpenRef.current(t => !t);
// } }
// }); });
// return ( return (
// <RpcContext.Provider value={rs}> <RpcContext.Provider value={rs}>
// {/* <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}> {/* <Details setOpenRef={setOpenRef as any} initiallyOpen={!config.autoOpenShowsGoal}>
// <summary className="mv2 pointer"> <summary className="mv2 pointer">
// All Messages ({diags.length}) All Messages ({diags.length})
// <span className="fr"> <span className="fr">
// <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue' : 'codicon-debug-pause')} <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue' : 'codicon-debug-pause')}
// onClick={e => { e.preventDefault(); setPaused(p => !p); }} onClick={e => { e.preventDefault(); setPaused(p => !p); }}
// title={isPaused ? 'continue updating' : 'pause updating'}> title={isPaused ? 'continue updating' : 'pause updating'}>
// </a> </a>
// </span> </span>
// </summary> */} </summary> */}
// <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} /> <AllMessagesBody uri={curPos.uri} key={curPos.uri} messages={iDiags0} curPos={curPos} />
// {/* </Details> */} {/* </Details> */}
// </RpcContext.Provider> </RpcContext.Provider>
// ) )
// } }
// /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */ /** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */
// function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise<InteractiveDiagnostic[]>}) { function AllMessagesBody({uri, curPos, messages}: {uri: DocumentUri, curPos: DocumentPosition | undefined , messages: () => Promise<InteractiveDiagnostic[]>}) {
// let { t } = useTranslation() let { t } = useTranslation()
// const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(undefined) const [msgs, setMsgs] = React.useState<InteractiveDiagnostic[] | undefined>(undefined)
// React.useEffect(() => { void messages().then( React.useEffect(() => { void messages().then(
// msgs => setMsgs(msgs.filter( msgs => setMsgs(msgs.filter(
// (d)=>{ (d)=>{
// //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`) //console.log(`message start: ${d.range.start.line}. CurPos: ${curPos.line}`)
// // Only show the messages from the line where the cursor is. // Only show the messages from the line where the cursor is.
// return d.range.start.line == curPos.line return d.range.start.line == curPos.line
// })) }))
// ) }, [messages, curPos]) ) }, [messages, curPos])
// if (msgs === undefined) return <div>{t("Loading messages…")}</div> if (msgs === undefined) return <div>{t("Loading messages…")}</div>
// else return <MessagesList uri={uri} messages={msgs}/> else return <MessagesList uri={uri} messages={msgs}/>
// } }
// /** /**
// * Provides a `LspDiagnosticsContext` which stores the latest version of the * Provides a `LspDiagnosticsContext` which stores the latest version of the
// * diagnostics as sent by the publishDiagnostics notification. * diagnostics as sent by the publishDiagnostics notification.
// */ */
// export function WithLspDiagnosticsContext({children}: React.PropsWithChildren<{}>) { export function WithLspDiagnosticsContext({children}: React.PropsWithChildren<{}>) {
// const [allDiags, _0] = useServerNotificationState( const [allDiags, _0] = useServerNotificationState(
// 'textDocument/publishDiagnostics', 'textDocument/publishDiagnostics',
// new Map<DocumentUri, Diagnostic[]>(), new Map<DocumentUri, Diagnostic[]>(),
// async (params: PublishDiagnosticsParams) => diags => async (params: PublishDiagnosticsParams) => diags =>
// new Map(diags).set(params.uri, params.diagnostics), new Map(diags).set(params.uri, params.diagnostics),
// [] []
// ) )
// return <LspDiagnosticsContext.Provider value={allDiags}>{children}</LspDiagnosticsContext.Provider> return <LspDiagnosticsContext.Provider value={allDiags}>{children}</LspDiagnosticsContext.Provider>
// } }
// /** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */ /** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */
// export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic { export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic {
// return { ...(diag as LeanDiagnostic), message: { text: diag.message } }; return { ...(diag as LeanDiagnostic), message: { text: diag.message } };
// } }

608
client/src/components/infoview/typewriter.tsx
Unescape Escape View File

@ -1,304 +1,304 @@
// import * as React from 'react' import * as React from 'react'
// import { useRef, useState, useEffect } from 'react' import { useRef, useState, useEffect } from 'react'
// import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
// import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons' import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
// import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
// // import { Registry } from 'monaco-textmate' // peer dependency // import { Registry } from 'monaco-textmate' // peer dependency
// // import { wireTmGrammars } from 'monaco-editor-textmate' // import { wireTmGrammars } from 'monaco-editor-textmate'
// import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol'; import { DiagnosticSeverity, PublishDiagnosticsParams, DocumentUri } from 'vscode-languageserver-protocol';
// import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
// // import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter'; // import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
// // import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; // import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
// // import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json' // import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
// // import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json' // import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
// // import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json' // import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
// // import languageConfig from 'lean4/language-configuration.json'; // import languageConfig from 'lean4/language-configuration.json';
// import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api'; import { InteractiveDiagnostic, RpcSessionAtPos, getInteractiveDiagnostics } from '@leanprover/infoview-api';
// import { Diagnostic } from 'vscode-languageserver-types'; import { Diagnostic } from 'vscode-languageserver-types';
// import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
// import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; import { RpcContext } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
// import { ChatContext, PageContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context' import { ChatContext, PageContext, MonacoEditorContext, ProofContext, GameIdContext } from '../../state/context'
// import { goalsToString, lastStepHasErrors, loadGoals } from './goals' import { goalsToString, lastStepHasErrors, loadGoals } from './goals'
// import { GameHint, ProofState } from './rpc_api' import { GameHint, ProofState } from './rpc_api'
// import { useTranslation } from 'react-i18next' import { useTranslation } from 'react-i18next'
// import { InputAbbreviationRewriter } from '@leanprover/unicode-input-component' import { InputAbbreviationRewriter } from '@leanprover/unicode-input-component'
// import ContentEditable from 'react-contenteditable' import ContentEditable from 'react-contenteditable'
// export interface GameDiagnosticsParams { export interface GameDiagnosticsParams {
// uri: DocumentUri; uri: DocumentUri;
// diagnostics: Diagnostic[]; diagnostics: Diagnostic[];
// } }
// /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */ /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
// // register Monaco languages // register Monaco languages
// monaco.languages.register({ monaco.languages.register({
// id: 'lean4cmd', id: 'lean4cmd',
// extensions: ['.leancmd'] extensions: ['.leancmd']
// }) })
// // register Monaco languages // TODO: JE. I dont understand why I suddenly had to add this when it worked without before. // register Monaco languages // TODO: JE. I dont understand why I suddenly had to add this when it worked without before.
// monaco.languages.register({ monaco.languages.register({
// id: 'lean4', id: 'lean4',
// extensions: ['.lean'] extensions: ['.lean']
// }) })
// // map of monaco "language id's" to TextMate scopeNames // map of monaco "language id's" to TextMate scopeNames
// const grammars = new Map() const grammars = new Map()
// grammars.set('lean4', 'source.lean') grammars.set('lean4', 'source.lean')
// grammars.set('lean4cmd', 'source.lean') grammars.set('lean4cmd', 'source.lean')
// // const registry = new Registry({ const registry = new Registry({
// // getGrammarDefinition: async (scopeName) => { getGrammarDefinition: async (scopeName) => {
// // if (scopeName === 'source.lean') { if (scopeName === 'source.lean') {
// // return { return {
// // format: 'json', format: 'json',
// // content: JSON.stringify(leanSyntax) content: JSON.stringify(leanSyntax)
// // } }
// // } else if (scopeName === 'source.lean.markdown') { } else if (scopeName === 'source.lean.markdown') {
// // return { return {
// // format: 'json', format: 'json',
// // content: JSON.stringify(leanMarkdownSyntax) content: JSON.stringify(leanMarkdownSyntax)
// // } }
// // } else { } else {
// // return { return {
// // format: 'json', format: 'json',
// // content: JSON.stringify(codeblockSyntax) content: JSON.stringify(codeblockSyntax)
// // } }
// // } }
// // } }
// // }); });
// // wireTmGrammars(monaco, registry, grammars) wireTmGrammars(monaco, registry, grammars)
// // let config: any = { ...languageConfig } let config: any = { ...languageConfig }
// // config.autoClosingPairs = config.autoClosingPairs.map( config.autoClosingPairs = config.autoClosingPairs.map(
// // pair => { return {'open': pair[0], 'close': pair[1]} } pair => { return {'open': pair[0], 'close': pair[1]} }
// // ) )
// // monaco.languages.setLanguageConfiguration('lean4cmd', config); monaco.languages.setLanguageConfiguration('lean4cmd', config);
// /** The input field */ /** The input field */
// export function Typewriter({disabled}: {disabled?: boolean}) { export function Typewriter({disabled}: {disabled?: boolean}) {
// let { t } = useTranslation() let { t } = useTranslation()
// /** Reference to the hidden multi-line editor */ /** Reference to the hidden multi-line editor */
// const editor = React.useContext(MonacoEditorContext) const editor = React.useContext(MonacoEditorContext)
// const model = editor?.getModel() const model = editor?.getModel()
// const uri = model?.uri.toString() const uri = model?.uri.toString()
// const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null) const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
// const [processing, setProcessing] = useState(false) const [processing, setProcessing] = useState(false)
// const {typewriterInput, setTypewriterInput} = React.useContext(PageContext) const {typewriterInput, setTypewriterInput} = React.useContext(PageContext)
// const inputRef = useRef() const inputRef = useRef()
// // The context storing all information about the current proof // The context storing all information about the current proof
// const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext) const {proof, setProof, interimDiags, setInterimDiags, setCrashed} = React.useContext(ProofContext)
// const {gameId, worldId, levelId} = React.useContext(GameIdContext) const {gameId, worldId, levelId} = React.useContext(GameIdContext)
// // state to store the last batch of deleted messages // state to store the last batch of deleted messages
// const {setDeletedChat} = React.useContext(ChatContext) const {setDeletedChat} = React.useContext(ChatContext)
// const rpcSess = React.useContext(RpcContext) const rpcSess = React.useContext(RpcContext)
// // Run the command // Run the command
// const runCommand = React.useCallback(() => { const runCommand = React.useCallback(() => {
// if (processing) {return} if (processing) {return}
// // TODO: Desired logic is to only reset this after a new *error-free* command has been entered // TODO: Desired logic is to only reset this after a new *error-free* command has been entered
// setDeletedChat([]) setDeletedChat([])
// const pos = editor?.getPosition() const pos = editor?.getPosition()
// if (typewriterInput) { if (typewriterInput) {
// setProcessing(true) setProcessing(true)
// editor?.executeEdits("typewriter", [{ editor?.executeEdits("typewriter", [{
// range: monaco.Selection.fromPositions( range: monaco.Selection.fromPositions(
// pos, pos,
// editor?.getModel()?.getFullModelRange()?.getEndPosition() editor?.getModel()?.getFullModelRange()?.getEndPosition()
// ), ),
// text: typewriterInput.trim() + "\n", text: typewriterInput.trim() + "\n",
// forceMoveMarkers: false forceMoveMarkers: false
// }]) }])
// setTypewriterInput('') setTypewriterInput('')
// // Load proof after executing edits // Load proof after executing edits
// loadGoals(rpcSess, uri, setProof, setCrashed) loadGoals(rpcSess, uri, setProof, setCrashed)
// } }
// editor?.setPosition(pos) editor?.setPosition(pos)
// }, [typewriterInput, editor]) }, [typewriterInput, editor])
// useEffect(() => { useEffect(() => {
// if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) { if (oneLineEditor && oneLineEditor.getValue() !== typewriterInput) {
// oneLineEditor.setValue(typewriterInput) oneLineEditor.setValue(typewriterInput)
// } }
// }, [typewriterInput]) }, [typewriterInput])
// /* Load proof on start/switching to typewriter */ /* Load proof on start/switching to typewriter */
// useEffect(() => { useEffect(() => {
// setProof(null) setProof(null)
// loadGoals(rpcSess, uri, setProof, setCrashed) loadGoals(rpcSess, uri, setProof, setCrashed)
// }, [gameId, worldId, levelId]) }, [gameId, worldId, levelId])
// /** If the last step has an error, add the command to the typewriter. */ /** If the last step has an error, add the command to the typewriter. */
// useEffect(() => { useEffect(() => {
// if (lastStepHasErrors(proof)) { if (lastStepHasErrors(proof)) {
// setTypewriterInput(proof?.steps[proof?.steps.length - 1].command) setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
// } }
// }, [proof]) }, [proof])
// // React when answer from the server comes back // React when answer from the server comes back
// useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => { useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
// if (params.uri == uri) { if (params.uri == uri) {
// setProcessing(false) setProcessing(false)
// console.log('Received lean diagnostics') console.log('Received lean diagnostics')
// console.log(params.diagnostics) console.log(params.diagnostics)
// setInterimDiags(params.diagnostics) setInterimDiags(params.diagnostics)
// //loadGoals(rpcSess, uri, setProof) //loadGoals(rpcSess, uri, setProof)
// // TODO: loadAllGoals() // TODO: loadAllGoals()
// if (!hasErrors(params.diagnostics)) { if (!hasErrors(params.diagnostics)) {
// //setTypewriterInput("") //setTypewriterInput("")
// editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition()) editor?.setPosition(editor?.getModel()?.getFullModelRange()?.getEndPosition())
// } }
// } else { } else {
// // console.debug(`expected uri: ${uri}, got: ${params.uri}`) // console.debug(`expected uri: ${uri}, got: ${params.uri}`)
// // console.debug(params) // console.debug(params)
// } }
// // TODO: This is the wrong place apparently. Where do wee need to load them? // TODO: This is the wrong place apparently. Where do wee need to load them?
// // TODO: instead of loading all goals every time, we could only load the last one // TODO: instead of loading all goals every time, we could only load the last one
// // loadAllGoals() // loadAllGoals()
// }, [uri]); }, [uri]);
// // // React when answer from the server comes back // // React when answer from the server comes back
// // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => { // useServerNotificationEffect('$/game/publishDiagnostics', (params: GameDiagnosticsParams) => {
// // console.log('Received game diagnostics') // console.log('Received game diagnostics')
// // console.log(`diag. uri : ${params.uri}`) // console.log(`diag. uri : ${params.uri}`)
// // console.log(params.diagnostics) // console.log(params.diagnostics)
// // }, [uri]); // }, [uri]);
// useEffect(() => { useEffect(() => {
// const myEditor = monaco.editor.create(inputRef.current!, { const myEditor = monaco.editor.create(inputRef.current!, {
// value: typewriterInput, value: typewriterInput,
// language: "lean4cmd", language: "lean4cmd",
// quickSuggestions: false, quickSuggestions: false,
// lightbulb: { lightbulb: {
// enabled: true enabled: true
// }, },
// unicodeHighlight: { unicodeHighlight: {
// ambiguousCharacters: false, ambiguousCharacters: false,
// }, },
// automaticLayout: true, automaticLayout: true,
// minimap: { minimap: {
// enabled: false enabled: false
// }, },
// lineNumbers: 'off', lineNumbers: 'off',
// tabSize: 2, tabSize: 2,
// glyphMargin: false, glyphMargin: false,
// folding: false, folding: false,
// lineDecorationsWidth: 0, lineDecorationsWidth: 0,
// lineNumbersMinChars: 0, lineNumbersMinChars: 0,
// 'semanticHighlighting.enabled': true, 'semanticHighlighting.enabled': true,
// overviewRulerLanes: 0, overviewRulerLanes: 0,
// hideCursorInOverviewRuler: true, hideCursorInOverviewRuler: true,
// scrollbar: { scrollbar: {
// vertical: 'hidden', vertical: 'hidden',
// horizontalScrollbarSize: 3 horizontalScrollbarSize: 3
// }, },
// overviewRulerBorder: false, overviewRulerBorder: false,
// theme: 'vs-code-theme-converted', theme: 'vs-code-theme-converted',
// fontFamily: "JuliaMono", fontFamily: "JuliaMono",
// contextmenu: false contextmenu: false
// }) })
// setOneLineEditor(myEditor) setOneLineEditor(myEditor)
// const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor) const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
// return () => {abbrevRewriter.dispose(); myEditor.dispose()} return () => {abbrevRewriter.dispose(); myEditor.dispose()}
// }, []) }, [])
// useEffect(() => { useEffect(() => {
// if (!oneLineEditor) return if (!oneLineEditor) return
// // Ensure that our one-line editor can only have a single line // Ensure that our one-line editor can only have a single line
// const l = oneLineEditor.getModel().onDidChangeContent((e) => { const l = oneLineEditor.getModel().onDidChangeContent((e) => {
// const value = oneLineEditor.getValue() const value = oneLineEditor.getValue()
// setTypewriterInput(value) setTypewriterInput(value)
// const newValue = value.replace(/[\n\r]/g, '') const newValue = value.replace(/[\n\r]/g, '')
// if (value != newValue) { if (value != newValue) {
// oneLineEditor.setValue(newValue) oneLineEditor.setValue(newValue)
// } }
// }) })
// return () => { l.dispose() } return () => { l.dispose() }
// }, [oneLineEditor, setTypewriterInput]) }, [oneLineEditor, setTypewriterInput])
// useEffect(() => { useEffect(() => {
// if (!oneLineEditor) return if (!oneLineEditor) return
// // Run command when pressing enter // Run command when pressing enter
// const l = oneLineEditor.onKeyUp((ev) => { const l = oneLineEditor.onKeyUp((ev) => {
// if (ev.code === "Enter" || ev.code === "NumpadEnter") { if (ev.code === "Enter" || ev.code === "NumpadEnter") {
// runCommand() runCommand()
// } }
// }) })
// return () => { l.dispose() } return () => { l.dispose() }
// }, [oneLineEditor, runCommand]) }, [oneLineEditor, runCommand])
// // BUG: Causes `file closed` error // BUG: Causes `file closed` error
// //TODO: Intention is to run once when loading, does that work? //TODO: Intention is to run once when loading, does that work?
// useEffect(() => { useEffect(() => {
// console.debug(`time to update: ${uri} \n ${rpcSess}`) console.debug(`time to update: ${uri} \n ${rpcSess}`)
// console.debug(rpcSess) console.debug(rpcSess)
// // console.debug('LOAD ALL GOALS') // console.debug('LOAD ALL GOALS')
// // TODO: loadAllGoals() // TODO: loadAllGoals()
// }, [rpcSess]) }, [rpcSess])
// /** Process the entered command */ /** Process the entered command */
// const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => { const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
// ev.preventDefault() ev.preventDefault()
// runCommand() runCommand()
// } }
// // do not display if the proof is completed (with potential warnings still present) // do not display if the proof is completed (with potential warnings still present)
// return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}> return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
// <form onSubmit={handleSubmit}> <form onSubmit={handleSubmit}>
// <div className="typewriter-input-wrapper"> <div className="typewriter-input-wrapper">
// <div ref={inputRef} className="typewriter-input" /> <div ref={inputRef} className="typewriter-input" />
// </div> </div>
// <button type="submit" disabled={processing} className="btn btn-inverted"> <button type="submit" disabled={processing} className="btn btn-inverted">
// <FontAwesomeIcon icon={faWandMagicSparkles} />&nbsp;{t("Execute")} <FontAwesomeIcon icon={faWandMagicSparkles} />&nbsp;{t("Execute")}
// </button> </button>
// </form> </form>
// </div> </div>
// } }
// /** Checks whether the diagnostics contain any errors or warnings to check whether the level has /** Checks whether the diagnostics contain any errors or warnings to check whether the level has
// been completed.*/ been completed.*/
// export function hasErrors(diags: Diagnostic[]) { export function hasErrors(diags: Diagnostic[]) {
// return diags.some( return diags.some(
// (d) => (d) =>
// !d.message.startsWith("unsolved goals") && !d.message.startsWith("unsolved goals") &&
// (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
// ) )
// } }
// // TODO: Didn't manage to unify this with the one above // TODO: Didn't manage to unify this with the one above
// export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) { export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
// return (typeof diags !== 'undefined') && diags.some( return (typeof diags !== 'undefined') && diags.some(
// (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning (d) => (d.severity == DiagnosticSeverity.Error ) // || d.severity == DiagnosticSeverity.Warning
// ) )
// } }
// export function getInteractiveDiagsAt (proof: ProofState, k : number) { export function getInteractiveDiagsAt (proof: ProofState, k : number) {
// if (k == 0) { if (k == 0) {
// return [] return []
// } else if (k >= proof?.steps.length-1) { } else if (k >= proof?.steps.length-1) {
// // TODO: Do we need that? // TODO: Do we need that?
// return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1) return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1)
// } else { } else {
// return proof?.diagnostics.filter(msg => msg.range.start.line == k-1) return proof?.diagnostics.filter(msg => msg.range.start.line == k-1)
// } }
// } }

622
client/src/components/level.tsx
Unescape Escape View File

@ -26,11 +26,11 @@ import { changedSelection, codeEdited, selectCode, selectSelections, selectCompl
selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress' selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
import { store } from '../state/store' import { store } from '../state/store'
import {InventoryPanel} from './inventory' import {InventoryPanel} from './inventory'
import { Typewriter } from './typewriter'
import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, import { ChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
ProofContext, PageContext, GameIdContext } from '../state/context' ProofContext, PageContext, GameIdContext } from '../state/context'
// import { DualEditor, ExerciseStatement } from './infoview/main' // import { DualEditor, ExerciseStatement } from './infoview/main'
import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api' // import { GameHint, InteractiveGoalsWithHints, ProofState } from './infoview/rpc_api'
import path from 'path'; import path from 'path';
import '@fontsource/roboto/300.css' import '@fontsource/roboto/300.css'
@ -449,409 +449,271 @@ export function LevelWrapper({visible = true}) {
export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
const {gameId, worldId, levelId} = React.useContext(GameIdContext)
const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
const gameInfo = useGetGameInfoQuery({game: gameId})
return <div className={`exercise-panel ${visible ? '' : 'hidden'}`}>
<div className="">
{/* <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} worldSize={gameInfo.data?.worldSize[worldId]}/> */}
</div>
</div>
}
<Split minSize={0} snapOffset={200} sizes={[25, 75]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<ChatPanel lastLevel={lastLevel}/>
<InventoryPanel />
</Split>
function IntroductionPanel({gameInfo}) {
let { t } = useTranslation()
const {gameId, worldId} = React.useContext(GameIdContext)
const {mobile} = React.useContext(PreferencesContext)
let text: Array<string> = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
return <div className="chat-panel">
<div className="chat">
{text?.filter(t => t.trim()).map(((t, i) =>
<Hint key={`intro-p-${i}`}
hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
))}
</div>
<ChatButtons />
</div>
}
/** The site with the introduction text of a world */
function Introduction() {
let { t } = useTranslation()
const {gameId, worldId} = React.useContext(GameIdContext)
const {mobile} = useContext(PreferencesContext)
const inventory = useLoadInventoryOverviewQuery({game: gameId})
const gameInfo = useGetGameInfoQuery({game: gameId})
let image: string = gameInfo.data?.worlds.nodes[worldId].image
// const toggleImpressum = () => {
// setImpressum(!impressum)
// }
// const togglePrivacy = () => {
// setPrivacy(!privacy)
// }
return <>
{/* <LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/> */}
{gameInfo.isLoading ?
<div className="app-content loading"><CircularProgress /></div>
: mobile ?
<IntroductionPanel gameInfo={gameInfo} />
:
// <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
// <IntroductionPanel gameInfo={gameInfo} />
<div className="world-image-container empty center">
{image &&
<img className="contain" src={path.join("data", gameId, image)} alt="" />
}
</div>
// {/* <InventoryPanel /> */}
// </Split>
}
</>
}
{mobile?
// TODO: This is copied from the `Split` component below...
<>
<div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
<ExercisePanel
impressum={impressum}
closeImpressum={closeImpressum}
codeviewRef={codeviewRef}
visible={pageNumber == 0} />
<InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
</div>
</>
:
<Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<ChatPanel lastLevel={lastLevel}/>
<ExercisePanel
impressum={impressum}
closeImpressum={closeImpressum}
codeviewRef={codeviewRef} />
<InventoryPanel levelInfo={level?.data} />
</Split>
}
function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
const {gameId, worldId, levelId} = React.useContext(GameIdContext)
const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)
const uriStr = `file:///${worldId}/${levelId}`
const uri = monaco.Uri.parse(uriStr)
const inventory: Array<String> = useSelector(selectInventory(gameId))
const difficulty: number = useSelector(selectDifficulty(gameId))
useEffect(() => {
// monaco.editor.getModels().forEach(model => model.dispose());
console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`)
const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
if (onDidChangeContent) {
model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
}
const editor = monaco.editor.create(codeviewRef.current!, {
model,
glyphMargin: true,
quickSuggestions: false,
lineDecorationsWidth: 5,
folding: false,
lineNumbers: 'on',
lightbulb: {
enabled: true
},
unicodeHighlight: {
ambiguousCharacters: false,
},
automaticLayout: true,
minimap: {
enabled: false
},
lineNumbersMinChars: 3,
tabSize: 2,
'semanticHighlighting.enabled': true,
fontFamily: "JuliaMono",
theme: 'vs-code-theme-converted'
})
if (onDidChangeSelection) {
editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
}
if (initialSelections) {
console.debug("Initial Selection: ", initialSelections)
// BUG: Somehow I get an `invalid arguments` bug here
// editor.setSelections(initialSelections)
}
setEditor(editor)
const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
const connectionProvider : IConnectionProvider = {
get: async () => {
return await new Promise((resolve, reject) => {
console.log(`connecting ${socketUrl}`)
const websocket = new WebSocket(socketUrl)
websocket.addEventListener('error', (ev) => {
reject(ev)
})
websocket.addEventListener('message', (msg) => {
// console.log(msg.data)
})
websocket.addEventListener('open', () => {
const socket = toSocket(websocket)
const reader = new DisposingWebSocketMessageReader(socket)
const writer = new WebSocketMessageWriter(socket)
resolve({
reader,
writer
})
})
})
}
}
// Following `vscode-lean4/webview/index.ts`
const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
const infoProvider = new InfoProvider(client)
// const div: HTMLElement = infoviewRef.current!
const imports = {
'@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
'react': `${window.location.origin}/react.production.min.js`,
'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
'react-dom': `${window.location.origin}/react-dom.production.min.js`,
'react-popper': `${window.location.origin}/react-popper.production.min.js`
}
// loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
setInfoProvider(infoProvider)
// TODO: it looks like we get errors "File Changed" here.
client.restart("Lean4Game")
const editorApi = infoProvider.getApi()
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(),
};
// Challenge: write a type-correct fn from `Eventify<T>` to `T` without using `any`
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),
// See https://rollupjs.org/guide/en/#avoiding-eval
// eslint-disable-next-line @typescript-eslint/no-implied-eval
runTestScript: async script => new Function(script)(),
getInfoviewHtml: async () => document.body.innerHTML,
};
const ec = new EditorConnection(editorApi, editorEvents);
setEditorConnection(ec)
editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc))
setEditor(editor)
setInfoProvider(infoProvider)
infoProvider.openPreview(editor, infoviewApi)
const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
// TODO:
// setRestart(() => restart)
return () => {
editor.dispose();
model.dispose();
abbrevRewriter.dispose();
taskgutter.dispose();
infoProvider.dispose();
client.dispose();
}
}, [gameId, worldId, levelId])
const showRestartMessage = () => {
// setRestartMessage(true)
console.log("TODO: SHOW RESTART MESSAGE")
}
return {editor, infoProvider, editorConnection}
// function ChatPanel({lastLevel, visible = true}) {
// let { t } = useTranslation()
// const chatRef = useRef<HTMLDivElement>(null)
// const {mobile} = useContext(PreferencesContext)
// const {gameId, worldId, levelId} = useContext(GameIdContext)
// const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
// const {proof, setProof} = useContext(ProofContext)
// const {deletedChat, setDeletedChat, showHelp, setShowHelp} = useContext(DeletedChatContext)
// const {selectedStep, setSelectedStep} = useContext(SelectionContext)
// const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
// let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
// function toggleSelection(line: number) {
// return (ev) => {
// 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, showHelp])
// // 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<string> = t(level?.data?.introduction, {ns: gameId}).split(/\n(\s*\n)+/)
// return <div className={`chat-panel ${visible ? '' : 'hidden'}`}>
// <div ref={chatRef} className="chat">
// {introText?.filter(t => t.trim()).map(((t, i) =>
// // Show the level's intro text as hints, too
// <Hint key={`intro-p-${i}`}
// hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
// ))}
// {proof?.steps.map((step, i) => {
// let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
// if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
// return <Hints key={`hints-${i}`}
// hints={filteredHints} showHidden={showHelp.has(i)} step={i}
// selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
// }
// })}
// {/* {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 <Hints key={`hints-${i}`}
// hints={step} showHidden={showHelp.has(i)} step={i}
// selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
// }
// })} */}
// <DeletedHints hints={deletedChat}/>
// {proof?.completed &&
// <>
// <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
// {t("Level completed! 🎉")}
// </div>
// {level?.data?.conclusion?.trim() &&
// <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
// <Markdown>{t(level?.data?.conclusion, {ns: gameId})}</Markdown>
// </div>
// }
// </>
// }
// </div>
// <div className="button-row">
// {proof?.completed && (lastLevel ?
// <Button to={`/${gameId}`}>
// <FontAwesomeIcon icon={faHome} />&nbsp;{t("Home")}
// </Button> :
// <Button to={`/${gameId}/world/${worldId}/level/${levelId + 1}`}>
// {t("Next")}&nbsp;<FontAwesomeIcon icon={faArrowRight} />
// </Button>)
// }
// <MoreHelpButton />
// </div>
// </div>
// }
export function ExercisePanel({codeviewRef, visible=true}: {codeviewRef: React.MutableRefObject<HTMLDivElement>, visible?: boolean}) {
const {gameId, worldId, levelId} = React.useContext(GameIdContext)
const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
const gameInfo = useGetGameInfoQuery({game: gameId})
return <div className={`exercise-panel ${visible ? '' : 'hidden'}`}>
<div className="">
{/* <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} worldSize={gameInfo.data?.worldSize[worldId]}/> */}
</div>
</div>
} }
// <Split minSize={0} snapOffset={200} sizes={[25, 75]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
// <ChatPanel lastLevel={lastLevel}/>
// <InventoryPanel />
// </Split>
// function IntroductionPanel({gameInfo}) {
// let { t } = useTranslation()
// const {gameId, worldId} = React.useContext(GameIdContext)
// const {mobile} = React.useContext(PreferencesContext)
// let text: Array<string> = t(gameInfo.data?.worlds.nodes[worldId].introduction, {ns: gameId}).split(/\n(\s*\n)+/)
// return <div className="chat-panel">
// <div className="chat">
// {text?.filter(t => t.trim()).map(((t, i) =>
// <Hint key={`intro-p-${i}`}
// hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
// ))}
// </div>
// <ChatButtons />
// </div>
// }
// /** The site with the introduction text of a world */
// function Introduction() {
// let { t } = useTranslation()
// const {gameId, worldId} = React.useContext(GameIdContext)
// const {mobile} = useContext(PreferencesContext)
// const inventory = useLoadInventoryOverviewQuery({game: gameId})
// const gameInfo = useGetGameInfoQuery({game: gameId})
// let image: string = gameInfo.data?.worlds.nodes[worldId].image
// // const toggleImpressum = () => {
// // setImpressum(!impressum)
// // }
// // const togglePrivacy = () => {
// // setPrivacy(!privacy)
// // }
// return <>
// {/* <LevelAppBar isLoading={gameInfo.isLoading} levelTitle={t("Introduction")} toggleImpressum={toggleImpressum} togglePrivacy={togglePrivacy} toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/> */}
// {gameInfo.isLoading ?
// <div className="app-content loading"><CircularProgress /></div>
// : mobile ?
// <IntroductionPanel gameInfo={gameInfo} />
// :
// // <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
// // <IntroductionPanel gameInfo={gameInfo} />
// <div className="world-image-container empty center">
// {image &&
// <img className="contain" src={path.join("data", gameId, image)} alt="" />
// }
// </div>
// // {/* <InventoryPanel /> */}
// // </Split>
// }
// </>
// }
// {mobile?
// // TODO: This is copied from the `Split` component below...
// <>
// <div className={`app-content level-mobile ${level.isLoading ? 'hidden' : ''}`}>
// <ExercisePanel
// impressum={impressum}
// closeImpressum={closeImpressum}
// codeviewRef={codeviewRef}
// visible={pageNumber == 0} />
// <InventoryPanel levelInfo={level?.data} visible={pageNumber == 1} />
// </div>
// </>
// :
// <Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
// <ChatPanel lastLevel={lastLevel}/>
// <ExercisePanel
// impressum={impressum}
// closeImpressum={closeImpressum}
// codeviewRef={codeviewRef} />
// <InventoryPanel levelInfo={level?.data} />
// </Split>
// }
// function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChangeContent, onDidChangeSelection) {
// const {gameId, worldId, levelId} = React.useContext(GameIdContext)
// const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor|null>(null)
// const [infoProvider, setInfoProvider] = useState<null|InfoProvider>(null)
// const [editorConnection, setEditorConnection] = useState<null|EditorConnection>(null)
// const uriStr = `file:///${worldId}/${levelId}`
// const uri = monaco.Uri.parse(uriStr)
// const inventory: Array<String> = useSelector(selectInventory(gameId))
// const difficulty: number = useSelector(selectDifficulty(gameId))
// useEffect(() => {
// // monaco.editor.getModels().forEach(model => model.dispose());
// console.info(`trying to create model: ${gameId} ${worldId} ${levelId} ${uri}`)
// const model = monaco.editor.createModel(initialCode ?? '', 'lean4', uri)
// if (onDidChangeContent) {
// model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
// }
// const editor = monaco.editor.create(codeviewRef.current!, {
// model,
// glyphMargin: true,
// quickSuggestions: false,
// lineDecorationsWidth: 5,
// folding: false,
// lineNumbers: 'on',
// lightbulb: {
// enabled: true
// },
// unicodeHighlight: {
// ambiguousCharacters: false,
// },
// automaticLayout: true,
// minimap: {
// enabled: false
// },
// lineNumbersMinChars: 3,
// tabSize: 2,
// 'semanticHighlighting.enabled': true,
// fontFamily: "JuliaMono",
// theme: 'vs-code-theme-converted'
// })
// if (onDidChangeSelection) {
// editor.onDidChangeCursorSelection(() => onDidChangeSelection(editor.getSelections()))
// }
// if (initialSelections) {
// console.debug("Initial Selection: ", initialSelections)
// // BUG: Somehow I get an `invalid arguments` bug here
// // editor.setSelections(initialSelections)
// }
// setEditor(editor)
// const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
// const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + '/websocket/' + gameId
// const connectionProvider : IConnectionProvider = {
// get: async () => {
// return await new Promise((resolve, reject) => {
// console.log(`connecting ${socketUrl}`)
// const websocket = new WebSocket(socketUrl)
// websocket.addEventListener('error', (ev) => {
// reject(ev)
// })
// websocket.addEventListener('message', (msg) => {
// // console.log(msg.data)
// })
// websocket.addEventListener('open', () => {
// const socket = toSocket(websocket)
// const reader = new DisposingWebSocketMessageReader(socket)
// const writer = new WebSocketMessageWriter(socket)
// resolve({
// reader,
// writer
// })
// })
// })
// }
// }
// // Following `vscode-lean4/webview/index.ts`
// const client = new LeanClient(connectionProvider, showRestartMessage, {inventory, difficulty})
// const infoProvider = new InfoProvider(client)
// // const div: HTMLElement = infoviewRef.current!
// const imports = {
// '@leanprover/infoview': `${window.location.origin}/index.production.min.js`,
// 'react': `${window.location.origin}/react.production.min.js`,
// 'react/jsx-runtime': `${window.location.origin}/react-jsx-runtime.production.min.js`,
// 'react-dom': `${window.location.origin}/react-dom.production.min.js`,
// 'react-popper': `${window.location.origin}/react-popper.production.min.js`
// }
// // loadRenderInfoview(imports, [infoProvider.getApi(), div], setInfoviewApi)
// setInfoProvider(infoProvider)
// // TODO: it looks like we get errors "File Changed" here.
// client.restart("Lean4Game")
// const editorApi = infoProvider.getApi()
// 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(),
// };
// // Challenge: write a type-correct fn from `Eventify<T>` to `T` without using `any`
// 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),
// // See https://rollupjs.org/guide/en/#avoiding-eval
// // eslint-disable-next-line @typescript-eslint/no-implied-eval
// runTestScript: async script => new Function(script)(),
// getInfoviewHtml: async () => document.body.innerHTML,
// };
// const ec = new EditorConnection(editorApi, editorEvents);
// setEditorConnection(ec)
// editorEvents.initialize.on((loc: Location) => ec.events.changedCursorLocation.fire(loc))
// setEditor(editor)
// setInfoProvider(infoProvider)
// infoProvider.openPreview(editor, infoviewApi)
// const taskgutter = new LeanTaskGutter(infoProvider.client, editor)
// // TODO:
// // setRestart(() => restart)
// return () => {
// editor.dispose();
// model.dispose();
// abbrevRewriter.dispose();
// taskgutter.dispose();
// infoProvider.dispose();
// client.dispose();
// }
// }, [gameId, worldId, levelId])
// const showRestartMessage = () => {
// // setRestartMessage(true)
// console.log("TODO: SHOW RESTART MESSAGE")
// }
// return {editor, infoProvider, editorConnection}
// }

7
client/src/components/typewriter.tsx
Unescape Escape View File

@ -1,7 +0,0 @@
import * as React from 'react'
export function Typewriter () {
return <p>
I'm a typewriter
</p>
}

10
client/src/css/editor.css
Unescape Escape View File

@ -1,5 +1,10 @@
.editor-wrapper { .editor-wrapper {
flex: 1; flex: 1;
position: relative;
}
.editor-wrapper .editor-split {
height: 100%;
} }
#editor { #editor {
@ -15,3 +20,8 @@
height: 95%; /* TODO: setting this to 100% makes it a few pixels too high... */ height: 95%; /* TODO: setting this to 100% makes it a few pixels too high... */
border: unset; border: unset;
} }
/* .typewriter {
background-color: lightpink;
min-height: 400px;
} */

18318
package-lock.json generated
View File

File diff suppressed because it is too large Load Diff

11
package.json
Unescape Escape View File

@ -14,8 +14,6 @@
"@fortawesome/free-regular-svg-icons": "^6.5.1", "@fortawesome/free-regular-svg-icons": "^6.5.1",
"@fortawesome/free-solid-svg-icons": "^6.5.1", "@fortawesome/free-solid-svg-icons": "^6.5.1",
"@fortawesome/react-fontawesome": "^0.2.0", "@fortawesome/react-fontawesome": "^0.2.0",
"@leanprover/infoview": "^0.7.1",
"@leanprover/unicode-input-component": "^0.1.0",
"@mui/icons-material": "^5.11.0", "@mui/icons-material": "^5.11.0",
"@mui/material": "^5.11.1", "@mui/material": "^5.11.1",
"@reduxjs/toolkit": "^1.9.1", "@reduxjs/toolkit": "^1.9.1",
@ -31,17 +29,17 @@
"i18next": "^23.10.1", "i18next": "^23.10.1",
"i18next-http-backend": "^2.5.0", "i18next-http-backend": "^2.5.0",
"i18next-scanner-typescript": "^1.2.0", "i18next-scanner-typescript": "^1.2.0",
"ip-anonymize": "^0.1.0",
"lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c", "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
"lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7", "lean4monaco": "^1.0.29",
"memfs": "^4.11.1",
"octokit": "^3.1.2", "octokit": "^3.1.2",
"path-browserify": "^1.0.1", "path-browserify": "^1.0.1",
"react": "^18.2.0",
"react-contenteditable": "^3.3.7", "react-contenteditable": "^3.3.7",
"react-country-flag": "^3.1.0", "react-country-flag": "^3.1.0",
"react-dom": "^18.2.0", "react-dom": "^18.2.0",
"react-i18next": "^14.1.0", "react-i18next": "^14.1.0",
"react-markdown": "^8.0.4", "react-markdown": "^8.0.4",
"react-native": "^0.72.3",
"react-redux": "^8.0.5", "react-redux": "^8.0.5",
"react-router-dom": "^6.5.0", "react-router-dom": "^6.5.0",
"react-split": "^2.0.14", "react-split": "^2.0.14",
@ -52,6 +50,7 @@
"request": "^2.88.2", "request": "^2.88.2",
"request-progress": "^3.0.0", "request-progress": "^3.0.0",
"vite": "^4.5.0", "vite": "^4.5.0",
"vite-plugin-node-polyfills": "0.17.0",
"vite-plugin-static-copy": "^0.17.0", "vite-plugin-static-copy": "^0.17.0",
"vite-plugin-svgr": "^4.1.0", "vite-plugin-svgr": "^4.1.0",
"vscode-ws-jsonrpc": "^2.0.1", "vscode-ws-jsonrpc": "^2.0.1",
@ -59,6 +58,7 @@
"ws": "^8.11.0" "ws": "^8.11.0"
}, },
"devDependencies": { "devDependencies": {
"@codingame/esbuild-import-meta-url-plugin": "https://gitpkg.vercel.app/hhu-adam/lean4monaco/esbuild-import-meta-url-plugin?main",
"@pmmmwh/react-refresh-webpack-plugin": "^0.5.10", "@pmmmwh/react-refresh-webpack-plugin": "^0.5.10",
"@redux-devtools/core": "^3.13.1", "@redux-devtools/core": "^3.13.1",
"@testing-library/react": "^13.4.0", "@testing-library/react": "^13.4.0",
@ -71,7 +71,6 @@
"react-refresh": "^0.14.0", "react-refresh": "^0.14.0",
"style-loader": "^3.3.1", "style-loader": "^3.3.1",
"ts-loader": "^9.4.2", "ts-loader": "^9.4.2",
"typescript": "^4.9.4",
"url-loader": "^4.1.1" "url-loader": "^4.1.1"
}, },
"scripts": { "scripts": {

23
relay/bubblewrap.sh
Unescape Escape View File

@ -1,17 +1,21 @@
#/bin/bash #/bin/bash
# Note: This fails if there is no default toolchain installed # Note: This fails if there is no default toolchain installed
ELAN_HOME=$(lake env printenv ELAN_HOME) LEAN_ROOT="$(cd $1 && lean --print-prefix)"
LEAN_PATH="$(cd $1 && lake env printenv LEAN_PATH)"
# $1 : the game directory # $1 : the game directory
# $2 : the lean4game folder # $2 : the lean4game folder
# $3 : the gameserver executable # $3 : the gameserver executable
# # print commands as they are executed
# set -x
(exec bwrap\ (exec bwrap\
--bind $2 /lean4game \ --ro-bind $2 /lean4game \
--bind $1 /game \ --ro-bind $1 /game \
--bind $ELAN_HOME /elan \ --ro-bind "$LEAN_ROOT" /lean \
--bind /usr /usr \ --ro-bind /usr /usr \
--dev /dev \ --dev /dev \
--proc /proc \ --proc /proc \
--symlink usr/lib /lib\ --symlink usr/lib /lib\
@ -19,8 +23,9 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
--symlink usr/bin /bin\ --symlink usr/bin /bin\
--symlink usr/sbin /sbin\ --symlink usr/sbin /sbin\
--clearenv \ --clearenv \
--setenv PATH "/elan/bin:/bin" \ --setenv PATH "/lean/bin" \
--setenv ELAN_HOME "/elan" \ --setenv LAKE "/no" `# tries to invoke git otherwise` \
--setenv LEAN_PATH "$LEAN_PATH" \
--unshare-user \ --unshare-user \
--unshare-pid \ --unshare-pid \
--unshare-net \ --unshare-net \
@ -30,3 +35,7 @@ ELAN_HOME=$(lake env printenv ELAN_HOME)
--chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \ --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
./gameserver --server /game ./gameserver --server /game
) )
# TODO
# --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \
# ./gameserver --server /game

232
relay/index.mjs
Unescape Escape View File

@ -1,15 +1,18 @@
import { WebSocketServer } from 'ws'; import { WebSocketServer } from 'ws'
import express from 'express' import express from 'express'
import path from 'path' import * as cp from 'child_process'
import * as cp from 'child_process'; import * as url from 'url'
import * as url from 'url'; import * as rpc from 'vscode-ws-jsonrpc'
import * as rpc from 'vscode-ws-jsonrpc'; import * as path from 'path'
import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'; import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'
import os from 'os'; // import nocache from 'nocache'
import fs from 'fs'; import anonymize from 'ip-anonymize'
import anonymize from 'ip-anonymize'; import os from 'os'
import fs from 'fs'
import http from 'http'
import https from 'https'
import { importTrigger, importStatus } from './import.mjs' import { importTrigger, importStatus } from './import.mjs'
// import fs from 'fs'
/** /**
* Add a game here if the server should keep a queue of pre-loaded games ready at all times. * Add a game here if the server should keep a queue of pre-loaded games ready at all times.
@ -23,44 +26,70 @@ const queueLength = {
"g/trequetrum/lean4game-logic": 0, "g/trequetrum/lean4game-logic": 0,
} }
const __filename = url.fileURLToPath(import.meta.url); let socketCounter = 0
const __dirname = url.fileURLToPath(new URL('.', import.meta.url));
function logStats() {
console.log(`[${new Date()}] Number of open sockets - ${socketCounter}`)
console.log(`[${new Date()}] Free RAM - ${Math.round(os.freemem() / 1024 / 1024)} / ${Math.round(os.totalmem() / 1024 / 1024)} MB`)
}
const __filename = url.fileURLToPath(import.meta.url)
const __dirname = url.fileURLToPath(new URL('.', import.meta.url))
const app = express()
const PORT = process.env.PORT || 8080; const environment = process.env.NODE_ENV
const isDevelopment = environment === 'development'
const crtFile = process.env.SSL_CRT_FILE
const keyFile = process.env.SSL_KEY_FILE
const app = express()
var router = express.Router(); var router = express.Router()
// Paths for game import logic
router.get('/import/status/:owner/:repo', importStatus) router.get('/import/status/:owner/:repo', importStatus)
router.get('/import/trigger/:owner/:repo', importTrigger) router.get('/import/trigger/:owner/:repo', importTrigger)
const server = app app.use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game
.use(express.static(path.join(__dirname, '..', 'client', 'dist'))) // TODO: add a dist folder from inside the game app.use('/i18n/g/:owner/:repo/:lang/*', (req, res, next) => {
.use('/i18n/g/:owner/:repo/:lang/*', (req, res, next) => { const owner = req.params.owner
const owner = req.params.owner;
const repo = req.params.repo const repo = req.params.repo
const lang = req.params.lang const lang = req.params.lang
const filename = req.params[0]; const filename = req.params[0]
req.url = filename; req.url = filename
express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next); express.static(path.join(getGameDir(owner,repo),".i18n",lang))(req, res, next)
}) })
.use('/data/g/:owner/:repo/*', (req, res, next) => { app.use('/data/g/:owner/:repo/*', (req, res, next) => {
const owner = req.params.owner; const owner = req.params.owner
const repo = req.params.repo const repo = req.params.repo
const filename = req.params[0]; const filename = req.params[0]
req.url = filename; req.url = filename
express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next); express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next)
}) })
.use('/', router) app.use('/', router)
.listen(PORT, () => console.log(`Listening on ${PORT}`));
const wss = new WebSocketServer({ server }) let server
if (crtFile && keyFile) {
var privateKey = fs.readFileSync(keyFile, 'utf8')
var certificate = fs.readFileSync(crtFile, 'utf8')
var credentials = {key: privateKey, cert: certificate}
var socketCounter = 0 const PORT = process.env.PORT ?? 443
server = https.createServer(credentials, app).listen(PORT,
() => console.log(`HTTPS on port ${PORT}`))
const environment = process.env.NODE_ENV // redirect http to https
const isDevelopment = environment === 'development' express().get('*', function(req, res) {
res.redirect('https://' + req.headers.host + req.url).listen(80)
})
} else {
const PORT = process.env.PORT ?? 8080
server = app.listen(PORT,
() => console.log(`HTTP on port ${PORT}`))
}
const wss = new WebSocketServer({ server })
/** We keep queues of started Lean Server processes to be ready when a user arrives */ /** We keep queues of started Lean Server processes to be ready when a user arrives */
const queue = {} const queue = {}
@ -85,7 +114,8 @@ function getGameDir(owner, repo) {
} }
let game_dir = (owner == 'local') ? let game_dir = (owner == 'local') ?
path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive // note: in the local case we need `repo` to be case sensitive
path.join(__dirname, '..', '..', repo) :
path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`) path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`)
if(!fs.existsSync(game_dir)) { if(!fs.existsSync(game_dir)) {
@ -93,16 +123,20 @@ function getGameDir(owner, repo) {
return "" return ""
} }
return game_dir; return game_dir
} }
function startServerProcess(owner, repo) { function startServerProcess(owner, repo) {
let game_dir = getGameDir(owner, repo) let game_dir = getGameDir(owner, repo)
if (!game_dir) return; if (!game_dir) { return }
let serverProcess let serverProcess
if (isDevelopment) { if (isDevelopment) {
console.warn("Running without Bubblewrap container!")
// TODO: use the gameserver
// serverProcess = cp.spawn("lean", ["--server"], { cwd: game_dir })
let args = ["--server", game_dir] let args = ["--server", game_dir]
let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin") let binDir = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin")
// Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again // Note: `cwd` is important to be the `bin` directory as `Watchdog` calls `./gameserver` again
@ -115,19 +149,24 @@ function startServerProcess(owner, repo) {
{ cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") }) { cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") })
} }
} else { } else {
serverProcess = cp.spawn("./bubblewrap.sh", console.info("Running with Bubblewrap container.")
serverProcess = cp.spawn(
"./bubblewrap.sh",
[ game_dir, path.join(__dirname, '..')], [ game_dir, path.join(__dirname, '..')],
{ cwd: __dirname }) { cwd: __dirname }
)
} }
serverProcess.stderr.on('data', data =>
console.error(`Lean Server: ${data}`)
)
serverProcess.on('error', error => serverProcess.on('error', error =>
console.error(`Launching Lean Server failed: ${error}`) console.error(`Launching Lean Server failed: ${error}`)
) )
if (serverProcess.stderr !== null) { serverProcess.on('close', (code, _signal) => {
serverProcess.stderr.on('data', data => console.log(`Lean server exited with code ${code}`)
console.error(`Lean Server: ${data}`) })
)
}
return serverProcess return serverProcess
} }
@ -152,61 +191,64 @@ function fillQueue(tag) {
// } // }
// } // }
const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)$/
wss.addListener("connection", function(ws, req) { wss.addListener("connection", function(ws, req) {
const reRes = urlRegEx.exec(req.url) // server expects URL of the form `/websocket/g/{owner}/{repo}`
if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; } const urlRegEx = /^\/websocket\/g\/([\w.-]+)\/([\w.-]+)\/?$/
const owner = reRes[1] const reRes = urlRegEx.exec(req.url)
const repo = reRes[2] if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return }
const owner = reRes[1]
const tag = getTag(owner, repo) const repo = reRes[2]
const tag = getTag(owner, repo)
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
let ps
if (!queue[tag] || queue[tag].length == 0) {
ps = startServerProcess(owner, repo)
} else {
console.info('Got process from the queue')
ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately
// TODO
// async () => {
// fillQueue(tag)
// }
}
if (ps == null) {
console.error('server process is undefined/null')
return
}
let ps const socket = {
if (!queue[tag] || queue[tag].length == 0) { onMessage: (cb) => { ws.on("message", cb) },
ps = startServerProcess(owner, repo) onError: (cb) => { ws.on("error", cb) },
} else { onClose: (cb) => { ws.on("close", cb) },
console.info('Got process from the queue') send: (data, cb) => { ws.send(data,cb) }
ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately }
fillQueue(tag) const reader = new rpc.WebSocketMessageReader(socket)
const writer = new rpc.WebSocketMessageWriter(socket)
const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
socketConnection.forward(serverConnection, message => {
if (isDevelopment) {
console.log(`CLIENT: ${JSON.stringify(message)}`)
} }
return message
if (ps == null) { })
console.error('server process is undefined/null') serverConnection.forward(socketConnection, message => {
return if (isDevelopment) {
console.log(`SERVER: ${JSON.stringify(message)}`)
} }
return message
})
socketCounter += 1; ws.on('close', () => {
const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress) console.log(`[${new Date()}] Socket closed - ${ip}`)
console.log(`[${new Date()}] Socket opened - ${ip}`) socketCounter -= 1
})
const socket = { socketConnection.onClose(() => serverConnection.dispose())
onMessage: (cb) => { ws.on("message", cb) }, serverConnection.onClose(() => socketConnection.dispose())
onError: (cb) => { ws.on("error", cb) },
onClose: (cb) => { ws.on("close", cb) }, console.log(`[${new Date()}] Socket opened - ${ip}`)
send: (data, cb) => { ws.send(data,cb) } socketCounter += 1
} logStats()
const reader = new rpc.WebSocketMessageReader(socket)
const writer = new rpc.WebSocketMessageWriter(socket)
const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close())
const serverConnection = jsonrpcserver.createProcessStreamConnection(ps)
socketConnection.forward(serverConnection, message => {
if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)}
return message;
})
serverConnection.forward(socketConnection, message => {
if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)}
return message;
});
console.log(`[${new Date()}] Number of open sockets - ${socketCounter}`)
console.log(`[${new Date()}] Free RAM - ${Math.round(os.freemem() / 1024 / 1024)} / ${Math.round(os.totalmem() / 1024 / 1024)} MB`)
ws.on('close', () => {
console.log(`[${new Date()}] Socket closed - ${ip}`)
socketCounter -= 1
})
socketConnection.onClose(() => serverConnection.dispose())
serverConnection.onClose(() => socketConnection.dispose())
}) })

19
server/GameServer/FileWorker.lean
Unescape Escape View File

@ -257,13 +257,13 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
-- Insert final `done` command to display unsolved goal error in the end -- Insert final `done` command to display unsolved goal error in the end
let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[] let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩) let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*) let tacticStx' := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
-- Always call `let_intros` to get rid `let` statements in the goal. -- Always call `let_intros` to get rid `let` statements in the goal.
-- This makes the experience for the user much nicer and allows for local -- This makes the experience for the user much nicer and allows for local
-- definitions in the exercise. -- definitions in the exercise.
let cmdStx ← `(command| let cmdStx ← `(command|
theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preamble⟩); $(⟨tacticStx⟩)} ) theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preamble⟩); $(⟨tacticStx'⟩)} )
Elab.Command.elabCommandTopLevel cmdStx) Elab.Command.elabCommandTopLevel cmdStx)
cmdCtx cmdStateRef cmdCtx cmdStateRef
let postNew := (← tacticCacheNew.get).post let postNew := (← tacticCacheNew.get).post
@ -742,7 +742,6 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
let _ ← IO.setStderr e let _ ← IO.setStderr e
try try
-- BIG MODIFICATION -- BIG MODIFICATION
let game ← loadGameData gameDir let game ← loadGameData gameDir
-- TODO: We misuse the `rootUri` field to the gameName -- TODO: We misuse the `rootUri` field to the gameName
@ -752,8 +751,18 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
initParams meta.mkInputContext.fileName initParams meta.mkInputContext.fileName
| throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}" | throwServerError s!"Could not determine level ID: {meta.mkInputContext.fileName}"
let levelInfo ← loadLevelData gameDir levelId.world levelId.level let levelInfo ← loadLevelData gameDir levelId.world levelId.level
let some initializationOptions := initRequest.param.initializationOptions?
| throwServerError "no initialization options found" -- TODO: I don't know how to pass these options to the Lean server
-- with the new lean4monaco setup!!
-- let some initializationOptions := initRequest.param.initializationOptions?
-- | throwServerError "no initialization options found"
let initializationOptions : Game.InitializationOptions := {
difficulty := 1
inventory := #[]
editDelay? := none
hasWidgets? := none
}
let gameWorkerState : WorkerState := { let gameWorkerState : WorkerState := {
inventory := initializationOptions.inventory inventory := initializationOptions.inventory
difficulty := initializationOptions.difficulty difficulty := initializationOptions.difficulty

9
server/GameServer/RpcHandlers.lean
Unescape Escape View File

@ -13,11 +13,16 @@ open Meta
namespace GameServer namespace GameServer
/-- expects a file name of the form `/{worldId}/Level_{levelId}.lean` where `{levelId}` is a Nat. -/
def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String) : Option LevelId := Id.run do def levelIdFromFileName? (initParams : Lsp.InitializeParams) (fileName : String) : Option LevelId := Id.run do
let fileParts := fileName.splitOn "/" let fileParts := fileName.splitOn "/"
if fileParts.length == 3 then if fileParts.length == 3 then
if let (some level, some game) := (fileParts[2]!.toNat?, initParams.rootUri?) then let some game := initParams.rootUri?
return some {game, world := fileParts[1]!, level := level} | return none
-- the filename has the form `Level_01.lean` and we extract `01`.
let some level := ((fileParts[2]!.splitOn ".")[0]!.splitOn "_")[1]!.toNat?
| return none
return some {game := game, world := fileParts[1]!, level := level}
return none return none
def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do def getLevelByFileName? [Monad m] [MonadEnv m] (initParams : Lsp.InitializeParams) (fileName : String) : m (Option GameLevel) := do

51
tsconfig.json
Unescape Escape View File

@ -1,20 +1,43 @@
{ {
"compilerOptions": { "compilerOptions": {
"outDir": "./client/dist/", "outDir": "./client/dist/",
"module": "esnext", "composite": true,
"target": "es5", "tsBuildInfoFile": "./node_modules/.tmp/tsconfig.app.tsbuildinfo",
"allowJs": true, "target": "ES2020",
"resolveJsonModule": true,
"esModuleInterop": true, "useDefineForClassFields": true,
"moduleResolution": "node",
"jsx": "react",
"downlevelIteration": true,
"experimentalDecorators": true,
"allowSyntheticDefaultImports": true,
"lib": [ "lib": [
"ES2021.String", "ES2020.String",
"DOM" "DOM",
] "DOM.Iterable"
],
"module": "ESNext",
"skipLibCheck": true,
/* Bundler mode */
"moduleResolution": "bundler",
"allowImportingTsExtensions": true,
"resolveJsonModule": true,
"isolatedModules": true,
"moduleDetection": "force",
"noEmit": true,
"jsx": "react-jsx",
/* Linting */
// "strict": true,
// "noUnusedLocals": true,
// "noUnusedParameters": true,
// "noFallthroughCasesInSwitch": true
// "allowJs": true,
// "esModuleInterop": true,
// "downlevelIteration": true,
// "experimentalDecorators": true,
// "allowSyntheticDefaultImports": true,
}, },
"exclude": ["server", "relay"] "exclude": [
"server",
"relay",
"node_modules"
]
} }

40
vite.config.ts
Unescape Escape View File

@ -2,35 +2,57 @@ import { defineConfig } from 'vite'
import react from '@vitejs/plugin-react-swc' import react from '@vitejs/plugin-react-swc'
import { viteStaticCopy } from 'vite-plugin-static-copy' import { viteStaticCopy } from 'vite-plugin-static-copy'
import svgr from "vite-plugin-svgr" import svgr from "vite-plugin-svgr"
import { nodePolyfills } from 'vite-plugin-node-polyfills'
import importMetaUrlPlugin from '@codingame/esbuild-import-meta-url-plugin'
import { normalizePath } from 'vite'
import path from 'node:path'
// https://vitejs.dev/config/ // https://vitejs.dev/config/
export default defineConfig({ export default defineConfig({
//root: 'client/src', optimizeDeps: {
esbuildOptions: {
plugins: [importMetaUrlPlugin]
},
exclude: ['games']
},
build: { build: {
// Relative to the root // Relative to the root
// Note: This has to match the path in `relay/index.mjs` // Note: This has to match the path in `relay/index.mjs` and in `tsconfig.json`
outDir: 'client/dist', outDir: 'client/dist',
}, },
plugins: [ plugins: [
react(), react(),
svgr({ svgr({
svgrOptions: { // svgr options: https://react-svgr.com/docs/options/
// svgr options svgrOptions: { exportType: "default", ref: true, svgo: false, titleProp: true },
include: "**/*.svg",
}),
nodePolyfills({
overrides: {
fs: 'memfs',
}, },
}), }),
viteStaticCopy({ viteStaticCopy({
targets: [ targets: [
{ {
src: 'node_modules/@leanprover/infoview/dist/*.production.min.js', src: [
dest: '.' normalizePath(path.resolve(__dirname, './node_modules/@leanprover/infoview/dist/*')),
normalizePath(path.resolve(__dirname, './node_modules/lean4monaco/dist/webview/webview.js')),
],
dest: 'infoview'
},
{
src: [
normalizePath(path.resolve(__dirname, './node_modules/@leanprover/infoview/dist/codicon.ttf'))
],
dest: 'assets'
} }
] ]
}) })
], ],
publicDir: "client/public", publicDir: "client/public",
optimizeDeps: { base: "/", // setting this to `/leanweb/` means the server is now accessible at `localhost:3000/leanweb`
exclude: ['games'] //root: 'client/src',
},
server: { server: {
port: 3000, port: 3000,
proxy: { proxy: {

Write Preview
Loading…
Cancel
Save