diff --git a/.env b/.env deleted file mode 100644 index 01fee6b..0000000 --- a/.env +++ /dev/null @@ -1 +0,0 @@ -LEAN4GAME_SINGLE_GAME=false diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 2e2d4bc..00d2e43 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -5,7 +5,17 @@ jobs: build: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - name: install elan + run: | + set -o pipefail + curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz + ./elan-init -y + echo "$HOME/.elan/bin" >> $GITHUB_PATH + - uses: actions/checkout@v4 - uses: actions/setup-node@v3 + - name: print lean and lake versions + run: | + lean --version + lake --version - run: npm install - run: npm run build diff --git a/.gitignore b/.gitignore index 407cbdf..f6fa519 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,5 @@ node_modules client/dist -server/build -server/lakefile.olean -**/lake-packages/ +games/ +server/.lake **/.DS_Store diff --git a/README.md b/README.md index 13a2aa2..b5a610a 100644 --- a/README.md +++ b/README.md @@ -2,30 +2,33 @@ This is the source code for a Lean 4 game platform hosted at [adam.math.hhu.de](https://adam.math.hhu.de). -The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game -(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) -of Kevin Buzzard and Mohammad Pedramfar. -The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4). - ## Creating a Game -Please follow the tutorial [Creating a Game](doc/create_game.md). -In particular step 5 thereof explains [How to Run Games Locally](doc/running_locally.md). +Please follow the tutorial [Creating a Game](doc/create_game.md). In particular, the following steps might be of interest: -### Publishing a Game +* Step 5: [How to Run Games Locally](doc/running_locally.md) +* Step 7: [How to Update an existing Game](doc/update_game.md) +* Step 8: [How to Publishing a Game](doc/publish_game.md) -We encourage anybody to have games hosted on our [Lean Game Server](https://adam.math.hhu.de) for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language. +## Documentation -For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster). +The documentation is very much work in progress but the linked documentation here +should be up-to-date: -## Documentation +### Game creation API + +- [Creating a Game](doc/create_game.md): **the main document to consult**. +- [More about Hints](doc/hints.md): describes the `Hint` and `Branch` tactic. -The documentation for the game engine itself is still missing, but there is [Creating a Game](doc/create_game.md) explaining the API to create a game. +### Frontend API -Some documentation: +* [How to Run Games Locally](doc/running_locally.md): play a game on your computer +* [How to Update an existing Game](doc/update_game.md): update to a new lean version +* [How to Publishing a Game](doc/publish_game.md): load your game to adam.math.hhu.de for others to play -- [NPM Scripts](doc/npm_scripts.md) -- [Old documentation](doc/DOCUMENTATION.md) +### Backend + +not written yet ## Contributing @@ -34,3 +37,10 @@ Contributions to `lean4game` are always welcome! ## Security Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap. + +## Credits + +The project is based on ideas from the [Lean Game Maker](https://github.com/mpedramfar/Lean-game-maker) and the [Natural Number Game +(NNG)](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/) +by Kevin Buzzard and Mohammad Pedramfar. +The project is based on Patrick Massot's prototype: [NNG4](https://github.com/PatrickMassot/NNG4). diff --git a/client/src/app.tsx b/client/src/app.tsx index 653d0db..4dda0fd 100644 --- a/client/src/app.tsx +++ b/client/src/app.tsx @@ -11,7 +11,7 @@ import './css/app.css'; import { MobileContext } from './components/infoview/context'; import { useMobile } from './hooks'; import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences'; - +import { connection } from './connection'; export const GameIdContext = React.createContext(undefined); @@ -37,6 +37,10 @@ function App() { } }, [lockMobile]) + React.useEffect(() => { + connection.startLeanClient(gameId); + }, [gameId]) + return (
diff --git a/client/src/assets/covers/formaloversum.png b/client/src/assets/covers/formaloversum.png deleted file mode 100644 index df9723d..0000000 Binary files a/client/src/assets/covers/formaloversum.png and /dev/null differ diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx index c766b52..ced97d5 100644 --- a/client/src/components/app_bar.tsx +++ b/client/src/components/app_bar.tsx @@ -166,7 +166,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres const [navOpen, setNavOpen] = React.useState(false) return
-
+
@@ -241,7 +241,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber= : <> {/* DESKTOP VERSION */} -
+
{worldTitle && `World: ${worldTitle}`}
diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index 2692a7d..037eb86 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -1,6 +1,7 @@ import { GameHint } from "./infoview/rpc_api"; import * as React from 'react'; import Markdown from './markdown'; +import { ProofStep } from "./infoview/context"; export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) { return
@@ -43,3 +44,24 @@ export function DeletedHints({hints} : {hints: GameHint[]}) { {hiddenHints.map((hint, i) => )} } + +/** Filter hints to not show consequtive identical hints twice. + * + * This function takes a `ProofStep[]` and extracts the hints in form of an + * element of type `GameHint[][]` where it removes hints that are identical to hints + * appearing in the previous step. Hidden hints are not filtered. + * + * This effectively means we prevent consequtive identical hints from being shown. + */ +export function filterHints(proof: ProofStep[]): GameHint[][] { + return proof.map((step, i) => { + if (i == 0){ + return step.hints + } else { + // TODO: Writing all fields explicitely is somewhat fragile to changes, is there a + // good way to shallow-compare objects? + return step.hints.filter((hint) => hint.hidden || + (proof[i-1].hints.find((x) => (x.text == hint.text && x.hidden == hint.hidden)) === undefined)) + } + }) +} diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index ab670a1..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. @@ -156,7 +156,7 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) { const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) - console.debug(`template: ${props.data.template}`) + console.debug(`template: ${props.data?.template}`) // React.useEffect (() => { // if (props.data.template) { @@ -347,6 +347,7 @@ export function TypewriterInterface({props}) { const uri = model.uri.toString() const [disableInput, setDisableInput] = React.useState(false) + const [loadingProgress, setLoadingProgress] = React.useState(0) const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext) const {mobile} = React.useContext(MobileContext) const { proof } = React.useContext(ProofContext) @@ -366,9 +367,9 @@ export function TypewriterInterface({props}) { function deleteProof(line: number) { return (ev) => { let deletedChat: Array = [] - proof.slice(line).map((step, i) => { + filterHints(proof).slice(line).map((hintsAtStep, i) => { // Only add these hidden hints to the deletion stack which were visible - deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))] + deletedChat = [...deletedChat, ...hintsAtStep.filter(hint => (!hint.hidden || showHelp.has(line + i)))] }) setDeletedChat(deletedChat) @@ -455,6 +456,17 @@ export function TypewriterInterface({props}) { let lastStepErrors = proof.length ? hasInteractiveErrors(proof[proof.length - 1].errors) : false + + useServerNotificationEffect("$/game/loading", (params : any) => { + if (params.kind == "loadConstants") { + setLoadingProgress(params.counter/100*50) + } else if (params.kind == "finalizeExtensions") { + setLoadingProgress(50 + params.counter/150*50) + } else { + console.error(`Unknown loading kind: ${params.kind}`) + } + }) + return
@@ -521,7 +533,7 @@ export function TypewriterInterface({props}) { }
} - : + : }
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 896b1f7..a358e5b 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -86,7 +86,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine {[...modifiedItems].sort( // For lemas, sort entries `available > disabled > locked` // otherwise alphabetically - (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) + (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) || x.displayName.localeCompare(y.displayName) ).filter(item => !item.hidden && ((tab ?? categories[0]) == item.category)).map((item, i) => { return {openDoc({name: item.name, type: docType})}} diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx index f4596b1..e2c870f 100644 --- a/client/src/components/landing_page.tsx +++ b/client/src/components/landing_page.tsx @@ -7,11 +7,12 @@ import '@fontsource/roboto/500.css'; import '@fontsource/roboto/700.css'; import '../css/landing_page.css' -import coverRobo from '../assets/covers/formaloversum.png' import bgImage from '../assets/bg.jpg' import Markdown from './markdown'; import {PrivacyPolicyPopup} from './popup/privacy_policy' +import { GameTile, useGetGameInfoQuery } from '../state/api' +import path from 'path'; const flag = { 'Dutch': '🇳🇱', @@ -19,6 +20,7 @@ const flag = { 'French': '🇫🇷', 'German': '🇩🇪', 'Italian': '🇮🇹', + 'Spanish': '🇪🇸', } function GithubIcon({url='https://github.com'}) { @@ -32,47 +34,42 @@ function GithubIcon({url='https://github.com'}) {
} -function GameTile({ - title, - gameId, - intro, // Catchy intro phrase. - image=null, - worlds='?', - levels='?', - prereq='–', // Optional list of games that this game builds on. Use markdown. - description, // Longer description. Supports Markdown. - language}) { +function Tile({gameId, data}: {gameId: string, data: GameTile|undefined}) { let navigate = useNavigate(); const routeChange = () =>{ navigate(gameId); } + if (typeof data === 'undefined') { + return <> + } + return
-
{title}
-
{intro} +
{data.title}
+
{data.short}
- { image ? :
} -
{description}
+ { data.image ? :
} +
{data.long}
- + - + - + - +
Prerequisites{prereq}{data.prerequisites.join(', ')}
Worlds{worlds}{data.worlds}
Levels{levels}{data.levels}
Language{flag[language]}{data.languages.map((lan) => flag[lan]).join(', ')}
@@ -88,6 +85,58 @@ function LandingPage() { const openImpressum = () => setImpressum(true); const closeImpressum = () => setImpressum(false); + // const [allGames, setAllGames] = React.useState([]) + // const [allTiles, setAllTiles] = React.useState([]) + + // const getTiles=()=>{ + // fetch('featured_games.json', { + // headers : { + // 'Content-Type': 'application/json', + // 'Accept': 'application/json' + // } + // } + // ).then(function(response){ + // return response.json() + // }).then(function(data) { + // setAllGames(data.featured_games) + + // }) + // } + + // React.useEffect(()=>{ + // getTiles() + // },[]) + + // React.useEffect(()=>{ + + // Promise.allSettled( + // allGames.map((gameId) => ( + // fetch(`data/g/${gameId}/game.json`).catch(err => {return undefined}))) + // ).then(responses => + // responses.forEach((result) => console.log(result))) + // // Promise.all(responses.map(res => { + // // if (res.status == "fulfilled") { + // // console.log(res.value.json()) + // // return res.value.json() + // // } else { + // // return undefined + // // } + // // })) + // // ).then(allData => { + // // setAllTiles(allData.map(data => data?.tile)) + // // }) + // },[allGames]) + + // TODO: I would like to read the supported games list form a JSON, + // Then load all these games in + // + let allGames = [ + "leanprover-community/nng4", + "hhu-adam/robo", + "djvelleman/stg4", + "miguelmarco/STG4", + ] + let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile)) return
@@ -104,49 +153,26 @@ function LandingPage() {
- - - - - - + {allTiles.length == 0 ? +

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

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

Development notes

As this server runs lean on our university machines, it has a limited capacity. - Our current estimate is about 55 copies of the NNG or 25 copies of games importing - mathlib. We hope to address this limitation in the future. + Our current estimate is about 70 simultaneous games. + We hope to address and test this limitation better in the future.

Most aspects of the games and the infrastructure are still in development. Feel free to @@ -160,18 +186,19 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet

Adding new games

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

- There is an option to load and run your own games 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.

@@ -189,9 +216,6 @@ Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet Impressum {impressum? : null} - - {/* */} -
} diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 806082d..1251645 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -22,7 +22,7 @@ import { ConnectionContext, connection, useLeanClient } from '../connection' import { useAppDispatch, useAppSelector } from '../hooks' import { useGetGameInfoQuery, useLoadInventoryOverviewQuery, useLoadLevelQuery } from '../state/api' import { changedSelection, codeEdited, selectCode, selectSelections, selectCompleted, helpEdited, - selectHelp, selectDifficulty, selectInventory } from '../state/progress' + selectHelp, selectDifficulty, selectInventory, selectTypewriterMode, changeTypewriterMode } from '../state/progress' import { store } from '../state/store' import { Button } from './button' import Markdown from './markdown' @@ -32,8 +32,9 @@ import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContex ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context' import { DualEditor } from './infoview/main' import { GameHint } from './infoview/rpc_api' -import { DeletedHints, Hint, Hints } from './hints' +import { DeletedHints, Hint, Hints, filterHints } from './hints' import { PrivacyPolicyPopup } from './popup/privacy_policy' +import path from 'path'; import '@fontsource/roboto/300.css' import '@fontsource/roboto/400.css' @@ -48,7 +49,6 @@ function Level() { const params = useParams() const levelId = parseInt(params.levelId) const worldId = params.worldId - // useLoadWorldFiles(worldId) const [impressum, setImpressum] = React.useState(false) @@ -138,19 +138,24 @@ function ChatPanel({lastLevel}) { let introText: Array = level?.data?.introduction.split(/\n(\s*\n)+/) + // experimental: Remove all hints that appeared identically in the previous step + // This effectively prevent consequtive hints being shown. + let modifiedHints : GameHint[][] = filterHints(proof) + return
{introText?.filter(t => t.trim()).map(((t, i) => + // Show the level's intro text as hints, too ))} - {proof.map((step, i) => { + {modifiedHints.map((step, i) => { // It the last step has errors, it will have the same hints // as the second-to-last step. Therefore we should not display them. if (!(i == proof.length - 1 && withErr)) { // TODO: Should not use index as key. return } })} @@ -204,11 +209,16 @@ function PlayableLevel({impressum, setImpressum}) { const {worldId, levelId} = useContext(WorldLevelIdContext) const {mobile} = React.useContext(MobileContext) + const dispatch = useAppDispatch() + const difficulty = useSelector(selectDifficulty(gameId)) const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) const inventory: Array = useSelector(selectInventory(gameId)) + const typewriterMode = useSelector(selectTypewriterMode(gameId)) + const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) + const gameInfo = useGetGameInfoQuery({game: gameId}) const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId}) @@ -221,12 +231,11 @@ function PlayableLevel({impressum, setImpressum}) { const [showHelp, setShowHelp] = useState>(new Set()) // Only for mobile layout const [pageNumber, setPageNumber] = useState(0) - const [typewriterMode, setTypewriterMode] = useState(true) + // set to true to prevent switching between typewriter and editor const [lockInputMode, setLockInputMode] = useState(false) const [typewriterInput, setTypewriterInput] = useState("") const lastLevel = levelId >= gameInfo.data?.worldSize[worldId] - const dispatch = useAppDispatch() // impressum pop-up function toggleImpressum() {setImpressum(!impressum)} @@ -320,8 +329,6 @@ function PlayableLevel({impressum, setImpressum}) { console.debug(`not inserting template.`) } } - } else { - setTypewriterMode(true) } }, [level, levelId, worldId, gameId, editor]) @@ -336,7 +343,7 @@ function PlayableLevel({impressum, setImpressum}) { }, [gameId, worldId, levelId]) useEffect(() => { - if (!typewriterMode) { + if (!typewriterMode && editor) { // Delete last input attempt from command line editor.executeEdits("typewriter", [{ range: editor.getSelection(), @@ -466,6 +473,11 @@ function Introduction({impressum, setImpressum}) { const gameInfo = useGetGameInfoQuery({game: gameId}) + const {worldId} = useContext(WorldLevelIdContext) + + let image: string = gameInfo.data?.worlds.nodes[worldId].image + + const toggleImpressum = () => { setImpressum(!impressum) } @@ -479,7 +491,13 @@ function Introduction({impressum, setImpressum}) { : -
+
+ {image && + // TODO: Temporary for testing + + } + +
} @@ -615,6 +633,7 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange return () => { editorConnection.api.sendClientNotification(uriStr, "textDocument/didClose", {textDocument: {uri: uriStr}}) + model.dispose(); } } }, [editor, levelId, connection, leanClientStarted]) @@ -637,27 +656,3 @@ function useLevelEditor(codeviewRef, initialCode, initialSelections, onDidChange return {editor, infoProvider, editorConnection} } - -/** Open all files in this world on the server so that they will load faster when accessed */ -function useLoadWorldFiles(worldId) { - const gameId = React.useContext(GameIdContext) - const gameInfo = useGetGameInfoQuery({game: gameId}) - const store = useStore() - - useEffect(() => { - if (gameInfo.data) { - const models = [] - for (let levelId = 1; levelId <= gameInfo.data.worldSize[worldId]; levelId++) { - const uri = monaco.Uri.parse(`file:///${worldId}/${levelId}`) - let model = monaco.editor.getModel(uri) - if (model) { - models.push(model) - } else { - const code = selectCode(gameId, worldId, levelId)(store.getState()) - models.push(monaco.editor.createModel(code, 'lean4', uri)) - } - } - return () => { for (let model of models) { model.dispose() } } - } - }, [gameInfo.data, worldId]) -} diff --git a/client/src/css/app.css b/client/src/css/app.css index 3226e1f..206638d 100644 --- a/client/src/css/app.css +++ b/client/src/css/app.css @@ -105,11 +105,18 @@ 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; + gap: .5em; +} + .app-bar-title, .app-bar-subtitle { color: white; font-weight: 500; diff --git a/client/src/css/landing_page.css b/client/src/css/landing_page.css index a42f184..71d8526 100644 --- a/client/src/css/landing_page.css +++ b/client/src/css/landing_page.css @@ -48,6 +48,7 @@ a { border: 1px solid rgb(140, 140, 140); border-radius: 20px; box-shadow: 5px 5px 8px rgb(140, 140, 140); + width: 100%; max-width: 500px; display: flex; flex-direction: column; diff --git a/client/src/css/level.css b/client/src/css/level.css index faa2c0d..564340a 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; } @@ -336,6 +331,21 @@ td code { background-color: #eee; } +.world-image-container { + display: flex; + flex-direction: column; + justify-content: center; +} + +.world-image-container img.contain { + object-fit: contain; +} + +.world-image-container img.cover { + height: 100%; + object-fit: cover; +} + .typewriter-interface .proof { background-color: #fff; } diff --git a/client/src/index.tsx b/client/src/index.tsx index 85c6c83..c42b6dc 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -15,15 +15,6 @@ import { monacoSetup } from 'lean4web/client/src/monacoSetup' monacoSetup() -// // Do not show the landing page in the dev-container context -// let root_path: RouteObject = (process.env.LEAN4GAME_SINGLE_GAME == "true") ? { -// path: "/", -// loader: () => redirect("/g/local/game") -// } : { -// path: "/", -// element: , -// } - // If `VITE_LEAN4GAME_SINGLE` is set to true, then `/` should be redirected to // `/g/local/game`. This is used for the devcontainer setup @@ -43,6 +34,11 @@ const router = createHashRouter([ path: "/game/nng", loader: () => redirect("/g/hhu-adam/NNG4") }, + { + // For backwards compatibility + path: "/g/hhu-adam/NNG4", + loader: () => redirect("/g/leanprover-community/NNG4") + }, { path: "/g/:owner/:repo", element: , diff --git a/client/src/state/api.ts b/client/src/state/api.ts index 725c7ad..2bdbe8b 100644 --- a/client/src/state/api.ts +++ b/client/src/state/api.ts @@ -2,16 +2,29 @@ * @fileOverview Define API of the server-client communication */ import { createApi, fetchBaseQuery } from '@reduxjs/toolkit/query/react' -import { Connection } from '../connection' + + +export interface GameTile { + title: string + short: string + long: string + languages: Array + prerequisites: Array + worlds: number + levels: number + image: string +} export interface GameInfo { title: null|string, introduction: null|string, info: null|string, - worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]}, + worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string, image: string}}, edges: string[][]}, worldSize: null|{[key: string]: number}, authors: null|string[], conclusion: null|string, + tile: null|GameTile, + image: null|string } export interface InventoryTile { @@ -37,7 +50,8 @@ export interface LevelInfo { lemmaTab: null|string, statementName: null|string, displayName: null|string, - template: null|string + template: null|string, + image: null|string } /** Used to display the inventory on the welcome page */ @@ -57,40 +71,22 @@ interface Doc { category: string, } - -const customBaseQuery = async ( - args : {game: string, method: string, params?: any}, - { signal, dispatch, getState, extra }, - extraOptions -) => { - try { - const connection : Connection = extra.connection - let leanClient = await connection.startLeanClient(args.game) - console.log(`Sending request ${args.method}`) - let res = await leanClient.sendRequest(args.method, args.params) - console.log('Received response') //, res) - return {'data': res} - } catch (e) { - return {'error': e} - } -} - // Define a service using a base URL and expected endpoints export const apiSlice = createApi({ reducerPath: 'gameApi', - baseQuery: customBaseQuery, + baseQuery: fetchBaseQuery({ baseUrl: window.location.origin + "/data" }), endpoints: (builder) => ({ getGameInfo: builder.query({ - query: ({game}) => {return {game, method: 'info', params: {}}}, + query: ({game}) => `${game}/game.json`, }), loadLevel: builder.query({ - query: ({game, world, level}) => {return {game, method: "loadLevel", params: {world, level}}}, + query: ({game, world, level}) => `${game}/level__${world}__${level}.json`, }), loadInventoryOverview: builder.query({ - query: ({game}) => {return {game, method: "loadInventoryOverview", params: {}}}, + query: ({game}) => `${game}/inventory.json`, }), loadDoc: builder.query({ - query: ({game, name, type}) => {return {game, method: "loadDoc", params: {name, type}}}, + query: ({game, type, name}) => `${game}/doc__${type}__${name}.json`, }), }), }) diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index f553159..c8c4242 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -26,7 +26,8 @@ export interface GameProgressState { inventory: string[], difficulty: number, openedIntro: boolean, - data: WorldProgressState + data: WorldProgressState, + typewriterMode?: boolean } /** @@ -126,6 +127,11 @@ export const progressSlice = createSlice({ addGameProgress(state, action) state.games[action.payload.game].openedIntro = action.payload.openedIntro }, + /** set the typewriter mode */ + changeTypewriterMode(state: ProgressState, action: PayloadAction<{game: string, typewriterMode: boolean}>) { + addGameProgress(state, action) + state.games[action.payload.game].typewriterMode = action.payload.typewriterMode + } } }) @@ -196,7 +202,14 @@ export function selectOpenedIntro(game: string) { } } +/** return typewriter mode for the current game if it exists */ +export function selectTypewriterMode(game: string) { + return (state) => { + return state.progress.games[game]?.typewriterMode ?? true + } +} + /** Export actions to modify the progress */ export const { changedSelection, codeEdited, levelCompleted, deleteProgress, deleteLevelProgress, loadProgress, helpEdited, changedInventory, changedOpenedIntro, - changedDifficulty } = progressSlice.actions + changedDifficulty, changeTypewriterMode} = progressSlice.actions diff --git a/doc/DOCUMENTATION.md b/doc/DOCUMENTATION.md index 2cd8725..68464ca 100644 --- a/doc/DOCUMENTATION.md +++ b/doc/DOCUMENTATION.md @@ -1,6 +1,8 @@ +**NOTE! This document is deprecated! The current documentation is [How To Create A Game](create_game.md)** + # Creating a game. -Ideally one takes the [NNG template](https://github.com/hhu-adam/NNG4) to create a new game. +Ideally one takes the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new game. ## Game Structure @@ -295,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/doc/create_game.md b/doc/create_game.md index ebe9fcb..303962e 100644 --- a/doc/create_game.md +++ b/doc/create_game.md @@ -4,7 +4,7 @@ This tutorial walks you through creating a new game for lean4. It covers from wr ## 1. Create the project -1. Use the [NNG template](https://github.com/hhu-adam/NNG4) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository". +1. Use the [GameSkeleton template](https://github.com/hhu-adam/GameSkeleton) to create a new github repo for your game: On github, click on "Use this template" > "Create a new repository". 2. Clone the game repo. 3. Call `lake update && lake exe cache get && lake build` to build the Lean project. @@ -223,25 +223,40 @@ One thing to keep in mind is that the game will look at the main proof to figure Most important for game development are probably the `Hints`. The hints will be displayed whenever the player's current goal matches the goal the hint is -placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. If you specify +placed at inside the sample proof. You can use `Branch` to place hints in dead ends or alternative proof strands. -``` -Hint (strict := true) "some hidden hint" -``` +Read [More about Hints](doc/hints.md) for how they work and what the options are. -a hint only matches iff the assumptions match exactly one-to-one. (Otherwise, it does not care if there are additional assumptions in context) +### 6. e) Extra: Images +You can add images on any layer of the game (i.e. game/world/level). These will be displayed in your game. -Further, you can choose to hide hints and only have them displayed when the player presses "More Help": -``` -Hint (hidden := true) "some hidden hint" -``` +The images need to be placed in `images/` and you need to add a command like `Image "images/path/to/myWorldImage.png"` +in one of the files you created in 2), 3), or 4) (i.e. game/world/level). -Lastly, you should put variable names in hints inside brackets: +NOTE: At present, only the images for a world are displayed. They appear in the introduction of the world. +## 7. Update your game + +In principle, it is as simple as modifying `lean-toolchain` to update your game to a new Lean version. However, you should read about the details in [Update An Existing Game](doc/update_game.md). + +## 8. Publish your game + +To publish your game on the official server, see [Publishing a game](doc/publish_game.md) + +There are a few more options you can add in `Game.lean` before the `MakeGame` command, which describe the tile that is visible on the server's landing page: + +```lean +Languages "English" +CaptionShort "Game Template" +CaptionLong "You should use this game as a template for your own game and add your own levels." +Prerequisites "NNG" +CoverImage "images/cover.png" ``` -Hint "now use `rw [{h}]` to use your assumption {h}." -``` -That way, the game will replace it with the actual name the assumption has in the player's proof state. +* `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag. +* `CaptionShort`: One catch phrase. Appears above the image. +* `CaptionLong`: 2-4 sentences to describe the game. +* `Prerequisites` a list of other games you should play before this one, e.g. `Prerequisites "NNG" "STG"`. The game names are free-text. +* `CoverImage`: You can create a folder `images/` and put images there for the game to use. The maximal ratio is ca. 500x200 (W x H) but it might be cropped horizontally on narrow screens. ## Further Notes diff --git a/doc/hints.md b/doc/hints.md new file mode 100644 index 0000000..f980695 --- /dev/null +++ b/doc/hints.md @@ -0,0 +1,87 @@ +# Hints + +Most important for game development are probably the "Hints". You can add Hints at any place in your proof using the `Hint` tactic + +``` +Statement .... := by + Hint "Hint to show at the start" + rw [h] + Hint "some tip after using rw" + ... +``` + +## 1. When do hints show? + +A hint will be displayed if the player's goal matches the one where the hint was placed in the +sample solutions and the entire context from the sample solutions is present in the +player's context. The player's context may contain additional items. + +This means if you have multiple identical +subgoals, you should only place a single hint in one of them and it will be displayed in +all of them. + +However, identical (non-hidden) hints which where already present in the step +before are omitted. This is to allow a player to add new assumptions to context, for example +with `have`, without seeing the same hint over and over again. +Hidden hints are not filtered. + +## 2. Alternative Proofs / `Branch` + +You can use `Branch` to place hints +in dead ends or alternative proof strands. + +A proof inside a `Branch`-block is normally evaluated by lean but it's discarded at the end +so that no progress has been made on proofing the goal. + +``` +Statement .... := by + Hint "Huse `rw` or `rewrite`." + Branch + rewrite [h] + Hint "now you still need `rfl`" + rw [h] +``` + +## 3. Variables names + +Put variables in the hint text inside brackets like this: `{h}`! This way the server can replace +the variable's name with the one the user actually used. + +For example, if the sample proof contains + +``` +have h : True := trivial +Hint "Now use `rw [{h}]` to use your assumption `{h}`." +``` + +but the player writes `have g : True := trivial`, they will see a hint saying +"Now use `rw [g]` to use your assumption `g`." + +## 4. Hidden hints + +Some hints can be hidden, and only show after the user clicks on a button to get additional +help. You mark a hint as hidden with `(hidden := true)`: + +``` +Hint (hidden := true) "some hidden hint" +``` + +## 5. Strict context matching + +If you use the attribute `(strict := true)` a hint is only shown if the entire context +matches exactly the one where the hint is placed. With `(hint := false)`, which is the default, +it does not matter if additional assumptions are present in the player's context. + +``` +Hint (strict := true) "now use `have` to create a new assumption." +``` + +You should probably use `(strict := true)` if you want to give fine-grained details about +tactics like `have` which do not modify the goal or any existing assumptions, but only +create new assumptions. + +## 6. Formatting + +You can add use markdown to format your hints, for example you can use KaTex: `$\\iff$` + +TODO: Write a doc about latex/markdown options available. diff --git a/doc/publish_game.md b/doc/publish_game.md new file mode 100644 index 0000000..1afd3d9 --- /dev/null +++ b/doc/publish_game.md @@ -0,0 +1,32 @@ +# Publishing games + +You can publish your game on the official (Lean Game Server)[https://adam.math.hhu.de] in a few simple +steps. + +## 1. Upload Game to github + +First, you need your game in a public Github repository and make sure the github action has run. +You can check this by spotting the green checkmark on the start page, or by looking at the "Actions" +tab. + +## 2. Import the game + +You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call +the URL of the form + +> adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY} + +where `{USER}` and `{REPOSITORY}` are replaced with the github user and repository name. + +You should see a white screen which shows import updates and eventually reports "Done." + +## 3. Play the game + +Now you can immediately play the game at `adam.math.hhu.de/#/g/{USER}/{REPOSITORY}`! + +## 4. Main page + +Adding games to the main page happens manually by the server maintainers. Tell us if you want us +to add a tile for your game! + +For example, you can [contact Jon on Zulip](https://leanprover.zulipchat.com/#narrow/dm/385895-Jon-Eugster). Or [via Email](https://www.math.hhu.de/en/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster). diff --git a/doc/running_locally.md b/doc/running_locally.md index 44a23d9..5ab890f 100644 --- a/doc/running_locally.md +++ b/doc/running_locally.md @@ -4,13 +4,15 @@ The installation instructions are not yet tested on Mac/Windows. Comments very w There are several options to play a game locally: -- VSCode Dev Container: needs `docker` installed on your machine -- Codespaces: Needs active internet connection and computing time is limited. -- Gitpod: does not work yet (I that true?) -- Manual installation: Needs `npm` installed on your system +1. VSCode Dev Container: needs `docker` installed on your machine +2. Codespaces: Needs active internet connection and computing time is limited. +3. Gitpod: does not work yet (Is that true?) +4. Manual installation: Needs `npm` installed on your system The recommended option is "VSCode Dev containers" but you may choose any option above depending on your setup. +The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) contains all the relevant files to make your local setup (dev container / gitpod / codespaces) work. You might need to update these files manually by copying them from there if you need any new improvements to the dev setup you're using in an existing game. + ## VSCode Dev Containers 1. **Install Docker and Dev Containers** *(once)*:
@@ -27,9 +29,9 @@ The recommended option is "VSCode Dev containers" but you may choose any option Once you have the Dev Containers Extension installed, (re)open the project folder of your game in VSCode. A message appears asking you to "Reopen in Container". - * The first start will take a while, ca. 2-10 minutes. After the first + * The first start will take a while, ca. 2-15 minutes. After the first start this should be very quickly. - * Once built, you can open http://localhost:3000 in your browser. which should load the game + * Once built, you can open http://localhost:3000 in your browser. which should load the game. 3. **Editing Files** *(everytime)*:
After editing some Lean files in VSCode, open VSCode's terminal (View > Terminal) and run `lake build`. Now you can reload your browser to see the changes. @@ -42,12 +44,13 @@ The recommended option is "VSCode Dev containers" but you may choose any option you might have deleted stuff from docker via your shell. Try deleting the container and image explicitely in VSCode (left side, "Docker" icon). Then reopen vscode and let it rebuild the container. (this will again take some time) +* On a working dev container setup, http://localhost:3000 should directly redirect you to http://localhost:3000/#/g/local/game, try if the latter is accessible. ## Codespaces You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). It it should run the game locally in the background. You can open it for example under "Ports" and clicking on "Open in Browser". -Note: You have to wait until npm started properly. In particular, this is after a message like `[client] webpack 5.81.0 compiled successfully in 38119 ms` appears in the terminal, which might take a good while. +Note: You have to wait until npm started properly, which might take a good while. As with devcontainers, you need to run `lake build` after changing any lean files and then reload the browser. @@ -73,27 +76,26 @@ Now install node: nvm install node ``` -Clone the game (e.g. `NNG4` here): +Clone the game (e.g. `GameSkeleton` here): ```bash -git clone https://github.com/hhu-adam/NNG4.git -# or: git clone git@github.com:hhu-adam/NNG4.git +git clone https://github.com/hhu-adam/GameSkeleton.git +# or: git clone git@github.com:hhu-adam/GameSkeleton.git ``` Download dependencies and build the game: ```bash -cd NNG4 -lake update -lake exe cache get # if your game depends on mathlib +cd GameSkeleton +lake update -R lake build ``` -Clone the game repository into a directory next to the game: +Clone the server repository into a directory next to the game: ```bash cd .. git clone https://github.com/leanprover-community/lean4game.git # or: git clone git@github.com:leanprover-community/lean4game.git ``` -The folders `NNG4` and `lean4game` must be in the same directory! +The folders `GameSkeleton` and `lean4game` must be in the same directory! In `lean4game`, install dependencies: ```bash @@ -106,16 +108,16 @@ Run the game: npm start ``` -This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/NNG4. Replace `NNG4` with the folder name of your local game. +This takes a little time. Eventually, the game is available on http://localhost:3000/#/g/local/GameSkeleton. Replace `GameSkeleton` with the folder name of your local game. ## Modifying the GameServer -When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by setting `export NODE_ENV=development` inside your local game before building it: +When modifying the game engine itself (in particular the content in `lean4game/server`) you can test it live with the same setup as above (manual installation) by using `lake update -R -Klean4game.local`: ```bash cd NNG4 -export NODE_ENV=development -lake update +lake update -R -Klean4game.local lake build ``` -This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, when you `lake build` your game, it will rebuild with the modified `GameServer`. +This causes lake to search locally for the `GameServer` lake package instead of using the version from github. Therefore, you can the local copy of the edit `GameServer` in `../lean4game` and +`lake build` will then directly use this modified copy to build your game. diff --git a/doc/server.md b/doc/server.md new file mode 100644 index 0000000..41698a0 --- /dev/null +++ b/doc/server.md @@ -0,0 +1,28 @@ + +# Notes for Server maintainer + +In order to set up the server to allow imports, one needs to create a +[Github Access token](https://docs.github.com/en/authentication/keeping-your-account-and-data-secure/managing-your-personal-access-tokens). A fine-grained access token with only reading rights for public +repos will suffice. + +You need to set the environment variables `LEAN4GAME_GITHUB_USER` and `LEAN4GAME_GITHUB_TOKEN` +with your user name and access token. For example, you can seet these in `ecosystem.config.cjs` if +you're using `pm2` + +Then people can call: + +> https://{website}/import/trigger/{owner}/{repo} + +where you replace: +- website: The website your server runs on, e.g. `localhost:3000` +- owner, repo: The owner and repository name of the game you want to load from github. + + will trigger to download the latest version of your game from github onto your server. + Once this import reports "Done", you should be able to play your game under: + +> https://{website}/#/g/{owner}/{repo} + +## data management +Everything downloaded remains in the folder `lean4game/games`. +the subfolder `tmp` contains downloaded artifacts and can be deleted without loss. +The other folders should only contain the built lean-games, sorted by owner and repo. diff --git a/doc/update_game.md b/doc/update_game.md new file mode 100644 index 0000000..ff4113d --- /dev/null +++ b/doc/update_game.md @@ -0,0 +1,52 @@ +# How to update your Game + +## New Lean version + +You can update the game to any Lean version by simply editing the `lean-toolchain` in your game repo to contain the +new lean version `leanprover/lean4:v4.X.0`. + +Before you continue, make sure there [exists a `v4.X.0`-tag in this repo](https://github.com/leanprover-community/lean4game/tags). + +Then, depending on the setup you use, do one of the following: + +* Dev Container: Rebuild the VSCode Devcontainer. +* Local Setup: in your game's folder run the following: + ``` + lake update -R + lake build + ``` + + * Additionally, if you have a local copy of the server `lean4game`, + you should update this one to the matching version. Run the following in the folder `lean4game/`: + ``` + git fetch + git checkout {VERSION_TAG} + npm install + ``` + where `{VERSION_TAG}` is the tag from above of the form `v4.X.0` +* Gitpod/Codespaces: Create a fresh one + +This will update your game (and the mathlib version you might be using) to the new lean version. + +## Newest developing setup + +There are a few files in your game repository which are used for the developing setup +(dev container/codespaces/gitpod). If you need to update your developing setup, for example because it doesn't work +anymore, you will need to copy the relevant files from the [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) template into your game repo. + +The relevant files are: + +``` +.devcontainer/ +.docker/ +.github/ +.gitpod/ +.vscode/ +lakefile.lean +``` + +simply copy them from the `GameSkeleton` into your game and proceed as above, +i.e. `lake update -R && lake build`. + +(Note: You should not need to modify any of these files, with the exception of the `lakefile.lean`, +where you need to add any dependencies of your game, or remove mathlib if you don't need it.) diff --git a/ecosystem.config.js b/ecosystem.config.cjs similarity index 52% rename from ecosystem.config.js rename to ecosystem.config.cjs index 20e44ee..e24dbd5 100644 --- a/ecosystem.config.js +++ b/ecosystem.config.cjs @@ -2,10 +2,12 @@ module.exports = { apps : [{ name : "lean4game", - script : "server/index.mjs", + script : "relay/index.mjs", env: { - NODE_ENV: "production", - PORT: 8002 + LEAN4GAME_GITHUB_USER: "", + LEAN4GAME_GITHUB_TOKEN: "", + NODE_ENV: "production", + PORT: 8002 }, }] } diff --git a/package-lock.json b/package-lock.json index 760e0f2..65f056c 100644 --- a/package-lock.json +++ b/package-lock.json @@ -40,6 +40,7 @@ "rehype-katex": "^6.0.2", "remark-gfm": "^3.0.1", "remark-math": "^5.1.1", + "request": "^2.88.2", "request-progress": "^3.0.0", "vite": "^4.5.0", "vite-plugin-static-copy": "^0.17.0", @@ -56,7 +57,7 @@ "concurrently": "^7.6.0", "css-loader": "^6.7.3", "file-loader": "^6.2.0", - "nodemon": "^2.0.20", + "nodemon": "^3.0.1", "react-refresh": "^0.14.0", "style-loader": "^3.3.1", "ts-loader": "^9.4.2", @@ -6014,7 +6015,6 @@ "version": "6.12.6", "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.6.tgz", "integrity": "sha512-j3fVLgvTo527anyYyJOGTYJbG+vnnQYvE0m5mmkc1TK+nxAppkCLMIL0aZ4dblVCNoGShhm+kzE4ZUykBoMg4g==", - "dev": true, "dependencies": { "fast-deep-equal": "^3.1.1", "fast-json-stable-stringify": "^2.0.0", @@ -6183,6 +6183,22 @@ "resolved": "https://registry.npmjs.org/asap/-/asap-2.0.6.tgz", "integrity": "sha512-BSHWgDSAiKs50o2Re8ppvp3seVHXSRM44cdSsT9FfNEUUZLOGWVCsiWaRPWM1Znn+mqZ1OfVZ3z3DWEzSp7hRA==" }, + "node_modules/asn1": { + "version": "0.2.6", + "resolved": "https://registry.npmjs.org/asn1/-/asn1-0.2.6.tgz", + "integrity": "sha512-ix/FxPn0MDjeyJ7i/yoHGFt/EX6LyNbxSEhPPXODPL+KB0VPk86UYfL0lMdy+KCnv+fmvIzySwaK5COwqVbWTQ==", + "dependencies": { + "safer-buffer": "~2.1.0" + } + }, + "node_modules/assert-plus": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/assert-plus/-/assert-plus-1.0.0.tgz", + "integrity": "sha512-NfJ4UzBCcQGLDlQq7nHxH+tv3kyZ0hHQqF5BO6J7tNJeP5do1llPr8dZ8zHonfhAu0PHAdMkSo+8o0wxg9lZWw==", + "engines": { + "node": ">=0.8" + } + }, "node_modules/ast-types": { "version": "0.15.2", "resolved": "https://registry.npmjs.org/ast-types/-/ast-types-0.15.2.tgz", @@ -6212,6 +6228,11 @@ "resolved": "https://registry.npmjs.org/async-limiter/-/async-limiter-1.0.1.tgz", "integrity": "sha512-csOlWGAcRFJaI6m+F2WKdnMKr4HhdhFVBk0H/QbJFMCr+uO2kwohwXQPxw/9OCxp05r5ghVBFSyioixx3gfkNQ==" }, + "node_modules/asynckit": { + "version": "0.4.0", + "resolved": "https://registry.npmjs.org/asynckit/-/asynckit-0.4.0.tgz", + "integrity": "sha512-Oei9OH4tRh0YqU3GxhX79dM/mwVgvbZJaSNaRk+bshkj0S5cfHcgYakreBjrHwatXKbz+IoIdYLxrKim2MjW0Q==" + }, "node_modules/available-typed-arrays": { "version": "1.0.5", "resolved": "https://registry.npmjs.org/available-typed-arrays/-/available-typed-arrays-1.0.5.tgz", @@ -6224,12 +6245,40 @@ "url": "https://github.com/sponsors/ljharb" } }, + "node_modules/aws-sign2": { + "version": "0.7.0", + "resolved": "https://registry.npmjs.org/aws-sign2/-/aws-sign2-0.7.0.tgz", + "integrity": "sha512-08kcGqnYf/YmjoRhfxyu+CLxBjUtHLXLXX/vUfx9l2LYzG3c1m61nrpyFUZI6zeS+Li/wWMMidD9KgrqtGq3mA==", + "engines": { + "node": "*" + } + }, + "node_modules/aws4": { + "version": "1.12.0", + "resolved": "https://registry.npmjs.org/aws4/-/aws4-1.12.0.tgz", + "integrity": "sha512-NmWvPnx0F1SfrQbYwOi7OeaNGokp9XhzNioJ/CSBs8Qa4vxug81mhJEAVZwxXuBmYB5KDRfMq/F3RR0BIU7sWg==" + }, "node_modules/axios": { - "version": "0.24.0", - "resolved": "https://registry.npmjs.org/axios/-/axios-0.24.0.tgz", - "integrity": "sha512-Q6cWsys88HoPgAaFAVUb0WpPk0O8iTeisR9IMqy9G8AbO4NlpVknrnQS03zzF9PGAWgO3cgletO3VjV/P7VztA==", + "version": "1.6.2", + "resolved": "https://registry.npmjs.org/axios/-/axios-1.6.2.tgz", + "integrity": "sha512-7i24Ri4pmDRfJTR7LDBhsOTtcm+9kjX5WiY1X3wIisx6G9So3pfMkEiU7emUBe46oceVImccTEM3k6C5dbVW8A==", "dependencies": { - "follow-redirects": "^1.14.4" + "follow-redirects": "^1.15.0", + "form-data": "^4.0.0", + "proxy-from-env": "^1.1.0" + } + }, + "node_modules/axios/node_modules/form-data": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/form-data/-/form-data-4.0.0.tgz", + "integrity": "sha512-ETEklSGi5t0QMZuiXoA/Q6vcnxcLQP5vdugSpuAyi6SVGi2clPPp+xgEhuMaHC+zGgn31Kd235W35f7Hykkaww==", + "dependencies": { + "asynckit": "^0.4.0", + "combined-stream": "^1.0.8", + "mime-types": "^2.1.12" + }, + "engines": { + "node": ">= 6" } }, "node_modules/babel-core": { @@ -6381,6 +6430,14 @@ "optional": true, "peer": true }, + "node_modules/bcrypt-pbkdf": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/bcrypt-pbkdf/-/bcrypt-pbkdf-1.0.2.tgz", + "integrity": "sha512-qeFIXtP4MSoi6NLqO12WfqARWWuCKi2Rn/9hJLEmtB5yTNr9DqFWkJRCf2qShWzPeAMRnOgCrq0sg/KLv5ES9w==", + "dependencies": { + "tweetnacl": "^0.14.3" + } + }, "node_modules/before-after-hook": { "version": "2.2.3", "resolved": "https://registry.npmjs.org/before-after-hook/-/before-after-hook-2.2.3.tgz", @@ -6671,6 +6728,11 @@ } ] }, + "node_modules/caseless": { + "version": "0.12.0", + "resolved": "https://registry.npmjs.org/caseless/-/caseless-0.12.0.tgz", + "integrity": "sha512-4tYFyifaFfGacoiObjJegolkwSU4xQNGbVgUiNYVUxbQ2x2lUsFvY4hVgVzGiIe6WLOPqycWXA40l+PWsxthUw==" + }, "node_modules/ccount": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/ccount/-/ccount-2.0.1.tgz", @@ -6908,6 +6970,17 @@ "resolved": "https://registry.npmjs.org/colorette/-/colorette-1.4.0.tgz", "integrity": "sha512-Y2oEozpomLn7Q3HFP7dpww7AtMJplbM9lGZP6RDfHqmbeRjiwRg4n6VM6j4KLmRke85uWEI7JqF17f3pqdRA0g==" }, + "node_modules/combined-stream": { + "version": "1.0.8", + "resolved": "https://registry.npmjs.org/combined-stream/-/combined-stream-1.0.8.tgz", + "integrity": "sha512-FQN4MRfuJeHf7cBbBMJFXhKSDq+2kAArBlmRBvcvFE5BB1HZKXtSFASDhdlz9zOYwxh8lDdnvmMOe/+5cdoEdg==", + "dependencies": { + "delayed-stream": "~1.0.0" + }, + "engines": { + "node": ">= 0.8" + } + }, "node_modules/comma-separated-tokens": { "version": "2.0.3", "resolved": "https://registry.npmjs.org/comma-separated-tokens/-/comma-separated-tokens-2.0.3.tgz", @@ -7424,6 +7497,17 @@ "cytoscape": "^3.2.0" } }, + "node_modules/dashdash": { + "version": "1.14.1", + "resolved": "https://registry.npmjs.org/dashdash/-/dashdash-1.14.1.tgz", + "integrity": "sha512-jRFi8UDGo6j+odZiEpjazZaWqEal3w/basFjQHQEwVtZJGDpxbH1MeYluwCS8Xq5wmLJooDlMgvVarmWfGM44g==", + "dependencies": { + "assert-plus": "^1.0.0" + }, + "engines": { + "node": ">=0.10" + } + }, "node_modules/date-fns": { "version": "2.30.0", "resolved": "https://registry.npmjs.org/date-fns/-/date-fns-2.30.0.tgz", @@ -7590,6 +7674,14 @@ "url": "https://github.com/sponsors/ljharb" } }, + "node_modules/delayed-stream": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/delayed-stream/-/delayed-stream-1.0.0.tgz", + "integrity": "sha512-ZySD7Nf91aLB0RxL4KGrKHBXl7Eds1DAmEdcoVawXnLD7SDhpNgtuII2aAkg7a7QS41jxPSZ17p4VdGnMHk3MQ==", + "engines": { + "node": ">=0.4.0" + } + }, "node_modules/denodeify": { "version": "1.2.1", "resolved": "https://registry.npmjs.org/denodeify/-/denodeify-1.2.1.tgz", @@ -7748,6 +7840,15 @@ "tslib": "^2.0.3" } }, + "node_modules/ecc-jsbn": { + "version": "0.1.2", + "resolved": "https://registry.npmjs.org/ecc-jsbn/-/ecc-jsbn-0.1.2.tgz", + "integrity": "sha512-eh9O+hwRHNbG4BLTjEl3nw044CkGm5X6LoaCf7LPp7UU8Qrt47JYNi6nPX8xjW97TKGKm1ouctg0QSpZe9qrnw==", + "dependencies": { + "jsbn": "~0.1.0", + "safer-buffer": "^2.1.0" + } + }, "node_modules/ecdsa-sig-formatter": { "version": "1.0.11", "resolved": "https://registry.npmjs.org/ecdsa-sig-formatter/-/ecdsa-sig-formatter-1.0.11.tgz", @@ -8136,11 +8237,18 @@ "resolved": "https://registry.npmjs.org/extend/-/extend-3.0.2.tgz", "integrity": "sha512-fjquC59cD7CyW6urNXK0FBufkZcoiGG80wTuPujX590cB5Ttln20E2UB4S/WARVqhXffZl2LNgS+gQdPIIim/g==" }, + "node_modules/extsprintf": { + "version": "1.3.0", + "resolved": "https://registry.npmjs.org/extsprintf/-/extsprintf-1.3.0.tgz", + "integrity": "sha512-11Ndz7Nv+mvAC1j0ktTa7fAb0vLyGGX+rMHNBYQviQDGU0Hw7lhctJANqbPhu9nV9/izT/IntTgZ7Im/9LJs9g==", + "engines": [ + "node >=0.6.0" + ] + }, "node_modules/fast-deep-equal": { "version": "3.1.3", "resolved": "https://registry.npmjs.org/fast-deep-equal/-/fast-deep-equal-3.1.3.tgz", - "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q==", - "dev": true + "integrity": "sha512-f3qQ9oQy9j2AhBe/H9VC91wLmKBCCU/gDOnKNAYG5hswO7BLKj09Hc5HYNz9cGI++xlpDCIgDaitVs03ATR84Q==" }, "node_modules/fast-glob": { "version": "3.3.1", @@ -8160,8 +8268,7 @@ "node_modules/fast-json-stable-stringify": { "version": "2.1.0", "resolved": "https://registry.npmjs.org/fast-json-stable-stringify/-/fast-json-stable-stringify-2.1.0.tgz", - "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw==", - "dev": true + "integrity": "sha512-lhd/wF+Lk98HZoTCtlVraHtfh5XYijIjalXck7saUtuanSDyLMxnHhSXEDJqHxD7msR8D0uCmqlkwjCV8xvwHw==" }, "node_modules/fast-plist": { "version": "0.1.3", @@ -8346,6 +8453,27 @@ "is-callable": "^1.1.3" } }, + "node_modules/forever-agent": { + "version": "0.6.1", + "resolved": "https://registry.npmjs.org/forever-agent/-/forever-agent-0.6.1.tgz", + "integrity": "sha512-j0KLYPhm6zeac4lz3oJ3o65qvgQCcPubiyotZrXqEaG4hNagNYO8qdlUrX5vwqv9ohqeT/Z3j6+yW067yWWdUw==", + "engines": { + "node": "*" + } + }, + "node_modules/form-data": { + "version": "2.3.3", + "resolved": "https://registry.npmjs.org/form-data/-/form-data-2.3.3.tgz", + "integrity": "sha512-1lLKB2Mu3aGP1Q/2eCOx0fNbRMe7XdwktwOruhfqqd0rIJWwN4Dh+E3hrPSlDCXnSR7UtZ1N38rVXm+6+MEhJQ==", + "dependencies": { + "asynckit": "^0.4.0", + "combined-stream": "^1.0.6", + "mime-types": "^2.1.12" + }, + "engines": { + "node": ">= 0.12" + } + }, "node_modules/forwarded": { "version": "0.2.0", "resolved": "https://registry.npmjs.org/forwarded/-/forwarded-0.2.0.tgz", @@ -8475,6 +8603,14 @@ "url": "https://github.com/sponsors/sindresorhus" } }, + "node_modules/getpass": { + "version": "0.1.7", + "resolved": "https://registry.npmjs.org/getpass/-/getpass-0.1.7.tgz", + "integrity": "sha512-0fzj9JxOLfJ+XGLhR8ze3unN0KZCgZwiSSDz168VERjK8Wl8kVSdcu2kspd4s4wtAa1y/qrVRiAA0WclVsu0ng==", + "dependencies": { + "assert-plus": "^1.0.0" + } + }, "node_modules/glob": { "version": "7.2.3", "resolved": "https://registry.npmjs.org/glob/-/glob-7.2.3.tgz", @@ -8545,6 +8681,27 @@ "optional": true, "peer": true }, + "node_modules/har-schema": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/har-schema/-/har-schema-2.0.0.tgz", + "integrity": "sha512-Oqluz6zhGX8cyRaTQlFMPw80bSJVG2x/cFb8ZPhUILGgHka9SsokCCOQgpveePerqidZOrT14ipqfJb7ILcW5Q==", + "engines": { + "node": ">=4" + } + }, + "node_modules/har-validator": { + "version": "5.1.5", + "resolved": "https://registry.npmjs.org/har-validator/-/har-validator-5.1.5.tgz", + "integrity": "sha512-nmT2T0lljbxdQZfspsno9hgrG3Uir6Ks5afism62poxqBM6sDnMEuPmzTq8XN0OEwqKLLdh1jQI3qyE66Nzb3w==", + "deprecated": "this library is no longer supported", + "dependencies": { + "ajv": "^6.12.3", + "har-schema": "^2.0.0" + }, + "engines": { + "node": ">=6" + } + }, "node_modules/has": { "version": "1.0.4", "resolved": "https://registry.npmjs.org/has/-/has-1.0.4.tgz", @@ -8975,6 +9132,20 @@ "url": "https://github.com/sponsors/sindresorhus" } }, + "node_modules/http-signature": { + "version": "1.2.0", + "resolved": "https://registry.npmjs.org/http-signature/-/http-signature-1.2.0.tgz", + "integrity": "sha512-CAbnr6Rz4CYQkLYUtSNXxQPUH2gK8f3iWexVlsnMeD+GjlsQ0Xsy1cOX+mN3dtxYomRy21CiOzU8Uhw6OwncEQ==", + "dependencies": { + "assert-plus": "^1.0.0", + "jsprim": "^1.2.2", + "sshpk": "^1.7.0" + }, + "engines": { + "node": ">=0.8", + "npm": ">=1.3.7" + } + }, "node_modules/human-signals": { "version": "2.1.0", "resolved": "https://registry.npmjs.org/human-signals/-/human-signals-2.1.0.tgz", @@ -9482,6 +9653,11 @@ "url": "https://github.com/sponsors/ljharb" } }, + "node_modules/is-typedarray": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/is-typedarray/-/is-typedarray-1.0.0.tgz", + "integrity": "sha512-cyA56iCMHAh5CdzjJIa4aohJyeO1YbwLi3Jc35MmRU6poroFjIGZzUzupGiRPOjgHg9TLu43xbpwXk523fMxKA==" + }, "node_modules/is-unicode-supported": { "version": "0.1.0", "resolved": "https://registry.npmjs.org/is-unicode-supported/-/is-unicode-supported-0.1.0.tgz", @@ -9542,6 +9718,11 @@ "node": ">=0.10.0" } }, + "node_modules/isstream": { + "version": "0.1.2", + "resolved": "https://registry.npmjs.org/isstream/-/isstream-0.1.2.tgz", + "integrity": "sha512-Yljz7ffyPbrLpLngrMtZ7NduUgVvi6wG9RJ9IUcyCd59YQ911PBJphODUcbOVbqYfxe1wuYf/LJ8PauMRwsM/g==" + }, "node_modules/jest-environment-node": { "version": "29.7.0", "resolved": "https://registry.npmjs.org/jest-environment-node/-/jest-environment-node-29.7.0.tgz", @@ -9950,6 +10131,11 @@ "js-yaml": "bin/js-yaml.js" } }, + "node_modules/jsbn": { + "version": "0.1.1", + "resolved": "https://registry.npmjs.org/jsbn/-/jsbn-0.1.1.tgz", + "integrity": "sha512-UVU9dibq2JcFWxQPA6KCqj5O42VOmAY3zQUfEKxU0KpTGXwNoCjkX1e13eHNvw/xPynt6pU0rZ1htjWTNTSXsg==" + }, "node_modules/jsc-android": { "version": "250231.0.0", "resolved": "https://registry.npmjs.org/jsc-android/-/jsc-android-250231.0.0.tgz", @@ -10077,11 +10263,20 @@ "resolved": "https://registry.npmjs.org/json-parse-even-better-errors/-/json-parse-even-better-errors-2.3.1.tgz", "integrity": "sha512-xyFwyhro/JEof6Ghe2iz2NcXoj2sloNsWr/XsERDK/oiPCfaNhl5ONfp+jQdAZRQQ0IJWNzH9zIZF7li91kh2w==" }, + "node_modules/json-schema": { + "version": "0.4.0", + "resolved": "https://registry.npmjs.org/json-schema/-/json-schema-0.4.0.tgz", + "integrity": "sha512-es94M3nTIfsEPisRafak+HDLfHXnKBhV3vU5eqPcS3flIWqcxJWgXHXiey3YrpaNsanY5ei1VoYEbOzijuq9BA==" + }, "node_modules/json-schema-traverse": { "version": "0.4.1", "resolved": "https://registry.npmjs.org/json-schema-traverse/-/json-schema-traverse-0.4.1.tgz", - "integrity": "sha512-xbbCH5dCYU5T8LcEhhuh7HJ88HXuW3qsI3Y0zOZFKfZEHcpWiHU/Jxzk629Brsab/mMiHQti9wMP+845RPe3Vg==", - "dev": true + "integrity": "sha512-xbbCH5dCYU5T8LcEhhuh7HJ88HXuW3qsI3Y0zOZFKfZEHcpWiHU/Jxzk629Brsab/mMiHQti9wMP+845RPe3Vg==" + }, + "node_modules/json-stringify-safe": { + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/json-stringify-safe/-/json-stringify-safe-5.0.1.tgz", + "integrity": "sha512-ZClg6AaYvamvYEE82d3Iyd3vSSIjQ+odgjaTzRuO3s7toCdFKczob2i0zCh7JE8kWn17yvAWhUVxvqGwUalsRA==" }, "node_modules/json5": { "version": "2.2.3", @@ -10153,6 +10348,20 @@ "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz", "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==" }, + "node_modules/jsprim": { + "version": "1.4.2", + "resolved": "https://registry.npmjs.org/jsprim/-/jsprim-1.4.2.tgz", + "integrity": "sha512-P2bSOMAc/ciLz6DzgjVlGJP9+BrJWu5UDGK70C2iweC5QBIeFf0ZXRvGjEj2uYgrY2MkAAhsSWHDWlFtEroZWw==", + "dependencies": { + "assert-plus": "1.0.0", + "extsprintf": "1.3.0", + "json-schema": "0.4.0", + "verror": "1.10.0" + }, + "engines": { + "node": ">=0.6.0" + } + }, "node_modules/jwa": { "version": "1.4.1", "resolved": "https://registry.npmjs.org/jwa/-/jwa-1.4.1.tgz", @@ -10229,22 +10438,22 @@ } }, "node_modules/lean4": { - "version": "0.0.99", - "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?79d345c739bf707024eef5057ccef81b404a2ddf", - "integrity": "sha512-jgl4gGQXvP+RhdAr9r0+K6I5SpPkad++zAql9BawHI7OE7vMwK+7GbYXoa5aAP8T1BSIZQ+y3w0cl8FCk5C++A==", + "version": "0.0.119", + "resolved": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985", + "integrity": "sha512-hA7bb0EFlNwtk7+/7gO5OZS7HtrhmoRacE/b2etFBYG4FbkZd/NKTcs5PHGcKsYXeVghkOOZjw0uhNWaeW3gvw==", "license": "Apache-2.0", "dependencies": { - "@leanprover/infoview": "~0.3.0", - "@leanprover/infoview-api": "~0.2.0", - "axios": "~0.24.0", + "@leanprover/infoview": "~0.4.3", + "@leanprover/infoview-api": "~0.2.1", + "axios": "^1.6.2", "cheerio": "^1.0.0-rc.10", - "es-module-shims": "^1.6.2", "mobx": "5.15.7", - "semver": "=7.3.5", - "vscode-languageclient": "=8.0.2" + "semver": "^7.5.4", + "vscode-languageclient": "=8.0.2", + "zod": "^3.22.4" }, "engines": { - "vscode": "^1.70.0" + "vscode": "^1.75.0" } }, "node_modules/lean4-infoview": { @@ -10263,19 +10472,6 @@ "vscode-languageserver-protocol": "^3.17.2" } }, - "node_modules/lean4/node_modules/@leanprover/infoview": { - "version": "0.3.0", - "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.3.0.tgz", - "integrity": "sha512-wVMd9Qc6AC8Ub4cfkENcyCqs342lqwS+4C1SpX+3z0RETxL+TxTFPdM8bYoLgtAg/eApdHhV1TDLSrBNkTWi5g==", - "dependencies": { - "@leanprover/infoview-api": "~0.2.0", - "@vscode/codicons": "^0.0.32", - "marked": "^4.2.2", - "react-fast-compare": "^3.2.0", - "tachyons": "^4.12.0", - "vscode-languageserver-protocol": "^3.17.2" - } - }, "node_modules/lean4/node_modules/lru-cache": { "version": "6.0.0", "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz", @@ -10297,9 +10493,9 @@ } }, "node_modules/lean4/node_modules/semver": { - "version": "7.3.5", - "resolved": "https://registry.npmjs.org/semver/-/semver-7.3.5.tgz", - "integrity": "sha512-PoeGJYh8HK4BTO/a9Tf6ZG3veo/A7ZVsYrSA6J8ny9nb3B1VrpkuN+z9OE5wfE5p6H4LchYZsegiQgbJD94ZFQ==", + "version": "7.5.4", + "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz", + "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==", "dependencies": { "lru-cache": "^6.0.0" }, @@ -10317,7 +10513,7 @@ }, "node_modules/lean4web": { "version": "0.1.0", - "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#b02044f3a3b9130b663c3619ce56c603fa3a4cf4", + "resolved": "git+ssh://git@github.com/hhu-adam/lean4web.git#6fc9c11179934cce7ca1f78140c57b6931186b42", "dependencies": { "@emotion/react": "^11.11.1", "@emotion/styled": "^11.11.0", @@ -10326,12 +10522,13 @@ "@fortawesome/fontawesome-svg-core": "^6.2.0", "@fortawesome/free-solid-svg-icons": "^6.2.0", "@fortawesome/react-fontawesome": "^0.2.0", - "@leanprover/infoview": "^0.4.1", + "@leanprover/infoview": "^0.4.3", "@mui/material": "^5.13.7", + "@vitejs/plugin-react-swc": "^3.4.0", "express": "^4.18.2", "file-saver": "^2.0.5", "ip-anonymize": "^0.1.0", - "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?79d345c739bf707024eef5057ccef81b404a2ddf", + "lean4": "https://gitpkg.now.sh/leanprover/vscode-lean4/vscode-lean4?8d0cc34dcfa00da8b4a48394ba1fb3a600e3f985", "mobx": "^6.6.2", "moment-timezone": "^0.5.39", "monaco-editor": "^0.34.1", @@ -10346,6 +10543,7 @@ "react-popper": "^2.3.0", "react-split": "^2.0.14", "stream-http": "^3.2.0", + "vite": "^4.5.0", "vscode-ws-jsonrpc": "^2.0.0", "ws": "^8.9.0" } @@ -12611,9 +12809,9 @@ } }, "node_modules/nodemon": { - "version": "2.0.22", - "resolved": "https://registry.npmjs.org/nodemon/-/nodemon-2.0.22.tgz", - "integrity": "sha512-B8YqaKMmyuCO7BowF1Z1/mkPqLk6cs/l63Ojtd6otKjMx47Dq1utxfRxcavH1I7VSaL8n5BUaoutadnsX3AAVQ==", + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/nodemon/-/nodemon-3.0.1.tgz", + "integrity": "sha512-g9AZ7HmkhQkqXkRc20w+ZfQ73cHLbE8hnPbtaFbFtCumZsjyMhKk9LajQ07U5Ux28lvFjZ5X7HvWR1xzU8jHVw==", "dev": true, "dependencies": { "chokidar": "^3.5.2", @@ -12621,8 +12819,8 @@ "ignore-by-default": "^1.0.1", "minimatch": "^3.1.2", "pstree.remy": "^1.1.8", - "semver": "^5.7.1", - "simple-update-notifier": "^1.0.7", + "semver": "^7.5.3", + "simple-update-notifier": "^2.0.0", "supports-color": "^5.5.0", "touch": "^3.1.0", "undefsafe": "^2.0.5" @@ -12631,7 +12829,7 @@ "nodemon": "bin/nodemon.js" }, "engines": { - "node": ">=8.10.0" + "node": ">=10" }, "funding": { "type": "opencollective", @@ -12647,15 +12845,39 @@ "ms": "^2.1.1" } }, + "node_modules/nodemon/node_modules/lru-cache": { + "version": "6.0.0", + "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz", + "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==", + "dev": true, + "dependencies": { + "yallist": "^4.0.0" + }, + "engines": { + "node": ">=10" + } + }, "node_modules/nodemon/node_modules/semver": { - "version": "5.7.2", - "resolved": "https://registry.npmjs.org/semver/-/semver-5.7.2.tgz", - "integrity": "sha512-cBznnQ9KjJqU67B52RMC65CMarK2600WFnbkcaiwWq3xy/5haFJlshgnpjovMVJ+Hff49d8GEn0b87C5pDQ10g==", + "version": "7.5.4", + "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz", + "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==", "dev": true, + "dependencies": { + "lru-cache": "^6.0.0" + }, "bin": { - "semver": "bin/semver" + "semver": "bin/semver.js" + }, + "engines": { + "node": ">=10" } }, + "node_modules/nodemon/node_modules/yallist": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz", + "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==", + "dev": true + }, "node_modules/nopt": { "version": "1.0.10", "resolved": "https://registry.npmjs.org/nopt/-/nopt-1.0.10.tgz", @@ -12706,6 +12928,14 @@ "resolved": "https://registry.npmjs.org/nullthrows/-/nullthrows-1.1.1.tgz", "integrity": "sha512-2vPPEi+Z7WqML2jZYddDIfy5Dqb0r2fze2zTxNNknZaFpVHU3mFB3R+DWeJWGVx0ecvttSGlJTI+WG+8Z4cDWw==" }, + "node_modules/oauth-sign": { + "version": "0.9.0", + "resolved": "https://registry.npmjs.org/oauth-sign/-/oauth-sign-0.9.0.tgz", + "integrity": "sha512-fexhUFFPTGV8ybAtSIGbV6gOkSv8UtRbDBnAyLQw4QPKkgNlsH2ByPGtMUqdWkos6YCRmAqViwgZrJc/mRDzZQ==", + "engines": { + "node": "*" + } + }, "node_modules/ob1": { "version": "0.76.8", "resolved": "https://registry.npmjs.org/ob1/-/ob1-0.76.8.tgz", @@ -13114,6 +13344,11 @@ "node": ">=8" } }, + "node_modules/performance-now": { + "version": "2.1.0", + "resolved": "https://registry.npmjs.org/performance-now/-/performance-now-2.1.0.tgz", + "integrity": "sha512-7EAHlyLHI56VEIdK57uwHdHKIaAGbnXPiw0yWbarQZOKaKpvUIgW0jWRVLiatnM+XXlSwsanIBH/hzGMJulMow==" + }, "node_modules/picocolors": { "version": "1.0.0", "resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.0.0.tgz", @@ -13344,6 +13579,16 @@ "node": ">= 0.10" } }, + "node_modules/proxy-from-env": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/proxy-from-env/-/proxy-from-env-1.1.0.tgz", + "integrity": "sha512-D+zkORCbA9f1tdWRK0RaCR3GPv50cMxcrz4X8k5LTSUD1Dkw47mKJEZQNunItRTkWwgtaUSo1RVFRIG9ZXiFYg==" + }, + "node_modules/psl": { + "version": "1.9.0", + "resolved": "https://registry.npmjs.org/psl/-/psl-1.9.0.tgz", + "integrity": "sha512-E/ZsdU4HLs/68gYzgGTkMicWTLPdAftJLfJFlLUAAKZGkStNU72sZjT66SnMDVOfOWY/YAoiD7Jxa9iHvngcag==" + }, "node_modules/pstree.remy": { "version": "1.1.8", "resolved": "https://registry.npmjs.org/pstree.remy/-/pstree.remy-1.1.8.tgz", @@ -13354,7 +13599,6 @@ "version": "2.3.0", "resolved": "https://registry.npmjs.org/punycode/-/punycode-2.3.0.tgz", "integrity": "sha512-rRV+zQD8tVFys26lAGR9WUuS4iUAngJScM+ZRSKtvl5tKeZ2t5bvdNFdNHBW9FWR4guGHlgmsZ1G7BSm2wTbuA==", - "dev": true, "engines": { "node": ">=6" } @@ -14066,6 +14310,37 @@ "url": "https://opencollective.com/unified" } }, + "node_modules/request": { + "version": "2.88.2", + "resolved": "https://registry.npmjs.org/request/-/request-2.88.2.tgz", + "integrity": "sha512-MsvtOrfG9ZcrOwAW+Qi+F6HbD0CWXEh9ou77uOb7FM2WPhwT7smM833PzanhJLsgXjN89Ir6V2PczXNnMpwKhw==", + "deprecated": "request has been deprecated, see https://github.com/request/request/issues/3142", + "dependencies": { + "aws-sign2": "~0.7.0", + "aws4": "^1.8.0", + "caseless": "~0.12.0", + "combined-stream": "~1.0.6", + "extend": "~3.0.2", + "forever-agent": "~0.6.1", + "form-data": "~2.3.2", + "har-validator": "~5.1.3", + "http-signature": "~1.2.0", + "is-typedarray": "~1.0.0", + "isstream": "~0.1.2", + "json-stringify-safe": "~5.0.1", + "mime-types": "~2.1.19", + "oauth-sign": "~0.9.0", + "performance-now": "^2.1.0", + "qs": "~6.5.2", + "safe-buffer": "^5.1.2", + "tough-cookie": "~2.5.0", + "tunnel-agent": "^0.6.0", + "uuid": "^3.3.2" + }, + "engines": { + "node": ">= 6" + } + }, "node_modules/request-progress": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/request-progress/-/request-progress-3.0.0.tgz", @@ -14074,6 +14349,23 @@ "throttleit": "^1.0.0" } }, + "node_modules/request/node_modules/qs": { + "version": "6.5.3", + "resolved": "https://registry.npmjs.org/qs/-/qs-6.5.3.tgz", + "integrity": "sha512-qxXIEh4pCGfHICj1mAJQ2/2XVZkjCDTcEgfoSQxc/fYivUZxTkk7L3bDBJSoNrEzXI17oUO5Dp07ktqE5KzczA==", + "engines": { + "node": ">=0.6" + } + }, + "node_modules/request/node_modules/uuid": { + "version": "3.4.0", + "resolved": "https://registry.npmjs.org/uuid/-/uuid-3.4.0.tgz", + "integrity": "sha512-HjSDRw6gZE5JMggctHBcjVak08+KEVhSIiDzFnT9S9aegmp85S/bReBVTb4QTFaRNptJ9kuYaNhnbNEOkbKb/A==", + "deprecated": "Please upgrade to version 7 or higher. Older versions may use Math.random() in certain circumstances, which is known to be problematic. See https://v8.dev/blog/math-random for details.", + "bin": { + "uuid": "bin/uuid" + } + }, "node_modules/require-directory": { "version": "2.1.1", "resolved": "https://registry.npmjs.org/require-directory/-/require-directory-2.1.1.tgz", @@ -14577,26 +14869,50 @@ "integrity": "sha512-wnD2ZE+l+SPC/uoS0vXeE9L1+0wuaMqKlfz9AMUo38JsyLSBWSFcHR1Rri62LZc12vLr1gb3jl7iwQhgwpAbGQ==" }, "node_modules/simple-update-notifier": { - "version": "1.1.0", - "resolved": "https://registry.npmjs.org/simple-update-notifier/-/simple-update-notifier-1.1.0.tgz", - "integrity": "sha512-VpsrsJSUcJEseSbMHkrsrAVSdvVS5I96Qo1QAQ4FxQ9wXFcB+pjj7FB7/us9+GcgfW4ziHtYMc1J0PLczb55mg==", + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/simple-update-notifier/-/simple-update-notifier-2.0.0.tgz", + "integrity": "sha512-a2B9Y0KlNXl9u/vsW6sTIu9vGEpfKu2wRV6l1H3XEas/0gUIzGzBoP/IouTcUQbm9JWZLH3COxyn03TYlFax6w==", "dev": true, "dependencies": { - "semver": "~7.0.0" + "semver": "^7.5.3" }, "engines": { - "node": ">=8.10.0" + "node": ">=10" + } + }, + "node_modules/simple-update-notifier/node_modules/lru-cache": { + "version": "6.0.0", + "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-6.0.0.tgz", + "integrity": "sha512-Jo6dJ04CmSjuznwJSS3pUeWmd/H0ffTlkXXgwZi+eq1UCmqQwCh+eLsYOYCwY991i2Fah4h1BEMCx4qThGbsiA==", + "dev": true, + "dependencies": { + "yallist": "^4.0.0" + }, + "engines": { + "node": ">=10" } }, "node_modules/simple-update-notifier/node_modules/semver": { - "version": "7.0.0", - "resolved": "https://registry.npmjs.org/semver/-/semver-7.0.0.tgz", - "integrity": "sha512-+GB6zVA9LWh6zovYQLALHwv5rb2PHGlJi3lfiqIHxR0uuwCgefcOJc59v9fv1w8GbStwxuuqqAjI9NMAOOgq1A==", + "version": "7.5.4", + "resolved": "https://registry.npmjs.org/semver/-/semver-7.5.4.tgz", + "integrity": "sha512-1bCSESV6Pv+i21Hvpxp3Dx+pSD8lIPt8uVjRrxAUt/nbswYc+tK6Y2btiULjd4+fnq15PX+nqQDC7Oft7WkwcA==", "dev": true, + "dependencies": { + "lru-cache": "^6.0.0" + }, "bin": { "semver": "bin/semver.js" + }, + "engines": { + "node": ">=10" } }, + "node_modules/simple-update-notifier/node_modules/yallist": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz", + "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==", + "dev": true + }, "node_modules/sisteransi": { "version": "1.0.5", "resolved": "https://registry.npmjs.org/sisteransi/-/sisteransi-1.0.5.tgz", @@ -14729,6 +15045,30 @@ "resolved": "https://registry.npmjs.org/sprintf-js/-/sprintf-js-1.0.3.tgz", "integrity": "sha512-D9cPgkvLlV3t3IzL0D0YLvGA9Ahk4PcvVwUbN0dSGr1aP0Nrt4AEnTUbuGvquEC0mA64Gqt1fzirlRs5ibXx8g==" }, + "node_modules/sshpk": { + "version": "1.18.0", + "resolved": "https://registry.npmjs.org/sshpk/-/sshpk-1.18.0.tgz", + "integrity": "sha512-2p2KJZTSqQ/I3+HX42EpYOa2l3f8Erv8MWKsy2I9uf4wA7yFIkXRffYdsx86y6z4vHtV8u7g+pPlr8/4ouAxsQ==", + "dependencies": { + "asn1": "~0.2.3", + "assert-plus": "^1.0.0", + "bcrypt-pbkdf": "^1.0.0", + "dashdash": "^1.12.0", + "ecc-jsbn": "~0.1.1", + "getpass": "^0.1.1", + "jsbn": "~0.1.0", + "safer-buffer": "^2.0.2", + "tweetnacl": "~0.14.0" + }, + "bin": { + "sshpk-conv": "bin/sshpk-conv", + "sshpk-sign": "bin/sshpk-sign", + "sshpk-verify": "bin/sshpk-verify" + }, + "engines": { + "node": ">=0.10.0" + } + }, "node_modules/stack-utils": { "version": "2.0.6", "resolved": "https://registry.npmjs.org/stack-utils/-/stack-utils-2.0.6.tgz", @@ -15132,6 +15472,18 @@ "nodetouch": "bin/nodetouch.js" } }, + "node_modules/tough-cookie": { + "version": "2.5.0", + "resolved": "https://registry.npmjs.org/tough-cookie/-/tough-cookie-2.5.0.tgz", + "integrity": "sha512-nlLsUzgm1kfLXSXfRZMc1KLAugd4hqJHDTvc2hDIwS3mZAfMEuMbc03SujMF+GEcpaX/qboeycw6iO8JwVv2+g==", + "dependencies": { + "psl": "^1.1.28", + "punycode": "^2.1.1" + }, + "engines": { + "node": ">=0.8" + } + }, "node_modules/tr46": { "version": "0.0.3", "resolved": "https://registry.npmjs.org/tr46/-/tr46-0.0.3.tgz", @@ -15301,6 +15653,22 @@ "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.6.2.tgz", "integrity": "sha512-AEYxH93jGFPn/a2iVAwW87VuUIkR1FVUKB77NwMF7nBTDkDrrT/Hpt/IrCJ0QXhW27jTBDcf5ZY7w6RiqTMw2Q==" }, + "node_modules/tunnel-agent": { + "version": "0.6.0", + "resolved": "https://registry.npmjs.org/tunnel-agent/-/tunnel-agent-0.6.0.tgz", + "integrity": "sha512-McnNiV1l8RYeY8tBgEpuodCC1mLUdbSN+CYBL7kJsJNInOP8UjDDEwdk6Mw60vdLLrr5NHKZhMAOSrR2NZuQ+w==", + "dependencies": { + "safe-buffer": "^5.0.1" + }, + "engines": { + "node": "*" + } + }, + "node_modules/tweetnacl": { + "version": "0.14.5", + "resolved": "https://registry.npmjs.org/tweetnacl/-/tweetnacl-0.14.5.tgz", + "integrity": "sha512-KXXFFdAbFXY4geFIwoyNK+f5Z1b7swfXABfL7HXCmoIWMKU3dmS26672A4EeQtDzLKy7SXmfBu51JolvEKwtGA==" + }, "node_modules/type-detect": { "version": "4.0.8", "resolved": "https://registry.npmjs.org/type-detect/-/type-detect-4.0.8.tgz", @@ -15598,7 +15966,6 @@ "version": "4.4.1", "resolved": "https://registry.npmjs.org/uri-js/-/uri-js-4.4.1.tgz", "integrity": "sha512-7rKUyy33Q1yc98pQ1DAmLtwX109F7TIfWlW1Ydo8Wl1ii1SeHieeh0HHfPeL2fMXK6z0s8ecKs9frCuLJvndBg==", - "dev": true, "dependencies": { "punycode": "^2.1.0" } @@ -15695,6 +16062,24 @@ "node": ">= 0.8" } }, + "node_modules/verror": { + "version": "1.10.0", + "resolved": "https://registry.npmjs.org/verror/-/verror-1.10.0.tgz", + "integrity": "sha512-ZZKSmDAEFOijERBLkmYfJ+vmk3w+7hOLYDNkRCuRuMJGEmqYNCNLyBBFwWKVMhfwaEF3WOd0Zlw86U/WC/+nYw==", + "engines": [ + "node >=0.6.0" + ], + "dependencies": { + "assert-plus": "^1.0.0", + "core-util-is": "1.0.2", + "extsprintf": "^1.2.0" + } + }, + "node_modules/verror/node_modules/core-util-is": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/core-util-is/-/core-util-is-1.0.2.tgz", + "integrity": "sha512-3lqz5YjWTYnW6dlDa5TLaTCcShfar1e40rmcJVwCBJC6mWlFuj0eCHIElmG1g5kyuJ/GD+8Wn4FFCcz4gJPfaQ==" + }, "node_modules/vfile": { "version": "5.3.7", "resolved": "https://registry.npmjs.org/vfile/-/vfile-5.3.7.tgz", @@ -15737,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", @@ -16640,6 +17025,14 @@ "url": "https://github.com/sponsors/sindresorhus" } }, + "node_modules/zod": { + "version": "3.22.4", + "resolved": "https://registry.npmjs.org/zod/-/zod-3.22.4.tgz", + "integrity": "sha512-iC+8Io04lddc+mVqQ9AZ7OQ2MrUKGN+oIQyq1vemgt46jwCwLfhq7/pwnBnNXXXZb8VTVLKwp9EDkx+ryxIWmg==", + "funding": { + "url": "https://github.com/sponsors/colinhacks" + } + }, "node_modules/zwitch": { "version": "2.0.4", "resolved": "https://registry.npmjs.org/zwitch/-/zwitch-2.0.4.tgz", diff --git a/package.json b/package.json index 2042253..4f25ac1 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,7 @@ { "name": "lean4-game", "version": "0.1.0", + "type": "module", "private": true, "homepage": ".", "dependencies": { @@ -36,6 +37,7 @@ "rehype-katex": "^6.0.2", "remark-gfm": "^3.0.1", "remark-math": "^5.1.1", + "request": "^2.88.2", "request-progress": "^3.0.0", "vite": "^4.5.0", "vite-plugin-static-copy": "^0.17.0", @@ -52,7 +54,7 @@ "concurrently": "^7.6.0", "css-loader": "^6.7.3", "file-loader": "^6.2.0", - "nodemon": "^2.0.20", + "nodemon": "^3.0.1", "react-refresh": "^0.14.0", "style-loader": "^3.3.1", "ts-loader": "^9.4.2", @@ -61,12 +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 58% rename from server/bubblewrap.sh rename to relay/bubblewrap.sh index 7d3f10e..a3e5f4c 100755 --- a/server/bubblewrap.sh +++ b/relay/bubblewrap.sh @@ -1,12 +1,17 @@ #/bin/bash +# Note: This fails if there is no default toolchain installed ELAN_HOME=$(lake env printenv ELAN_HOME) +# $1 : the game directory +# $2 : the lean4game folder +# $3 : the gameserver executable + (exec bwrap\ - --ro-bind ../../lean4game /lean4game \ - --ro-bind ../../$1 /game \ - --ro-bind $ELAN_HOME /elan \ - --ro-bind /usr /usr \ + --bind $2 /lean4game \ + --bind $1 /game \ + --bind $ELAN_HOME /elan \ + --bind /usr /usr \ --dev /dev \ --proc /proc \ --symlink usr/lib /lib\ @@ -22,6 +27,6 @@ ELAN_HOME=$(lake env printenv ELAN_HOME) --unshare-uts \ --unshare-cgroup \ --die-with-parent \ - --chdir "/lean4game/server/build/bin/" \ + --chdir "/game/.lake/packages/GameServer/server/.lake/build/bin/" \ ./gameserver --server /game ) diff --git a/server/import.mjs b/relay/import.mjs similarity index 61% rename from server/import.mjs rename to relay/import.mjs index e1de9b9..a98ab39 100644 --- a/server/import.mjs +++ b/relay/import.mjs @@ -11,6 +11,7 @@ const __filename = fileURLToPath(import.meta.url); const __dirname = path.dirname(__filename); const TOKEN = process.env.LEAN4GAME_GITHUB_TOKEN +const USERNAME = process.env.LEAN4GAME_GITHUB_USER const octokit = new Octokit({ auth: TOKEN }) @@ -41,9 +42,10 @@ async function download(id, url, dest) { requestProgress(request({ url, headers: { - 'User-Agent': 'abentkamp', + 'accept': 'application/vnd.github+json', + 'User-Agent': USERNAME, 'X-GitHub-Api-Version': '2022-11-28', - 'Authorization': 'Bearer '+TOKEN + 'Authorization': 'Bearer ' + TOKEN } })) .on('progress', function (state) { @@ -76,35 +78,44 @@ async function doImport (owner, repo, id) { .reduce((acc, cur) => acc.created_at < cur.created_at ? cur : acc) artifactId = artifact.id const url = artifact.archive_download_url - if (!fs.existsSync("tmp")){ - fs.mkdirSync("tmp"); + // Make sure the download folder exists + if (!fs.existsSync(path.join(__dirname, "..", "games"))){ + fs.mkdirSync(path.join(__dirname, "..", "games")); + } + 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, `tmp/artifact_${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],".") - let manifest = fs.readFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`); - manifest = JSON.parse(manifest); - if (manifest.length !== 1) { - throw `Unexpected manifest: ${JSON.stringify(manifest)}` - } - manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`] - fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest)); - await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`) - await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`]) + + 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`); + // manifest = JSON.parse(manifest); + // if (manifest.length !== 1) { + // throw `Unexpected manifest: ${JSON.stringify(manifest)}` + // } + // manifest[0].RepoTags = [`g/${owner.toLowerCase()}/${repo.toLowerCase()}:latest`] + // fs.writeFileSync(`tmp/artifact_${artifactId}_inner/manifest.json`, JSON.stringify(manifest)); + // await runProcess(id, "tar", ["-cvf", `../archive_${artifactId}.tar`, "."], `tmp/artifact_${artifactId}_inner/`) + // // await runProcess(id, "docker", ["load", "-i", `tmp/archive_${artifactId}.tar`]) + progress[id].done = true - progress[id].output += `Done.\n` + progress[id].output += `Done!\n` + progress[id].output += `Play the game at: {your website}/#/g/${owner}/${repo}\n` } catch (e) { progress[id].output += `Error: ${e.toString()}\n${e.stack}` } finally { + // clean-up temp. files if (artifactId) { - fs.rmSync(`tmp/artifact_${artifactId}.zip`, {force: true, recursive: true}); - fs.rmSync(`tmp/artifact_${artifactId}`, {force: true, recursive: true}); - fs.rmSync(`tmp/artifact_${artifactId}_inner`, {force: true, recursive: true}); - fs.rmSync(`tmp/archive_${artifactId}.tar`, {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 } + await new Promise(resolve => setTimeout(resolve, 10000)) } export const importTrigger = (req, res) => { diff --git a/server/index.mjs b/relay/index.mjs similarity index 50% rename from server/index.mjs rename to relay/index.mjs index 3def2bb..a0dd7ea 100644 --- a/server/index.mjs +++ b/relay/index.mjs @@ -6,25 +6,20 @@ import * as url from 'url'; import * as rpc from 'vscode-ws-jsonrpc'; import * as jsonrpcserver from 'vscode-ws-jsonrpc/server'; import os from 'os'; +import fs from 'fs'; import anonymize from 'ip-anonymize'; -// import { importTrigger, importStatus } from './import.mjs' +import { importTrigger, importStatus } from './import.mjs' // import fs from 'fs' /** + * Add a game here if the server should keep a queue of pre-loaded games ready at all times. + * + * IMPORTANT! Tags here need to be lower case! */ -const games = { - "g/hhu-adam/robo": { - dir: "Robo", - queueLength: 5 - }, - "g/hhu-adam/nng4": { - dir: "NNG4", - queueLength: 5 - }, - "g/hhu-adam/nng4-old": { - dir: "NNG4-OLD", - queueLength: 0 - } +const queueLength = { + "g/hhu-adam/robo": 2, + "g/hhu-adam/nng4": 5, + "g/djvelleman/stg4": 2, } const __filename = url.fileURLToPath(import.meta.url); @@ -36,11 +31,18 @@ const PORT = process.env.PORT || 8080; var router = express.Router(); -// router.get('/import/status/:owner/:repo', importStatus) -// router.get('/import/trigger/:owner/:repo', importTrigger) +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/'))) + .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 + const filename = req.params[0]; + req.url = filename; + express.static(path.join(getGameDir(owner,repo),".lake","gamedata"))(req, res, next); + }) .use('/', router) .listen(PORT, () => console.log(`Listening on ${PORT}`)); @@ -54,41 +56,61 @@ const isDevelopment = environment === 'development' /** We keep queues of started Lean Server processes to be ready when a user arrives */ const queue = {} -function tag(owner, repo) { +function getTag(owner, repo) { return `g/${owner.toLowerCase()}/${repo.toLowerCase()}` } -function startServerProcess(owner, repo) { - let game_dir = (owner == 'local') ? - repo : games[tag(owner, repo)]?.dir - +function getGameDir(owner, repo) { + owner = owner.toLowerCase() if (owner == 'local') { if(!isDevelopment) { console.error(`No local games in production mode.`) - return + return "" + } + } else { + if(!fs.existsSync(path.join(__dirname, '..', 'games'))) { + console.error(`Did not find the following folder: ${path.join(__dirname, '..', 'games')}`) + console.error('Did you already import any games?') + return "" } - // TODO: This test does not work - // if (!fs.existsSync(path.join("../", game_dir))) { - // console.error(`Game folder does not exists: ${game_dir}`) - // return - // } } - if (!game_dir) { - console.error(`Unknown game: ${tag(owner, repo)}`) - return + let game_dir = (owner == 'local') ? + path.join(__dirname, '..', '..', repo) : // note: here we need `repo` to be case sensitive + path.join(__dirname, '..', 'games', `${owner}`, `${repo.toLowerCase()}`) + + if(!fs.existsSync(game_dir)) { + console.error(`Game '${game_dir}' does not exist!`) + return "" } + return game_dir; +} + +function startServerProcess(owner, repo) { + + let game_dir = getGameDir(owner, repo) + if (!game_dir) return; + let serverProcess if (isDevelopment) { - let args = ["--server", path.join("../../../../", game_dir)] - serverProcess = cp.spawn("./gameserver", args, - { cwd: path.join(__dirname, "./build/bin/") }) + let args = ["--server", game_dir] + 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("./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, + { cwd: path.join(__dirname, "..", "server", ".lake", "build", "bin") }) + } } else { serverProcess = cp.spawn("./bubblewrap.sh", - [game_dir], + [ game_dir, path.join(__dirname, '..')], { cwd: __dirname }) } + serverProcess.on('error', error => console.error(`Launching Lean Server failed: ${error}`) ) @@ -101,15 +123,21 @@ function startServerProcess(owner, repo) { } /** start Lean Server processes to refill the queue */ -function fillQueue(owner, repo) { - while (queue[tag(owner, repo)].length < games[tag(owner, repo)].queueLength) { - const serverProcess = startServerProcess(tag(owner, repo)) - queue[tag(owner, repo)].push(serverProcess) +function fillQueue(tag) { + while (queue[tag].length < queueLength[tag]) { + let serverProcess + serverProcess = startServerProcess(tag) + if (serverProcess == null) { + console.error('serverProcess was undefined/null') + return } + queue[tag].push(serverProcess) + } } +// // TODO: We disabled queue for now // if (!isDevelopment) { // Don't use queue in development -// for (let tag in games) { +// for (let tag in queueLength) { // queue[tag] = [] // fillQueue(tag) // } @@ -122,19 +150,21 @@ wss.addListener("connection", function(ws, req) { if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; } const owner = reRes[1] const repo = reRes[2] - // const tag = `g/${owner.toLowerCase()}/${repo.toLowerCase()}` - // // TODO - // if (isDevelopment && process.env.DEV_CONTAINER) { - // tag = `g/local/game` - // } + const tag = getTag(owner, repo) - let ps; - if (!queue[tag(owner, repo)] || queue[tag(owner, repo)].length == 0) { - ps = startServerProcess(owner, repo) + let ps + if (!queue[tag] || queue[tag].length == 0) { + ps = startServerProcess(owner, repo) } else { - ps = queue[tag(owner, repo)].shift() // Pick the first Lean process; it's likely to be ready immediately - fillQueue(owner, repo) + console.info('Got process from the queue') + ps = queue[tag].shift() // Pick the first Lean process; it's likely to be ready immediately + fillQueue(tag) + } + + if (ps == null) { + console.error('server process is undefined/null') + return } socketCounter += 1; @@ -147,14 +177,14 @@ wss.addListener("connection", function(ws, req) { onClose: (cb) => { ws.on("close", cb) }, send: (data, cb) => { ws.send(data,cb) } } - const reader = new rpc.WebSocketMessageReader(socket); - const writer = new rpc.WebSocketMessageWriter(socket); + const reader = new rpc.WebSocketMessageReader(socket) + const writer = new rpc.WebSocketMessageWriter(socket) const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close()) - const serverConnection = jsonrpcserver.createProcessStreamConnection(ps); + const serverConnection = jsonrpcserver.createProcessStreamConnection(ps) socketConnection.forward(serverConnection, message => { if (isDevelopment) {console.log(`CLIENT: ${JSON.stringify(message)}`)} return message; - }); + }) serverConnection.forward(socketConnection, message => { if (isDevelopment) {console.log(`SERVER: ${JSON.stringify(message)}`)} return message; @@ -165,9 +195,9 @@ wss.addListener("connection", function(ws, req) { ws.on('close', () => { console.log(`[${new Date()}] Socket closed - ${ip}`) - socketCounter -= 1; + socketCounter -= 1 }) - socketConnection.onClose(() => serverConnection.dispose()); - serverConnection.onClose(() => socketConnection.dispose()); + socketConnection.onClose(() => serverConnection.dispose()) + serverConnection.onClose(() => socketConnection.dispose()) }) diff --git a/relay/unpack.sh b/relay/unpack.sh new file mode 100755 index 0000000..b475847 --- /dev/null +++ b/relay/unpack.sh @@ -0,0 +1,30 @@ +#/bin/bash + +ARTIFACT_ID=$1 +OWNER=$2 +REPO=$3 + +# mkdir -p games +cd games + +# mkdir -p tmp +mkdir -p ${OWNER} + +echo "Unpacking ZIP." +unzip -o tmp/${OWNER}_${REPO}_${ARTIFACT_ID}.zip -d tmp/${OWNER}_${REPO}_${ARTIFACT_ID} +echo "Unpacking game." + +# exit the npm project to avoid reloading. TODO: Where should we actually save these? + + + +echo "Delete old version of the game" +rm -rf ${OWNER}/${REPO} +mkdir -p ${OWNER}/${REPO} + +for f in tmp/${OWNER}_${REPO}_${ARTIFACT_ID}/* #Should only be one file +do + echo "Unpacking $f" + #tar -xvzf $f -C games/${OWNER}/${REPO} + unzip -q -o $f -d ${OWNER}/${REPO} +done diff --git a/server/.gitignore b/server/.gitignore deleted file mode 100644 index 103f95b..0000000 --- a/server/.gitignore +++ /dev/null @@ -1,3 +0,0 @@ -build -adam -nng 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 9ccbbb0..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"` -/ @@ -46,31 +35,92 @@ elab "Title" t:str : command => do match ← getCurLayer with | .Level => modifyCurLevel fun level => pure {level with title := t.getString} | .World => modifyCurWorld fun world => pure {world with title := t.getString} - | .Game => modifyCurGame fun game => pure {game with title := t.getString} + | .Game => modifyCurGame fun game => pure {game with + title := t.getString + tile := {game.tile with title := t.getString}} /-- 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 => pure () - | .World => pure () - | .Game => modifyCurGame fun game => pure {game with info := t.getString} + | .Level => + logError "Can't use `Info` in a level!" + pure () + | .World => + logError "Can't use `Info` in a world" + pure () + | .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. -/ +elab "Image" t:str : command => do + let file := t.getString + if not <| ← System.FilePath.pathExists file then + logWarningAt t s!"Make sure the cover image '{file}' exists." + if not <| file.startsWith "images/" then + logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder." + match ← getCurLayer with + | .Level => + logWarning "Level-images not implemented yet" -- TODO + modifyCurLevel fun level => pure {level with image := file} + | .World => + modifyCurWorld fun world => pure {world with image := file} + | .Game => + logWarning "Main image of the game not implemented yet" -- TODO + modifyCurGame fun game => pure {game with image := file} /-- 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 + modifyCurGame fun game => pure {game with + tile := {game.tile with prerequisites := t.map (·.getString) |>.toList}} + +/-- 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 := 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 := 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. + -/ +elab "Languages" t:str* : command => do + modifyCurGame fun game => pure {game with + tile := {game.tile with languages := t.map (·.getString) |>.toList}} + +/-- The Image of the game (optional). TODO: Not impementeds -/ +elab "CoverImage" t:str : command => do + let file := t.getString + if not <| ← System.FilePath.pathExists file then + logWarningAt t s!"Make sure the cover image '{file}' exists." + if not <| file.startsWith "images/" then + logWarningAt t s!"The file name should start with `images/`. Make sure all images are in that folder." + modifyCurGame fun game => pure {game with + tile := {game.tile with image := file}} /-! # Inventory @@ -80,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: ``` @@ -196,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: @@ -218,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` @@ -246,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 @@ -349,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 := {} }) @@ -497,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. -/ @@ -626,6 +496,7 @@ elab "Template" tacs:tacticSeq : tactic => do modifyLevel (←getCurLevelId) fun level => do return {level with template := s!"{template}"} + -- TODO: Notes for testing if a declaration has the simp attribute -- -- Test: From zulip @@ -644,98 +515,6 @@ elab "Template" tacs:tacticSeq : tactic => do /-! # Make Game -/ -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₃`. -/ @@ -810,8 +589,12 @@ elab "MakeGame" : command => do -- Items that should not be displayed in inventory let mut hiddenItems : HashSet Name := {} + let allWorlds := game.worlds.nodes.toArray + let nrWorlds := allWorlds.size + let mut nrLevels := 0 + -- Calculate which "items" are used/new in which world - for (worldId, world) in game.worlds.nodes.toArray do + for (worldId, world) in allWorlds do let mut usedItems : HashSet Name := {} let mut newItems : HashSet Name := {} for inventoryType in #[.Tactic, .Definition, .Lemma] do @@ -850,9 +633,12 @@ elab "MakeGame" : command => do -- logInfo m!"{worldId} uses: {usedItems.toList}" -- logInfo m!"{worldId} introduces: {newItems.toList}" + -- Moreover, count the number of levels in the game + nrLevels := nrLevels + world.levels.toArray.size + /- for each "item" this is a HashSet of `worldId`s that introduce this item -/ let mut worldsWithNewItem : HashMap Name (HashSet Name) := {} - for (worldId, _world) in game.worlds.nodes.toArray do + for (worldId, _world) in allWorlds do for newItem in newItemsInWorld.findD worldId {} do worldsWithNewItem := worldsWithNewItem.insert newItem $ (worldsWithNewItem.findD newItem {}).insert worldId @@ -864,7 +650,7 @@ elab "MakeGame" : command => do let mut dependencyReasons : HashMap (Name × Name) (HashSet Name) := {} -- Calculate world dependency graph `game.worlds` - for (dependentWorldId, _dependentWorld) in game.worlds.nodes.toArray do + for (dependentWorldId, _dependentWorld) in allWorlds do let mut dependsOnWorlds : HashSet Name := {} -- Adding manual dependencies that were specified via the `Dependency` command. for (sourceId, targetId) in game.worlds.edges do @@ -915,14 +701,25 @@ elab "MakeGame" : command => do logError m!"{w1} depends on {w2} because of {items.toList}." else worldDependsOnWorlds ← removeTransitive worldDependsOnWorlds + + -- need to delete all existing edges as they are already present in `worldDependsOnWorlds`. + modifyCurGame fun game => + pure {game with worlds := {game.worlds with edges := Array.empty}} + for (dependentWorldId, worldIds) in worldDependsOnWorlds.toArray do modifyCurGame fun game => pure {game with worlds := {game.worlds with edges := game.worlds.edges.append (worldIds.toArray.map fun wid => (wid, dependentWorldId))}} + -- Add the number of levels and worlds to the tile for the landing page + modifyCurGame fun game => pure {game with tile := {game.tile with + levels := nrLevels + worlds := nrWorlds }} + -- Apparently we need to reload `game` to get the changes to `game.worlds` we just made let game ← getCurGame + let mut allItemsByType : HashMap InventoryType (HashSet Name) := {} -- Compute which inventory items are available in which level: for inventoryType in #[.Tactic, .Definition, .Lemma] do @@ -1052,17 +849,6 @@ elab "MakeGame" : command => do modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do return level.setComputedInventory inventoryType itemsArray + allItemsByType := allItemsByType.insert inventoryType allItems -/-! # 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 + saveGameData allItemsByType diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index b1662f3..fdbd351 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -108,6 +108,12 @@ structure InventoryTile where hidden := false deriving ToJson, FromJson, Repr, Inhabited +def InventoryItem.toTile (item : InventoryItem) : InventoryTile := { + name := item.name, + displayName := item.displayName + category := item.category +} + /-- The extension that stores the doc templates. Note that you can only add, but never modify entries! -/ initialize inventoryTemplateExt : @@ -135,7 +141,18 @@ def getInventoryItem? [Monad m] [MonadEnv m] (n : Name) (type : InventoryType) : m (Option InventoryItem) := do return (inventoryExt.getState (← getEnv)).find? (fun x => x.name == n && x.type == type) +structure InventoryOverview where + tactics : Array InventoryTile + lemmas : Array InventoryTile + definitions : Array InventoryTile + 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 -/ @@ -254,8 +271,61 @@ structure GameLevel where lemmas: InventoryInfo := default /-- A proof template that is printed in an empty editor. -/ template: Option String := none - deriving Inhabited, Repr - + /-- The image for this level. -/ + image : String := default +deriving Inhabited, Repr + +/-- Json-encodable version of `GameLevel` +Fields: +- description: Lemma in mathematical language. +- descriptionGoal: Lemma printed as Lean-Code. +-/ +structure LevelInfo where + index : Nat + title : String + tactics : Array InventoryTile + lemmas : Array InventoryTile + definitions : Array InventoryTile + introduction : String + conclusion : String + descrText : Option String := none + descrFormat : String := "" + lemmaTab : Option String + displayName : Option String + statementName : Option String + template : Option String + image: Option String +deriving ToJson, FromJson + +def GameLevel.toInfo (lvl : GameLevel) (env : Environment) : LevelInfo := + { index := lvl.index, + title := lvl.title, + tactics := lvl.tactics.tiles, + lemmas := lvl.lemmas.tiles, + definitions := lvl.definitions.tiles, + descrText := lvl.descrText, + descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO + introduction := lvl.introduction + conclusion := lvl.conclusion + lemmaTab := match lvl.lemmaTab with + | some tab => tab + | none => + -- Try to set the lemma tab to the category of the first added lemma + match lvl.lemmas.tiles.find? (·.new) with + | some tile => tile.category + | none => none + statementName := lvl.statementName.toString + displayName := match lvl.statementName with + | .anonymous => none + | name => match (inventoryExt.getState env).find? + (fun x => x.name == name && x.type == .Lemma) with + | some n => n.displayName + | none => name.toString + -- Note: we could call `.find!` because we check in `Statement` that the + -- lemma doc must exist. + template := lvl.template + image := lvl.image + } /-! ## World -/ @@ -271,17 +341,46 @@ structure World where conclusion : String := default /-- The levels of the world. -/ levels: HashMap Nat GameLevel := default + /-- The introduction image of the world. -/ + image: String := default deriving Inhabited instance : ToJson World := ⟨ fun world => Json.mkObj [ ("name", toJson world.name), ("title", world.title), - ("introduction", world.introduction)] + ("introduction", world.introduction), + ("image", world.image)] ⟩ /-! ## Game -/ +/-- A tile as they are displayed on the servers landing page. -/ +structure GameTile where + /-- The title of the game -/ + title: String + /-- One catch phrase about the game -/ + short: String := default + /-- One paragraph description what the game is about -/ + long: String := default + /-- List of languages the game supports + + TODO: What's the expectected format + TODO: Must be a list with a single language currently + -/ + languages: List String := default + /-- A list of games which this one builds upon -/ + prerequisites: List String := default + /-- Number of worlds in the game -/ + worlds: Nat := default + /-- Number of levels in the game -/ + levels: Nat := default + /-- A cover image of the game + + TODO: What's the format? -/ + image: String := default +deriving Inhabited, ToJson + structure Game where /-- Internal name of the game. -/ name : Name @@ -296,8 +395,19 @@ structure Game where /-- TODO: currently unused. -/ authors : List String := default worlds : Graph Name World := default + /-- The tile displayed on the server's landing page. -/ + tile : GameTile := default + /-- The path to the background image of the world. -/ + image : String := default deriving Inhabited, ToJson +def getGameJson (game : «Game») : Json := Id.run do + let gameJson : Json := toJson game + -- Add world sizes to Json object + let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) + let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) + return gameJson + /-! ## Game environment extension -/ def HashMap.merge [BEq α] [Hashable α] (old : HashMap α β) (new : HashMap α β) (merge : β → β → β) : diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 0cca9c1..43abb73 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -1,6 +1,7 @@ /- This file is mostly copied from `Lean/Server/FileWorker.lean`. -/ import Lean.Server.FileWorker import GameServer.Game +import GameServer.ImportModules namespace MyModule open Lean @@ -412,7 +413,7 @@ section Initialization -- Set the search path Lean.searchPathRef.set paths - let env ← importModules #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] {} 0 + let env ← importModules' #[{ module := `Init : Import }, { module := levelParams.levelModule : Import }] -- return (env, paths) -- use empty header diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index 13cc25b..fb59fdb 100644 --- a/server/GameServer/Game.lean +++ b/server/GameServer/Game.lean @@ -25,53 +25,6 @@ open Lsp open JsonRpc open IO -def getGame (game : Name): GameServerM Json := do - let some game ← getGame? game - | throwServerError "Game not found" - let gameJson : Json := toJson game - -- Add world sizes to Json object - let worldSize := game.worlds.nodes.toList.map (fun (n, w) => (n.toString, w.levels.size)) - let gameJson := gameJson.mergeObj (Json.mkObj [("worldSize", Json.mkObj worldSize)]) - return gameJson - -/-- -Fields: -- description: Lemma in mathematical language. -- descriptionGoal: Lemma printed as Lean-Code. --/ -structure LevelInfo where - index : Nat - title : String - tactics : Array InventoryTile - lemmas : Array InventoryTile - definitions : Array InventoryTile - introduction : String - conclusion : String - descrText : Option String := none - descrFormat : String := "" - lemmaTab : Option String - displayName : Option String - statementName : Option String - template : Option String -deriving ToJson, FromJson - -structure InventoryOverview where - tactics : Array InventoryTile - lemmas : Array InventoryTile - definitions : Array InventoryTile - lemmaTab : Option String -deriving ToJson, FromJson - -structure LoadLevelParams where - world : Name - level : Nat - deriving ToJson, FromJson - --- structure LoadTemplateParams where --- world : Name --- level : Nat --- deriving ToJson, FromJson - structure DidOpenLevelParams where uri : String gameDir : String @@ -91,11 +44,6 @@ structure DidOpenLevelParams where statementName : Name deriving ToJson, FromJson -structure LoadDocParams where - name : Name - type : InventoryType -deriving ToJson, FromJson - structure SetInventoryParams where inventory : Array String difficulty : Nat @@ -131,86 +79,10 @@ def handleDidOpenLevel (params : Json) : GameServerM Unit := do } } - partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do match ev with | ServerEvent.clientMsg msg => match msg with - | Message.request id "info" _ => - let s ← get - let c ← read - c.hOut.writeLspResponse ⟨id, (← getGame s.game)⟩ - return true - | Message.request id "loadLevel" params => - let p ← parseParams LoadLevelParams (toJson params) - let s ← get - let c ← read - let some lvl ← getLevel? {game := s.game, world := p.world, level := p.level} - | do - c.hOut.writeLspResponseError ⟨id, .invalidParams, s!"Level not found: world {p.world}, level {p.level}", none⟩ - return true - - let env ← getEnv - - let levelInfo : LevelInfo := - { index := lvl.index, - title := lvl.title, - tactics := lvl.tactics.tiles, - lemmas := lvl.lemmas.tiles, - definitions := lvl.definitions.tiles, - descrText := lvl.descrText, - descrFormat := lvl.descrFormat --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO - introduction := lvl.introduction - conclusion := lvl.conclusion - lemmaTab := match lvl.lemmaTab with - | some tab => tab - | none => - -- Try to set the lemma tab to the category of the first added lemma - match lvl.lemmas.tiles.find? (·.new) with - | some tile => tile.category - | none => none - statementName := lvl.statementName.toString - displayName := match lvl.statementName with - | .anonymous => none - | name => match (inventoryExt.getState env).find? - (fun x => x.name == name && x.type == .Lemma) with - | some n => n.displayName - | none => name.toString - -- Note: we could call `.find!` because we check in `Statement` that the - -- lemma doc must exist. - template := lvl.template - } - c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩ - return true - -- | Message.request id "loadTemplate" params => - -- let p ← parseParams LoadTemplateParams (toJson params) - -- let s ← get - -- let c ← read - - -- let some game ← getGame? s.game - -- | throwServerError "Game not found" - -- let some world := game.worlds.nodes.find? p.world - -- | throwServerError "World not found" - - -- let mut templates : Array <| Option String := #[] - -- for (_, level) in world.levels.toArray do - -- templates := templates.push level.template - -- c.hOut.writeLspResponse ⟨id, ToJson.toJson templates⟩ - -- return true - | Message.request id "loadDoc" params => - let p ← parseParams LoadDocParams (toJson params) - let c ← read - let some doc ← getInventoryItem? p.name p.type - | do - c.hOut.writeLspResponseError ⟨id, .invalidParams, - s!"Documentation not found: {p.name}", none⟩ - return true - -- TODO: not necessary at all? - -- Here we only need to convert the fields that were not `String` in the `InventoryDocEntry` - -- let doc : InventoryItem := { doc with - -- name := doc.name.toString } - c.hOut.writeLspResponse ⟨id, ToJson.toJson doc⟩ - return true | Message.notification "$/game/setInventory" params => let p := (← parseParams SetInventoryParams (toJson params)) let s ← get @@ -221,30 +93,6 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do fw.stdin.writeLspMessage msg return true - | Message.request id "loadInventoryOverview" _ => - let s ← get - let some game ← getGame? s.game - | return false - -- All Levels have the same tiles, so we just load them from level 1 of an arbitrary world - -- and reset `new`, `disabled` and `unlocked`. - -- Note: as we allow worlds without any levels (for developing), we might need - -- to try until we find the first world with levels. - for ⟨worldId, _⟩ in game.worlds.nodes.toList do - let some lvl ← getLevel? {game := s.game, world := worldId, level := 1} - | do continue - let inventory : InventoryOverview := { - tactics := lvl.tactics.tiles.map - ({ · with locked := true, disabled := false, new := false }), - lemmas := lvl.lemmas.tiles.map - ({ · with locked := true, disabled := false, new := false }), - definitions := lvl.definitions.tiles.map - ({ · with locked := true, disabled := false, new := false }), - lemmaTab := none - } - let c ← read - c.hOut.writeLspResponse ⟨id, ToJson.toJson inventory⟩ - return true - return false | _ => return false | _ => return false 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/ImportModules.lean b/server/GameServer/ImportModules.lean new file mode 100644 index 0000000..055bed1 --- /dev/null +++ b/server/GameServer/ImportModules.lean @@ -0,0 +1,108 @@ +import Lean.Environment +import Std.Tactic.OpenPrivate +import Lean.Data.Lsp.Communication + +open Lean + +inductive LoadingKind := | finalizeExtensions | loadConstants + deriving ToJson + +structure LoadingParams : Type where + counter : Nat + kind : LoadingKind + deriving ToJson + +-- Code adapted from `Lean/Environment.lean` + +partial def importModulesCore' (imports : Array Import) : ImportStateM Unit := do + for i in imports do + if i.runtimeOnly || (← get).moduleNameSet.contains i.module then + continue + modify fun s => { s with moduleNameSet := s.moduleNameSet.insert i.module } + let mFile ← findOLean i.module + unless (← mFile.pathExists) do + throw <| IO.userError s!"object file '{mFile}' of module {i.module} does not exist" + let (mod, region) ← readModuleData mFile + importModulesCore' mod.imports + modify fun s => { s with + moduleData := s.moduleData.push mod + regions := s.regions.push region + moduleNames := s.moduleNames.push i.module + } + +open private mkInitialExtensionStates Environment.mk setImportedEntries finalizePersistentExtensions + ensureExtensionsArraySize from Lean.Environment + +private partial def finalizePersistentExtensions' (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do + loop 0 env +where + loop (i : Nat) (env : Environment) : IO Environment := do + (← IO.getStdout).writeLspNotification { + method := "$/game/loading", + param := {counter := i, kind := .finalizeExtensions : LoadingParams} } + -- Recall that the size of the array stored `persistentEnvExtensionRef` may increase when we import user-defined environment extensions. + let pExtDescrs ← persistentEnvExtensionsRef.get + if i < pExtDescrs.size then + let extDescr := pExtDescrs[i]! + let s := extDescr.toEnvExtension.getState env + let prevSize := (← persistentEnvExtensionsRef.get).size + let prevAttrSize ← getNumBuiltinAttributes + let newState ← extDescr.addImportedFn s.importedEntries { env := env, opts := opts } + let mut env := extDescr.toEnvExtension.setState env { s with state := newState } + env ← ensureExtensionsArraySize env + if (← persistentEnvExtensionsRef.get).size > prevSize || (← getNumBuiltinAttributes) > prevAttrSize then + -- This branch is executed when `pExtDescrs[i]` is the extension associated with the `init` attribute, and + -- a user-defined persistent extension is imported. + -- Thus, we invoke `setImportedEntries` to update the array `importedEntries` with the entries for the new extensions. + env ← setImportedEntries env mods prevSize + -- See comment at `updateEnvAttributesRef` + env ← updateEnvAttributes env + loop (i + 1) env + else + return env + +def finalizeImport' (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment := do + let numConsts := s.moduleData.foldl (init := 0) fun numConsts mod => + numConsts + mod.constants.size + mod.extraConstNames.size + let mut const2ModIdx : HashMap Name ModuleIdx := mkHashMap (capacity := numConsts) + let mut constantMap : HashMap Name ConstantInfo := mkHashMap (capacity := numConsts) + for h:modIdx in [0:s.moduleData.size] do + if modIdx % 100 = 0 then + let percentage := modIdx * 100 / s.moduleData.size + (← IO.getStdout).writeLspNotification { + method := "$/game/loading", + param := {counter := percentage, kind := .loadConstants : LoadingParams} } + let mod := s.moduleData[modIdx]'h.upper + for cname in mod.constNames, cinfo in mod.constants do + match constantMap.insert' cname cinfo with + | (constantMap', replaced) => + constantMap := constantMap' + if replaced then + throwAlreadyImported s const2ModIdx modIdx cname + const2ModIdx := const2ModIdx.insert cname modIdx + for cname in mod.extraConstNames do + const2ModIdx := const2ModIdx.insert cname modIdx + let constants : ConstMap := SMap.fromHashMap constantMap false + let exts ← mkInitialExtensionStates + let env : Environment := Environment.mk + (const2ModIdx := const2ModIdx) + (constants := constants) + (extraConstNames := {}) + (extensions := exts) + (header := { + quotInit := !imports.isEmpty -- We assume `core.lean` initializes quotient module + trustLevel := trustLevel + imports := imports + regions := s.regions + moduleNames := s.moduleNames + moduleData := s.moduleData + }) + + let env ← setImportedEntries env s.moduleData + finalizePersistentExtensions' env s.moduleData opts + +def importModules' (imports : Array Import) : IO Environment := do + withImporting do + let (_, s) ← importModulesCore' imports |>.run + let env ← finalizeImport' s imports {} 0 + return env 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/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean index ed6286d..54ac6b1 100644 --- a/server/GameServer/RpcHandlers.lean +++ b/server/GameServer/RpcHandlers.lean @@ -78,7 +78,7 @@ partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) : | _, _ => none /-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/ -def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do +def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM (Option FVarBijection) := do -- We iterate through the array backwards hoping that this will find us faster results -- TODO: implement backtracking let mut bij := initBij @@ -97,11 +97,11 @@ def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (in -- usedFvars := usedFvars.set! (fvars.size - j - 1) true bij := bij'.insert pattern.fvarId! fvar.fvarId! break - if ! bij.forward.contains pattern.fvarId! then return false + if ! bij.forward.contains pattern.fvarId! then return none - if strict then - return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!) - return true + if !strict || fvars.all (fun fvar => bij.backward.contains fvar.fvarId!) + then return some bij + else return none unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) := evalExpr (Array Expr → MessageData) @@ -122,10 +122,11 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal) then let lctx := (← goal.getDecl).lctx - if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij) + if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij) then - let text := (← evalHintMessage hint.text) hintFVars - let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}} + let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId! + let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar) + let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := lctx, opts := {}} let text ← (MessageData.withContext ctx text).toString return some { text := text, hidden := hint.hidden } else return none 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/lake-manifest.json b/server/lake-manifest.json index 5c8f511..2554a52 100644 --- a/server/lake-manifest.json +++ b/server/lake-manifest.json @@ -1,4 +1,14 @@ -{"version": 6, - "packagesDir": "lake-packages", - "packages": [], - "name": "GameServer"} +{"version": 7, + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover/std4.git", + "type": "git", + "subDir": null, + "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087", + "name": "std", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.3.0", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "GameServer", + "lakeDir": ".lake"} diff --git a/server/lakefile.lean b/server/lakefile.lean index 4ffee6f..fc337ce 100644 --- a/server/lakefile.lean +++ b/server/lakefile.lean @@ -3,10 +3,25 @@ open Lake DSL package GameServer +-- Using this assumes that each dependency has a tag of the form `v4.X.0`. +def leanVersion : String := s!"v{Lean.versionString}" + +require std from git "https://github.com/leanprover/std4.git" @ leanVersion + lean_lib GameServer @[default_target] lean_exe gameserver { - root := `Main + root := `GameServer 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 + discard <| runBuild gameserver.build >>= (·.await) diff --git a/server/lean-toolchain b/server/lean-toolchain index 2f868c6..5cadc9d 100644 --- a/server/lean-toolchain +++ b/server/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0 +leanprover/lean4:v4.3.0 diff --git a/server/unpack.sh b/server/unpack.sh deleted file mode 100644 index 5a765db..0000000 --- a/server/unpack.sh +++ /dev/null @@ -1,13 +0,0 @@ -#/bin/bash - -ARTIFACT_ID=$1 - -echo "Unpacking ZIP." -unzip -o tmp/artifact_${ARTIFACT_ID}.zip -d tmp/artifact_${ARTIFACT_ID} -echo "Unpacking TAR." -for f in tmp/artifact_${ARTIFACT_ID}/* #Should only be one file -do - echo "Unpacking $f" - mkdir tmp/artifact_${ARTIFACT_ID}_inner - tar -xvf $f -C tmp/artifact_${ARTIFACT_ID}_inner -done 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 59ade19..9bc8d40 100644 --- a/vite.config.ts +++ b/vite.config.ts @@ -5,6 +5,12 @@ import svgr from "vite-plugin-svgr" // https://vitejs.dev/config/ export default defineConfig({ + //root: 'client/src', + build: { + // Relative to the root + // Note: This has to match the path in `relay/index.mjs` + outDir: 'client/dist', + }, plugins: [ react(), svgr({ @@ -22,6 +28,9 @@ export default defineConfig({ }) ], publicDir: "client/public", + optimizeDeps: { + exclude: ['games'] + }, server: { port: 3000, proxy: { @@ -29,6 +38,12 @@ export default defineConfig({ target: 'ws://localhost:8080', ws: true }, + '/import': { + target: 'http://localhost:8080', + }, + '/data': { + target: 'http://localhost:8080', + }, } }, resolve: { diff --git a/webpack.config.js b/webpack.config.js deleted file mode 100644 index be3c8f6..0000000 --- a/webpack.config.js +++ /dev/null @@ -1,106 +0,0 @@ -const path = require("path"); -const webpack = require('webpack'); -const ReactRefreshWebpackPlugin = require('@pmmmwh/react-refresh-webpack-plugin'); -const WebpackShellPluginNext = require('webpack-shell-plugin-next'); - -module.exports = env => { - - const single_game = process.env.LEAN4GAME_SINGLE_GAME - - - const environment = process.env.NODE_ENV - const isDevelopment = environment === 'development' - - const babelOptions = { - presets: ['@babel/preset-env', '@babel/preset-react', '@babel/preset-typescript'], - plugins: [ - isDevelopment && require.resolve('react-refresh/babel'), - ].filter(Boolean), - }; - - global.$RefreshReg$ = () => {}; - global.$RefreshSig$ = () => () => {}; - - return { - entry: [single_game ? "./client/src/index_local.tsx" : "./client/src/index.tsx"], - mode: isDevelopment ? 'development' : 'production', - module: { - rules: [ - { - test: /\.(js|jsx)$/, - exclude: [/server/, /node_modules/], - use: [{ - loader: require.resolve('babel-loader'), - options: babelOptions, - }] - }, - { - test: /\.tsx?$/, - use: [{ - loader: 'ts-loader', - options: { allowTsInNodeModules: true } - }], - // exclude: /node_modules(?!\/(lean4web|lean4|lean4-infoview))/, - // Allow .ts imports from node_modules/lean4web and node_modules/lean4 - }, - { - test: /\.css$/, - use: ["style-loader", "css-loader"] - }, - { - test: /\.(jpg|png)$/, - use: { - loader: 'file-loader', - }, - }, - ] - }, - resolve: { - extensions: ["*", ".js", ".jsx", ".tsx", ".ts"], - fallback: { - "http": require.resolve("stream-http") , - "path": require.resolve("path-browserify") - }, - }, - output: { - path: path.resolve(__dirname, "client/dist/"), - filename: "bundle.js", - }, - devServer: { - proxy: { - '/websocket': { - target: 'ws://localhost:8080', - ws: true - }, - '/import': { - target: 'http://localhost:3000', - router: () => 'http://localhost:8080', - }, - }, - static: path.join(__dirname, 'client/public/'), - port: 3000, - hot: true, - }, - devtool: "source-map", - plugins: [ - !isDevelopment && new WebpackShellPluginNext({ - onBuildEnd:{ - scripts: [ - // It's hard to set up webpack to copy the index.html correctly, - // so we copy it explicitly after every build: - 'cp client/public/index.html client/dist/', - // Similarly, I haven't been able to load `onigasm.wasm` properly: - 'cp client/public/onigasm.wasm client/dist/',], - blocking: false, - parallel: true - } - }), - isDevelopment && new ReactRefreshWebpackPlugin(), - ].filter(Boolean), - - // Webpack is not happy about the dynamically loaded widget code in the function - // `dynamicallyLoadComponent` in `infoview/userWidget.tsx`. If we want to support - // dynamically loaded widget code, we need to make sure that the files are available. - ignoreWarnings: [/Critical dependency: the request of a dependency is an expression/] - }; -}