diff --git a/.env b/.env deleted file mode 100644 index 01fee6b..0000000 --- a/.env +++ /dev/null @@ -1 +0,0 @@ -LEAN4GAME_SINGLE_GAME=false diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 2e2d4bc..00d2e43 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -5,7 +5,17 @@ jobs: build: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - name: install elan + run: | + set -o pipefail + curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y + echo "$HOME/.elan/bin" >> $GITHUB_PATH + - uses: actions/checkout@v4 - uses: actions/setup-node@v3 + - name: print lean and lake versions + run: | + lean --version + lake --version - run: npm install - run: npm run build diff --git a/.gitignore b/.gitignore index 26b77df..f6fa519 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ node_modules client/dist -server/build -**/lake-packages/ +games/ +server/.lake +**/.DS_Store diff --git a/NOTES.md b/NOTES.md index 0d8de95..a4bc3f1 100644 --- a/NOTES.md +++ b/NOTES.md @@ -15,9 +15,6 @@ npm install -g http-server ``` git clone https://github.com/hhu-adam/NNG4.git -cd NNG4 -docker rmi nng4:latest -docker build --pull --rm -f "Dockerfile" -t nng4:latest "." ``` @@ -146,12 +143,6 @@ Activate config: ``` -## Install `unzip` for Importing Docker Images - -``` -sudo apt-get install unzip -``` - ## Install bubblewrap (bwrap) ``` sudo apt-get install bubblewrap diff --git a/README.md b/README.md index 13a2aa2..b5a610a 100644 --- a/README.md +++ b/README.md @@ -2,30 +2,33 @@ This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de). -The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game -(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) -of Kevin Buzzard and Mohammad Pedramfar. -The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4). - ## Creating a Game -Please follow the tutorial [Creating a Game](doc/create_game.md). -In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md). +Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest: -### Publishing a Game +* Step 5: [How to Run Games Locally](doc/running_locally.md) +* Step 7: [How to Update an existing Game](doc/update_game.md) +* Step 8: [How to Publishing a Game](doc/publish_game.md) -We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language. +## Documentation -For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster). +The documentation is very much work in progress but the linked documentation here +should be up-to-date: -## Documentation +### Game creation API + +- [Creating a Game](doc/create_game.md): **the main document to consult**. +- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic. -The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game. +### Frontend API -Some documentation: +* [How to Run Games Locally](doc/running_locally.md): play a game on your computer +* [How to Update an existing Game](doc/update_game.md): update to a new lean version +* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play -- [NPM Scripts](doc/npm_scripts.md) -- [Old documentation](doc/DOCUMENTATION.md) +### Backend + +not written yet ## Contributing @@ -34,3 +37,10 @@ Contributions to `lean4game` are always welcome! ## Security Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap. + +## Credits + +The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game +(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) +by Kevin Buzzard and Mohammad Pedramfar. +The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4). diff --git a/client/src/app.tsx b/client/src/app.tsx index b0ef13c..8420d4b 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -6,33 +6,28 @@ import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; -import './reset.css'; -import './app.css'; +import './css/reset.css'; +import './css/app.css'; import { MobileContext } from './components/infoview/context'; import { useWindowDimensions } from './window_width'; -import { selectOpenedIntro } from './state/progress'; -import { useSelector } from 'react-redux'; +import { connection } from './connection'; export const GameIdContext = React.createContext(undefined); function App() { const params = useParams() const gameId = "g/" + params.owner + "/" + params.repo - - // TODO: Make mobileLayout be changeable in settings - // TODO: Handle resize Events const {width, height} = useWindowDimensions() const [mobile, setMobile] = React.useState(width < 800) - // On mobile, there are multiple pages on the welcome page to switch between - const openedIntro = useSelector(selectOpenedIntro(gameId)) - // On mobile, there are multiple pages to switch between - const [pageNumber, setPageNumber] = React.useState(openedIntro ? 1 : 0) + React.useEffect(() => { + connection.startLeanClient(gameId); + }, [gameId]) return (
- + diff --git a/client/src/assets/covers/formaloversum.png b/client/src/assets/covers/formaloversum.png deleted file mode 100644 index df9723d..0000000 Binary files a/client/src/assets/covers/formaloversum.png and /dev/null differ diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index 530636e..2c65a81 100644 --- a/client/src/components/app_bar.tsx +++ b/client/src/components/app_bar.tsx @@ -1,45 +1,45 @@ +/** + * @file contains the navigation bars of the app. + */ 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' import { GameIdContext } from "../app" import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context" import { GameInfo, useGetGameInfoQuery } from '../state/api' import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress' -import { useSelector } from 'react-redux' import { useAppDispatch, useAppSelector } from '../hooks' import { Button } from './button' -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' -import { PrivacyPolicyPopup } from './popup/privacy_policy' -import { WorldSelectionMenu, downloadFile } from './world_tree' +import { downloadProgress } from './popup/erase' -/** navigation to switch between pages on mobile */ -function MobileNav({pageNumber, setPageNumber}: +/** navigation buttons for mobile welcome page to switch between intro/tree/inventory. */ +function MobileNavButtons({pageNumber, setPageNumber}: { pageNumber: number, setPageNumber: any}) { const gameId = React.useContext(GameIdContext) const dispatch = useAppDispatch() - let prevText = {0 : null, 1: "Intro", 2: null}[pageNumber] - let prevIcon = {0 : null, 1: null, 2: faBookOpen}[pageNumber] - let prevTitle = { - 0: null, - 1: "Game Introduction", - 2: "World selection"}[pageNumber] - let nextText = {0 : "Start", 1: null, 2: null}[pageNumber] - let nextIcon = {0 : null, 1: faBook, 2: null}[pageNumber] - let nextTitle = { - 0: "World selection", - 1: "Inventory", - 2: null}[pageNumber] + // if `prevText` or `prevIcon` is set, show a button to go back + let prevText = {0: null, 1: "Intro", 2: null}[pageNumber] + let prevIcon = {0: null, 1: null, 2: faBookOpen}[pageNumber] + let prevTitle = {0: null, 1: "Game Introduction", 2: "World selection"}[pageNumber] + // if `nextText` or `nextIcon` is set, show a button to go forward + let nextText = {0: "Start", 1: null, 2: null}[pageNumber] + let nextIcon = {0: null, 1: faBook, 2: null}[pageNumber] + let nextTitle = {0: "World selection", 1: "Inventory", 2: null}[pageNumber] return <> - {(prevText || prevTitle || prevIcon) && - } - {(nextText || nextTitle || nextIcon) && + {(nextText || nextIcon) && +} + +/** button to go one level futher. + * for the last level, this button turns into a button going back to the welcome page. + */ +function NextButton({worldSize, difficulty, completed, setNavOpen}) { const gameId = React.useContext(GameIdContext) - const {mobile, pageNumber, setPageNumber} = React.useContext(MobileContext) - const [navOpen, setNavOpen] = React.useState(false) + const {worldId, levelId} = React.useContext(WorldLevelIdContext) + return (levelId < worldSize ? + + : + + ) +} +/** button to go one level back. + * only renders if the current level id is > 0. + */ +function PreviousButton({setNavOpen}) { + const gameId = React.useContext(GameIdContext) + const {worldId, levelId} = React.useContext(WorldLevelIdContext) + return (levelId > 0 && <> + + ) +} +/** button to toggle between editor and typewriter */ +function InputModeButton({setNavOpen, isDropdown}) { + const {levelId} = React.useContext(WorldLevelIdContext) + const {typewriterMode, setTypewriterMode, lockInputMode} = React.useContext(InputModeContext) - /** Download the current progress (i.e. what's saved in the browser store) */ - const gameProgress = useSelector(selectProgress(gameId)) - const downloadProgress = (e) => { - e.preventDefault() - downloadFile({ - data: JSON.stringify(gameProgress, null, 2), - fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`, - fileType: 'text/json', - }) + /** toggle input mode if allowed */ + function toggleInputMode(ev: React.MouseEvent) { + if (!lockInputMode){ + setTypewriterMode(!typewriterMode) + setNavOpen(false) + } } + return +} - return
- <> -
- - -
-
- - {mobile ? '' : gameInfo?.title} - -
-
- {mobile && <> - {/* BUTTONS for MOBILE */} - +/** button to toggle iimpressum popup */ +function ImpressumButton({setNavOpen, toggleImpressum, isDropdown}) { + return +} - } +/** button to go back to welcome page */ +function HomeButton({isDropdown}) { + const gameId = React.useContext(GameIdContext) + return +} - +/** button in mobile level to toggle inventory. + * only displays a button if `setPageNumber` is set. + */ +function InventoryButton({pageNumber, setPageNumber}) { + return (setPageNumber && + + ) +} -
-
- {/* {levelId < gameInfo.data?.worldSize[worldId] && - - } - {levelId > 0 && <> - - } - - */} +/** the navigation bar on the welcome page */ +export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpressum, toggleEraseMenu, toggleUploadMenu, toggleInfo} : { + pageNumber: number, + setPageNumber: any, + gameInfo: GameInfo, + toggleImpressum: any, + toggleEraseMenu: any, + toggleUploadMenu: any, + toggleInfo: any +}) { + const gameId = React.useContext(GameIdContext) + const gameProgress = useAppSelector(selectProgress(gameId)) + const {mobile} = React.useContext(MobileContext) + const [navOpen, setNavOpen] = React.useState(false) - - - - - -
- + return
+
+ + +
+
+ {!mobile && {gameInfo?.title}} +
+
+ {mobile && } + +
+
+ + + + + +
- - - } -// /** The menu that is shown next to the world selection graph */ -// function WorldSelectionMenu() { -// const [file, setFile] = React.useState(); - -// const gameId = React.useContext(GameIdContext) -// const store = useStore() -// const difficulty = useSelector(selectDifficulty(gameId)) - - -// /* state variables to toggle the pop-up menus */ -// const [eraseMenu, setEraseMenu] = React.useState(false); -// const openEraseMenu = () => setEraseMenu(true); -// const closeEraseMenu = () => setEraseMenu(false); -// const [uploadMenu, setUploadMenu] = React.useState(false); -// const openUploadMenu = () => setUploadMenu(true); -// const closeUploadMenu = () => setUploadMenu(false); - -// const gameProgress = useSelector(selectProgress(gameId)) -// const dispatch = useAppDispatch() - -// /** Download the current progress (i.e. what's saved in the browser store) */ -// const downloadProgress = (e) => { -// e.preventDefault() -// downloadFile({ -// data: JSON.stringify(gameProgress, null, 2), -// fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`, -// fileType: 'text/json', -// }) -// } - -// const handleFileChange = (e) => { -// if (e.target.files) { -// setFile(e.target.files[0]) -// } -// } - -// /** Upload progress from a */ -// const uploadProgress = (e) => { -// if (!file) {return} -// const fileReader = new FileReader() -// fileReader.readAsText(file, "UTF-8") -// fileReader.onload = (e) => { -// const data = JSON.parse(e.target.result.toString()) as GameProgressState -// console.debug("Json Data", data) -// dispatch(loadProgress({game: gameId, data: data})) -// } -// closeUploadMenu() -// } - -// const eraseProgress = () => { -// dispatch(deleteProgress({game: gameId})) -// closeEraseMenu() -// } - -// const downloadAndErase = (e) => { -// downloadProgress(e) -// eraseProgress() -// } - -// function label(x : number) { -// return x == 0 ? 'none' : x == 1 ? 'lax' : 'regular' -// } - -// return -// } - - -/** The top-navigation bar */ -export function LevelAppBar({ - isLoading, levelTitle, impressum, toggleImpressum, - pageNumber = undefined, setPageNumber = undefined, lockEditorMode=false}) { +/** the navigation bar in a level */ +export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=undefined, setPageNumber=undefined} : { + isLoading: boolean, + levelTitle: string, + toggleImpressum: any, + pageNumber?: number, + setPageNumber?: any, +}) { const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) - const gameInfo = useGetGameInfoQuery({game: gameId}) - const {mobile} = React.useContext(MobileContext) - - const difficulty = useSelector(selectDifficulty(gameId)) - const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) - - const { typewriterMode, setTypewriterMode } = React.useContext(InputModeContext) - const [navOpen, setNavOpen] = React.useState(false) + const gameInfo = useGetGameInfoQuery({game: gameId}) + const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) + const difficulty = useAppSelector(selectDifficulty(gameId)) - function toggleEditor(ev) { - if (!lockEditorMode){ - setTypewriterMode(!typewriterMode) - setNavOpen(false) - } - } + let worldTitle = gameInfo.data?.worlds.nodes[worldId].title return
{mobile ? <> {/* MOBILE VERSION */}
- - {levelTitle} - + {levelTitle}
- {mobile && pageNumber == 0 ? - - : pageNumber == 1 && - - } - + +
- {levelId < gameInfo.data?.worldSize[worldId] && - - } - {levelId > 0 && <> - - } - - - + + + + +
- - : + : <> {/* DESKTOP VERSION */}
- - - {gameInfo.data?.worlds.nodes[worldId].title && `World: ${gameInfo.data?.worlds.nodes[worldId].title}`} - + + {worldTitle && `World: ${worldTitle}`}
- - {levelTitle} - + {levelTitle}
- {levelId > 0 && <> - - } - {levelId < gameInfo.data?.worldSize[worldId] ? - - : - - } - - + + + +
} 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 e5b4037..fb0ef2b 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -65,13 +65,9 @@ export const ProofStateContext = React.createContext<{ export const MobileContext = React.createContext<{ mobile : boolean, setMobile: React.Dispatch>, - pageNumber: number, - setPageNumber: React.Dispatch> }>({ mobile : false, setMobile: () => {}, - pageNumber: 0, - setPageNumber: () => {} }) export const WorldLevelIdContext = React.createContext<{ @@ -108,10 +104,14 @@ export const InputModeContext = React.createContext<{ typewriterMode: boolean, setTypewriterMode: React.Dispatch>, typewriterInput: string, - setTypewriterInput: React.Dispatch> + setTypewriterInput: React.Dispatch>, + lockInputMode: boolean, + setLockInputMode: React.Dispatch>, }>({ typewriterMode: true, setTypewriterMode: () => {}, typewriterInput: "", setTypewriterInput: () => {}, + lockInputMode: false, + setLockInputMode: () => {}, }); diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index c9848fe..048aef8 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -6,7 +6,7 @@ import type { DidCloseTextDocumentParams, DidChangeTextDocumentParams, Location, import 'tachyons/css/tachyons.css'; import '@vscode/codicons/dist/codicon.css'; import '../../../../node_modules/lean4-infoview/src/infoview/index.css'; -import './infoview.css' +import '../../css/infoview.css' import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api'; import { useClientNotificationEffect, useServerNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util'; @@ -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. @@ -137,9 +137,7 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
{data?.descrText && - {data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : "" // data?.descrText && "**Exercise**: " - + data?.descrText - } + {(data?.displayName ? `**Theorem** \`${data?.displayName}\`: ` : '') + data?.descrText} } {data?.descrFormat && showLeanStatement && @@ -158,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) { @@ -349,6 +347,7 @@ export function TypewriterInterface({props}) { const uri = model.uri.toString() const [disableInput, setDisableInput] = React.useState(false) + const [loadingProgress, setLoadingProgress] = React.useState(0) const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) const {mobile} = React.useContext(MobileContext) const { proof } = React.useContext(ProofContext) @@ -368,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) @@ -457,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
@@ -523,7 +533,7 @@ export function TypewriterInterface({props}) { }
} - : + : }
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 04bd9ba..b2432a0 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -1,6 +1,6 @@ import * as React from 'react'; import { useState, useEffect } from 'react'; -import './inventory.css' +import '../css/inventory.css' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faLock, faBan } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app'; @@ -159,7 +159,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 {openDoc({name: item.name, type: docType})}} diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index b395c89..e2c870f 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -6,12 +6,13 @@ import '@fontsource/roboto/400.css'; import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; -import './landing_page.css' -import coverRobo from '../assets/covers/formaloversum.png' +import '../css/landing_page.css' 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'}) {
} -function GameTile({ - title, - gameId, - intro, // Catchy intro phrase. - image=null, - worlds='?', - levels='?', - prereq='–', // 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
-
{title}
-
{intro} +
{data.title}
+
{data.short}
- { image ? :
} -
{description}
+ { data.image ? :
} +
{data.long}
- + - + - + - +
Prerequisites{prereq}{data.prerequisites.join(', ')}
Worlds{worlds}{data.worlds}
Levels{levels}{data.levels}
Language{flag[language]}{data.languages.map((lan) => flag[lan]).join(', ')}
@@ -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
@@ -104,49 +153,26 @@ function LandingPage() {
- - - - - - + {allTiles.length == 0 ? +

No Games loaded. Use http://localhost:3000/#/g/local/FOLDER to open a + game directly from a local folder. +

+ : allGames.map((id, i) => ( + + )) + }

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 @@ -160,18 +186,19 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet

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

@@ -189,9 +216,6 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet Impressum {impressum? : null} - - {/* */} -
} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 11bae70..579b947 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -4,7 +4,7 @@ import { useSelector, useStore } from 'react-redux' import Split from 'react-split' import { useParams } from 'react-router-dom' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faBars, faCode, faXmark, faHome, faCircleInfo, faArrowRight, faArrowLeft, faTerminal } from '@fortawesome/free-solid-svg-icons' +import { faHome, faArrowRight } from '@fortawesome/free-solid-svg-icons' import { CircularProgress } from '@mui/material' import type { Location } from 'vscode-languageserver-protocol' import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' @@ -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' @@ -41,14 +42,13 @@ import '@fontsource/roboto/500.css' import '@fontsource/roboto/700.css' import 'lean4web/client/src/editor/infoview.css' import 'lean4web/client/src/editor/vscode.css' -import './level.css' +import '../css/level.css' import { LevelAppBar } from './app_bar' 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 = 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 } })} @@ -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 = 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,10 +231,11 @@ function PlayableLevel({impressum, setImpressum}) { const [showHelp, setShowHelp] = useState>(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)} @@ -318,8 +329,6 @@ function PlayableLevel({impressum, setImpressum}) { console.debug(`not inserting template.`) } } - } else { - setTypewriterMode(true) } }, [level, levelId, worldId, gameId, editor]) @@ -334,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(), @@ -392,18 +401,16 @@ function PlayableLevel({impressum, setImpressum}) {
- + + toggleImpressum={toggleImpressum} /> {mobile? // TODO: This is copied from the `Split` component below... <> @@ -466,12 +473,17 @@ 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) } return <> - + {gameInfo.isLoading ?
: mobile ? @@ -479,8 +491,14 @@ function Introduction({impressum, setImpressum}) { : -
- +
+ {image && + // TODO: Temporary for testing + + } + +
+ } @@ -615,7 +633,8 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange return () => { editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}}) - model.dispose(); } + 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]) -} diff --git a/client/src/components/popup/erase.tsx b/client/src/components/popup/erase.tsx index 73088f8..b445532 100644 --- a/client/src/components/popup/erase.tsx +++ b/client/src/components/popup/erase.tsx @@ -9,6 +9,15 @@ import { deleteProgress, selectProgress } from '../../state/progress' import { downloadFile } from '../world_tree' import { Button } from '../button' +/** download the current progress (i.e. what's saved in the browser store) */ +export function downloadProgress(gameId: string, gameProgress: any, ev: React.MouseEvent) { + ev.preventDefault() + downloadFile({ + data: JSON.stringify(gameProgress, null, 2), + fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`, + fileType: 'text/json', + }) +} /** Pop-up to delete game progress. * @@ -20,23 +29,13 @@ export function ErasePopup ({handleClose}) { const gameProgress = useSelector(selectProgress(gameId)) const dispatch = useAppDispatch() - /** Download the current progress (i.e. what's saved in the browser store) */ - const downloadProgress = (e) => { - e.preventDefault() - downloadFile({ - data: JSON.stringify(gameProgress, null, 2), - fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`, - fileType: 'text/json', - }) - } - const eraseProgress = () => { dispatch(deleteProgress({game: gameId})) handleClose() } - const downloadAndErase = (e) => { - downloadProgress(e) + const downloadAndErase = (ev) => { + downloadProgress(gameId, gameProgress, ev) eraseProgress() } diff --git a/client/src/components/welcome.tsx b/client/src/components/welcome.tsx index b4b12e8..cc2e0af 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -1,13 +1,13 @@ import * as React from 'react' -import { useState, useEffect } from 'react' +import { useEffect } from 'react' import Split from 'react-split' import { Box, CircularProgress } from '@mui/material' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faGlobe, faArrowRight, faArrowLeft } from '@fortawesome/free-solid-svg-icons' +import { faArrowRight } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' -import { useAppDispatch } from '../hooks' -import { changedOpenedIntro } from '../state/progress' +import { useAppDispatch, useAppSelector } from '../hooks' +import { changedOpenedIntro, selectOpenedIntro } from '../state/progress' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api' import { Button } from './button' import { MobileContext } from './infoview/context' @@ -19,14 +19,14 @@ import { RulesHelpPopup } from './popup/rules_help' import { UploadPopup } from './popup/upload' import { WorldTreePanel } from './world_tree' -import './welcome.css' +import '../css/welcome.css' import { WelcomeAppBar } from './app_bar' import { Hint } from './hints' -/** The panel showing the game's introduction text */ -function IntroductionPanel({introduction}: {introduction: string}) { - const {mobile, setPageNumber} = React.useContext(MobileContext) +/** the panel showing the game's introduction text */ +function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) { + const {mobile} = React.useContext(MobileContext) const gameId = React.useContext(GameIdContext) const dispatch = useAppDispatch() @@ -46,11 +46,6 @@ function IntroductionPanel({introduction}: {introduction: string}) { : <> ))}
- {/* -

{title}

- {introduction} - - */} {mobile &&