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

move hints to chat

Browse Source
This commit is contained in:
Jon Eugster
2023-06-20 11:39:27 +02:00
parent c0b7b7a048
commit a32baeb8e7
5 changed files with 67 additions and 47 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/Level.tsx
+45 -20
View File
@@ -34,26 +34,52 @@ import {Inventory, Documentation} from './Inventory';
import Markdown from './Markdown';
import { EditorInterface, CommandLineInterface } from './infoview/main'
import { Hints } from './infoview/hints';
import { GameHint } from './infoview/rpcApi';
import { GameHint, InteractiveGoals } from './infoview/rpcApi';
import { GameIdContext } from '../App';
import { ConnectionContext, useLeanClient } from '../connection';
import { useAppDispatch, useAppSelector } from '../hooks';
import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress';
import { DocumentPosition } from '../../../node_modules/lean4-infoview/src/infoview/util';
import { getInteractiveTermGoal, InteractiveDiagnostic,
UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(null as any);
export const HintContext = React.createContext<{
showHiddenHints : boolean,
setShowHiddenHints: React.Dispatch<React.SetStateAction<boolean>>
hints: Array<GameHint>,
setHints: React.Dispatch<React.SetStateAction<Array<GameHint>>>
}>({
showHiddenHints: true,
setShowHiddenHints: () => {},
hints: [],
setHints: () => {},
});
export type InfoStatus = 'updating' | 'error' | 'ready';
export interface ProofStateProps {
// pos: DocumentPosition;
status: InfoStatus;
messages: InteractiveDiagnostic[];
goals?: InteractiveGoals;
termGoal?: InteractiveTermGoal;
error?: string;
// userWidgets: UserWidgetInstance[];
// rpcSess: RpcSessionAtPos;
// triggerUpdate: () => Promise<void>;
}
export const ProofStateContext = React.createContext<{
proofState : ProofStateProps,
setProofState: React.Dispatch<React.SetStateAction<ProofStateProps>>
}>({
proofState : {
status: 'updating',
messages: [],
goals: undefined,
termGoal: undefined,
error: undefined},
setProofState: () => {},
});
@@ -96,11 +122,16 @@ function PlayableLevel({worldId, levelId}) {
const [commandLineInput, setCommandLineInput] = useState("")
const [canUndo, setCanUndo] = useState(initialCode.trim() !== "")
// The array of all shown hints. This excludes introduction and conclusion
// TODO: Not used yet
const [hints, setHints] = useState(Array<GameHint>)
const [showHiddenHints, setShowHiddenHints] = useState(false)
const [proofState, setProofState] = React.useState<ProofStateProps>({
status: 'updating',
messages: [],
goals: undefined,
termGoal: undefined,
error: undefined,
})
const theme = useTheme();
@@ -205,8 +236,9 @@ function PlayableLevel({worldId, levelId}) {
return <>
<div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
<ProofStateContext.Provider value={{proofState, setProofState}}>
<InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
<HintContext.Provider value={{showHiddenHints, setShowHiddenHints, hints, setHints}}>
<HintContext.Provider value={{showHiddenHints, setShowHiddenHints}}>
<LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
<Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<div ref={chatPanelRef} className="chat-panel">
@@ -216,15 +248,8 @@ function PlayableLevel({worldId, levelId}) {
<Markdown>{level?.data?.introduction}</Markdown>
</div>
}
{/* {openHints.map(hint => <Hint hint={hint} />)}
{hiddenHints.length > 0 &&
<FormControlLabel
control={<Switch checked={showHints} onChange={() => setShowHints((prev) => !prev)} />}
label="I need help!"
/>}
{showHints && hiddenHints.map(hint => <Hint hint={hint} />)} */}
{hints.map(hint =>
<div className="message info"><Markdown>{hint.text}</Markdown></div>)
{proofState.goals?.goals.length &&
<Hints hints={proofState.goals?.goals[0].hints} showHidden={showHiddenHints}/>
}
{completed &&
<>
@@ -244,7 +269,6 @@ function PlayableLevel({worldId, levelId}) {
}
{/* { hints.map(hint => <div className="message info"><Markdown>{hint.text}</Markdown></div>) } */}
<Hints hints={hints} showHidden={showHiddenHints}/>
{/* TODO: Remove this debugging message: */}
{showHiddenHints && <p>Hidden Hints are displayed</p>}
</div>
@@ -284,6 +308,7 @@ function PlayableLevel({worldId, levelId}) {
</Split>
</HintContext.Provider>
</InputModeContext.Provider>
</ProofStateContext.Provider>
</>
}
client/src/components/infoview/info.tsx
+18 -25
View File
@@ -17,11 +17,10 @@ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-i
import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
import { CircularProgress } from '@mui/material';
import { InputModeContext, MonacoEditorContext, HintContext } from '../Level'
import { InputModeContext, MonacoEditorContext, HintContext, ProofStateProps, InfoStatus, ProofStateContext } from '../Level'
import { Hint } from './hints';
type InfoStatus = 'updating' | 'error' | 'ready';
type InfoKind = 'cursor' | 'pin';
interface InfoPinnable {
@@ -169,18 +168,13 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
interface InfoDisplayProps {
pos: DocumentPosition;
status: InfoStatus;
messages: InteractiveDiagnostic[];
goals?: InteractiveGoals;
termGoal?: InteractiveTermGoal;
error?: string;
userWidgets: UserWidgetInstance[];
rpcSess: RpcSessionAtPos;
triggerUpdate: () => Promise<void>;
}
/** Displays goal state and messages. Can be paused. */
function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) {
// Used to update the paused state *just once* if it is paused,
// but a display update is triggered
const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(false);
@@ -218,7 +212,7 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
<RpcContext.Provider value={rpcSess}>
{/* <details open> */}
{/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
<div>
<div className="vscode-light">
<InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
</div>
{/* </details> */}
@@ -257,8 +251,11 @@ function useIsProcessingAt(p: DocumentPosition): boolean {
function InfoAux(props: InfoProps) {
// TODO
// TODO: proofStateContext is not quite implemented correctly yet.
// i.e. there is an asynchronous state in this file that seems to partally overlap
// search for `const [state, triggerUpdateCore]`
const hintContext = React.useContext(HintContext)
const proofStateContext = React.useContext(ProofStateContext)
const config = React.useContext(ConfigContext)
@@ -294,7 +291,7 @@ function InfoAux(props: InfoProps) {
// 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
// with e.g. a new `pos`.
type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
type InfoRequestResult = Omit<ProofStateProps & InfoDisplayProps, 'triggerUpdate'>
const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((resolve, reject) => {
const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos));
const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos))
@@ -393,11 +390,6 @@ function InfoAux(props: InfoProps) {
const [displayProps, setDisplayProps] = React.useState<InfoDisplayProps>({
pos,
status: 'updating',
messages: [],
goals: undefined,
termGoal: undefined,
error: undefined,
userWidgets: [],
rpcSess,
triggerUpdate
@@ -410,20 +402,21 @@ function InfoAux(props: InfoProps) {
React.useEffect(() => {
if (state.state === 'notStarted')
void triggerUpdate()
else if (state.state === 'loading')
setDisplayProps(dp => ({ ...dp, status: 'updating' }))
else if (state.state === 'loading') {
proofStateContext.setProofState(dp => ({ ...dp, status: 'updating' }))
setDisplayProps(dp => ({ ...dp, status: 'updating' }))
}
else if (state.state === 'resolved') {
setDisplayProps({ ...state.value, triggerUpdate })
// if (state.value.goals) {
// hintContext.setHints(state.value.goals[0]?.hints)
// }
// NOT Working
// if (state.value.goals?.goals?.length) {
// hintContext.setHints(state.value.goals.goals[0].hints)
// }
proofStateContext.setProofState({ ...state.value })
setDisplayProps({ ...state.value, triggerUpdate })
} else if (state.state === 'rejected' && state.error !== 'retry') {
// The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception.
console.warn('Unreachable code reached with error: ', state.error)
}
}, [state])
return <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} />
return <InfoDisplay kind={props.kind} onPin={props.onPin} {...proofStateContext.proofState} {...displayProps} />
}
client/src/components/infoview/infoview.css
+1 -1
View File
@@ -41,7 +41,7 @@
padding: 0.5em;
font-family: var(--ff-primary);
border-radius: 0.2em;
margin: 0.2em 0 0;
/* margin: 0.2em 0 0; */
}
.command-line form {
client/src/components/infoview/main.tsx
+1
View File
@@ -31,6 +31,7 @@ import { LevelInfo } from '../../state/api';
// - Theorem xyz
// - Exercises: description
function ExerciseStatement({data}) {
if (!data?.descrText) { return <></> }
return <div className="exercise-statement"><Markdown>
{(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}` }
</Markdown></div>
client/src/components/level.css
+2 -1
View File
@@ -29,7 +29,7 @@
overflow: auto;
}
.chat-panel, .infoview, .exercise {
.chat-panel, .infoview {
padding-top: 1em;
padding-bottom: 0;
}
@@ -209,4 +209,5 @@ td code {
.commandline-interface .content {
flex: 1 1 auto;
overflow-y: scroll;
padding: 1em;
}