From 0a057913bebd79459460fa93f90173bb76819814 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 03:16:26 +0100 Subject: [PATCH 01/32] update landing page --- client/src/components/landing_page.tsx | 53 ++++++++------------------ 1 file changed, 15 insertions(+), 38 deletions(-) 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} - - {/* */} - } From a1a6862b5afc06209e75eff912dc98b2bf049048 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 10:18:00 +0100 Subject: [PATCH 02/32] add tmp option to test images --- client/src/components/level.tsx | 5 +++-- client/src/css/level.css | 7 ++++++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 1246398..859711c 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -214,7 +214,7 @@ function PlayableLevel({impressum, setImpressum}) { 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` @@ -488,7 +488,8 @@ function Introduction({impressum, setImpressum}) {
{image && - + // TODO: Temporary for testing + }
diff --git a/client/src/css/level.css b/client/src/css/level.css index 01d36b6..3dc397b 100644 --- a/client/src/css/level.css +++ b/client/src/css/level.css @@ -342,10 +342,15 @@ td code { justify-content: center; } -.world-image-container img { +.world-image-container img.contain { object-fit: contain; } +.world-image-container img.cover { + height: 100%; + object-fit: cover; +} + .typewriter-interface .proof { background-color: #fff; } From c2b9175fe5fbde9e442d1122e8d1d651b6dda9d2 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 18:14:35 +0100 Subject: [PATCH 03/32] use the gameserver of each game individually --- server/bubblewrap.sh | 6 ++++-- server/index.mjs | 15 ++++++++++++--- server/lakefile.lean | 20 ++++++++++++++++++++ 3 files changed, 36 insertions(+), 5 deletions(-) diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh index 6f6cd20..53ed95f 100755 --- a/server/bubblewrap.sh +++ b/server/bubblewrap.sh @@ -2,7 +2,9 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) - +# $1 : the game directory +# $2 : the lean4game folder +# $3 : the gameserver executable (exec bwrap\ --bind $2 /lean4game \ @@ -25,5 +27,5 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) --unshare-cgroup \ --die-with-parent \ --chdir "/lean4game/server/.lake/build/bin/" \ - ./gameserver --server /game + $3 --server /game ) diff --git a/server/index.mjs b/server/index.mjs index 743af10..4b78bb8 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -95,11 +95,20 @@ function startServerProcess(owner, repo) { let serverProcess if (isDevelopment) { let args = ["--server", game_dir] - serverProcess = cp.spawn("./gameserver", args, // TODO: find gameserver inside the games - { cwd: path.join(__dirname, "./.lake/build/bin/") }) + let executable = path.join(game_dir, ".lake", "packages", "GameServer", ".lake", "build", "bin", "gameserver") + if (fs.existsSync(executable)) { + // Try to use the game's own copy of `gameserver`. + serverProcess = cp.spawn(executable, args, { cwd: game_dir }) + } else { + // If the game is built with `-Klean4game.local` there is no copy in the lake packages. + serverProcess = cp.spawn("./gameserver", args, + { cwd: path.join(__dirname, ".lake", "build", "bin") }) + } } else { serverProcess = cp.spawn("./bubblewrap.sh", - [game_dir, path.join(__dirname, '..')], + [ game_dir, + path.join(__dirname, '..'), + path.join(game_dir, ".lake", "packages", "GameServer", ".lake", "build", "bin", "gameserver")], { cwd: __dirname }) } serverProcess.on('error', error => diff --git a/server/lakefile.lean b/server/lakefile.lean index 851c78d..1adad98 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -15,3 +15,23 @@ lean_exe gameserver { root := `Main supportInterpreter := true } + +/-- +When a package depending on GameServer updates its dependencies, +build the `gameserver` executable. +-/ +post_update pkg do + let rootPkg ← getRootPackage + if rootPkg.name = pkg.name then + return -- do not run in GameServer itself + + /- + TODO: Could we use the Lake API instead of spawning a new process? + -/ + let toolchain := ← IO.FS.readFile <| pkg.dir / "lean-toolchain" + let exitCode ← IO.Process.spawn { + cmd := "elan" + args := #["run", toolchain.trim, "lake", "build", "gameserver"] + } >>= (·.wait) + if exitCode ≠ 0 then + logError s!"{pkg.name}: failed to build gameserver" From 4f5256fa88068d2124f682bac88590cb1a3ae580 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 18:32:45 +0100 Subject: [PATCH 04/32] fix bubblewrap script --- server/bubblewrap.sh | 4 ++-- server/index.mjs | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/server/bubblewrap.sh b/server/bubblewrap.sh index 53ed95f..1d21183 100755 --- a/server/bubblewrap.sh +++ b/server/bubblewrap.sh @@ -26,6 +26,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) --unshare-uts \ --unshare-cgroup \ --die-with-parent \ - --chdir "/lean4game/server/.lake/build/bin/" \ - $3 --server /game + --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \ + ./gameserver --server /game ) diff --git a/server/index.mjs b/server/index.mjs index 4b78bb8..ed07215 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -106,11 +106,11 @@ function startServerProcess(owner, repo) { } } else { serverProcess = cp.spawn("./bubblewrap.sh", - [ game_dir, - path.join(__dirname, '..'), - path.join(game_dir, ".lake", "packages", "GameServer", ".lake", "build", "bin", "gameserver")], + [ game_dir, path.join(__dirname, '..')], { cwd: __dirname }) } + + serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`) ) From 72e4011c6298871da4f10a5f9624cf90b1c9aac1 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 18:35:29 +0100 Subject: [PATCH 05/32] update vite --- package-lock.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/package-lock.json b/package-lock.json index 5f190c3..65f056c 100644 --- a/package-lock.json +++ b/package-lock.json @@ -16122,9 +16122,9 @@ } }, "node_modules/vite": { - "version": "4.5.0", - "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.0.tgz", - "integrity": "sha512-ulr8rNLA6rkyFAlVWw2q5YJ91v098AFQ2R0PRFwPzREXOUJQPtFUG0t+/ZikhaOCDqFoDhN6/v8Sq0o4araFAw==", + "version": "4.5.1", + "resolved": "https://registry.npmjs.org/vite/-/vite-4.5.1.tgz", + "integrity": "sha512-AXXFaAJ8yebyqzoNB9fu2pHoo/nWX+xZlaRwoeYUxEqBO+Zj4msE5G+BhGBll9lYEKv9Hfks52PAF2X7qDYXQA==", "dependencies": { "esbuild": "^0.18.10", "postcss": "^8.4.27", From 13d54ff0ff3db47f85f778fdeca090bba08632f3 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 20:38:35 +0100 Subject: [PATCH 06/32] fix gameserver path --- server/index.mjs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/index.mjs b/server/index.mjs index ed07215..9336cb5 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -95,7 +95,7 @@ function startServerProcess(owner, repo) { let serverProcess if (isDevelopment) { let args = ["--server", game_dir] - let executable = path.join(game_dir, ".lake", "packages", "GameServer", ".lake", "build", "bin", "gameserver") + let executable = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin", "gameserver") if (fs.existsSync(executable)) { // Try to use the game's own copy of `gameserver`. serverProcess = cp.spawn(executable, args, { cwd: game_dir }) From cb7224934cd914f0c51fca0e208bdb8d711f90b0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 8 Dec 2023 21:06:31 +0100 Subject: [PATCH 07/32] fix cwd for gameserver --- server/index.mjs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/server/index.mjs b/server/index.mjs index 9336cb5..32dea26 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -95,10 +95,11 @@ function startServerProcess(owner, repo) { let serverProcess if (isDevelopment) { let args = ["--server", game_dir] - let executable = path.join(game_dir, ".lake", "packages", "GameServer", "server", ".lake", "build", "bin", "gameserver") - if (fs.existsSync(executable)) { + 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 + if (fs.existsSync(binDir)) { // Try to use the game's own copy of `gameserver`. - serverProcess = cp.spawn(executable, args, { cwd: game_dir }) + serverProcess = cp.spawn("./gameserver", args, { cwd: binDir }) } else { // If the game is built with `-Klean4game.local` there is no copy in the lake packages. serverProcess = cp.spawn("./gameserver", args, From f6738faf461e827ced6e0c9e0035004963c13155 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 9 Dec 2023 10:52:41 +0100 Subject: [PATCH 08/32] golf --- server/lakefile.lean | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/server/lakefile.lean b/server/lakefile.lean index 1adad98..dc2f526 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -24,14 +24,4 @@ post_update pkg do let rootPkg ← getRootPackage if rootPkg.name = pkg.name then return -- do not run in GameServer itself - - /- - TODO: Could we use the Lake API instead of spawning a new process? - -/ - let toolchain := ← IO.FS.readFile <| pkg.dir / "lean-toolchain" - let exitCode ← IO.Process.spawn { - cmd := "elan" - args := #["run", toolchain.trim, "lake", "build", "gameserver"] - } >>= (·.wait) - if exitCode ≠ 0 then - logError s!"{pkg.name}: failed to build gameserver" + discard <| runBuild gameserver.build >>= (·.await) From c89e2e40203f6afeb679bfb3749a383ca52deda2 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 9 Dec 2023 13:27:03 +0100 Subject: [PATCH 09/32] remove consequtive identical hints #142 --- client/src/components/hints.tsx | 21 +++++++++++++++++++++ client/src/components/infoview/main.tsx | 6 +++--- client/src/components/level.tsx | 11 ++++++++--- 3 files changed, 32 insertions(+), 6 deletions(-) diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index 2692a7d..a2379d2 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,23 @@ 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. + * + * 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) => proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined) + } + }) +} diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index c7f553a..048aef8 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) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 859711c..1251645 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -32,7 +32,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'; @@ -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 } })} From 25f166f57f7bf78b52e622a8477922a9a7de6649 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 9 Dec 2023 22:06:12 +0100 Subject: [PATCH 10/32] do not filter hidden hints #142 --- client/src/components/hints.tsx | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index a2379d2..037eb86 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -49,7 +49,7 @@ export function DeletedHints({hints} : {hints: GameHint[]}) { * * 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. + * appearing in the previous step. Hidden hints are not filtered. * * This effectively means we prevent consequtive identical hints from being shown. */ @@ -60,7 +60,8 @@ export function filterHints(proof: ProofStep[]): GameHint[][] { } 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) => proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined) + return step.hints.filter((hint) => hint.hidden || + (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)) } }) } From 527f58e3a46523efeeae07f70c180ff20143a257 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 9 Dec 2023 22:42:40 +0100 Subject: [PATCH 11/32] separate lean server from socket server --- .gitignore | 1 - doc/DOCUMENTATION.md | 3 ++- ecosystem.config.cjs | 2 +- package.json | 4 ++-- {server => relay}/bubblewrap.sh | 0 {server => relay}/import.mjs | 16 ++++++++-------- {server => relay}/index.mjs | 5 ++--- {server => relay}/unpack.sh | 2 +- server/.gitignore | 3 --- tsconfig.json | 2 +- vite.config.ts | 2 +- 11 files changed, 18 insertions(+), 22 deletions(-) rename {server => relay}/bubblewrap.sh (100%) rename {server => relay}/import.mjs (83%) rename {server => relay}/index.mjs (97%) rename {server => relay}/unpack.sh (99%) delete mode 100644 server/.gitignore 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/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md index 2ff0ab7..68464ca 100644 --- a/doc/DOCUMENTATION.md +++ b/doc/DOCUMENTATION.md @@ -297,8 +297,9 @@ cd lean4game npm install ``` +TODO: This is outdated! If you are developing a game other than `Robo` or `NNG4`, adapt the -code at the beginning of `lean4game/server/index.mjs`: +code at the beginning of `lean4game/relay/index.mjs`: ```typescript const games = { "g/hhu-adam/robo": { diff --git a/ecosystem.config.cjs b/ecosystem.config.cjs index b3665a0..e24dbd5 100644 --- a/ecosystem.config.cjs +++ b/ecosystem.config.cjs @@ -2,7 +2,7 @@ module.exports = { apps : [{ name : "lean4game", - script : "server/index.mjs", + script : "relay/index.mjs", env: { LEAN4GAME_GITHUB_USER: "", LEAN4GAME_GITHUB_TOKEN: "", diff --git a/package.json b/package.json index d81a59c..4f25ac1 100644 --- a/package.json +++ b/package.json @@ -63,13 +63,13 @@ }, "scripts": { "start": "concurrently -n server,client -c blue,green \"npm run start_server\" \"npm run start_client\"", - "start_server": "cd server && lake build && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\"", + "start_server": "(cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec \"node ./index.mjs\")", "start_client": "cross-env NODE_ENV=development vite --host", "build": "npm run build_server && npm run build_client", "preview": "vite preview", "build_server": "cd server && lake build", "build_client": "cross-env NODE_ENV=production vite build", - "production": "cross-env NODE_ENV=production node server/index.mjs" + "production": "cross-env NODE_ENV=production node relay/index.mjs" }, "eslintConfig": { "extends": [ diff --git a/server/bubblewrap.sh b/relay/bubblewrap.sh similarity index 100% rename from server/bubblewrap.sh rename to relay/bubblewrap.sh diff --git a/server/import.mjs b/relay/import.mjs similarity index 83% rename from server/import.mjs rename to relay/import.mjs index 1701b14..a98ab39 100644 --- a/server/import.mjs +++ b/relay/import.mjs @@ -79,17 +79,17 @@ async function doImport (owner, repo, id) { artifactId = artifact.id const url = artifact.archive_download_url // Make sure the download folder exists - if (!fs.existsSync(`${__dirname}/../games`)){ - fs.mkdirSync(`${__dirname}/../games`); + if (!fs.existsSync(path.join(__dirname, "..", "games"))){ + fs.mkdirSync(path.join(__dirname, "..", "games")); } - if (!fs.existsSync(`${__dirname}/../games/tmp`)){ - fs.mkdirSync(`${__dirname}/../games/tmp`); + if (!fs.existsSync(path.join(__dirname, "..", "games", "tmp"))){ + fs.mkdirSync(path.join(__dirname, "..", "games", "tmp")); } progress[id].output += `Download from ${url}\n` - await download(id, url, `${__dirname}/../games/tmp/${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`) + await download(id, url, path.join(__dirname, "..", "games", "tmp", `${owner.toLowerCase()}_${repo.toLowerCase()}_${artifactId}.zip`)) progress[id].output += `Download finished.\n` - await runProcess(id, "/bin/bash", [`${__dirname}/unpack.sh`, artifactId, owner.toLowerCase(), repo.toLowerCase()], `${__dirname}/..`) + await runProcess(id, "/bin/bash", [path.join(__dirname, "unpack.sh"), artifactId, owner.toLowerCase(), repo.toLowerCase()], path.join(__dirname, "..")) // let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`); @@ -110,8 +110,8 @@ async function doImport (owner, repo, id) { } finally { // clean-up temp. files if (artifactId) { - fs.rmSync(`${__dirname}/../games/tmp/${owner}_${repo}_${artifactId}.zip`, {force: true, recursive: false}); - fs.rmSync(`${__dirname}/../games/tmp/${owner}_${repo}_${artifactId}`, {force: true, recursive: true}); + fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}.zip`), {force: true, recursive: false}); + fs.rmSync(path.join(__dirname, "..", "games", "tmp", `${owner}_${repo}_${artifactId}`), {force: true, recursive: true}); } progress[id].done = true } diff --git a/server/index.mjs b/relay/index.mjs similarity index 97% rename from server/index.mjs rename to relay/index.mjs index 32dea26..a0dd7ea 100644 --- a/server/index.mjs +++ b/relay/index.mjs @@ -35,7 +35,7 @@ router.get('/import/status/:owner/:repo', importStatus) router.get('/import/trigger/:owner/:repo', importTrigger) const server = 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 .use('/data/g/:owner/:repo/*', (req, res, next) => { const owner = req.params.owner; const repo = req.params.repo @@ -103,7 +103,7 @@ function startServerProcess(owner, repo) { } else { // If the game is built with `-Klean4game.local` there is no copy in the lake packages. serverProcess = cp.spawn("./gameserver", args, - { cwd: path.join(__dirname, ".lake", "build", "bin") }) + { cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") }) } } else { serverProcess = cp.spawn("./bubblewrap.sh", @@ -111,7 +111,6 @@ function startServerProcess(owner, repo) { { cwd: __dirname }) } - serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`) ) diff --git a/server/unpack.sh b/relay/unpack.sh similarity index 99% rename from server/unpack.sh rename to relay/unpack.sh index dc1bfb1..b475847 100755 --- a/server/unpack.sh +++ b/relay/unpack.sh @@ -6,7 +6,7 @@ REPO=$3 # mkdir -p games cd games -pwd + # mkdir -p tmp mkdir -p ${OWNER} diff --git a/server/.gitignore b/server/.gitignore deleted file mode 100644 index 6eac252..0000000 --- a/server/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -build/ -games/ -.lake diff --git a/tsconfig.json b/tsconfig.json index 5fe8ea1..545c5c3 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -12,5 +12,5 @@ "experimentalDecorators": true, "allowSyntheticDefaultImports": true, }, - "exclude": ["server"] + "exclude": ["server", "relay"] } diff --git a/vite.config.ts b/vite.config.ts index a647c0e..9bc8d40 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -8,7 +8,7 @@ export default defineConfig({ //root: 'client/src', build: { // Relative to the root - // Note: This has to match the path in `server/index.mjs` + // Note: This has to match the path in `relay/index.mjs` outDir: 'client/dist', }, plugins: [ From 8c39fb6664ada38b04178973fcfadc015ec69fe6 Mon Sep 17 00:00:00 2001 From: joneugster Date: Mon, 11 Dec 2023 19:38:58 +0100 Subject: [PATCH 12/32] cleanup; including using doc comment syntax for documentation like TacticDoc --- server/{Main.lean => GameServer.lean} | 0 server/GameServer/Commands.lean | 411 ++------------------------ server/GameServer/EnvExtensions.lean | 6 + server/GameServer/Helpers.lean | 190 ++++++++++++ server/GameServer/Inventory.lean | 152 ++++++++++ server/GameServer/Options.lean | 17 ++ server/GameServer/SaveData.lean | 65 ++++ server/lakefile.lean | 2 +- 8 files changed, 460 insertions(+), 383 deletions(-) rename server/{Main.lean => GameServer.lean} (100%) create mode 100644 server/GameServer/Helpers.lean create mode 100644 server/GameServer/Inventory.lean create mode 100644 server/GameServer/Options.lean create mode 100644 server/GameServer/SaveData.lean diff --git a/server/Main.lean b/server/GameServer.lean similarity index 100% rename from server/Main.lean rename to server/GameServer.lean diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index a7fafc8..5b15847 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -1,23 +1,12 @@ -import GameServer.EnvExtensions +import GameServer.Helpers +import GameServer.Inventory +import GameServer.Options +import GameServer.SaveData open Lean Meta Elab Command set_option autoImplicit false -/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/ -register_option lean4game.showDependencyReasons : Bool := { - defValue := false - descr := "show reasons for calculated world dependencies." -} - -/-- Let `MakeGame` print the reasons why the worlds depend on each other. - -Note: currently unused in favour of setting `set_option trace.debug true`. -/ -register_option lean4game.verbose : Bool := { - defValue := false - descr := "display more info messages to help developing the game." -} - /-! # Game metadata -/ /-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/ @@ -52,13 +41,15 @@ elab "Title" t:str : command => do /-- Define the introduction of the current game/world/level. -/ elab "Introduction" t:str : command => do + let intro := t.getString match ← getCurLayer with - | .Level => modifyCurLevel fun level => pure {level with introduction := t.getString} - | .World => modifyCurWorld fun world => pure {world with introduction := t.getString} - | .Game => modifyCurGame fun game => pure {game with introduction := t.getString} + | .Level => modifyCurLevel fun level => pure {level with introduction := intro} + | .World => modifyCurWorld fun world => pure {world with introduction := intro} + | .Game => modifyCurGame fun game => pure {game with introduction := intro} /-- Define the info of the current game. Used for e.g. credits -/ elab "Info" t:str : command => do + let info:= t.getString match ← getCurLayer with | .Level => logError "Can't use `Info` in a level!" @@ -66,7 +57,7 @@ elab "Info" t:str : command => do | .World => logError "Can't use `Info` in a world" pure () - | .Game => modifyCurGame fun game => pure {game with info := t.getString} + | .Game => modifyCurGame fun game => pure {game with info := info} /-- Provide the location of the image for the current game/world/level. Paths are relative to the lean project's root. -/ @@ -90,10 +81,11 @@ elab "Image" t:str : command => do /-- Define the conclusion of the current game or current level if some building a level. -/ elab "Conclusion" t:str : command => do + let conclusion := t.getString match ← getCurLayer with - | .Level => modifyCurLevel fun level => pure {level with conclusion := t.getString} - | .World => modifyCurWorld fun world => pure {world with conclusion := t.getString} - | .Game => modifyCurGame fun game => pure {game with conclusion := t.getString} + | .Level => modifyCurLevel fun level => pure {level with conclusion := conclusion} + | .World => modifyCurWorld fun world => pure {world with conclusion := conclusion} + | .Game => modifyCurGame fun game => pure {game with conclusion := conclusion} /-- A list of games that should be played before this one. Example `Prerequisites "NNG" "STG"`. -/ elab "Prerequisites" t:str* : command => do @@ -102,13 +94,15 @@ elab "Prerequisites" t:str* : command => do /-- Short caption for the game (1 sentence) -/ elab "CaptionShort" t:str : command => do + let caption := t.getString modifyCurGame fun game => pure {game with - tile := {game.tile with short := t.getString}} + tile := {game.tile with short := caption}} /-- More detailed description what the game is about (2-4 sentences). -/ elab "CaptionLong" t:str : command => do + let caption := t.getString modifyCurGame fun game => pure {game with - tile := {game.tile with long := t.getString}} + tile := {game.tile with long := caption}} /-- A list of Languages the game is translated to. For example `Languages "German" "English"`. NOTE: For the time being, only a single language is supported. @@ -136,113 +130,6 @@ in the first level and get enabled during the game. /-! ## Doc entries -/ -/-- Copied from `Mathlib.Tactic.HelpCmd`. - -Gets the initial string token in a parser description. For example, for a declaration like -`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations -that don't start with a string constant. -/ -partial def getHeadTk (e : Expr) : Option String := - match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with - | (``ParserDescr.node, #[_, _, p]) => getHeadTk p - | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p - | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p - | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p - | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk - | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk - | (``Parser.withAntiquot, #[_, p]) => getHeadTk p - | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p - | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p - | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk - | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk - | _ => none - -/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/ -def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do - let name := name.toString (escape := false) - let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {} - - let catName : Name := `tactic - let catStx : Ident := mkIdent catName -- TODO - let some cat := (Parser.parserExtension.getState env).categories.find? catName - | throwErrorAt catStx "{catStx} is not a syntax category" - liftTermElabM <| Term.addCategoryInfo catStx catName - for (k, _) in cat.kinds do - let mut used := false - if let some tk := do getHeadTk (← (← env.find? k).value?) then - let tk := tk.trim - if name ≠ tk then -- was `!name.isPrefixOf tk` - continue - used := true - decls := decls.insert tk ((decls.findD tk #[]).push k) - for (_name, ks) in decls do - for k in ks do - if let some doc ← findDocString? env k then - return doc - - logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++ - m!"using `TacticDoc {name} \"some doc\"`" - return none - -/-- Retrieve the docstring associated to an inventory item. For Tactics, this -is not guaranteed to work. -/ -def getDocstring (env : Environment) (name : Name) (type : InventoryType) : - CommandElabM (Option String) := - match type with - -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one. - | .Tactic => getTacticDocstring env name - | .Lemma => findDocString? env name - -- TODO: for definitions not implemented yet, does it work? - | .Definition => findDocString? env name - -/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields -a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a -warning. - -`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`. -I used this workaround, because I needed a new name (with correct namespace etc) -to be used, and I don't know how to create a new ident with same position but different name. --/ -def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId) - (template : Option String := none) : CommandElabM Unit := do - -- note: `name` is an `Ident` (instead of `Name`) for the log messages. - let env ← getEnv - let n := name - -- Find a key with matching `(type, name)`. - match (inventoryTemplateExt.getState env).findIdx? - (fun x => x.name == n && x.type == type) with - -- Nothing to do if the entry exists - | some _ => pure () - | none => - match template with - -- Warn about missing documentation - | none => - let docstring ← match (← getDocstring env name type) with - | some ds => - logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++ - m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.") - pure s!"*(lean docstring)*\\\n{ds}" - | none => - logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++ - m!"somewhere above this statement.") - pure "(missing)" - - -- We just add a dummy entry - modifyEnv (inventoryTemplateExt.addEntry · { - type := type - name := name - category := if type == .Lemma then s!"{n.getPrefix}" else "" - content := docstring}) - -- Add the default documentation - | some s => - modifyEnv (inventoryTemplateExt.addEntry · { - type := type - name := name - category := if type == .Lemma then s!"{n.getPrefix}" else "" - content := s }) - logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++ - m!"docstring) instead. If you want to write a different description, add " ++ - m!"`{type}Doc {name}` somewhere above this statement.") - /-- Documentation entry of a tactic. Example: ``` @@ -252,12 +139,13 @@ TacticDoc rw "`rw` stands for rewrite, etc. " * The identifier is the tactics name. Some need to be escaped like `«have»`. * The description is a string supporting Markdown. -/ -elab "TacticDoc" name:ident content:str : command => +elab doc:docComment ? "TacticDoc" name:ident content:str ? : command => do + let doc ← parseDocCommentLegacy doc content modifyEnv (inventoryTemplateExt.addEntry · { type := .Tactic name := name.getId displayName := name.getId.toString - content := content.getString }) + content := doc }) /-- Documentation entry of a lemma. Example: @@ -274,13 +162,15 @@ LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc." Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires The lemma/definition to have the same fully qualified name as in mathlib. -/ -elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command => +elab doc:docComment ? "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str ? : + command => do + let doc ← parseDocCommentLegacy doc content modifyEnv (inventoryTemplateExt.addEntry · { type := .Lemma name := name.getId category := category.getString displayName := displayName.getString - content := content.getString }) + content := doc }) -- TODO: Catch the following behaviour. -- 1. if `LemmaDoc` appears in the same file as `Statement`, it will silently use -- it but display the info that it wasn't found in `Statement` @@ -302,33 +192,16 @@ DefinitionDoc Function.Bijective as "Bijective" "defined as `Injective f ∧ Sur Use `[[mathlib_doc]]` in the string to insert a link to the mathlib doc page. This requires The lemma/definition to have the same fully qualified name as in mathlib. -/ -elab "DefinitionDoc" name:ident "as" displayName:str template:str : command => +elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:str ? : command => do + let doc ← parseDocCommentLegacy doc template modifyEnv (inventoryTemplateExt.addEntry · { type := .Definition name := name.getId, displayName := displayName.getString, - content := template.getString }) + content := doc }) /-! ## Add inventory items -/ -def getStatement (name : Name) : CommandElabM MessageData := do - return ← addMessageContextPartial (.ofPPFormat { pp := fun - | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name - | none => return "that's a bug." }) - --- Note: We use `String` because we can't send `MessageData` as json, but --- `MessageData` might be better for interactive highlighting. -/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`. - -Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into -`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/ -def getStatementString (name : Name) : CommandElabM String := do - try - return ← (← getStatement name).toString - catch - | _ => throwError m!"Could not find {name} in context." - -- TODO: I think it would be nicer to unresolve Namespaces as much as possible. - /-- Declare tactics that are introduced by this level. -/ elab "NewTactic" args:ident* : command => do for name in ↑args do @@ -405,54 +278,12 @@ elab "LemmaTab" category:str : command => /-! # Exercise Statement -/ -/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/ -syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")" --- TODO - --- TODO: Reuse the following code for checking available tactics in user code: -structure UsedInventory where -(tactics : HashSet Name := {}) -(definitions : HashSet Name := {}) -(lemmas : HashSet Name := {}) - -partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do - match stx with - | .missing => return acc - | .node _info kind args => - if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc - return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc - | .atom _info val => - -- ignore syntax elements that do not start with a letter - -- and ignore some standard keywords - let allowed := ["with", "fun", "at", "only", "by"] - if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then - let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` - return {acc with tactics := acc.tactics.insert val} - else - return acc - | .ident _info _rawVal val _preresolved => - let ns ← - try resolveGlobalConst (mkIdent val) - catch | _ => pure [] -- catch "unknown constant" error - return ← ns.foldlM (fun acc n => do - if let some (.thmInfo ..) := (← getEnv).find? n then - return {acc with lemmas := acc.lemmas.insertMany ns} - else - return {acc with definitions := acc.definitions.insertMany ns} - ) acc - --- #check expandOptDocComment? - /-- Define the statement of the current level. -/ elab doc:docComment ? attrs:Parser.Term.attributes ? "Statement" statementName:ident ? sig:declSig val:declVal : command => do let lvlIdx ← getCurLevelIdx - let docContent : Option String := match doc with - | none => none - | some s => match s.raw[1] with - | .atom _ val => val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩)) - | _ => none --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}" + let docContent ← parseDocComment doc -- Save the messages before evaluation of the proof. let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} }) @@ -553,23 +384,6 @@ elab doc:docComment ? attrs:Parser.Term.attributes ? /-! # Hints -/ -syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")") - -/-- Remove any spaces at the beginning of a new line -/ -partial def removeIndentation (s : String) : String := - let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String := - let c := s.get i - let i := s.next i - if s.atEnd i then - acc.push c - else if removeSpaces && c == ' ' then - loop i acc (removeSpaces := true) - else if c == '\n' then - loop i (acc.push c) (removeSpaces := true) - else - loop i (acc.push c) - loop ⟨0⟩ "" - /-- A tactic that can be used inside `Statement`s to indicate in which proof states players should see hints. The tactic does not affect the goal state. -/ @@ -683,26 +497,6 @@ elab "Template" tacs:tacticSeq : tactic => do return {level with template := s!"{template}"} - -open IO.FS System FilePath in -/-- Copies the folder `images/` to `.lake/gamedata/images/` -/ -def copyImages : IO Unit := do - let target : FilePath := ".lake" / "gamedata" - if ← FilePath.pathExists "images" then - for file in ← walkDir "images" do - let outFile := target.join file - -- create the directories - if ← file.isDir then - createDirAll outFile - else - if let some parent := outFile.parent then - createDirAll parent - -- copy file - let content ← readBinFile file - writeBinFile outFile content - - - -- TODO: Notes for testing if a declaration has the simp attribute -- -- Test: From zulip @@ -721,139 +515,6 @@ def copyImages : IO Unit := do /-! # Make Game -/ -#eval IO.FS.createDirAll ".lake/gamedata/" - --- TODO: register all of this as ToJson instance? -def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do - let game ← getCurGame - let env ← getEnv - let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata" - - if ← path.isDir then - IO.FS.removeDirAll path - IO.FS.createDirAll path - - -- copy the images folder - copyImages - - for (worldId, world) in game.worlds.nodes.toArray do - for (levelId, level) in world.levels.toArray do - IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env))) - - IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game)) - - for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do - for name in allItemsByType.findD inventoryType {} do - let some item ← getInventoryItem? name inventoryType - | throwError "Expected item to exist: {name}" - IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item)) - - let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do - (allItemsByType.findD type {}).toArray.mapM (fun name => do - let some item ← getInventoryItem? name type - | throwError "Expected item to exist: {name}" - return item.toTile) - let inventory : InventoryOverview := { - lemmas := ← getTiles .Lemma - tactics := ← getTiles .Tactic - definitions := ← getTiles .Definition - lemmaTab := none - } - IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory)) - - -def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo -| .Tactic => level.tactics -| .Definition => level.definitions -| .Lemma => level.lemmas - -def GameLevel.setComputedInventory (level : GameLevel) : - InventoryType → Array InventoryTile → GameLevel -| .Tactic, v => {level with tactics := {level.tactics with tiles := v}} -| .Definition, v => {level with definitions := {level.definitions with tiles := v}} -| .Lemma, v => {level with lemmas := {level.lemmas with tiles := v}} - -partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name)) - (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) : - HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do - match (newArrows.find? id, decendants.find? id) with - | (some _, some _) => return (newArrows, decendants) - | _ => - let mut newArr := newArrows - let mut desc := decendants - desc := desc.insert id {} -- mark as worked in case of loops - newArr := newArr.insert id {} -- mark as worked in case of loops - let children := arrows.findD id {} - let mut trimmedChildren := children - let mut theseDescs := children - for child in children do - (newArr, desc) := removeTransitiveAux child arrows newArr desc - let childDescs := desc.findD child {} - theseDescs := theseDescs.insertMany childDescs - for d in childDescs do - trimmedChildren := trimmedChildren.erase d - desc := desc.insert id theseDescs - newArr := newArr.insert id trimmedChildren - return (newArr, desc) - -def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do - let mut newArr := {} - let mut desc := {} - for id in arrows.toArray.map Prod.fst do - (newArr, desc) := removeTransitiveAux id arrows newArr desc - if (desc.findD id {}).contains id then - logError <| m!"Loop at {id}. " ++ - m!"This should not happen and probably means that `findLoops` has a bug." - -- DEBUG: - -- for ⟨x, hx⟩ in desc.toList do - -- m := m ++ m!"{x}: {hx.toList}\n" - -- logError m - - return newArr - -/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`. - -For performance reason it returns a HashSet of visited -nodes as well. This is filled with all nodes ever looked at as they cannot be -part of a loop anymore. -/ -partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name) - (path : Array Name := #[]) (visited : HashSet Name := {}) : - Array Name × HashSet Name := Id.run do - let mut visited := visited - match path.getIdx? node with - | some i => - -- Found a loop: `node` is already the iᵗʰ element of the path - return (path.extract i path.size, visited.insert node) - | none => - for successor in arrows.findD node {} do - -- If we already visited the successor, it cannot be part of a loop anymore - if visited.contains successor then - continue - -- Find any loop involving `successor` - let (loop, _) := findLoopsAux arrows successor (path.push node) visited - visited := visited.insert successor - -- No loop found in the dependants of `successor` - if loop.isEmpty then - continue - -- Found a loop, return it - return (loop, visited) - return (#[], visited.insert node) - -/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/ -partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do - let mut visited : HashSet Name := {} - for node in arrows.toArray.map (·.1) do - -- Skip a node if it was already visited - if visited.contains node then - continue - -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its - -- search starting from `node` - let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited)) - visited := moreVisited - if !loop.isEmpty then - return loop.toList - return [] - /-- The worlds of a game are joint by dependencies. These are automatically computed but can also be defined with the syntax `Dependency World₁ → World₂ → World₃`. -/ @@ -1191,17 +852,3 @@ elab "MakeGame" : command => do allItemsByType := allItemsByType.insert inventoryType allItems saveGameData allItemsByType - -/-! # Debugging tools -/ - --- /-- Print current game for debugging purposes. -/ --- elab "PrintCurGame" : command => do --- logInfo (toJson (← getCurGame)) - -/-- Print current level for debugging purposes. -/ -elab "PrintCurLevel" : command => do - logInfo (repr (← getCurLevel)) - -/-- Print levels for debugging purposes. -/ -elab "PrintLevels" : command => do - logInfo $ repr $ (← getCurWorld).levels.toArray diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index a1e15f3..fdbd351 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -148,6 +148,12 @@ structure InventoryOverview where lemmaTab : Option String deriving ToJson, FromJson +-- TODO: Reuse the following code for checking available tactics in user code: +structure UsedInventory where +(tactics : HashSet Name := {}) +(definitions : HashSet Name := {}) +(lemmas : HashSet Name := {}) + /-! ## Environment extensions for game specification -/ /-- Register a (non-persistent) environment extension to hold the current level -/ diff --git a/server/GameServer/Helpers.lean b/server/GameServer/Helpers.lean new file mode 100644 index 0000000..4a59e75 --- /dev/null +++ b/server/GameServer/Helpers.lean @@ -0,0 +1,190 @@ +import Lean + +/-! This document contains various things which cluttered `Commands.lean`. -/ + +open Lean Meta Elab Command + +syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")") + +/-! ## Doc Comment Parsing -/ + +/-- Read a doc comment and get its content. Return `""` if no doc comment available. -/ +def parseDocComment! (doc: Option (TSyntax `Lean.Parser.Command.docComment)) : + CommandElabM String := do + match doc with + | none => + logWarning "Add a text to this command with `/-- yada yada -/ MyCommand`!" + pure "" + | some s => match s.raw[1] with + | .atom _ val => pure <| val.dropRight 2 |>.trim -- some (val.extract 0 (val.endPos - ⟨2⟩)) + | _ => pure "" --panic "not implemented error message" --throwErrorAt s "unexpected doc string{indentD s.raw[1]}" + +/-- Read a doc comment and get its content. Return `none` if no doc comment available. -/ +def parseDocComment (doc: Option (TSyntax `Lean.Parser.Command.docComment)) : + CommandElabM <| Option String := do + match doc with + | none => pure none + | some _ => parseDocComment! doc + + +/-- TODO: This is only used to provide some backwards compatibility and you can +replace `parseDocCommentLegacy` with `parseDocComment` in the future. -/ +def parseDocCommentLegacy (doc: Option (TSyntax `Lean.Parser.Command.docComment)) + (t : Option (TSyntax `str)) : CommandElabM <| String := do + match doc with + | none => + match t with + | none => + pure <| ← parseDocComment! doc + | some t => + logWarningAt t "You should use the new Syntax: + + /-- yada yada -/ + YourCommand + + instead of + + YourCommand \"yada yada\" + " + pure t.getString + | some _ => + match t with + | none => + pure <| ← parseDocComment! doc + | some t => + logErrorAt t "You must not provide both, a docstring and a string following the command! + Only use + + /-- yada yada -/ + YourCommand + + and remove the string following it!" + pure <| ← parseDocComment! doc + +/-! ## Statement string -/ + +def getStatement (name : Name) : CommandElabM MessageData := do + return ← addMessageContextPartial (.ofPPFormat { pp := fun + | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature name + | none => return "that's a bug." }) + +-- Note: We use `String` because we can't send `MessageData` as json, but +-- `MessageData` might be better for interactive highlighting. +/-- Get a string of the form `my_lemma (n : ℕ) : n + n = 2 * n`. + +Note: A statement like `theorem abc : ∀ x : Nat, x ≥ 0` would be turned into +`theorem abc (x : Nat) : x ≥ 0` by `PrettyPrinter.ppSignature`. -/ +def getStatementString (name : Name) : CommandElabM String := do + try + return ← (← getStatement name).toString + catch + | _ => throwError m!"Could not find {name} in context." + -- TODO: I think it would be nicer to unresolve Namespaces as much as possible. + +/-- A `attr := ...` option for `Statement`. Add attributes to the defined theorem. -/ +syntax statementAttr := "(" &"attr" ":=" Parser.Term.attrInstance,* ")" +-- TODO + + +/-- Remove any spaces at the beginning of a new line -/ +partial def removeIndentation (s : String) : String := + let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String := + let c := s.get i + let i := s.next i + if s.atEnd i then + acc.push c + else if removeSpaces && c == ' ' then + loop i acc (removeSpaces := true) + else if c == '\n' then + loop i (acc.push c) (removeSpaces := true) + else + loop i (acc.push c) + loop ⟨0⟩ "" + + +/-! ## Loops in Graph-like construct + +TODO: Why are we not using graphs here but our own construct `HashMap Name (HashSet Name)`? +-/ + +partial def removeTransitiveAux (id : Name) (arrows : HashMap Name (HashSet Name)) + (newArrows : HashMap Name (HashSet Name)) (decendants : HashMap Name (HashSet Name)) : + HashMap Name (HashSet Name) × HashMap Name (HashSet Name) := Id.run do + match (newArrows.find? id, decendants.find? id) with + | (some _, some _) => return (newArrows, decendants) + | _ => + let mut newArr := newArrows + let mut desc := decendants + desc := desc.insert id {} -- mark as worked in case of loops + newArr := newArr.insert id {} -- mark as worked in case of loops + let children := arrows.findD id {} + let mut trimmedChildren := children + let mut theseDescs := children + for child in children do + (newArr, desc) := removeTransitiveAux child arrows newArr desc + let childDescs := desc.findD child {} + theseDescs := theseDescs.insertMany childDescs + for d in childDescs do + trimmedChildren := trimmedChildren.erase d + desc := desc.insert id theseDescs + newArr := newArr.insert id trimmedChildren + return (newArr, desc) + + +def removeTransitive (arrows : HashMap Name (HashSet Name)) : CommandElabM (HashMap Name (HashSet Name)) := do + let mut newArr := {} + let mut desc := {} + for id in arrows.toArray.map Prod.fst do + (newArr, desc) := removeTransitiveAux id arrows newArr desc + if (desc.findD id {}).contains id then + logError <| m!"Loop at {id}. " ++ + m!"This should not happen and probably means that `findLoops` has a bug." + -- DEBUG: + -- for ⟨x, hx⟩ in desc.toList do + -- m := m ++ m!"{x}: {hx.toList}\n" + -- logError m + + return newArr + +/-- The recursive part of `findLoops`. Finds loops that appear as successors of `node`. + +For performance reason it returns a HashSet of visited +nodes as well. This is filled with all nodes ever looked at as they cannot be +part of a loop anymore. -/ +partial def findLoopsAux (arrows : HashMap Name (HashSet Name)) (node : Name) + (path : Array Name := #[]) (visited : HashSet Name := {}) : + Array Name × HashSet Name := Id.run do + let mut visited := visited + match path.getIdx? node with + | some i => + -- Found a loop: `node` is already the iᵗʰ element of the path + return (path.extract i path.size, visited.insert node) + | none => + for successor in arrows.findD node {} do + -- If we already visited the successor, it cannot be part of a loop anymore + if visited.contains successor then + continue + -- Find any loop involving `successor` + let (loop, _) := findLoopsAux arrows successor (path.push node) visited + visited := visited.insert successor + -- No loop found in the dependants of `successor` + if loop.isEmpty then + continue + -- Found a loop, return it + return (loop, visited) + return (#[], visited.insert node) + +/-- Find a loop in the graph and return it. Returns `[]` if there are no loops. -/ +partial def findLoops (arrows : HashMap Name (HashSet Name)) : List Name := Id.run do + let mut visited : HashSet Name := {} + for node in arrows.toArray.map (·.1) do + -- Skip a node if it was already visited + if visited.contains node then + continue + -- `findLoopsAux` returns a loop or `[]` together with a set of nodes it visited on its + -- search starting from `node` + let (loop, moreVisited) := (findLoopsAux arrows node (visited := visited)) + visited := moreVisited + if !loop.isEmpty then + return loop.toList + return [] diff --git a/server/GameServer/Inventory.lean b/server/GameServer/Inventory.lean new file mode 100644 index 0000000..bff10d4 --- /dev/null +++ b/server/GameServer/Inventory.lean @@ -0,0 +1,152 @@ +import Lean +import GameServer.EnvExtensions + +open Lean Elab Command + +/-- Copied from `Mathlib.Tactic.HelpCmd`. + +Gets the initial string token in a parser description. For example, for a declaration like +`syntax "bla" "baz" term : tactic`, it returns `some "bla"`. Returns `none` for syntax declarations +that don't start with a string constant. -/ +partial def getHeadTk (e : Expr) : Option String := + match (Expr.withApp e λ e a => (e.constName?.getD Name.anonymous, a)) with + | (``ParserDescr.node, #[_, _, p]) => getHeadTk p + | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getHeadTk p + | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getHeadTk p + | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getHeadTk p + | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk + | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => some tk + | (``Parser.withAntiquot, #[_, p]) => getHeadTk p + | (``Parser.leadingNode, #[_, _, p]) => getHeadTk p + | (``HAndThen.hAndThen, #[_, _, _, _, p, _]) => getHeadTk p + | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => some tk + | (``Parser.symbol, #[.lit (.strVal tk)]) => some tk + | _ => none + +/-! ## Doc entries -/ + +/-- Modified from `#help` in `Mathlib.Tactic.HelpCmd` -/ +def getTacticDocstring (env : Environment) (name: Name) : CommandElabM (Option String) := do + let name := name.toString (escape := false) + let mut decls : Lean.RBMap String (Array SyntaxNodeKind) compare := {} + + let catName : Name := `tactic + let catStx : Ident := mkIdent catName -- TODO + let some cat := (Parser.parserExtension.getState env).categories.find? catName + | throwErrorAt catStx "{catStx} is not a syntax category" + liftTermElabM <| Term.addCategoryInfo catStx catName + for (k, _) in cat.kinds do + let mut used := false + if let some tk := do getHeadTk (← (← env.find? k).value?) then + let tk := tk.trim + if name ≠ tk then -- was `!name.isPrefixOf tk` + continue + used := true + decls := decls.insert tk ((decls.findD tk #[]).push k) + for (_name, ks) in decls do + for k in ks do + if let some doc ← findDocString? env k then + return doc + + logWarning <| m!"Could not find a docstring for tactic {name}, consider adding one " ++ + m!"using `TacticDoc {name} \"some doc\"`" + return none + +/-- Retrieve the docstring associated to an inventory item. For Tactics, this +is not guaranteed to work. -/ +def getDocstring (env : Environment) (name : Name) (type : InventoryType) : + CommandElabM (Option String) := + match type with + -- for tactics it's a lookup following mathlib's `#help`. not guaranteed to be the correct one. + | .Tactic => getTacticDocstring env name + | .Lemma => findDocString? env name + -- TODO: for definitions not implemented yet, does it work? + | .Definition => findDocString? env name + +/-- Checks if `inventoryTemplateExt` contains an entry with `(type, name)` and yields +a warning otherwise. If `template` is provided, it will add such an entry instead of yielding a +warning. + +`ref` is the syntax piece. If `name` is not provided, it will use `ident.getId`. +I used this workaround, because I needed a new name (with correct namespace etc) +to be used, and I don't know how to create a new ident with same position but different name. +-/ +def checkInventoryDoc (type : InventoryType) (ref : Ident) (name : Name := ref.getId) + (template : Option String := none) : CommandElabM Unit := do + -- note: `name` is an `Ident` (instead of `Name`) for the log messages. + let env ← getEnv + let n := name + -- Find a key with matching `(type, name)`. + match (inventoryTemplateExt.getState env).findIdx? + (fun x => x.name == n && x.type == type) with + -- Nothing to do if the entry exists + | some _ => pure () + | none => + match template with + -- Warn about missing documentation + | none => + let docstring ← match (← getDocstring env name type) with + | some ds => + logInfoAt ref (m!"Missing {type} Documentation. Using existing docstring. " ++ + m!"Add {name}\nAdd `{type}Doc {name}` somewhere above this statement.") + pure s!"*(lean docstring)*\\\n{ds}" + | none => + logWarningAt ref (m!"Missing {type} Documentation: {name}\nAdd `{type}Doc {name}` " ++ + m!"somewhere above this statement.") + pure "(missing)" + + -- We just add a dummy entry + modifyEnv (inventoryTemplateExt.addEntry · { + type := type + name := name + category := if type == .Lemma then s!"{n.getPrefix}" else "" + content := docstring}) + -- Add the default documentation + | some s => + modifyEnv (inventoryTemplateExt.addEntry · { + type := type + name := name + category := if type == .Lemma then s!"{n.getPrefix}" else "" + content := s }) + logInfoAt ref (m!"Missing {type} Documentation: {name}, used default (e.g. provided " ++ + m!"docstring) instead. If you want to write a different description, add " ++ + m!"`{type}Doc {name}` somewhere above this statement.") + +partial def collectUsedInventory (stx : Syntax) (acc : UsedInventory := {}) : CommandElabM UsedInventory := do + match stx with + | .missing => return acc + | .node _info kind args => + if kind == `GameServer.Tactic.Hint || kind == `GameServer.Tactic.Branch then return acc + return ← args.foldlM (fun acc arg => collectUsedInventory arg acc) acc + | .atom _info val => + -- ignore syntax elements that do not start with a letter + -- and ignore some standard keywords + let allowed := ["with", "fun", "at", "only", "by"] + if 0 < val.length ∧ val.data[0]!.isAlpha ∧ not (allowed.contains val) then + let val := val.dropRightWhile (fun c => c == '!' || c == '?') -- treat `simp?` and `simp!` like `simp` + return {acc with tactics := acc.tactics.insert val} + else + return acc + | .ident _info _rawVal val _preresolved => + let ns ← + try resolveGlobalConst (mkIdent val) + catch | _ => pure [] -- catch "unknown constant" error + return ← ns.foldlM (fun acc n => do + if let some (.thmInfo ..) := (← getEnv).find? n then + return {acc with lemmas := acc.lemmas.insertMany ns} + else + return {acc with definitions := acc.definitions.insertMany ns} + ) acc + +-- #check expandOptDocComment? + +def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo +| .Tactic => level.tactics +| .Definition => level.definitions +| .Lemma => level.lemmas + +def GameLevel.setComputedInventory (level : GameLevel) : + InventoryType → Array InventoryTile → GameLevel +| .Tactic, v => {level with tactics := {level.tactics with tiles := v}} +| .Definition, v => {level with definitions := {level.definitions with tiles := v}} +| .Lemma, v => {level with lemmas := {level.lemmas with tiles := v}} diff --git a/server/GameServer/Options.lean b/server/GameServer/Options.lean new file mode 100644 index 0000000..f467876 --- /dev/null +++ b/server/GameServer/Options.lean @@ -0,0 +1,17 @@ +import Lean + +/-! This document contains custom options available in the game. -/ + +/-- Let `MakeGame` print the reasons why the worlds depend on each other. -/ +register_option lean4game.showDependencyReasons : Bool := { + defValue := false + descr := "show reasons for calculated world dependencies." +} + +/-- Let `MakeGame` print the reasons why the worlds depend on each other. + +Note: currently unused in favour of setting `set_option trace.debug true`. -/ +register_option lean4game.verbose : Bool := { + defValue := false + descr := "display more info messages to help developing the game." +} diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean new file mode 100644 index 0000000..4718717 --- /dev/null +++ b/server/GameServer/SaveData.lean @@ -0,0 +1,65 @@ +import GameServer.EnvExtensions + +open Lean Meta Elab Command + + +/-! ## Copy images -/ + +open IO.FS System FilePath in +/-- Copies the folder `images/` to `.lake/gamedata/images/` -/ +def copyImages : IO Unit := do + let target : FilePath := ".lake" / "gamedata" + if ← FilePath.pathExists "images" then + for file in ← walkDir "images" do + let outFile := target.join file + -- create the directories + if ← file.isDir then + createDirAll outFile + else + if let some parent := outFile.parent then + createDirAll parent + -- copy file + let content ← readBinFile file + writeBinFile outFile content + + +-- TODO: I'm not sure this should be happening here... +#eval IO.FS.createDirAll ".lake/gamedata/" + +-- TODO: register all of this as ToJson instance? +def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do + let game ← getCurGame + let env ← getEnv + let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata" + + if ← path.isDir then + IO.FS.removeDirAll path + IO.FS.createDirAll path + + -- copy the images folder + copyImages + + for (worldId, world) in game.worlds.nodes.toArray do + for (levelId, level) in world.levels.toArray do + IO.FS.writeFile (path / s!"level__{worldId}__{levelId}.json") (toString (toJson (level.toInfo env))) + + IO.FS.writeFile (path / s!"game.json") (toString (getGameJson game)) + + for inventoryType in [InventoryType.Lemma, .Tactic, .Definition] do + for name in allItemsByType.findD inventoryType {} do + let some item ← getInventoryItem? name inventoryType + | throwError "Expected item to exist: {name}" + IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item)) + + let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do + (allItemsByType.findD type {}).toArray.mapM (fun name => do + let some item ← getInventoryItem? name type + | throwError "Expected item to exist: {name}" + return item.toTile) + let inventory : InventoryOverview := { + lemmas := ← getTiles .Lemma + tactics := ← getTiles .Tactic + definitions := ← getTiles .Definition + lemmaTab := none + } + IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory)) diff --git a/server/lakefile.lean b/server/lakefile.lean index dc2f526..fc337ce 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -12,7 +12,7 @@ lean_lib GameServer @[default_target] lean_exe gameserver { - root := `Main + root := `GameServer supportInterpreter := true } From 7515561883f8f70f390f4c34ee09e9f31b2fbe70 Mon Sep 17 00:00:00 2001 From: ran Date: Tue, 12 Dec 2023 19:17:55 +0800 Subject: [PATCH 13/32] Add a button to toggle mobile --- client/src/components/app_bar.tsx | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index 2c65a81..d07f80f 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 } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from "../app" import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context" import { GameInfo, useGetGameInfoQuery } from '../state/api' @@ -161,7 +161,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres }) { 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
@@ -182,6 +182,12 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres + {mobile ? : + } @@ -208,7 +214,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= }) { const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) - const {mobile} = React.useContext(MobileContext) + const {mobile, setMobile} = React.useContext(MobileContext) const [navOpen, setNavOpen] = React.useState(false) const gameInfo = useGetGameInfoQuery({game: gameId}) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) @@ -231,6 +237,9 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= +
@@ -248,6 +257,9 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= +
From a2726ae287ad6e4c0c32f93ceb1208dc7587de04 Mon Sep 17 00:00:00 2001 From: ran Date: Tue, 12 Dec 2023 19:29:21 +0800 Subject: [PATCH 14/32] Adjust the top navigation bar so that it is centered above and below --- client/src/components/app_bar.tsx | 4 ++-- client/src/css/app.css | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index 2c65a81..6cdb7ed 100644 --- a/client/src/components/app_bar.tsx +++ b/client/src/components/app_bar.tsx @@ -165,7 +165,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres const [navOpen, setNavOpen] = React.useState(false) return
-
+
@@ -237,7 +237,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= : <> {/* DESKTOP VERSION */} -
+
{worldTitle && `World: ${worldTitle}`}
diff --git a/client/src/css/app.css b/client/src/css/app.css index 3226e1f..824381b 100644 --- a/client/src/css/app.css +++ b/client/src/css/app.css @@ -105,11 +105,17 @@ em { position: relative; flex-direction: row; justify-content: space-between; + align-items: center; padding: 1.1em; filter: drop-shadow(0 0 5px rgba(0,0,0,0.5)); z-index: 2; } +.app-bar > .app-bar-left{ + display: flex; + align-items: center; +} + .app-bar-title, .app-bar-subtitle { color: white; font-weight: 500; From 2ba36b91d5fa021b9a2f87ae3565b8adc96b7744 Mon Sep 17 00:00:00 2001 From: ran Date: Tue, 12 Dec 2023 19:51:20 +0800 Subject: [PATCH 15/32] Adjust the margin of the home button --- client/src/css/app.css | 1 + client/src/css/level.css | 5 ----- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/client/src/css/app.css b/client/src/css/app.css index 824381b..206638d 100644 --- a/client/src/css/app.css +++ b/client/src/css/app.css @@ -114,6 +114,7 @@ em { .app-bar > .app-bar-left{ display: flex; align-items: center; + gap: .5em; } .app-bar-title, .app-bar-subtitle { diff --git a/client/src/css/level.css b/client/src/css/level.css index faa2c0d..fda530f 100644 --- a/client/src/css/level.css +++ b/client/src/css/level.css @@ -317,11 +317,6 @@ td code { margin-right: 0; } -#home-btn { - margin-right: .5em; - margin-left: 0; -} - .menu.dropdown .svg-inline--fa { width: 1.8rem; } From 5aa07648447d22b330d1b08a1753ee3107234824 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 12 Dec 2023 14:41:54 +0100 Subject: [PATCH 16/32] add comment --- relay/bubblewrap.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/relay/bubblewrap.sh b/relay/bubblewrap.sh index 1d21183..a3e5f4c 100755 --- a/relay/bubblewrap.sh +++ b/relay/bubblewrap.sh @@ -1,5 +1,6 @@ #/bin/bash +# Note: This fails if there is no default toolchain installed ELAN_HOME=$(lake env printenv ELAN_HOME) # $1 : the game directory From 47d7f606c6f350a70cd41024d0125169194df6e4 Mon Sep 17 00:00:00 2001 From: ran Date: Wed, 13 Dec 2023 00:34:38 +0800 Subject: [PATCH 17/32] Add basic preference framework and mobile options --- client/src/app.tsx | 26 +++++++++++++++++++---- client/src/components/app_bar.tsx | 24 +++++++-------------- client/src/components/infoview/context.ts | 12 ++++++++--- client/src/components/welcome.tsx | 11 ++++++++-- client/src/hooks.ts | 24 +++++++++++++++++++++ client/src/state/local_storage.ts | 21 ++++++++++++++++++ client/src/state/store.ts | 5 ++++- client/src/window_width.tsx | 21 ------------------ 8 files changed, 97 insertions(+), 47 deletions(-) delete mode 100644 client/src/window_width.tsx diff --git a/client/src/app.tsx b/client/src/app.tsx index c45f6d0..653d0db 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -9,20 +9,38 @@ 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 { 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) + + 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 d07f80f..c766b52 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, faMobileScreenButton, faDesktop } 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,14 +150,15 @@ 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)) @@ -182,12 +183,6 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres - {mobile ? : - } @@ -200,6 +195,9 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres +
} @@ -214,7 +212,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= }) { const gameId = React.useContext(GameIdContext) const {worldId, levelId} = React.useContext(WorldLevelIdContext) - const {mobile, setMobile} = React.useContext(MobileContext) + const {mobile} = React.useContext(MobileContext) const [navOpen, setNavOpen] = React.useState(false) const gameInfo = useGetGameInfoQuery({game: gameId}) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) @@ -237,9 +235,6 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= -
@@ -257,9 +252,6 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= -
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/welcome.tsx b/client/src/components/welcome.tsx index 6c6c977..89b9adc 100644 --- a/client/src/components/welcome.tsx +++ b/client/src/components/welcome.tsx @@ -17,6 +17,7 @@ import { InfoPopup } from './popup/game_info' import { PrivacyPolicyPopup } from './popup/privacy_policy' import { RulesHelpPopup } from './popup/rules_help' import { UploadPopup } from './popup/upload' +import { PreferencesPopup} from "./popup/preferences" import { WorldTreePanel } from './world_tree' import '../css/welcome.css' @@ -63,7 +64,7 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string, /** main page of the game showing among others the tree of worlds/levels */ function Welcome() { const gameId = React.useContext(GameIdContext) - const {mobile} = React.useContext(MobileContext) + const {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext) const gameInfo = useGetGameInfoQuery({game: gameId}) const inventory = useLoadInventoryOverviewQuery({game: gameId}) @@ -77,15 +78,20 @@ function Welcome() { const [info, setInfo] = React.useState(false) const [rulesHelp, setRulesHelp] = React.useState(false) const [uploadMenu, setUploadMenu] = React.useState(false) + const [preferencesPopup, setPreferencesPopup] = React.useState(false) + function closeEraseMenu() {setEraseMenu(false)} function closeImpressum() {setImpressum(false)} function closeInfo() {setInfo(false)} function closeRulesHelp() {setRulesHelp(false)} function closeUploadMenu() {setUploadMenu(false)} + function closePreferencesPopup() {setPreferencesPopup(false)} function toggleEraseMenu() {setEraseMenu(!eraseMenu)} function toggleImpressum() {setImpressum(!impressum)} function toggleInfo() {setInfo(!info)} function toggleUploadMenu() {setUploadMenu(!uploadMenu)} + function togglePreferencesPopup() {setPreferencesPopup(!preferencesPopup)} + // set the window title useEffect(() => { @@ -101,7 +107,7 @@ function Welcome() { : <> + toggleInfo={toggleInfo} togglePreferencesPopup={togglePreferencesPopup}/>
{ mobile ?
@@ -128,6 +134,7 @@ function Welcome() { {eraseMenu? : null} {uploadMenu? : null} {info ? : null} + {preferencesPopup ? : null} } diff --git a/client/src/hooks.ts b/client/src/hooks.ts index afdce0a..0ac6e2f 100644 --- a/client/src/hooks.ts +++ b/client/src/hooks.ts @@ -1,6 +1,30 @@ import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux' import type { RootState, AppDispatch } from './state/store' +import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences" + // Use throughout your app instead of plain `useDispatch` and `useSelector` export const useAppDispatch: () => AppDispatch = useDispatch export const useAppSelector: TypedUseSelectorHook = useSelector + +export const useMobile = () => { + const dispatch = useAppDispatch(); + + const mobile = useAppSelector((state) => state.preferences.mobile); + const lockMobile = useAppSelector((state) => state.preferences.lockMobile); + + const setMobile = (val: boolean) => { + dispatch(setMobileState(val)); + }; + + const setLockMobile = (val: boolean) => { + dispatch(setLockMobileState(val)); + }; + + return { + mobile, + setMobile, + lockMobile, + setLockMobile, + }; +}; diff --git a/client/src/state/local_storage.ts b/client/src/state/local_storage.ts index 6e88db2..ea165ce 100644 --- a/client/src/state/local_storage.ts +++ b/client/src/state/local_storage.ts @@ -36,3 +36,24 @@ export async function saveState(state: any) { // Ignore } } + +const PREFERENCES_KEY = "preferences" + +/** Load from browser storage */ +export function loadPreferences() { + try { + const serializedState = localStorage.getItem(PREFERENCES_KEY); + return JSON.parse(serializedState) + } catch (e) { + return undefined; + } +} + +export function savePreferences(state: any) { + try { + const serializedState = JSON.stringify(state) + localStorage.setItem(PREFERENCES_KEY, serializedState); + } catch (e) { + // Ignore + } +} diff --git a/client/src/state/store.ts b/client/src/state/store.ts index 4079ebd..a2294de 100644 --- a/client/src/state/store.ts +++ b/client/src/state/store.ts @@ -7,13 +7,15 @@ import { debounce } from "debounce"; import { connection } from '../connection' import { apiSlice } from './api' import { progressSlice } from './progress' -import { saveState } from "./local_storage"; +import { preferencesSlice } from "./preferences" +import { saveState, savePreferences } from "./local_storage"; export const store = configureStore({ reducer: { [apiSlice.reducerPath]: apiSlice.reducer, [progressSlice.name]: progressSlice.reducer, + [preferencesSlice.name]: preferencesSlice.reducer, }, // Make connection available in thunks: middleware: getDefaultMiddleware => @@ -31,6 +33,7 @@ export const store = configureStore({ store.subscribe( debounce(() => { saveState(store.getState()[progressSlice.name]); + savePreferences(store.getState()[preferencesSlice.name]); }, 800) ); diff --git a/client/src/window_width.tsx b/client/src/window_width.tsx deleted file mode 100644 index 9e8b484..0000000 --- a/client/src/window_width.tsx +++ /dev/null @@ -1,21 +0,0 @@ -import {useState, useEffect} from 'react' - -function getWindowDimensions() { - const {innerWidth: width, innerHeight: height } = window - return {width, height} -} - -export function useWindowDimensions() { - const [windowDimensions, setWindowDimensions] = useState(getWindowDimensions()) - - useEffect(() => { - function handleResize() { - setWindowDimensions(getWindowDimensions()) - } - window.addEventListener('resize', handleResize) - return () => window.removeEventListener('resize', handleResize) - - }, []) - - return windowDimensions -} From 9f692ccf619d2cc3172fb0b1a16d3c6223b602ea Mon Sep 17 00:00:00 2001 From: ran Date: Wed, 13 Dec 2023 00:37:50 +0800 Subject: [PATCH 18/32] Add basic preference framework and mobile options and Add missing files --- client/src/components/popup/preferences.tsx | 55 +++++++++++++++++++++ client/src/state/preferences.ts | 37 ++++++++++++++ 2 files changed, 92 insertions(+) create mode 100644 client/src/components/popup/preferences.tsx create mode 100644 client/src/state/preferences.ts diff --git a/client/src/components/popup/preferences.tsx b/client/src/components/popup/preferences.tsx new file mode 100644 index 0000000..73b2dbe --- /dev/null +++ b/client/src/components/popup/preferences.tsx @@ -0,0 +1,55 @@ +import * as React from 'react' +import { Input, Typography } from '@mui/material' +import Markdown from '../markdown' +import Switch from '@mui/material/Switch'; +import FormControlLabel from '@mui/material/FormControlLabel'; + +import { IMobileContext } from "../infoview/context" + +interface PreferencesPopupProps extends IMobileContext{ + handleClose: () => void +} + +export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) { + return
+
+
+
+ +
+
+

Mobile layout

+
+
+ setMobile(!mobile)} + name="checked" + color="primary" + /> + } + label="Enable" + labelPlacement="start" + /> +
+
+ setLockMobile(!lockMobile)} + name="checked" + color="primary" + /> + } + label="Auto" + labelPlacement="start" + /> +
+
+ +
+
+} diff --git a/client/src/state/preferences.ts b/client/src/state/preferences.ts new file mode 100644 index 0000000..6ee0fa1 --- /dev/null +++ b/client/src/state/preferences.ts @@ -0,0 +1,37 @@ +import { createSlice } from "@reduxjs/toolkit"; + +import { loadPreferences } from "./local_storage"; + +interface PreferencesState { + mobile: boolean; + lockMobile: boolean; +} + +export function getWindowDimensions() { + const {innerWidth: width, innerHeight: height } = window + return {width, height} +} + +const { width } = getWindowDimensions() + +export const AUTO_SWITCH_THRESHOLD = 800 + +const initialState: PreferencesState = loadPreferences() ?? { + mobile: width < AUTO_SWITCH_THRESHOLD, + lockMobile: false +} + +export const preferencesSlice = createSlice({ + name: "preferences", + initialState, + reducers: { + setMobile: (state, action) => { + state.mobile = action.payload; + }, + setLockMobile: (state, action) => { + state.lockMobile = action.payload; + }, + }, +}); + +export const { setMobile, setLockMobile } = preferencesSlice.actions; From ae636a03edf69f9066976f2852d75c585bd83fee Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 19:01:11 +0100 Subject: [PATCH 19/32] fix: hide hidden inventory items in overview #169 --- server/GameServer/Commands.lean | 16 ++++++++++++++-- server/GameServer/SaveData.lean | 14 ++------------ 2 files changed, 16 insertions(+), 14 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 5b15847..8bd5fd5 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -819,7 +819,7 @@ elab "MakeGame" : command => do displayName := data.displayName category := data.category locked := false - hidden := levelInfo.hidden.contains item } + hidden := hiddenItems.contains item } -- add the exercise statement from the previous level -- if it was named @@ -851,4 +851,16 @@ elab "MakeGame" : command => do return level.setComputedInventory inventoryType itemsArray allItemsByType := allItemsByType.insert inventoryType allItems - saveGameData allItemsByType + let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do + (allItemsByType.findD type {}).toArray.mapM (fun name => do + let some item ← getInventoryItem? name type + | throwError "Expected item to exist: {name}" + return item.toTile) + let inventory : InventoryOverview := { + lemmas := (← getTiles .Lemma).map (fun tile => {tile with hidden := hiddenItems.contains tile.name}) + tactics := (← getTiles .Tactic).map (fun tile => {tile with hidden := hiddenItems.contains tile.name}) + definitions := (← getTiles .Definition).map (fun tile => {tile with hidden := hiddenItems.contains tile.name}) + lemmaTab := none + } + + saveGameData allItemsByType inventory diff --git a/server/GameServer/SaveData.lean b/server/GameServer/SaveData.lean index 4718717..4aa17fc 100644 --- a/server/GameServer/SaveData.lean +++ b/server/GameServer/SaveData.lean @@ -27,7 +27,8 @@ def copyImages : IO Unit := do #eval IO.FS.createDirAll ".lake/gamedata/" -- TODO: register all of this as ToJson instance? -def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : CommandElabM Unit := do +def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) + (inventory : InventoryOverview): CommandElabM Unit := do let game ← getCurGame let env ← getEnv let path : System.FilePath := s!"{← IO.currentDir}" / ".lake" / "gamedata" @@ -51,15 +52,4 @@ def saveGameData (allItemsByType : HashMap InventoryType (HashSet Name)) : Comma | throwError "Expected item to exist: {name}" IO.FS.writeFile (path / s!"doc__{inventoryType}__{name}.json") (toString (toJson item)) - let getTiles (type : InventoryType) : CommandElabM (Array InventoryTile) := do - (allItemsByType.findD type {}).toArray.mapM (fun name => do - let some item ← getInventoryItem? name type - | throwError "Expected item to exist: {name}" - return item.toTile) - let inventory : InventoryOverview := { - lemmas := ← getTiles .Lemma - tactics := ← getTiles .Tactic - definitions := ← getTiles .Definition - lemmaTab := none - } IO.FS.writeFile (path / s!"inventory.json") (toString (toJson inventory)) From aec196deff21b86797ca624f7480203c095cde4a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 20:26:31 +0100 Subject: [PATCH 20/32] add button to copy inventory item name to clipboard #144 --- client/src/components/inventory.tsx | 21 +++++++++++++++++++-- client/src/css/inventory.css | 24 +++++++++++++++++++++++- package-lock.json | 22 ++++++++++++++++++++++ package.json | 1 + 4 files changed, 65 insertions(+), 3 deletions(-) diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index a358e5b..c379859 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -2,7 +2,8 @@ import * as React from 'react'; import { useState, useEffect } from 'react'; import '../css/inventory.css' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { faLock, faBan } from '@fortawesome/free-solid-svg-icons' +import { faLock, faBan, faCheck } from '@fortawesome/free-solid-svg-icons' +import { faClipboard } from '@fortawesome/free-regular-svg-icons' import { GameIdContext } from '../app'; import Markdown from './markdown'; import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview, useLoadInventoryOverviewQuery } from '../state/api'; @@ -105,13 +106,29 @@ function InventoryItem({name, displayName, locked, disabled, newly, showDoc, ena const title = locked ? "Not unlocked yet" : disabled ? "Not available in this level" : "" + const [copied, setCopied] = useState(false) + const handleClick = () => { if (enableAll || !locked) { showDoc() } } - 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}) { diff --git a/client/src/css/inventory.css b/client/src/css/inventory.css index 3e02805..fb6fb0f 100644 --- a/client/src/css/inventory.css +++ b/client/src/css/inventory.css @@ -26,7 +26,11 @@ .inventory .item { background: #fff; border: solid 1px #777; - padding: .1em .5em; + padding-left: .5rem; + padding-right: 1.0rem; + padding-top: .1rem; + padding-bottom: .1rem; + position: relative; } .inventory .item.locked { @@ -72,3 +76,21 @@ color: black; border-bottom: 0.3em solid #999; } + + +.inventory .item .copy-button { + min-width: 3px; + min-height: 3px; + display: inline-block; + color: #ccc; + font-size: 0.6em; + padding-right: .2rem; + vertical-align: top; + position: absolute; + top: 0; + right: 0; + height: 100%; + width: 1rem; + align-items: end; + text-align: end; +} diff --git a/package-lock.json b/package-lock.json index 65f056c..1bef0fd 100644 --- a/package-lock.json +++ b/package-lock.json @@ -13,6 +13,7 @@ "@emotion/styled": "^11.10.5", "@fontsource/roboto": "^4.5.8", "@fontsource/roboto-mono": "^4.5.8", + "@fortawesome/free-regular-svg-icons": "^6.5.1", "@leanprover/infoview": "^0.4.3", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", @@ -2616,6 +2617,27 @@ "node": ">=6" } }, + "node_modules/@fortawesome/free-regular-svg-icons": { + "version": "6.5.1", + "resolved": "https://registry.npmjs.org/@fortawesome/free-regular-svg-icons/-/free-regular-svg-icons-6.5.1.tgz", + "integrity": "sha512-m6ShXn+wvqEU69wSP84coxLbNl7sGVZb+Ca+XZq6k30SzuP3X4TfPqtycgUh9ASwlNh5OfQCd8pDIWxl+O+LlQ==", + "hasInstallScript": true, + "dependencies": { + "@fortawesome/fontawesome-common-types": "6.5.1" + }, + "engines": { + "node": ">=6" + } + }, + "node_modules/@fortawesome/free-regular-svg-icons/node_modules/@fortawesome/fontawesome-common-types": { + "version": "6.5.1", + "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.1.tgz", + "integrity": "sha512-GkWzv+L6d2bI5f/Vk6ikJ9xtl7dfXtoRu3YGE6nq0p/FFqA1ebMOAWg3XgRyb0I6LYyYkiAo+3/KrwuBp8xG7A==", + "hasInstallScript": true, + "engines": { + "node": ">=6" + } + }, "node_modules/@fortawesome/free-solid-svg-icons": { "version": "6.4.2", "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.4.2.tgz", diff --git a/package.json b/package.json index 4f25ac1..3f0ca44 100644 --- a/package.json +++ b/package.json @@ -10,6 +10,7 @@ "@emotion/styled": "^11.10.5", "@fontsource/roboto": "^4.5.8", "@fontsource/roboto-mono": "^4.5.8", + "@fortawesome/free-regular-svg-icons": "^6.5.1", "@leanprover/infoview": "^0.4.3", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", From 4b7d540a80a3d5eb2074a21c33de0d474298ae9b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 20:49:38 +0100 Subject: [PATCH 21/32] update fortawesome packages to matching versions --- package-lock.json | 482 ++-------------------------------------------- package.json | 3 + 2 files changed, 17 insertions(+), 468 deletions(-) diff --git a/package-lock.json b/package-lock.json index 1bef0fd..0d8025f 100644 --- a/package-lock.json +++ b/package-lock.json @@ -13,7 +13,10 @@ "@emotion/styled": "^11.10.5", "@fontsource/roboto": "^4.5.8", "@fontsource/roboto-mono": "^4.5.8", + "@fortawesome/fontawesome-svg-core": "^6.5.1", "@fortawesome/free-regular-svg-icons": "^6.5.1", + "@fortawesome/free-solid-svg-icons": "^6.5.1", + "@fortawesome/react-fontawesome": "^0.2.0", "@leanprover/infoview": "^0.4.3", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", @@ -2222,231 +2225,6 @@ "resolved": "https://registry.npmjs.org/@emotion/weak-memoize/-/weak-memoize-0.3.1.tgz", "integrity": "sha512-EsBwpc7hBUJWAsNPBmJy4hxWx12v6bshQsldrVmjxJoc3isbxhOrF2IcCpaXxfvq03NwkI7sbsOLXbYuqF/8Ww==" }, - "node_modules/@esbuild/android-arm": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.18.20.tgz", - "integrity": "sha512-fyi7TDI/ijKKNZTUJAQqiG5T7YjJXgnzkURqmGj13C6dCqckZBLdl4h7bkhHt/t0WP+zO9/zwroDvANaOqO5Sw==", - "cpu": [ - "arm" - ], - "optional": true, - "os": [ - "android" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/android-arm64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.18.20.tgz", - "integrity": "sha512-Nz4rJcchGDtENV0eMKUNa6L12zz2zBDXuhj/Vjh18zGqB44Bi7MBMSXjgunJgjRhCmKOjnPuZp4Mb6OKqtMHLQ==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "android" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/android-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.18.20.tgz", - "integrity": "sha512-8GDdlePJA8D6zlZYJV/jnrRAi6rOiNaCC/JclcXpB+KIuvfBN4owLtgzY2bsxnx666XjJx2kDPUmnTtR8qKQUg==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "android" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/darwin-arm64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.18.20.tgz", - "integrity": "sha512-bxRHW5kHU38zS2lPTPOyuyTm+S+eobPUnTNkdJEfAddYgEcll4xkT8DB9d2008DtTbl7uJag2HuE5NZAZgnNEA==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "darwin" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/darwin-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.18.20.tgz", - "integrity": "sha512-pc5gxlMDxzm513qPGbCbDukOdsGtKhfxD1zJKXjCCcU7ju50O7MeAZ8c4krSJcOIJGFR+qx21yMMVYwiQvyTyQ==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "darwin" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/freebsd-arm64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.18.20.tgz", - "integrity": "sha512-yqDQHy4QHevpMAaxhhIwYPMv1NECwOvIpGCZkECn8w2WFHXjEwrBn3CeNIYsibZ/iZEUemj++M26W3cNR5h+Tw==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "freebsd" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/freebsd-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.18.20.tgz", - "integrity": "sha512-tgWRPPuQsd3RmBZwarGVHZQvtzfEBOreNuxEMKFcd5DaDn2PbBxfwLcj4+aenoh7ctXcbXmOQIn8HI6mCSw5MQ==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "freebsd" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-arm": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.18.20.tgz", - "integrity": "sha512-/5bHkMWnq1EgKr1V+Ybz3s1hWXok7mDFUMQ4cG10AfW3wL02PSZi5kFpYKrptDsgb2WAJIvRcDm+qIvXf/apvg==", - "cpu": [ - "arm" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-arm64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.18.20.tgz", - "integrity": "sha512-2YbscF+UL7SQAVIpnWvYwM+3LskyDmPhe31pE7/aoTMFKKzIc9lLbyGUpmmb8a8AixOL61sQ/mFh3jEjHYFvdA==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-ia32": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.18.20.tgz", - "integrity": "sha512-P4etWwq6IsReT0E1KHU40bOnzMHoH73aXp96Fs8TIT6z9Hu8G6+0SHSw9i2isWrD2nbx2qo5yUqACgdfVGx7TA==", - "cpu": [ - "ia32" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-loong64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.18.20.tgz", - "integrity": "sha512-nXW8nqBTrOpDLPgPY9uV+/1DjxoQ7DoB2N8eocyq8I9XuqJ7BiAMDMf9n1xZM9TgW0J8zrquIb/A7s3BJv7rjg==", - "cpu": [ - "loong64" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-mips64el": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.18.20.tgz", - "integrity": "sha512-d5NeaXZcHp8PzYy5VnXV3VSd2D328Zb+9dEq5HE6bw6+N86JVPExrA6O68OPwobntbNJ0pzCpUFZTo3w0GyetQ==", - "cpu": [ - "mips64el" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-ppc64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.18.20.tgz", - "integrity": "sha512-WHPyeScRNcmANnLQkq6AfyXRFr5D6N2sKgkFo2FqguP44Nw2eyDlbTdZwd9GYk98DZG9QItIiTlFLHJHjxP3FA==", - "cpu": [ - "ppc64" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-riscv64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.18.20.tgz", - "integrity": "sha512-WSxo6h5ecI5XH34KC7w5veNnKkju3zBRLEQNY7mv5mtBmrP/MjNBCAlsM2u5hDBlS3NGcTQpoBvRzqBcRtpq1A==", - "cpu": [ - "riscv64" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/linux-s390x": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.18.20.tgz", - "integrity": "sha512-+8231GMs3mAEth6Ja1iK0a1sQ3ohfcpzpRLH8uuc5/KVDFneH6jtAJLFGafpzpMRO6DzJ6AvXKze9LfFMrIHVQ==", - "cpu": [ - "s390x" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=12" - } - }, "node_modules/@esbuild/linux-x64": { "version": "0.18.20", "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.18.20.tgz", @@ -2462,96 +2240,6 @@ "node": ">=12" } }, - "node_modules/@esbuild/netbsd-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.18.20.tgz", - "integrity": "sha512-iO1c++VP6xUBUmltHZoMtCUdPlnPGdBom6IrO4gyKPFFVBKioIImVooR5I83nTew5UOYrk3gIJhbZh8X44y06A==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "netbsd" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/openbsd-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.18.20.tgz", - "integrity": "sha512-e5e4YSsuQfX4cxcygw/UCPIEP6wbIL+se3sxPdCiMbFLBWu0eiZOJ7WoD+ptCLrmjZBK1Wk7I6D/I3NglUGOxg==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "openbsd" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/sunos-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.18.20.tgz", - "integrity": "sha512-kDbFRFp0YpTQVVrqUd5FTYmWo45zGaXe0X8E1G/LKFC0v8x0vWrhOWSLITcCn63lmZIxfOMXtCfti/RxN/0wnQ==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "sunos" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/win32-arm64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.18.20.tgz", - "integrity": "sha512-ddYFR6ItYgoaq4v4JmQQaAI5s7npztfV4Ag6NrhiaW0RrnOXqBkgwZLofVTlq1daVTQNhtI5oieTvkRPfZrePg==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "win32" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/win32-ia32": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.18.20.tgz", - "integrity": "sha512-Wv7QBi3ID/rROT08SABTS7eV4hX26sVduqDOTe1MvGMjNd3EjOz4b7zeexIR62GTIEKrfJXKL9LFxTYgkyeu7g==", - "cpu": [ - "ia32" - ], - "optional": true, - "os": [ - "win32" - ], - "engines": { - "node": ">=12" - } - }, - "node_modules/@esbuild/win32-x64": { - "version": "0.18.20", - "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.18.20.tgz", - "integrity": "sha512-kTdfRcSiDfQca/y9QIkng02avJ+NCaQvrMejlsB3RRv5sE9rRoeBPISaZpKxHELzRxZyLvNts1P27W3wV+8geQ==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "win32" - ], - "engines": { - "node": ">=12" - } - }, "node_modules/@floating-ui/core": { "version": "1.5.0", "resolved": "https://registry.npmjs.org/@floating-ui/core/-/core-1.5.0.tgz", @@ -2597,21 +2285,21 @@ "integrity": "sha512-KrJdmkqz6DszT2wV/bbhXef4r0hV3B0vw2mAqei8A2kRnvq+gcJLmmIeQ94vu9VEXrUQzos5M9lH1TAAXpRphw==" }, "node_modules/@fortawesome/fontawesome-common-types": { - "version": "6.4.2", - "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.4.2.tgz", - "integrity": "sha512-1DgP7f+XQIJbLFCTX1V2QnxVmpLdKdzzo2k8EmvDOePfchaIGQ9eCHj2up3/jNEbZuBqel5OxiaOJf37TWauRA==", + "version": "6.5.1", + "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.1.tgz", + "integrity": "sha512-GkWzv+L6d2bI5f/Vk6ikJ9xtl7dfXtoRu3YGE6nq0p/FFqA1ebMOAWg3XgRyb0I6LYyYkiAo+3/KrwuBp8xG7A==", "hasInstallScript": true, "engines": { "node": ">=6" } }, "node_modules/@fortawesome/fontawesome-svg-core": { - "version": "6.4.2", - "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.4.2.tgz", - "integrity": "sha512-gjYDSKv3TrM2sLTOKBc5rH9ckje8Wrwgx1CxAPbN5N3Fm4prfi7NsJVWd1jklp7i5uSCVwhZS5qlhMXqLrpAIg==", + "version": "6.5.1", + "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-svg-core/-/fontawesome-svg-core-6.5.1.tgz", + "integrity": "sha512-MfRCYlQPXoLlpem+egxjfkEuP9UQswTrlCOsknus/NcMoblTH2g0jPrapbcIb04KGA7E2GZxbAccGZfWoYgsrQ==", "hasInstallScript": true, "dependencies": { - "@fortawesome/fontawesome-common-types": "6.4.2" + "@fortawesome/fontawesome-common-types": "6.5.1" }, "engines": { "node": ">=6" @@ -2629,22 +2317,13 @@ "node": ">=6" } }, - "node_modules/@fortawesome/free-regular-svg-icons/node_modules/@fortawesome/fontawesome-common-types": { - "version": "6.5.1", - "resolved": "https://registry.npmjs.org/@fortawesome/fontawesome-common-types/-/fontawesome-common-types-6.5.1.tgz", - "integrity": "sha512-GkWzv+L6d2bI5f/Vk6ikJ9xtl7dfXtoRu3YGE6nq0p/FFqA1ebMOAWg3XgRyb0I6LYyYkiAo+3/KrwuBp8xG7A==", - "hasInstallScript": true, - "engines": { - "node": ">=6" - } - }, "node_modules/@fortawesome/free-solid-svg-icons": { - "version": "6.4.2", - "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.4.2.tgz", - "integrity": "sha512-sYwXurXUEQS32fZz9hVCUUv/xu49PEJEyUOsA51l6PU/qVgfbTb2glsTEaJngVVT8VqBATRIdh7XVgV1JF1LkA==", + "version": "6.5.1", + "resolved": "https://registry.npmjs.org/@fortawesome/free-solid-svg-icons/-/free-solid-svg-icons-6.5.1.tgz", + "integrity": "sha512-S1PPfU3mIJa59biTtXJz1oI0+KAXW6bkAb31XKhxdxtuXDiUIFsih4JR1v5BbxY7hVHsD1RKq+jRkVRaf773NQ==", "hasInstallScript": true, "dependencies": { - "@fortawesome/fontawesome-common-types": "6.4.2" + "@fortawesome/fontawesome-common-types": "6.5.1" }, "engines": { "node": ">=6" @@ -5099,81 +4778,6 @@ } } }, - "node_modules/@swc/core-darwin-arm64": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-darwin-arm64/-/core-darwin-arm64-1.3.95.tgz", - "integrity": "sha512-VAuBAP3MNetO/yBIBzvorUXq7lUBwhfpJxYViSxyluMwtoQDhE/XWN598TWMwMl1ZuImb56d7eUsuFdjgY7pJw==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "darwin" - ], - "engines": { - "node": ">=10" - } - }, - "node_modules/@swc/core-darwin-x64": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-darwin-x64/-/core-darwin-x64-1.3.95.tgz", - "integrity": "sha512-20vF2rvUsN98zGLZc+dsEdHvLoCuiYq/1B+TDeE4oolgTFDmI1jKO+m44PzWjYtKGU9QR95sZ6r/uec0QC5O4Q==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "darwin" - ], - "engines": { - "node": ">=10" - } - }, - "node_modules/@swc/core-linux-arm-gnueabihf": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-linux-arm-gnueabihf/-/core-linux-arm-gnueabihf-1.3.95.tgz", - "integrity": "sha512-oEudEM8PST1MRNGs+zu0cx5i9uP8TsLE4/L9HHrS07Ck0RJ3DCj3O2fU832nmLe2QxnAGPwBpSO9FntLfOiWEQ==", - "cpu": [ - "arm" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=10" - } - }, - "node_modules/@swc/core-linux-arm64-gnu": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-gnu/-/core-linux-arm64-gnu-1.3.95.tgz", - "integrity": "sha512-pIhFI+cuC1aYg+0NAPxwT/VRb32f2ia8oGxUjQR6aJg65gLkUYQzdwuUmpMtFR2WVf7WVFYxUnjo4UyMuyh3ng==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=10" - } - }, - "node_modules/@swc/core-linux-arm64-musl": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-linux-arm64-musl/-/core-linux-arm64-musl-1.3.95.tgz", - "integrity": "sha512-ZpbTr+QZDT4OPJfjPAmScqdKKaT+wGurvMU5AhxLaf85DuL8HwUwwlL0n1oLieLc47DwIJEMuKQkYhXMqmJHlg==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "linux" - ], - "engines": { - "node": ">=10" - } - }, "node_modules/@swc/core-linux-x64-gnu": { "version": "1.3.95", "resolved": "https://registry.npmjs.org/@swc/core-linux-x64-gnu/-/core-linux-x64-gnu-1.3.95.tgz", @@ -5204,51 +4808,6 @@ "node": ">=10" } }, - "node_modules/@swc/core-win32-arm64-msvc": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-win32-arm64-msvc/-/core-win32-arm64-msvc-1.3.95.tgz", - "integrity": "sha512-YaP4x/aZbUyNdqCBpC2zL8b8n58MEpOUpmOIZK6G1SxGi+2ENht7gs7+iXpWPc0sy7X3YPKmSWMAuui0h8lgAA==", - "cpu": [ - "arm64" - ], - "optional": true, - "os": [ - "win32" - ], - "engines": { - "node": ">=10" - } - }, - "node_modules/@swc/core-win32-ia32-msvc": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-win32-ia32-msvc/-/core-win32-ia32-msvc-1.3.95.tgz", - "integrity": "sha512-w0u3HI916zT4BC/57gOd+AwAEjXeUlQbGJ9H4p/gzs1zkSHtoDQghVUNy3n/ZKp9KFod/95cA8mbVF9t1+6epQ==", - "cpu": [ - "ia32" - ], - "optional": true, - "os": [ - "win32" - ], - "engines": { - "node": ">=10" - } - }, - "node_modules/@swc/core-win32-x64-msvc": { - "version": "1.3.95", - "resolved": "https://registry.npmjs.org/@swc/core-win32-x64-msvc/-/core-win32-x64-msvc-1.3.95.tgz", - "integrity": "sha512-5RGnMt0S6gg4Gc6QtPUJ3Qs9Un4sKqccEzgH/tj7V/DVTJwKdnBKxFZfgQ34OR2Zpz7zGOn889xwsFVXspVWNA==", - "cpu": [ - "x64" - ], - "optional": true, - "os": [ - "win32" - ], - "engines": { - "node": ">=10" - } - }, "node_modules/@swc/counter": { "version": "0.1.2", "resolved": "https://registry.npmjs.org/@swc/counter/-/counter-0.1.2.tgz", @@ -8557,19 +8116,6 @@ "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz", "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw==" }, - "node_modules/fsevents": { - "version": "2.3.3", - "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.3.tgz", - "integrity": "sha512-5xoDfX+fL7faATnagmWPpbFtwh/R77WmMMqqHGS65C3vvB0YHrgF+B1YmZ3441tMj5n63k0212XNoJwzlhffQw==", - "hasInstallScript": true, - "optional": true, - "os": [ - "darwin" - ], - "engines": { - "node": "^8.16.0 || ^10.6.0 || >=11.0.0" - } - }, "node_modules/function-bind": { "version": "1.1.1", "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz", diff --git a/package.json b/package.json index 3f0ca44..d0d6793 100644 --- a/package.json +++ b/package.json @@ -10,7 +10,10 @@ "@emotion/styled": "^11.10.5", "@fontsource/roboto": "^4.5.8", "@fontsource/roboto-mono": "^4.5.8", + "@fortawesome/fontawesome-svg-core": "^6.5.1", "@fortawesome/free-regular-svg-icons": "^6.5.1", + "@fortawesome/free-solid-svg-icons": "^6.5.1", + "@fortawesome/react-fontawesome": "^0.2.0", "@leanprover/infoview": "^0.4.3", "@mui/icons-material": "^5.11.0", "@mui/material": "^5.11.1", From 5fd49abb9025fa7148931c7c2acc3d87919edfa1 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 21:05:37 +0100 Subject: [PATCH 22/32] improve hover text for inventory items #144 --- client/src/components/inventory.tsx | 11 +++++++---- client/src/state/api.ts | 1 + server/GameServer/Commands.lean | 4 ++++ server/GameServer/EnvExtensions.lean | 2 ++ 4 files changed, 14 insertions(+), 4 deletions(-) diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index c379859..95a5980 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -90,21 +90,24 @@ 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.substring(item.altTitle.indexOf(' ') + 1) const [copied, setCopied] = useState(false) diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 2bdbe8b..1a64597 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -35,6 +35,7 @@ export interface InventoryTile { locked: boolean, new: boolean, hidden: boolean + altTitle: string, } export interface LevelInfo { diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 8bd5fd5..a12a94a 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -781,6 +781,7 @@ elab "MakeGame" : command => do name := item displayName := data.displayName category := data.category + altTitle := data.statement hidden := hiddenItems.contains item }) @@ -800,6 +801,7 @@ elab "MakeGame" : command => do displayName := data.displayName category := data.category locked := false + altTitle := data.statement hidden := hiddenItems.contains item } itemsInWorld := itemsInWorld.insert worldId items @@ -819,6 +821,7 @@ elab "MakeGame" : command => do displayName := data.displayName category := data.category locked := false + altTitle := data.statement hidden := hiddenItems.contains item } -- add the exercise statement from the previous level @@ -832,6 +835,7 @@ elab "MakeGame" : command => do name := name displayName := data.displayName category := data.category + altTitle := data.statement locked := false } -- add marks for `disabled` and `new` lemmas here, so that they only apply to diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index fdbd351..d2fa975 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -106,6 +106,8 @@ structure InventoryTile where new := false /-- hide the item in the inventory display -/ hidden := false + /-- hover text -/ + altTitle : String := default deriving ToJson, FromJson, Repr, Inhabited def InventoryItem.toTile (item : InventoryItem) : InventoryTile := { From e76e28776397c1fe0ba14f84ffdb41db1c4dfd9a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 21:14:42 +0100 Subject: [PATCH 23/32] fix: persistent lemma tab #144 --- client/src/components/inventory.tsx | 33 ++++++++++++++++------------- 1 file changed, 18 insertions(+), 15 deletions(-) diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 95a5980..d83719c 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -11,10 +11,12 @@ import { selectDifficulty, selectInventory } from '../state/progress'; import { store } from '../state/store'; import { useSelector } from 'react-redux'; -export function Inventory({levelInfo, openDoc, enableAll=false} : +export function Inventory({levelInfo, openDoc, lemmaTab, setLemmaTab, enableAll=false} : { levelInfo: LevelInfo|InventoryOverview, openDoc: (props: {name: string, type: string}) => void, + lemmaTab: any, + setLemmaTab: any, enableAll?: boolean, }) { @@ -32,19 +34,20 @@ export function Inventory({levelInfo, openDoc, enableAll=false} : }

Theorems

{levelInfo?.lemmas && - + }
) } -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 @@ -60,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 @@ -69,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 &&
@@ -151,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 ? : - + }
} From 1ab50710f5c18b61b66f7c7c07af086e3a00567b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 21:24:08 +0100 Subject: [PATCH 24/32] fix: update rules slider on erasing progress #157 --- client/src/components/world_tree.tsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index 13619bf..68168f3 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -213,7 +213,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) { title="Game Rules" min={0} max={2} aria-label="Game Rules" - defaultValue={difficulty} + value={difficulty} marks={[ {value: 0, label: label(0)}, {value: 1, label: label(1)}, From 2d0f69d337b7573463ed7391fe3b2146534d5d5f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 21:44:36 +0100 Subject: [PATCH 25/32] fix: prevent multiple NewTactic per level #125 --- server/GameServer/Commands.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index a12a94a..e4e84f0 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -202,8 +202,13 @@ elab doc:docComment ? "DefinitionDoc" name:ident "as" displayName:str template:s /-! ## Add inventory items -/ +def checkCommandNotDuplicated (items : Array Name) (cmd := "Command") : CommandElabM Unit := do + if ¬ items.isEmpty then + logWarning s!"You should only use one `{cmd}` per level, but it takes multiple arguments: `{cmd} obj₁ obj₂ obj₃`!" + /-- Declare tactics that are introduced by this level. -/ elab "NewTactic" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).tactics.new) "NewTactic" for name in ↑args do checkInventoryDoc .Tactic name -- TODO: Add (template := "[docstring]") modifyCurLevel fun level => pure {level with @@ -211,6 +216,7 @@ elab "NewTactic" args:ident* : command => do /-- Declare tactics that are introduced by this level but do not show up in inventory. -/ elab "NewHiddenTactic" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).tactics.hidden) "NewHiddenTactic" for name in ↑args do checkInventoryDoc .Tactic name (template := "") modifyCurLevel fun level => pure {level with @@ -219,6 +225,7 @@ elab "NewHiddenTactic" args:ident* : command => do /-- Declare lemmas that are introduced by this level. -/ elab "NewLemma" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).lemmas.new) "NewLemma" for name in ↑args do try let _decl ← getConstInfo name.getId catch | _ => logErrorAt name m!"unknown identifier '{name}'." @@ -228,6 +235,7 @@ elab "NewLemma" args:ident* : command => do /-- Declare definitions that are introduced by this level. -/ elab "NewDefinition" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).definitions.new) "NewDefinition" for name in ↑args do checkInventoryDoc .Definition name -- TODO: Add (template := "[mathlib]") modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := args.map (·.getId)}} @@ -235,6 +243,7 @@ elab "NewDefinition" args:ident* : command => do /-- Declare tactics that are temporarily disabled in this level. This is ignored if `OnlyTactic` is set. -/ elab "DisabledTactic" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).tactics.disabled) "DisabledTactic" for name in ↑args do checkInventoryDoc .Tactic name modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := args.map (·.getId)}} @@ -242,24 +251,28 @@ elab "DisabledTactic" args:ident* : command => do /-- Declare lemmas that are temporarily disabled in this level. This is ignored if `OnlyLemma` is set. -/ elab "DisabledLemma" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).lemmas.disabled) "DisabledLemma" for name in ↑args do checkInventoryDoc .Lemma name modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := args.map (·.getId)}} /-- Declare definitions that are temporarily disabled in this level -/ elab "DisabledDefinition" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).definitions.disabled) "DisabledDefinition" for name in ↑args do checkInventoryDoc .Definition name modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := args.map (·.getId)}} /-- Temporarily disable all tactics except the ones declared here -/ elab "OnlyTactic" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).tactics.only) "OnlyTactic" for name in ↑args do checkInventoryDoc .Tactic name modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := args.map (·.getId)}} /-- Temporarily disable all lemmas except the ones declared here -/ elab "OnlyLemma" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).lemmas.only) "OnlyLemma" for name in ↑args do checkInventoryDoc .Lemma name modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := args.map (·.getId)}} @@ -267,6 +280,7 @@ elab "OnlyLemma" args:ident* : command => do /-- Temporarily disable all definitions except the ones declared here. This is ignored if `OnlyDefinition` is set. -/ elab "OnlyDefinition" args:ident* : command => do + checkCommandNotDuplicated ((←getCurLevel).definitions.only) "OnlyDefinition" for name in ↑args do checkInventoryDoc .Definition name modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := args.map (·.getId)}} From eaa214ec3728ddb4463ce99505d4d53f9e61bfd4 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 14 Dec 2023 21:59:47 +0100 Subject: [PATCH 26/32] improve world tree on mobile #101 --- client/src/components/world_tree.tsx | 6 ++++-- client/src/css/world_tree.css | 5 ++++- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/client/src/components/world_tree.tsx b/client/src/components/world_tree.tsx index 68168f3..1aa495b 100644 --- a/client/src/components/world_tree.tsx +++ b/client/src/components/world_tree.tsx @@ -11,7 +11,7 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons' import { GameIdContext } from '../app' -import { useAppDispatch } from '../hooks' +import { useAppDispatch, useMobile } from '../hooks' import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress' import { store } from '../state/store' @@ -197,13 +197,15 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) { const gameId = React.useContext(GameIdContext) const difficulty = useSelector(selectDifficulty(gameId)) const dispatch = useAppDispatch() + const { mobile } = useMobile() + function label(x : number) { return x == 0 ? 'none' : x == 1 ? 'relaxed' : 'regular' } - return