diff --git a/.gitignore b/.gitignore index 9508154..f6fa519 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,4 @@ node_modules -games/ client/dist games/ server/.lake diff --git a/client/src/app.tsx b/client/src/app.tsx index 8420d4b..871c226 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -9,25 +9,37 @@ import '@fontsource/roboto/700.css'; import './css/reset.css'; import './css/app.css'; import { MobileContext } from './components/infoview/context'; -import { useWindowDimensions } from './window_width'; -import { connection } from './connection'; +import { useMobile } from './hooks'; +import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences'; export const GameIdContext = React.createContext(undefined); function App() { + const { mobile, setMobile, lockMobile, setLockMobile } = useMobile(); + const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo - const {width, height} = useWindowDimensions() - const [mobile, setMobile] = React.useState(width < 800) - React.useEffect(() => { - connection.startLeanClient(gameId); - }, [gameId]) + const automaticallyAdjustLayout = () => { + const {width} = getWindowDimensions() + setMobile(width < AUTO_SWITCH_THRESHOLD) + } + + React.useEffect(()=>{ + if (!lockMobile){ + void automaticallyAdjustLayout() + window.addEventListener('resize', automaticallyAdjustLayout) + + return () => { + window.removeEventListener('resize', automaticallyAdjustLayout) + } + } + }, [lockMobile]) return (
- + diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index 2c65a81..ced97d5 100644 --- a/client/src/components/app_bar.tsx +++ b/client/src/components/app_bar.tsx @@ -5,7 +5,7 @@ import * as React from 'react' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, - faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons' + faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from "../app" import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context" import { GameInfo, useGetGameInfoQuery } from '../state/api' @@ -150,22 +150,23 @@ function InventoryButton({pageNumber, setPageNumber}) { } /** the navigation bar on the welcome page */ -export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : { +export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo, togglePreferencesPopup} : { pageNumber: number, setPageNumber: any, gameInfo: GameInfo, toggleImpressum: any, toggleEraseMenu: any, toggleUploadMenu: any, - toggleInfo: any + toggleInfo: any, + togglePreferencesPopup: () => void; }) { const gameId = React.useContext(GameIdContext) const gameProgress = useAppSelector(selectProgress(gameId)) - const {mobile} = React.useContext(MobileContext) + const {mobile, setMobile} = React.useContext(MobileContext) const [navOpen, setNavOpen] = React.useState(false) return
-
+
@@ -194,6 +195,9 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres +
} @@ -237,7 +241,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= : <> {/* DESKTOP VERSION */} -
+
{worldTitle && `World: ${worldTitle}`}
diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index 2692a7d..037eb86 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -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
@@ -43,3 +44,24 @@ export function DeletedHints({hints} : {hints: GameHint[]}) { {hiddenHints.map((hint, i) => )} } + +/** 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)) + } + }) +} diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index fb0ef2b..8a62b36 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -62,12 +62,18 @@ export const ProofStateContext = React.createContext<{ setProofState: () => {}, }) -export const MobileContext = React.createContext<{ +export interface IMobileContext { mobile : boolean, setMobile: React.Dispatch>, -}>({ - mobile : false, + lockMobile: boolean, + setLockMobile: React.Dispatch>, +} + +export const MobileContext = React.createContext({ + mobile: false, setMobile: () => {}, + lockMobile: false, + setLockMobile: () => {} }) export const WorldLevelIdContext = React.createContext<{ diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index c7f553a..c90eba8 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -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. @@ -367,9 +367,9 @@ export function TypewriterInterface({props}) { function deleteProof(line: number) { return (ev) => { let deletedChat: Array = [] - 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) @@ -493,18 +493,20 @@ export function TypewriterInterface({props}) { {props.data?.introduction}
} - {mobile && <> + {mobile && - {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && - - } - } setDisableInput(n > 0) : (n) => {}}/> + + {mobile && i == proof.length - 1 && + hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && + + } + {/* Show a message that there are no goals left */} {!step.goals.length && (
@@ -521,7 +523,7 @@ export function TypewriterInterface({props}) { } })} {mobile && completed && -
+
{props.level >= props.worldSize ?
) } -function InventoryList({items, docType, openDoc, defaultTab=null, level=undefined, enableAll=false} : +function InventoryList({items, docType, openDoc, tab=null, setTab=undefined, level=undefined, enableAll=false} : { items: InventoryTile[], docType: string, openDoc(props: {name: string, type: string}): void, - defaultTab? : string, - level? : LevelInfo|InventoryOverview, + tab?: any, + setTab?: any, + level?: LevelInfo|InventoryOverview, enableAll?: boolean, }) { // TODO: `level` is only used in the `useEffect` below to check if a new level has @@ -59,8 +63,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine } const categories = Array.from(categorySet).sort() - const [tab, setTab] = useState(defaultTab) - // Add inventory items from local store as unlocked. // Items are unlocked if they are in the local store, or if the server says they should be // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different @@ -68,13 +70,6 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine let inv: string[] = selectInventory(gameId)(store.getState()) let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile) - useEffect(() => { - // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading. - // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch. - if (defaultTab) { - setTab(defaultTab) - }}, [level]) - return <> {categories.length > 1 &&
@@ -89,21 +84,26 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine (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 {openDoc({name: item.name, type: docType})}} name={item.name} displayName={item.displayName} locked={difficulty > 0 ? item.locked : false} - disabled={item.disabled} newly={item.new} enableAll={enableAll}/> + disabled={item.disabled} newly={item.new} enableAll={enableAll} /> }) }
} -function InventoryItem({name, displayName, locked, disabled, newly, showDoc, enableAll=false}) { +function InventoryItem({item, name, displayName, locked, disabled, newly, showDoc, enableAll=false}) { const icon = locked ? : - disabled ? : "" + disabled ? : item.st const className = locked ? "locked" : disabled ? "disabled" : newly ? "new" : "" + // Note: This is somewhat a hack as the statement of lemmas comes currently in the form + // `Namespace.statement_name (x y : Nat) : some type` const title = locked ? "Not unlocked yet" : - disabled ? "Not available in this level" : "" + disabled ? "Not available in this level" : (item.altTitle ? item.altTitle.substring(item.altTitle.indexOf(' ') + 1) : '') + + const [copied, setCopied] = useState(false) const handleClick = () => { if (enableAll || !locked) { @@ -111,7 +111,21 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena } } - return
{icon} {displayName}
+ const copyItemName = (ev) => { + navigator.clipboard.writeText(displayName) + setCopied(true) + setInterval(() => { + setCopied(false) + }, 3000); + ev.stopPropagation() + } + +return
+ {icon} {displayName} +
+ {copied ? : } +
+
} export function Documentation({name, type, handleClose}) { @@ -131,16 +145,25 @@ export function Documentation({name, type, handleClose}) { export function InventoryPanel({levelInfo, visible = true}) { const gameId = React.useContext(GameIdContext) + const [lemmaTab, setLemmaTab] = useState(levelInfo?.lemmaTab) + // The inventory is overlayed by the doc entry of a clicked item const [inventoryDoc, setInventoryDoc] = useState<{name: string, type: string}>(null) // Set `inventoryDoc` to `null` to close the doc function closeInventoryDoc() {setInventoryDoc(null)} + useEffect(() => { + // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading. + // `defaultTab` is `null` or `undefined` otherwise, in which case we don't want to switch. + if (levelInfo?.lemmaTab) { + setLemmaTab(levelInfo?.lemmaTab) + }}, [levelInfo]) + return
{inventoryDoc ? : - + }
} diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index c36730a..e2c870f 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -20,6 +20,7 @@ const flag = { 'French': '🇫🇷', 'German': '🇩🇪', 'Italian': '🇮🇹', + 'Spanish': '🇪🇸', } function GithubIcon({url='https://github.com'}) { @@ -131,8 +132,10 @@ function LandingPage() { // let allGames = [ "leanprover-community/nng4", + "hhu-adam/robo", "djvelleman/stg4", - "hhu-adam/robo"] + "miguelmarco/STG4", + ] let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) return
@@ -162,38 +165,14 @@ function LandingPage() { /> )) } - {/* - - - */}

Development notes

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.

Most aspects of the games and the infrastructure are still in development. Feel free to @@ -207,18 +186,19 @@ This is a good first introduction to Lean!"

Adding new games

If you are considering writing your own game, you should use - the NNG Github Repo as - a template. + the GameSkeleton Github Repo as + a template and read How to Create a Game.

- 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 instructions above 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.

- 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.

@@ -236,9 +216,6 @@ This is a good first introduction to Lean!" Impressum {impressum? : null} - - {/* */} -
} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 1246398..4b5a53d 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -18,7 +18,6 @@ import { EditorConnection, EditorEvents } from '../../../node_modules/lean4-info import { EventEmitter } from '../../../node_modules/lean4-infoview/src/infoview/event' import { GameIdContext } from '../app' -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, @@ -32,7 +31,7 @@ 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'; @@ -44,6 +43,15 @@ import 'lean4web/client/src/editor/infoview.css' import 'lean4web/client/src/editor/vscode.css' import '../css/level.css' import { LevelAppBar } from './app_bar' +import { LeanClient } from 'lean4web/client/src/editor/leanclient' +import { DisposingWebSocketMessageReader } from 'lean4web/client/src/reader' +import { WebSocketMessageWriter, toSocket } from 'vscode-ws-jsonrpc' +import { IConnectionProvider } from 'monaco-languageclient' +import { monacoSetup } from 'lean4web/client/src/monacoSetup' +import { onigasmH } from 'onigasm/lib/onigasmH' + + +monacoSetup() function Level() { const params = useParams() @@ -138,19 +146,24 @@ function ChatPanel({lastLevel}) { let introText: Array = 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
{introText?.filter(t => t.trim()).map(((t, i) => + // Show the level's intro text as hints, too ))} - {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 } })} @@ -206,15 +219,13 @@ function PlayableLevel({impressum, setImpressum}) { 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 = useSelector(selectInventory(gameId)) const typewriterMode = useSelector(selectTypewriterMode(gameId)) const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) - const gameInfo = useGetGameInfoQuery({game: gameId}) + const gameInfo = useGetGameInfoQuery({game: gameId}) const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) // The state variables for the `ProofContext` @@ -288,12 +299,6 @@ function PlayableLevel({impressum, setImpressum}) { // a hint at the beginning of the proof... const [selectedStep, setSelectedStep] = useState() - // if the user inventory changes, notify the server - useEffect(() => { - let leanClient = connection.getLeanClient(gameId) - leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty}) - }, [inventory]) - useEffect (() => { // Lock editor mode if (level?.data?.template) { @@ -367,7 +372,7 @@ function PlayableLevel({impressum, setImpressum}) { // Effect when command line mode gets enabled useEffect(() => { - if (editor && typewriterMode) { + if (onigasmH && editor && typewriterMode) { let code = editor.getModel().getLinesContent().filter(line => line.trim()) editor.executeEdits("typewriter", [{ range: editor.getModel().getFullModelRange(), @@ -390,7 +395,7 @@ function PlayableLevel({impressum, setImpressum}) { // editor.setSelection(monaco.Selection.fromPositions(endPos, endPos)) // } } - }, [editor, typewriterMode]) + }, [editor, typewriterMode, onigasmH == null]) return <>
@@ -436,6 +441,7 @@ function PlayableLevel({impressum, setImpressum}) { function IntroductionPanel({gameInfo}) { const gameId = React.useContext(GameIdContext) const {worldId} = useContext(WorldLevelIdContext) + const {mobile} = React.useContext(MobileContext) let text: Array = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/) @@ -446,7 +452,7 @@ function IntroductionPanel({gameInfo}) { hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} /> ))}
-
+
{gameInfo.data?.worldSize[worldId] == 0 ? :