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

Merge branch 'dev' into mobile-option

Browse Source
This commit is contained in:
Jon Eugster
2023-12-13 15:20:24 +01:00
committed by GitHub
parent 9f692ccf61 5aa0764844
commit deec431620
51 changed files with 1967 additions and 980 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/app_bar.tsx
+2 -2
View File
@@ -166,7 +166,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
const [navOpen, setNavOpen] = React.useState(false)
return <div className="app-bar">
<div>
<div className='app-bar-left'>
<Button inverted="false" title="back to games selection" to="/">
<FontAwesomeIcon icon={faArrowLeft} />&nbsp;<FontAwesomeIcon icon={faGlobe} />
</Button>
@@ -241,7 +241,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
</> :
<>
{/* DESKTOP VERSION */}
<div>
<div className='app-bar-left'>
<HomeButton isDropdown={false} />
<span className="app-bar-title">{worldTitle && `World: ${worldTitle}`}</span>
</div>
client/src/components/hints.tsx
+22
View File
@@ -1,6 +1,7 @@
import { GameHint } from "./infoview/rpc_api";
import * as React from 'react';
import Markdown from './markdown';
import { ProofStep } from "./infoview/context";
export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
@@ -43,3 +44,24 @@ export function DeletedHints({hints} : {hints: GameHint[]}) {
{hiddenHints.map((hint, i) => <DeletedHint key={`deleted-hidden-hint-${i}`} hint={hint}/>)}
</>
}
/** Filter hints to not show consequtive identical hints twice.
*
* This function takes a `ProofStep[]` and extracts the hints in form of an
* element of type `GameHint[][]` where it removes hints that are identical to hints
* appearing in the previous step. Hidden hints are not filtered.
*
* This effectively means we prevent consequtive identical hints from being shown.
*/
export function filterHints(proof: ProofStep[]): GameHint[][] {
return proof.map((step, i) => {
if (i == 0){
return step.hints
} else {
// TODO: Writing all fields explicitely is somewhat fragile to changes, is there a
// good way to shallow-compare objects?
return step.hints.filter((hint) => hint.hidden ||
(proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined))
}
})
}
client/src/components/infoview/main.tsx
+17 -5
View File
@@ -34,7 +34,7 @@ import { Button } from '../button';
import { CircularProgress } from '@mui/material';
import { GameHint } from './rpc_api';
import { store } from '../../state/store';
import { Hints } from '../hints';
import { Hints, filterHints } from '../hints';
/** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is
* always present, or the monaco editor cannot start.
@@ -156,7 +156,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
const completed = useAppSelector(selectCompleted(gameId, props.world, props.level))
console.debug(`template: ${props.data.template}`)
console.debug(`template: ${props.data?.template}`)
// React.useEffect (() => {
// if (props.data.template) {
@@ -347,6 +347,7 @@ export function TypewriterInterface({props}) {
const uri = model.uri.toString()
const [disableInput, setDisableInput] = React.useState<boolean>(false)
const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
const {mobile} = React.useContext(MobileContext)
const { proof } = React.useContext(ProofContext)
@@ -366,9 +367,9 @@ export function TypewriterInterface({props}) {
function deleteProof(line: number) {
return (ev) => {
let deletedChat: Array<GameHint> = []
proof.slice(line).map((step, i) => {
filterHints(proof).slice(line).map((hintsAtStep, i) => {
// Only add these hidden hints to the deletion stack which were visible
deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))]
})
setDeletedChat(deletedChat)
@@ -455,6 +456,17 @@ export function TypewriterInterface({props}) {
let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : 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">
@@ -521,7 +533,7 @@ export function TypewriterInterface({props}) {
}
</div>
}
</> : <CircularProgress />
</> : <CircularProgress variant="determinate" value={loadingProgress} />
}
</div>
</div>
client/src/components/inventory.tsx
+1 -1
View File
@@ -86,7 +86,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine
{[...modifiedItems].sort(
// For lemas, sort entries `available > disabled > locked`
// otherwise alphabetically
(x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled)
(x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName)
).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => {
return <InventoryItem key={`${item.category}-${item.name}`}
showDoc={() => {openDoc({name: item.name, type: docType})}}
client/src/components/landing_page.tsx
+91 -67
View File
@@ -7,11 +7,12 @@ import '@fontsource/roboto/500.css';
import '@fontsource/roboto/700.css';
import '../css/landing_page.css'
import coverRobo from '../assets/covers/formaloversum.png'
import bgImage from '../assets/bg.jpg'
import Markdown from './markdown';
import {PrivacyPolicyPopup} from './popup/privacy_policy'
import { GameTile, useGetGameInfoQuery } from '../state/api'
import path from 'path';
const flag = {
'Dutch': '🇳🇱',
@@ -19,6 +20,7 @@ const flag = {
'French': '🇫🇷',
'German': '🇩🇪',
'Italian': '🇮🇹',
'Spanish': '🇪🇸',
}
function GithubIcon({url='https://github.com'}) {
@@ -32,47 +34,42 @@ function GithubIcon({url='https://github.com'}) {
</div>
}
function GameTile({
title,
gameId,
intro, // Catchy intro phrase.
image=null,
worlds='?',
levels='?',
prereq='&ndash;', // Optional list of games that this game builds on. Use markdown.
description, // Longer description. Supports Markdown.
language}) {
function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) {
let navigate = useNavigate();
const routeChange = () =>{
navigate(gameId);
}
if (typeof data === 'undefined') {
return <></>
}
return <div className="game" onClick={routeChange}>
<div className="wrapper">
<div className="title">{title}</div>
<div className="short-description">{intro}
<div className="title">{data.title}</div>
<div className="short-description">{data.short}
</div>
{ image ? <img className="image" src={image} alt="" /> : <div className="image"/> }
<div className="long description"><Markdown>{description}</Markdown></div>
{ data.image ? <img className="image" src={path.join("data", gameId, data.image)} alt="" /> : <div className="image"/> }
<div className="long description"><Markdown>{data.long}</Markdown></div>
</div>
<table className="info">
<tbody>
<tr>
<td title="consider playing these games first.">Prerequisites</td>
<td><Markdown>{prereq}</Markdown></td>
<td><Markdown>{data.prerequisites.join(', ')}</Markdown></td>
</tr>
<tr>
<td>Worlds</td>
<td>{worlds}</td>
<td>{data.worlds}</td>
</tr>
<tr>
<td>Levels</td>
<td>{levels}</td>
<td>{data.levels}</td>
</tr>
<tr>
<td>Language</td>
<td title={`in ${language}`}>{flag[language]}</td>
<td title={`in ${data.languages.join(', ')}`}>{data.languages.map((lan) => flag[lan]).join(', ')}</td>
</tr>
</tbody>
</table>
@@ -88,6 +85,58 @@ function LandingPage() {
const openImpressum = () => setImpressum(true);
const closeImpressum = () => setImpressum(false);
// const [allGames, setAllGames] = React.useState([])
// const [allTiles, setAllTiles] = React.useState([])
// const getTiles=()=>{
// fetch('featured_games.json', {
// headers : {
// 'Content-Type': 'application/json',
// 'Accept': 'application/json'
// }
// }
// ).then(function(response){
// return response.json()
// }).then(function(data) {
// setAllGames(data.featured_games)
// })
// }
// React.useEffect(()=>{
// getTiles()
// },[])
// React.useEffect(()=>{
// Promise.allSettled(
// allGames.map((gameId) => (
// fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined})))
// ).then(responses =>
// responses.forEach((result) => console.log(result)))
// // Promise.all(responses.map(res => {
// // if (res.status == "fulfilled") {
// // console.log(res.value.json())
// // return res.value.json()
// // } else {
// // return undefined
// // }
// // }))
// // ).then(allData => {
// // setAllTiles(allData.map(data => data?.tile))
// // })
// },[allGames])
// TODO: I would like to read the supported games list form a JSON,
// Then load all these games in
//
let allGames = [
"leanprover-community/nng4",
"hhu-adam/robo",
"djvelleman/stg4",
"miguelmarco/STG4",
]
let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
return <div className="landing-page">
<header style={{backgroundImage: `url(${bgImage})`}}>
@@ -104,49 +153,26 @@ function LandingPage() {
</div>
</header>
<div className="game-list">
<GameTile
title="Natural Number Game"
gameId="g/hhu-adam/NNG4"
intro="The classical introduction game for Lean."
description="In this game you recreate the natural numbers $\mathbb{N}$ from the Peano axioms,
learning the basics about theorem proving in Lean.
This is a good first introduction to Lean!"
worlds="4"
levels="30"
language="English"
/>
<GameTile
title="Formaloversum"
gameId="g/hhu-adam/Robo"
intro="Erkunde das Leansche Universum mit deinem Robo, welcher dir bei der Verständigung mit den Formalosophen zur Seite steht."
description="
Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach verschiedene Bereiche des Bachelorstudiums an.
(Das Spiel befindet sich noch in der Entstehungsphase.)"
image={coverRobo}
language="German"
/>
<GameTile
title="NNG (OLD)"
gameId="g/hhu-adam/nng4-old"
intro="The old version of the NNG copied from lean3."
description="This version is not maintained and might break at any point. You should play the new version instead"
worlds="9"
levels="72"
language="English"
/>
{allTiles.length == 0 ?
<p>No Games loaded. Use <a>http://localhost:3000/#/g/local/FOLDER</a> to open a
game directly from a local folder.
</p>
: allGames.map((id, i) => (
<Tile
key={id}
gameId={`g/${id}`}
data={allTiles[i]}
/>
))
}
</div>
<section>
<div className="wrapper">
<h2>Development notes</h2>
<p>
As this server runs lean on our university machines, it has a limited capacity.
Our current estimate is about 55 copies of the NNG or 25 copies of games importing
mathlib. We hope to address this limitation in the future.
Our current estimate is about 70 simultaneous games.
We hope to address and test this limitation better in the future.
</p>
<p>
Most aspects of the games and the infrastructure are still in development. Feel free to
@@ -160,18 +186,19 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
<h2>Adding new games</h2>
<p>
If you are considering writing your own game, you should use
the <a target="_blank" href="https://github.com/hhu-adam/NNG4">NNG Github Repo</a> as
a template.
the <a target="_blank" href="https://github.com/hhu-adam/GameSkeleton">GameSkeleton Github Repo</a> as
a template and read <a target="_blank" href="https://github.com/leanprover-community/lean4game/">How to Create a Game</a>.
</p>
<p>
There is an option to load and run your own games directly on the server,
instructions are in the NNG repo. Since this is still in development we'd like to
encourage you to contact us for support creating your own game. The documentation is
not polished yet.
You can directly load your games into the server and play it using
the correct URL. The <a target="_blank" href="https://github.com/leanprover-community/lean4game/">instructions above</a> also
explain the details for how to load your game to the server.
We'd like to encourage you to contact us if you have any questions.
</p>
<p>
To add games to this main page, you should get in contact as
games will need to be added manually.
Featured games on this page are added manually.
Please get in contact and we-ll happily add yours.
</p>
</div>
</section>
@@ -189,9 +216,6 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet
<a className="link" onClick={openImpressum}>Impressum</a>
{impressum? <PrivacyPolicyPopup handleClose={closeImpressum} />: null}
</footer>
{/* <PrivacyPolicy/> */}
</div>
}
client/src/components/level.tsx
+30 -35
View File
@@ -22,7 +22,7 @@ import { ConnectionContext, connection, useLeanClient } from '../connection'
import { useAppDispatch, useAppSelector } from '../hooks'
import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api'
import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited,
selectHelp, selectDifficulty, selectInventory } from '../state/progress'
selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress'
import { store } from '../state/store'
import { Button } from './button'
import Markdown from './markdown'
@@ -32,8 +32,9 @@ import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContex
ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
import { DualEditor } from './infoview/main'
import { GameHint } from './infoview/rpc_api'
import { DeletedHints, Hint, Hints } from './hints'
import { DeletedHints, Hint, Hints, filterHints } from './hints'
import { PrivacyPolicyPopup } from './popup/privacy_policy'
import path from 'path';
import '@fontsource/roboto/300.css'
import '@fontsource/roboto/400.css'
@@ -48,7 +49,6 @@ function Level() {
const params = useParams()
const levelId = parseInt(params.levelId)
const worldId = params.worldId
// useLoadWorldFiles(worldId)
const [impressum, setImpressum] = React.useState(false)
@@ -138,19 +138,24 @@ function ChatPanel({lastLevel}) {
let introText: Array<string> = level?.data?.introduction.split(/\n(\s*\n)+/)
// experimental: Remove all hints that appeared identically in the previous step
// This effectively prevent consequtive hints being shown.
let modifiedHints : GameHint[][] = filterHints(proof)
return <div className="chat-panel">
<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}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
))}
{proof.map((step, i) => {
{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.length - 1 && withErr)) {
// TODO: Should not use index as key.
return <Hints key={`hints-${i}`}
hints={step.hints} showHidden={showHelp.has(i)} step={i}
hints={step} showHidden={showHelp.has(i)} step={i}
selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
}
})}
@@ -204,11 +209,16 @@ function PlayableLevel({impressum, setImpressum}) {
const {worldId, levelId} = useContext(WorldLevelIdContext)
const {mobile} = React.useContext(MobileContext)
const dispatch = useAppDispatch()
const difficulty = useSelector(selectDifficulty(gameId))
const initialCode = useAppSelector(selectCode(gameId, worldId, levelId))
const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId))
const inventory: Array<String> = useSelector(selectInventory(gameId))
const typewriterMode = useSelector(selectTypewriterMode(gameId))
const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode}))
const gameInfo = useGetGameInfoQuery({game: gameId})
const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -221,12 +231,11 @@ function PlayableLevel({impressum, setImpressum}) {
const [showHelp, setShowHelp] = useState<Set<number>>(new Set())
// Only for mobile layout
const [pageNumber, setPageNumber] = useState(0)
const [typewriterMode, setTypewriterMode] = useState(true)
// set to true to prevent switching between typewriter and editor
const [lockInputMode, setLockInputMode] = useState(false)
const [typewriterInput, setTypewriterInput] = useState("")
const lastLevel = levelId >= gameInfo.data?.worldSize[worldId]
const dispatch = useAppDispatch()
// impressum pop-up
function toggleImpressum() {setImpressum(!impressum)}
@@ -320,8 +329,6 @@ function PlayableLevel({impressum, setImpressum}) {
console.debug(`not inserting template.`)
}
}
} else {
setTypewriterMode(true)
}
}, [level, levelId, worldId, gameId, editor])
@@ -336,7 +343,7 @@ function PlayableLevel({impressum, setImpressum}) {
}, [gameId, worldId, levelId])
useEffect(() => {
if (!typewriterMode) {
if (!typewriterMode && editor) {
// Delete last input attempt from command line
editor.executeEdits("typewriter", [{
range: editor.getSelection(),
@@ -466,6 +473,11 @@ function Introduction({impressum, setImpressum}) {
const gameInfo = useGetGameInfoQuery({game: gameId})
const {worldId} = useContext(WorldLevelIdContext)
let image: string = gameInfo.data?.worlds.nodes[worldId].image
const toggleImpressum = () => {
setImpressum(!impressum)
}
@@ -479,7 +491,13 @@ function Introduction({impressum, setImpressum}) {
:
<Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level`}>
<IntroductionPanel gameInfo={gameInfo} />
<div className="world-image-container empty"></div>
<div className="world-image-container empty">
{image &&
// TODO: Temporary for testing
<img className={worldId=="Proposition" ? "cover" : "contain"} src={path.join("data", gameId, image)} alt="" />
}
</div>
<InventoryPanel levelInfo={inventory?.data} />
</Split>
}
@@ -615,6 +633,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
return () => {
editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}})
model.dispose();
}
}
}, [editor, levelId, connection, leanClientStarted])
@@ -637,27 +656,3 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange
return {editor, infoProvider, editorConnection}
}
/** Open all files in this world on the server so that they will load faster when accessed */
function useLoadWorldFiles(worldId) {
const gameId = React.useContext(GameIdContext)
const gameInfo = useGetGameInfoQuery({game: gameId})
const store = useStore()
useEffect(() => {
if (gameInfo.data) {
const models = []
for (let levelId = 1; levelId <= gameInfo.data.worldSize[worldId]; levelId++) {
const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`)
let model = monaco.editor.getModel(uri)
if (model) {
models.push(model)
} else {
const code = selectCode(gameId, worldId, levelId)(store.getState())
models.push(monaco.editor.createModel(code, 'lean4', uri))
}
}
return () => { for (let model of models) { model.dispose() } }
}
}, [gameInfo.data, worldId])
}