update npm deps

Modify logic for preferences

.vscode/ltex.dictionary.en-US.txt

@@ -0,0 +1,7 @@
+GameSkeleton
+HiddenTactic
+subgoals
+KaTex
+gameserver
+lakefile
+Zulip

README.md

@@ -9,6 +9,7 @@ Please follow the tutorial [Creating a Game](doc/create_game.md). In particular,
 * 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)
+* [Troubleshooting](doc/troubleshoot.md)
 
 ## Documentation
 

client/src/app.tsx

@@ -8,40 +8,24 @@ import '@fontsource/roboto/700.css';
 
 import './css/reset.css';
 import './css/app.css';
-import { MobileContext } from './components/infoview/context';
+import { PreferencesContext} from './components/infoview/context';
-import { useMobile } from './hooks';
+import UsePreferences from "./state/hooks/use_preferences"
-import { AUTO_SWITCH_THRESHOLD, getWindowDimensions} from './state/preferences';
 
 export const GameIdContext = React.createContext<string>(undefined);
 
 function App() {
-  const { mobile, setMobile, lockMobile, setLockMobile } = useMobile();
 
   const params = useParams()
   const gameId = "g/" + params.owner + "/" + params.repo
 
-  const automaticallyAdjustLayout = () => {
+  const {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences} = UsePreferences()
-    const {width} = getWindowDimensions()
-    setMobile(width < AUTO_SWITCH_THRESHOLD)
-  }
-
-  React.useEffect(()=>{
-    if (!lockMobile){
-      void automaticallyAdjustLayout()
-      window.addEventListener('resize', automaticallyAdjustLayout)
-
-      return () => {
-        window.removeEventListener('resize', automaticallyAdjustLayout)
-      }
-    }
-  }, [lockMobile])
 
   return (
     <div className="app">
       <GameIdContext.Provider value={gameId}>
-        <MobileContext.Provider value={{mobile, setMobile, lockMobile, setLockMobile}}>
+          <PreferencesContext.Provider value={{mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}}>
             <Outlet />
-        </MobileContext.Provider>
+          </PreferencesContext.Provider>
       </GameIdContext.Provider>
     </div>
   )

client/src/components/app_bar.tsx

@@ -7,7 +7,7 @@ import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome,
   faArrowRight, faArrowLeft, faXmark, faBars, faCode,
   faCircleInfo, faTerminal, faMobileScreenButton, faDesktop, faGear } from '@fortawesome/free-solid-svg-icons'
 import { GameIdContext } from "../app"
-import { InputModeContext, MobileContext, WorldLevelIdContext } from "./infoview/context"
+import { InputModeContext, PreferencesContext, WorldLevelIdContext } from "./infoview/context"
 import { GameInfo, useGetGameInfoQuery } from '../state/api'
 import { changedOpenedIntro, selectCompleted, selectDifficulty, selectProgress } from '../state/progress'
 import { useAppDispatch, useAppSelector } from '../hooks'
@@ -162,7 +162,7 @@ export function WelcomeAppBar({pageNumber, setPageNumber, gameInfo, toggleImpres
 }) {
   const gameId = React.useContext(GameIdContext)
   const gameProgress = useAppSelector(selectProgress(gameId))
-  const {mobile, setMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const [navOpen, setNavOpen] = React.useState(false)
 
   return <div className="app-bar">
@@ -212,7 +212,7 @@ export function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber=
 }) {
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = React.useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const [navOpen, setNavOpen] = React.useState(false)
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))

client/src/components/infoview/context.ts

@@ -5,6 +5,7 @@ import * as React from 'react';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 import { InteractiveDiagnostic, InteractiveTermGoal } from '@leanprover/infoview-api';
 import { GameHint, InteractiveGoal, InteractiveGoals } from './rpc_api';
+import { PreferencesState } from '../../state/preferences';
 
 export const MonacoEditorContext = React.createContext<monaco.editor.IStandaloneCodeEditor>(
   null as any)
@@ -62,18 +63,18 @@ export const ProofStateContext = React.createContext<{
   setProofState: () => {},
 })
 
-export interface IMobileContext {
+export interface IPreferencesContext extends PreferencesState{
-  mobile : boolean,
+  mobile: boolean, // The variables that actually control the page 'layout' can only be changed through layout.
-  setMobile: React.Dispatch<React.SetStateAction<Boolean>>,
+  setLayout: React.Dispatch<React.SetStateAction<PreferencesState["layout"]>>;
-  lockMobile: boolean,
+  setIsSavePreferences: React.Dispatch<React.SetStateAction<Boolean>>;
-  setLockMobile: React.Dispatch<React.SetStateAction<Boolean>>,
 }
 
-export const MobileContext = React.createContext<IMobileContext>({
+export const PreferencesContext = React.createContext<IPreferencesContext>({
   mobile: false,
-  setMobile: () => {},
+  layout: "auto",
-  lockMobile: false,
+  isSavePreferences: false,
-  setLockMobile: () => {}
+  setLayout: () => {},
+  setIsSavePreferences: () => {}
 })
 
 export const WorldLevelIdContext = React.createContext<{

client/src/components/infoview/main.tsx

@@ -27,7 +27,7 @@ import Markdown from '../markdown';
 import { Infos } from './infos';
 import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
 import { Goal } from './goals';
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './context';
 import { Typewriter, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { Button } from '../button';
@@ -349,7 +349,7 @@ export function TypewriterInterface({props}) {
   const [disableInput, setDisableInput] = React.useState<boolean>(false)
   const [loadingProgress, setLoadingProgress] = React.useState<number>(0)
   const { setDeletedChat, showHelp, setShowHelp } = React.useContext(DeletedChatContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const { proof } = React.useContext(ProofContext)
   const { setTypewriterInput } = React.useContext(InputModeContext)
   const { selectedStep, setSelectedStep } = React.useContext(SelectionContext)

client/src/components/landing_page.tsx

@@ -134,7 +134,8 @@ function LandingPage() {
     "leanprover-community/nng4",
     "hhu-adam/robo",
     "djvelleman/stg4",
-    "miguelmarco/STG4",
+    "miguelmarco/stg4",
+    "trequetrum/lean4game-logic",
   ]
   let allTiles = allGames.map((gameId) => (useGetGameInfoQuery({game: `g/${gameId}`}).data?.tile))
 

client/src/components/level.tsx

@@ -27,7 +27,7 @@ import { Button } from './button'
 import Markdown from './markdown'
 import {InventoryPanel} from './inventory'
 import { hasInteractiveErrors } from './infoview/typewriter'
-import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContext,
+import { DeletedChatContext, InputModeContext, PreferencesContext, MonacoEditorContext,
   ProofContext, ProofStep, SelectionContext, WorldLevelIdContext } from './infoview/context'
 import { DualEditor } from './infoview/main'
 import { GameHint } from './infoview/rpc_api'
@@ -74,7 +74,7 @@ function Level() {
 
 function ChatPanel({lastLevel}) {
   const chatRef = useRef<HTMLDivElement>(null)
-  const {mobile} = useContext(MobileContext)
+  const {mobile} = useContext(PreferencesContext)
   const gameId = useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
   const level = useLoadLevelQuery({game: gameId, world: worldId, level: levelId})
@@ -215,7 +215,7 @@ function PlayableLevel({impressum, setImpressum}) {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const gameId = React.useContext(GameIdContext)
   const {worldId, levelId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
 
   const dispatch = useAppDispatch()
 
@@ -441,7 +441,7 @@ function PlayableLevel({impressum, setImpressum}) {
 function IntroductionPanel({gameInfo}) {
   const gameId = React.useContext(GameIdContext)
   const {worldId} = useContext(WorldLevelIdContext)
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
 
   let text: Array<string> = gameInfo.data?.worlds.nodes[worldId].introduction.split(/\n(\s*\n)+/)
 
@@ -468,7 +468,7 @@ export default Level
 /** The site with the introduction text of a world */
 function Introduction({impressum, setImpressum}) {
   const gameId = React.useContext(GameIdContext)
-  const {mobile} = useContext(MobileContext)
+  const {mobile} = useContext(PreferencesContext)
 
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 

client/src/components/popup/preferences.tsx

@@ -1,16 +1,42 @@
 import * as React from 'react'
 import { Input, Typography } from '@mui/material'
 import Markdown from '../markdown'
-import Switch from '@mui/material/Switch';
+import { Switch, Button, ButtonGroup } from '@mui/material';
+import Box from '@mui/material/Box';
+import Slider from '@mui/material/Slider';
+
 import FormControlLabel from '@mui/material/FormControlLabel';
 
-import { IMobileContext } from "../infoview/context"
+import { IPreferencesContext } from "../infoview/context"
 
-interface PreferencesPopupProps extends IMobileContext{
+interface PreferencesPopupProps extends Omit<IPreferencesContext, 'mobile'> {
     handleClose: () => void
 }
 
-export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
+export function PreferencesPopup({ layout, setLayout, isSavePreferences, setIsSavePreferences, handleClose }: PreferencesPopupProps) {
+
+    const marks = [
+        {
+            value: 0,
+            label: 'Mobile',
+            key: "mobile"
+        },
+        {
+            value: 1,
+            label: 'Auto',
+            key: "auto"
+        },
+        {
+            value: 2,
+            label: 'Desktop',
+            key: "desktop"
+        },
+    ];
+
+    const handlerChangeLayout = (_: Event, value: number) => {
+        setLayout(marks[value].key as IPreferencesContext["layout"])
+    }
+
     return <div className="modal-wrapper">
         <div className="modal-backdrop" onClick={handleClose} />
         <div className="modal">
@@ -18,34 +44,43 @@ export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile,
             <Typography variant="body1" component="div" className="settings">
                 <div className='preferences-category'>
                     <div className='category-title'>
-                        <h3>Mobile layout</h3>
+                        <h3>Layout</h3>
                     </div>
+                    <div className='preferences-item first leave-left-gap'>
+                        <FormControlLabel
+                            control={
+                                <Box sx={{ width: 300 }}>
+                                    <Slider
+                                        aria-label="Always visible"
+                                        value={marks.find(item => item.key === layout).value}
+                                        step={1}
+                                        marks={marks}
+                                        max={2}
+                                        sx={{
+                                            '& .MuiSlider-track': { display: 'none', },
+                                        }}
+                                        onChange={handlerChangeLayout}
+                                    />
+                                </Box>
+                            }
+                            label=""
+                        />
+                    </div>
+                </div>
+
+                <div className='preferences-category tail-category'>
                     <div className='preferences-item'>
                         <FormControlLabel
                             control={
                                 <Switch
-                                checked={mobile}
+                                    checked={isSavePreferences}
-                                onChange={() => setMobile(!mobile)}
+                                    onChange={() => setIsSavePreferences(!isSavePreferences)}
                                     name="checked"
                                     color="primary"
                                 />
                             }
-                            label="Enable"
+                            label="Save my settings (in the browser store)"
-                            labelPlacement="start"
+                            labelPlacement="end"
-                        />
-                    </div>
-                    <div className='preferences-item'>
-                        <FormControlLabel
-                            control={
-                            <Switch
-                                checked={!lockMobile}
-                                onChange={() => setLockMobile(!lockMobile)}
-                                name="checked"
-                                color="primary"
-                            />
-                            }
-                            label="Auto"
-                            labelPlacement="start"
                         />
                     </div>
                 </div>

client/src/components/welcome.tsx

@@ -10,7 +10,7 @@ import { useAppDispatch, useAppSelector } from '../hooks'
 import { changedOpenedIntro, selectOpenedIntro } from '../state/progress'
 import { useGetGameInfoQuery, useLoadInventoryOverviewQuery } from '../state/api'
 import { Button } from './button'
-import { MobileContext } from './infoview/context'
+import { PreferencesContext } from './infoview/context'
 import { InventoryPanel } from './inventory'
 import { ErasePopup } from './popup/erase'
 import { InfoPopup } from './popup/game_info'
@@ -27,7 +27,7 @@ import { Hint } from './hints'
 
 /** the panel showing the game's introduction text */
 function IntroductionPanel({introduction, setPageNumber}: {introduction: string, setPageNumber}) {
-  const {mobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
   const gameId = React.useContext(GameIdContext)
   const dispatch = useAppDispatch()
 
@@ -64,7 +64,9 @@ function IntroductionPanel({introduction, setPageNumber}: {introduction: string,
 /** main page of the game showing among others the tree of worlds/levels */
 function Welcome() {
   const gameId = React.useContext(GameIdContext)
-  const {mobile, setMobile, lockMobile, setLockMobile} = React.useContext(MobileContext)
+  const {mobile} = React.useContext(PreferencesContext)
+  const {layout, isSavePreferences, setLayout, setIsSavePreferences} = React.useContext(PreferencesContext)
+
   const gameInfo = useGetGameInfoQuery({game: gameId})
   const inventory = useLoadInventoryOverviewQuery({game: gameId})
 
@@ -134,7 +136,7 @@ function Welcome() {
     {eraseMenu? <ErasePopup handleClose={closeEraseMenu}/> : null}
     {uploadMenu? <UploadPopup handleClose={closeUploadMenu}/> : null}
     {info ? <InfoPopup info={gameInfo.data?.info} handleClose={closeInfo}/> : null}
-    {preferencesPopup ? <PreferencesPopup mobile={mobile} setMobile={setMobile} lockMobile={lockMobile} setLockMobile={setLockMobile} handleClose={closePreferencesPopup}/> : null}
+    {preferencesPopup ? <PreferencesPopup layout={layout} isSavePreferences={isSavePreferences} setLayout={setLayout} setIsSavePreferences={setIsSavePreferences} handleClose={closePreferencesPopup}/> : null}
   </>
 }
 

client/src/components/world_tree.tsx

@@ -11,11 +11,12 @@ import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faXmark, faCircleQuestion } from '@fortawesome/free-solid-svg-icons'
 
 import { GameIdContext } from '../app'
-import { useAppDispatch, useMobile } from '../hooks'
+import { useAppDispatch } from '../hooks'
 import { selectDifficulty, changedDifficulty, selectCompleted } from '../state/progress'
 import { store } from '../state/store'
 
 import '../css/world_tree.css'
+import { PreferencesContext } from './infoview/context'
 
 // Settings for the world tree
 cytoscape.use( klay )
@@ -197,7 +198,7 @@ export function WorldSelectionMenu({rulesHelp, setRulesHelp}) {
   const gameId = React.useContext(GameIdContext)
   const difficulty = useSelector(selectDifficulty(gameId))
   const dispatch = useAppDispatch()
-  const { mobile } = useMobile()
+  const { mobile } = React.useContext(PreferencesContext)
 
 
   function label(x : number) {

client/src/css/welcome.css

@@ -187,3 +187,15 @@ h5, h6 {
   margin-left: 0.3rem;
   margin-right: 0.3rem;
 }
+
+.preferences-category.tail-category{
+  margin-top: 2em;
+}
+
+.preferences-item.first{
+  margin-top: 1em;
+}
+
+.preferences-item.leave-left-gap{
+  margin-left: 3em;
+}

client/src/hooks.ts

@@ -1,30 +1,6 @@
 import { TypedUseSelectorHook, useDispatch, useSelector } from 'react-redux'
 import type { RootState, AppDispatch } from './state/store'
 
-import { setMobile as setMobileState, setLockMobile as setLockMobileState} from "./state/preferences"
-
 // Use throughout your app instead of plain `useDispatch` and `useSelector`
 export const useAppDispatch: () => AppDispatch = useDispatch
 export const useAppSelector: TypedUseSelectorHook<RootState> = useSelector
-
-export const useMobile = () => {
-  const dispatch = useAppDispatch();
-
-  const mobile = useAppSelector((state) => state.preferences.mobile);
-  const lockMobile = useAppSelector((state) => state.preferences.lockMobile);
-
-  const setMobile = (val: boolean) => {
-    dispatch(setMobileState(val));
-  };
-
-  const setLockMobile = (val: boolean) => {
-    dispatch(setLockMobileState(val));
-  };
-
-  return {
-    mobile,
-    setMobile,
-    lockMobile,
-    setLockMobile,
-  };
-};

client/src/state/hooks/use_preferences.ts

@@ -0,0 +1,41 @@
+import React, { useState } from "react";
+import { useAppDispatch, useAppSelector } from "../../hooks";
+import { 
+    PreferencesState, 
+    setLayout as setPreferencesLayout, 
+    setIsSavePreferences as setPreferencesIsSavePreferences,
+    getWindowDimensions,
+    AUTO_SWITCH_THRESHOLD
+} from "../preferences";
+
+
+const UsePreferences = () => {
+    const dispatch = useAppDispatch()
+    const [mobile, setMobile] = React.useState<boolean>()
+
+    const layout = useAppSelector((state) => state.preferences.layout);
+    const setLayout = (layout: PreferencesState["layout"]) => dispatch(setPreferencesLayout(layout))
+
+    const isSavePreferences = useAppSelector((state) => state.preferences.isSavePreferences);
+    const setIsSavePreferences = (isSave: boolean) => dispatch(setPreferencesIsSavePreferences(isSave))
+
+    const automaticallyAdjustLayout = () => {
+        const {width} = getWindowDimensions()
+        setMobile(width < AUTO_SWITCH_THRESHOLD)
+    }
+
+    React.useEffect(()=>{
+        if (layout === "auto"){
+          void automaticallyAdjustLayout()
+          window.addEventListener('resize', automaticallyAdjustLayout)
+    
+          return () => window.removeEventListener('resize', automaticallyAdjustLayout)
+        } else {
+          setMobile(layout === "mobile")
+        }
+    }, [layout])
+
+    return {mobile, layout, isSavePreferences, setLayout, setIsSavePreferences}
+} 
+
+export default UsePreferences;

client/src/state/local_storage.ts

@@ -57,3 +57,12 @@ export function savePreferences(state: any) {
     // Ignore
   }
 }
+
+export function removePreferences() {
+  try {
+    localStorage.removeItem(PREFERENCES_KEY);
+  } catch (e) {
+    // Ignore
+  }
+}
+

client/src/state/preferences.ts

@@ -1,10 +1,10 @@
 import { createSlice } from "@reduxjs/toolkit";
 
-import { loadPreferences } from "./local_storage";
+import { loadPreferences, removePreferences, savePreferences } from "./local_storage";
 
-interface PreferencesState {
+export interface PreferencesState {
-  mobile: boolean;
+  layout: "mobile" | "auto" | "desktop";
-  lockMobile: boolean;
+  isSavePreferences: boolean;
 }
 
 export function getWindowDimensions() {
@@ -12,26 +12,24 @@ export function getWindowDimensions() {
   return {width, height}
 }
 
-const { width } = getWindowDimensions()
-
 export const AUTO_SWITCH_THRESHOLD = 800
 
-const initialState: PreferencesState = loadPreferences() ?? {
+const initialState: PreferencesState = loadPreferences() ??{
-    mobile: width < AUTO_SWITCH_THRESHOLD,
+    layout: "auto",
-    lockMobile: false
+    isSavePreferences: false
 }
 
 export const preferencesSlice = createSlice({
   name: "preferences",
   initialState,
   reducers: {
-    setMobile: (state, action) => {
+    setLayout: (state, action) => {
-      state.mobile = action.payload;
+      state.layout = action.payload;
     },
-    setLockMobile: (state, action) => {
+    setIsSavePreferences: (state, action) => {
-      state.lockMobile = action.payload;
+      state.isSavePreferences = action.payload;
     },
   },
 });
 
-export const { setMobile, setLockMobile } = preferencesSlice.actions;
+export const { setLayout, setIsSavePreferences } = preferencesSlice.actions;

client/src/state/progress.ts

@@ -53,22 +53,22 @@ const initalLevelProgressState: LevelProgressState = {code: "", completed: false
 
 /** Add an empty skeleton with progress for the current game */
 function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) {
-  if (!state.games[action.payload.game]) {
+  if (!state.games[action.payload.game.toLowerCase()]) {
-    state.games[action.payload.game] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
+    state.games[action.payload.game.toLowerCase()] = {inventory: [], openedIntro: true, data: {}, difficulty: DEFAULT_DIFFICULTY}
   }
-  if (!state.games[action.payload.game].data) {
+  if (!state.games[action.payload.game.toLowerCase()].data) {
-    state.games[action.payload.game].data = {}
+    state.games[action.payload.game.toLowerCase()].data = {}
   }
 }
 
 /** Add an empty skeleton with progress for the current level */
 function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
   addGameProgress(state, action)
-  if (!state.games[action.payload.game].data[action.payload.world]) {
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world]) {
-    state.games[action.payload.game].data[action.payload.world] = {}
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world] = {}
   }
-  if (!state.games[action.payload.game].data[action.payload.world][action.payload.level]) {
+  if (!state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level]) {
-    state.games[action.payload.game].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
+    state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = {...initalLevelProgressState}
   }
 }
 
@@ -79,58 +79,58 @@ export const progressSlice = createSlice({
     /** put edited code in the state and set completed to false */
     codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].code = action.payload.code
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].code = action.payload.code
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = false
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = false
     },
     /** TODO: docstring */
     changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].selections = action.payload.selections
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].selections = action.payload.selections
     },
     /** mark level as completed */
     levelCompleted(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = true
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].completed = true
     },
     /** Set the list of rows where help is displayed */
     helpEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, help: number[]}>) {
       addLevelProgress(state, action)
       console.debug(`!setting help to: ${action.payload.help}`)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level].help = action.payload.help
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level].help = action.payload.help
     },
     /** delete all progress for this game */
     deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) {
-      state.games[action.payload.game] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
+      state.games[action.payload.game.toLowerCase()] = {inventory: [], data: {}, openedIntro: true, difficulty: DEFAULT_DIFFICULTY}
     },
     /** delete progress for this level */
     deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
       addLevelProgress(state, action)
-      state.games[action.payload.game].data[action.payload.world][action.payload.level] = initalLevelProgressState
+      state.games[action.payload.game.toLowerCase()].data[action.payload.world][action.payload.level] = initalLevelProgressState
     },
     /** load progress, e.g. from external import */
     loadProgress(state: ProgressState, action: PayloadAction<{game: string, data:GameProgressState}>) {
       console.debug(`setting data to:\n ${action.payload.data}`)
-      state.games[action.payload.game] = action.payload.data
+      state.games[action.payload.game.toLowerCase()] = action.payload.data
     },
     /** set the current inventory */
     changedInventory(state: ProgressState, action: PayloadAction<{game: string, inventory: string[]}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].inventory = action.payload.inventory
+      state.games[action.payload.game.toLowerCase()].inventory = action.payload.inventory
     },
     /** set the difficulty */
     changedDifficulty(state: ProgressState, action: PayloadAction<{game: string, difficulty: number}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].difficulty = action.payload.difficulty
+      state.games[action.payload.game.toLowerCase()].difficulty = action.payload.difficulty
     },
     /** set the difficulty */
     changedOpenedIntro(state: ProgressState, action: PayloadAction<{game: string, openedIntro: boolean}>) {
       addGameProgress(state, action)
-      state.games[action.payload.game].openedIntro = action.payload.openedIntro
+      state.games[action.payload.game.toLowerCase()].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
+      state.games[action.payload.game.toLowerCase()].typewriterMode = action.payload.typewriterMode
     }
   }
 })
@@ -138,74 +138,74 @@ export const progressSlice = createSlice({
 /** if the level does not exist, return default values */
 export function selectLevel(game: string, world: string, level: number) {
   return (state) =>{
-    if (!state.progress.games[game]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()]) { return initalLevelProgressState }
-    if (!state.progress.games[game].data[world]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()].data[world]) { return initalLevelProgressState }
-    if (!state.progress.games[game].data[world][level]) { return initalLevelProgressState }
+    if (!state.progress.games[game.toLowerCase()].data[world][level]) { return initalLevelProgressState }
-    return state.progress.games[game].data[world][level]
+    return state.progress.games[game.toLowerCase()].data[world][level]
   }
 }
 
 /** return the code of the current level */
 export function selectCode(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).code
+    return selectLevel(game.toLowerCase(), world, level)(state).code
   }
 }
 
 /** return the current inventory */
 export function selectInventory(game: string) {
   return (state) => {
-    if (!state.progress.games[game]) { return [] }
+    if (!state.progress.games[game.toLowerCase()]) { return [] }
-    return state.progress.games[game].inventory
+    return state.progress.games[game.toLowerCase()].inventory
   }
 }
 
 /** return the code of the current level */
 export function selectHelp(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).help
+    return selectLevel(game.toLowerCase(), world, level)(state).help
   }
 }
 
 /** return the selections made in the current level */
 export function selectSelections(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).selections
+    return selectLevel(game.toLowerCase(), world, level)(state).selections
   }
 }
 
 /** return whether the current level is clompleted */
 export function selectCompleted(game: string, world: string, level: number) {
   return (state) => {
-    return selectLevel(game, world, level)(state).completed
+    return selectLevel(game.toLowerCase(), world, level)(state).completed
   }
 }
 
 /** return progress for the current game if it exists */
 export function selectProgress(game: string) {
   return (state) => {
-    return state.progress.games[game] ?? null
+    return state.progress.games[game.toLowerCase()] ?? null
   }
 }
 
 /** return difficulty for the current game if it exists */
 export function selectDifficulty(game: string) {
   return (state) => {
-    return state.progress.games[game]?.difficulty ?? DEFAULT_DIFFICULTY
+    return state.progress.games[game.toLowerCase()]?.difficulty ?? DEFAULT_DIFFICULTY
   }
 }
 
 /** return whether the intro has been read */
 export function selectOpenedIntro(game: string) {
   return (state) => {
-    return state.progress.games[game]?.openedIntro
+    return state.progress.games[game.toLowerCase()]?.openedIntro
   }
 }
 
 /** return typewriter mode for the current game if it exists */
 export function selectTypewriterMode(game: string) {
   return (state) => {
-    return state.progress.games[game]?.typewriterMode ?? true
+    return state.progress.games[game.toLowerCase()]?.typewriterMode ?? true
   }
 }
 

client/src/state/store.ts

@@ -8,7 +8,7 @@ import { connection } from '../connection'
 import { apiSlice } from './api'
 import { progressSlice } from './progress'
 import { preferencesSlice } from "./preferences"
-import { saveState, savePreferences } from "./local_storage";
+import { saveState, savePreferences, removePreferences} from "./local_storage";
 
 
 export const store = configureStore({
@@ -29,7 +29,9 @@ export const store = configureStore({
 store.subscribe(
   debounce(() => {
     saveState(store.getState()[progressSlice.name]);
-    savePreferences(store.getState()[preferencesSlice.name]);
+
+    const preferencesState = store.getState()[preferencesSlice.name]
+    preferencesState.isSavePreferences ? savePreferences(preferencesState) : removePreferences()
   }, 800)
 );
 

doc/DOCUMENTATION.md

@@ -8,7 +8,7 @@ relays messages between the lean server and the client. `index.mjs` is the file
 be run, which is done for example using `pm2` or by calling `npm run start_server` or
 `npm run production`, see more later.
 
-The latter, "server", is the lean server which has two jobs. For one it produces the "gameserver"
+The latter, "server", is the lean server which has two jobs. For one, it produces the "gameserver"
 executable which is the lean server that handles the files the player plays on. The second job
 is to provide the lean commands which are used when creating a game. These are located in
 `Commands.lean`.
@@ -27,7 +27,7 @@ saved to lean env-extensions which the lean server has access to after loading t
 
 For games to be run successfully, it is important that the "gameserver" executable inside
 the game's `.lake` folder is actually built.
-Currently this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
+Currently, this happens through a lake-post-update-hook when calling `lake update -R` (in the game's folder), but if this fails, you can always build it manually by calling `lake build gameserver`.
 (both commands are to be executed in the game's directory!)
 
 ## Modifying the server
@@ -50,7 +50,7 @@ npm run start_client
 npm run production
 ```
 
-(in two separate terminals) to test the production modus of the server. This way it will only
+(in two separate terminals) to test the production mode of the server. This way it will only
 change once you build and restart the server.
 
 ### Modifying the lean server

doc/changelog.md

@@ -0,0 +1,9 @@
+# Changelog
+
+## v4.5.0
+
+### Breaking changes
+
+* Fix (#183): local store accepts case insensitive URL. The game progress has previously been saved under case sensitive URLs. You might need to recover old progress from your browser storage.
+
+## Other

doc/create_game.md

@@ -98,7 +98,7 @@ This introduction text is shown when one first enters a world.
 1. Use the template above and make sure you import all levels of this world.
 1. In `Game.lean` import the world with `import Game.Levels.MyWorld`
 
-Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently it shows
+Now you created a world with one level and added it🎉 The command `MakeGame` in `Game.lean` shows you any problems you might need to fix. Currently, it shows
 
 ```text
 No world introducing sorry, but required by MyWorld
@@ -125,26 +125,32 @@ The player has an inventory with tactics, theorems, and definitions that unlock
 
 ```lean
 NewTactic induction simp
-NewLemma Nat.zero_mul
+NewTheorem Nat.zero_mul
 NewDefinition Pow
 ```
 
 **Important:** All commands in this section 6a) expect the `Name` they take as input
-to be **fully qualified**. For example `NewLemma Nat.zero_mul` and not `NewLemma zero_mul`.
+to be **fully qualified**. For example `NewTheorem Nat.zero_mul` and not `NewTheorem zero_mul`.
 
 #### Doc entries
 
-You'll see a warning about a missing Lemma documentation. You can fix it by adding doc-entries like the following somewhere above it.
+You'll see a warning about a missing Theorem documentation. You can fix it by adding doc-entries like the following somewhere above it.
 
 ```lean
-LemmaDoc Nat.zero_mul as "zero_mul" in "Mul"
+/--
-"some description"
+some description
+-/
+TheoremDoc Nat.zero_mul as "zero_mul" in "Mul"
 
+/--
+some description
+-/
 TacticDoc simp
-"some description"
 
+/--
+some description
+-/
 DefinitionDoc Pow as "^"
-"some description"
 ```
 
 (e.g. you could also create a file `Game/Doc/MyTheorems.lean`, add there your documentation and import it)
@@ -156,7 +162,7 @@ If you do not provide any content for the inventory, the game will try to find a
 You have a few options to disable inventory items that have been unlocked in previous levels:
 
 ```lean
-DisableTactic, DisableLemma, OnlyTactic, OnlyLemma
+DisabledTactic, DisabledTheorem, OnlyTactic, OnlyTheorem
 ```
 
 have the same syntax as above. The former two disable items for this level, the latter two
@@ -164,7 +170,7 @@ disable all items except the ones specified.
 
 #### Theorem Tab
 
-Theorems are sorted into tabs. with `LemmaTab "Mul"` you specify which tab should be open by default in this level.
+Theorems are sorted into tabs. With `TheoremTab "Mul"` you specify which tab should be open by default in this level.
 
 #### HiddenTactic
 
@@ -179,7 +185,7 @@ and only `rw` would show up in the inventory.
 
 ### 6. b) Statement
 
-The statement is the exercise of the level. the basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
+The statement is the exercise of the level. The basics work the same as they would in `example` or `theorem`. Note however, that you **must** do a tactic proof, i.e. the `:= by` is a hard-coded part of the syntax
 
 #### Name
 
@@ -210,12 +216,12 @@ Statement my_simp_lemma ...
 
 The proof must always be a tactic proof, i.e. `:= by` is a mandatory part of the syntax.
 
-There are a few extra tactics that help you structuring the proof:
+There are a few extra tactics that help you with structuring the proof:
 
 - `Hint`: You can use `Hint "text"` to display text if the goal state in-game matches
   the one where `Hint` is placed. For more options about hints, see below.
 - `Branch`: In the proof you can add a `Branch` that runs an alternative tactic sequence, which
-  helps setting `Hints` in different places. The `Branch` does not affect the main
+  helps to set `Hints` in different places. The `Branch` does not affect the main
   proof and does not need to finish any goals.
 - `Template`/`Hole`: Used to provide a sample proof template. Anything inside `Template`
   will be copied into the editor with all `Hole`s replaced with `sorry`. Note that
@@ -230,7 +236,7 @@ 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.
 
-Read [More about Hints](doc/hints.md) for how they work and what the options are.
+Read [More about Hints](hints.md) for how they work and what the options are.
 
 ### 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.
@@ -242,11 +248,11 @@ NOTE: At present, only the images for a world are displayed. They appear in the
 
 ## 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).
+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](update_game.md).
 
 ## 8. Publish your game
 
-To publish your game on the official server, see [Publishing a game](doc/publish_game.md)
+To publish your game on the official server, see [Publishing a game](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:
 
@@ -258,7 +264,7 @@ Prerequisites "NNG"
 CoverImage "images/cover.png"
 ```
 * `Languages`: Currently only a single language (capital English name). The tile will show a corresponding flag.
-* `CaptionShort`: One catch phrase. Appears above the image.
+* `CaptionShort`: One catchphrase. 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.

doc/hints.md

@@ -10,7 +10,7 @@ Statement .... := by
   ...
 ```
 
-Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof.
+Note that hints are only **context-aware but not history-aware**. In particular, they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps to place hints outside the sample solution's proof.
 
 ## 1. When do hints show?
 
@@ -19,7 +19,7 @@ sample solutions and the entire context from the sample solutions is present in
 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
+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
@@ -32,12 +32,12 @@ Hidden hints are not filtered.
 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
+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`."
+  Hint "use `rw` or `rewrite`."
   Branch
     rewrite [h]
     Hint "now you still need `rfl`"

doc/publish_game.md

@@ -11,7 +11,7 @@ tab.
 
 ## 2. Import the game
 
-You call the URL that's listed under "What's Next?" in the latest action run. Explicitely you call
+You call the URL that's listed under "What's Next?" in the latest action run. Explicitly you call
 the URL of the form
 
 > adam.math.hhu.de/import/trigger/{USER}/{REPOSITORY}

doc/running_locally.md

@@ -2,7 +2,7 @@
 
 The installation instructions are not yet tested on Mac/Windows. Comments very welcome!
 
-Please also consult the [Troubleshooting Collection](doc/troubleshoot.md), where some known pitfalls are collected.
+Please also consult the [Troubleshooting Collection](troubleshoot.md), where some known pitfalls are collected.
 
 There are several options to play a game locally:
 
@@ -33,14 +33,14 @@ The template game [GameSkeleton](https://github.com/hhu-adam/GameSkeleton) conta
 
     * 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)*:<br/>
     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.
 
 ## 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".
+You can work on your game using Github codespaces (click "Code" and then "Codespaces" and then "create codespace on main"). 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, which might take a good while.
 
@@ -100,6 +100,29 @@ Run the game:
 npm start
 ```
 
+You should see a message like this:
+```bash
+[server] > lean4-game@0.1.0 start_server
+[server] > (cd server && lake build) && (cd relay && cross-env NODE_ENV=development nodemon -e mjs --exec "node ./index.mjs")
+[server]
+[client]
+[client] > lean4-game@0.1.0 start_client
+[client] > cross-env NODE_ENV=development vite --host
+[client]
+[server] [nodemon] 3.0.#
+[server] [nodemon] to restart at any time, enter `rs`
+[server] [nodemon] watching path(s): *.*
+[server] [nodemon] watching extensions: mjs
+[server] [nodemon] starting `node ./index.mjs`
+[client]
+[client]   VITE v4.5.1  ready in \#\#\# ms
+[client]
+[client]   ➜  Local:   http://localhost:3000/
+[client]   ➜  Network: http://###.###.###.##:3000/
+[client] [vite-plugin-static-copy] Collected 7 items.
+[server] (node:#####) [DEP0040] [server] Listening on 8080
+```
+
 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

doc/server.md

@@ -6,7 +6,7 @@ In order to set up the server to allow imports, one needs to create a
 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
+with your user name and access token. For example, you can set these in `ecosystem.config.cjs` if
 you're using `pm2`
 
 Then people can call:
@@ -22,7 +22,7 @@ where you replace:
 
 > https://{website}/#/g/{owner}/{repo}
 
-## data management
+## Data management
 Everything downloaded remains in the folder `lean4game/games`.
-the subfolder `tmp` contains downloaded artifacts and can be deleted without loss.
+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.

doc/troubleshoot.md

@@ -0,0 +1,37 @@
+# Troubleshooting
+
+Here are some issues experienced by users.
+
+- You can reset the lake projects involved (i.e. the `server/` folder here as well as your [game's folder](https://github.com/hhu-adam/GameSkeleton)) with the following commands:
+  ```
+  cd [THE PROJECT]
+  rm -rf .lake/
+  lake update -R
+  lake build
+  ```
+  If you experience problems related to Lean or lake, you should first try to reset it this way.
+
+# VSCode Dev-Container
+* If you don't get the pop-up, you might have disabled them, and you can reenable it by
+  running the `remote-containers.showReopenInContainerNotificationReset` command in vscode.
+* If the starting the container fails, in particular with a message `Error: network xyz not found`,
+  you might have deleted stuff from docker via your shell. Try deleting the container and image
+  explicitly 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.
+
+
+# Manual Installation
+Here are known issues/pitfalls with the local setup using `npm`.
+
+* If `CDPATH` is set on your mac/linux system, it might provide issues with `npm start` resulting in a server crash or blank screen. In particular `npm start` will display
+  ```
+  [server] sh: line 0: cd: server: No such file or directory
+  [server] npm run start_server exited with code 1
+  ```
+  As a fix you might need to delete your manually set `CDPATH` environment variable.
+
+# Publication
+Errors concerning uploads to the server.
+
+* Your game overview loads but the server crashes on loading a level: Check your game's github action is identical to the [GameSkeleton's](https://github.com/hhu-adam/GameSkeleton/blob/main/.github/workflows/build.yml), in particular that there is a step about building the "`gameserver`-executable".

package.json

@@ -28,8 +28,8 @@
     "debounce": "^1.2.1",
     "express": "^4.18.2",
     "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
-    "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
+    "lean4web": "github:hhu-adam/lean4web#414d9e62638a392fca278761b4c61a1d2e138bc7",
-    "octokit": "^2.0.14",
+    "octokit": "^3.1.2",
     "path-browserify": "^1.0.1",
     "react": "^18.2.0",
     "react-dom": "^18.2.0",

relay/index.mjs

@@ -19,7 +19,8 @@ import { importTrigger, importStatus } from './import.mjs'
 const queueLength = {
   "g/hhu-adam/robo": 2,
   "g/hhu-adam/nng4": 5,
-  "g/djvelleman/stg4": 2,
+  "g/djvelleman/stg4": 0,
+  "g/trequetrum/lean4game-logic": 0,
 }
 
 const __filename = url.fileURLToPath(import.meta.url);

server/GameServer.lean

@@ -11,7 +11,7 @@ unsafe def main : List String → IO UInt32 := fun args => do
 
   -- TODO: remove this argument
   if args[0]? == some "--server" then
-    MyServer.FileWorker.workerMain {} args
+    GameServer.FileWorker.workerMain {} args
   else
     e.putStrLn s!"Expected `--server`"
     return 1

server/GameServer/FileWorker.lean

@@ -5,6 +5,7 @@ import GameServer.ImportModules
 import GameServer.SaveData
 
 namespace MyModule
+
 open Lean
 open Elab
 open Parser
@@ -48,7 +49,8 @@ partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
 
 end MyModule
 
-namespace MyServer.FileWorker
+namespace GameServer.FileWorker
+
 open Lean
 open Lean.Server
 open Lean.Server.FileWorker
@@ -57,22 +59,50 @@ open IO
 open Snapshots
 open JsonRpc
 
-structure GameWorkerState :=
+/--
+Game-specific state to be packed on top of the `Lean.Server.FileWorker.WorkerState`
+used by the lean server.
+-/
+structure WorkerState :=
+  /--
+  Collection of items which are considered unlocked.
+  Tactics and theorems are mixed together.
+  -/
   inventory : Array String
   /--
-  Check for tactics/theorems that are not unlocked.
+  Difficulty determines whether tactics/theorems can be locked.
-  0: no check
+  * 0: do not check
-  1: give warnings
+  * 1: give warnings when locked items are used
-  2: give errors
+  * 2: give errors when locked items are used
   -/
   difficulty : Nat
+  /--
+  `levelInfo` contains all the (static) information about the level which is not influenced
+  by the user's progress.
+  -/
   levelInfo : LevelInfo
-  deriving ToJson, FromJson
+deriving ToJson, FromJson
 
-abbrev GameWorkerM := StateT GameWorkerState Server.FileWorker.WorkerM
+/--
+Pack the `GameServer.FileWorker.WorkerState` on top of the normal worker monad
+`Server.FileWorker.WorkerM`.
+-/
+abbrev WorkerM := StateT WorkerState Server.FileWorker.WorkerM
 
 section Elab
 
+/-- Add a message. use `(severity := .warning)` to specify the severity-/
+def addMessage (info : SourceInfo) (inputCtx : Parser.InputContext)
+    (severity := MessageSeverity.warning) (s : MessageData) :
+    Elab.Command.CommandElabM Unit := do
+  modify fun st => { st with
+    messages := st.messages.add {
+      fileName := inputCtx.fileName
+      severity := severity
+      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      data     := s }}
+
+/-- Deprecated! -/
 def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : MessageData) :
     Elab.Command.CommandElabM Unit := do
   modify fun st => { st with
@@ -80,80 +110,96 @@ def addErrorMessage (info : SourceInfo) (inputCtx : Parser.InputContext) (s : Me
       fileName := inputCtx.fileName
       severity := MessageSeverity.error
       pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-        data     := s
+      data     := s }}
-      }
-    }
 
 -- TODO: use HashSet for allowed tactics?
-/-- Find all tactics in syntax object that are forbidden according to a
+/--
-set `allowed` of allowed tactics. -/
+Find all tactics in syntax object that are forbidden according to a
-partial def findForbiddenTactics (inputCtx : Parser.InputContext)
+set `allowed` of allowed tactics.
-    (gameWorkerState : GameWorkerState) (stx : Syntax) :
+-/
-    Elab.Command.CommandElabM Unit := do
+partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState : WorkerState)
-  let levelInfo := gameWorkerState.levelInfo
+    (stx : Syntax) : Elab.Command.CommandElabM Unit := do
+  let levelInfo := workerState.levelInfo
+  -- Parse the syntax object and look for tactics and declarations.
   match stx with
   | .missing => return ()
   | .node _info _kind args =>
+    -- Go inside a node.
     for arg in args do
-      findForbiddenTactics inputCtx gameWorkerState arg
+      findForbiddenTactics inputCtx workerState arg
   | .atom info val =>
-    -- ignore syntax elements that do not start with a letter
+    -- Atoms might be tactic names or other keywords.
-    -- and ignore "with" keyword
+    -- Note: We whitelisted known keywords because we cannot
-    let allowed := ["with", "fun", "at", "only", "by", "to"]
+    -- distinguish keywords from tactic names.
+    let allowed := ["with", "fun", "at", "only", "by", "to", "generalizing", "says"]
+    -- Ignore syntax elements that do not start with a letter or are listed above.
     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`
+      -- Treat `simp?` and `simp!` like `simp`
+      let val := val.dropRightWhile (fun c => c == '!' || c == '?')
       match levelInfo.tactics.find? (·.name.toString == val) with
       | none =>
-        -- Note: This case means that the tactic will never be introduced in the game.
+        -- Tactic will never be introduced in the game.
-        match gameWorkerState.inventory.find? (· == val) with
+        match workerState.inventory.find? (· == val) with
+        | some _ =>
+          -- Tactic is in the inventory, allow it.
+          -- Note: This case shouldn't be possible...
+          pure ()
         | none =>
-          addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
+          -- Tactic is not in the inventory.
-        | some _ => pure () -- tactic is in the inventory, allow it.
+          addMessageByDifficulty info s!"The tactic '{val}' is not available in this game!"
       | some tac =>
-        if tac.locked then
+        -- Tactic is introduced at some point in the game.
-          match gameWorkerState.inventory.find? (· == val) with
+        if tac.disabled then
+          -- Tactic is disabled in this level.
+          addMessageByDifficulty info s!"The tactic '{val}' is disabled in this level!"
+        else if tac.locked then
+          match workerState.inventory.find? (· == val) with
           | none =>
-            addWarningMessage info s!"You have not unlocked the tactic '{val}' yet!"
+            -- Tactic is marked as locked and not in the inventory.
-          | some _ => pure () -- tactic is in the inventory, allow it.
+            addMessageByDifficulty info s!"You have not unlocked the tactic '{val}' yet!"
-        else if tac.disabled then
+          | some _ =>
-          addWarningMessage info s!"The tactic '{val}' is disabled in this level!"
+            -- Tactic is in the inventory, allow it.
+            pure ()
   | .ident info _rawVal val _preresolved =>
+    -- Try to resolve the name
     let ns ←
       try resolveGlobalConst (mkIdent val)
-        catch | _ => pure [] -- catch "unknown constant" error
+      -- Catch "unknown constant" error
+      catch | _ => pure []
     for n in ns do
       let some (.thmInfo ..) := (← getEnv).find? n
-          | return () -- not a theorem -> ignore
+        -- Not a theorem, no checks needed.
-        -- Forbid the theorem we are proving currently
+        | return ()
       if some n = levelInfo.statementName then
-          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+        -- Forbid the theorem we are proving currently
+        addMessage info inputCtx (severity := .error)
+          s!"Structural recursion: you can't use '{n}' to proof itself!"
+      let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+      match theoremsAndDefs.find? (·.name == n) with
+      | none =>
+        -- Theorem will never be introduced in this game
+        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+      | some thm =>
+        -- Theorem is introduced at some point in the game.
+        if thm.disabled then
+          -- Theorem is disabled in this level.
+          addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
+        else if thm.locked then
+          -- Theorem is still locked.
+          addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
 
-        let lemmasAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
-        match lemmasAndDefs.find? (fun l => l.name == n) with
+  -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors
-        | none => addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
+  -- deppending on difficulty.
-        | some lem =>
+  let difficulty := workerState.difficulty
-          if lem.locked then
-            addWarningMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
-          else if lem.disabled then
-            addWarningMessage info s!"The lemma/definition '{n}' is disabled in this level!"
-where addWarningMessage (info : SourceInfo) (s : MessageData) :=
-  let difficulty := gameWorkerState.difficulty
   if difficulty > 0 then
-    modify fun st => { st with
+    addMessage info inputCtx (if difficulty > 1 then .error else .warning) s
-      messages := st.messages.add {
-        fileName := inputCtx.fileName
-        severity := if difficulty > 1 then MessageSeverity.error else MessageSeverity.warning
-        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
-        data     := s
-      }
-    }
   else pure ()
--- where addErrorMessage (info : SourceInfo) (s : MessageData) :=
---   pure ()
 
 open Elab Meta Expr in
+
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool)
-    (couldBeEndSnap : Bool) (gameWorkerState : GameWorkerState)
+    (couldBeEndSnap : Bool) (gameWorkerState : WorkerState)
     (initParams : Lsp.InitializeParams) : IO Snapshot := do
   -- Recognize end snap
   if inputCtx.input.atEnd snap.mpState.pos ∧ couldBeEndSnap then
@@ -287,7 +333,7 @@ where
 
   /-- Elaborates the next command after `parentSnap` and emits diagnostics into `hOut`. -/
   private def nextSnap (ctx : WorkerContext) (m : DocumentMeta) (cancelTk : CancelToken)
-      (gameWorkerState : GameWorkerState) (initParams : Lsp.InitializeParams)
+      (gameWorkerState : WorkerState) (initParams : Lsp.InitializeParams)
       : AsyncElabM (Option Snapshot) := do
     cancelTk.check
     let s ← get
@@ -327,7 +373,7 @@ where
 
   /-- Elaborates all commands after the last snap (at least the header snap is assumed to exist), emitting the diagnostics into `hOut`. -/
   def unfoldSnaps (m : DocumentMeta) (snaps : Array Snapshot) (cancelTk : CancelToken)
-      (startAfterMs : UInt32) (gameWorkerState : GameWorkerState)
+      (startAfterMs : UInt32) (gameWorkerState : WorkerState)
       : ReaderT WorkerContext IO (AsyncList ElabTaskError Snapshot) := do
     let ctx ← read
     let some headerSnap := snaps[0]? | panic! "empty snapshots"
@@ -350,7 +396,7 @@ end Elab
 section Updates
 
 /-- Given the new document, updates editable doc state. -/
-  def updateDocument (newMeta : DocumentMeta) : GameWorkerM Unit := do
+def updateDocument (newMeta : DocumentMeta) : WorkerM Unit := do
   let s ← get
   let ctx ← read
   let oldDoc := (← StateT.lift get).doc
@@ -402,12 +448,12 @@ end Updates
 
 section Initialization
 
-  def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
+def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
   input    := "" -- No header!
   fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
   fileMap  := default
 
-  def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
+def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) (hasWidgets : Bool)
     (gameDir : String) (module : Name):
     IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
   -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
@@ -467,8 +513,8 @@ section Initialization
     publishDiagnostics m headerSnap.diagnostics.toArray hOut
     return (headerSnap, srcSearchPath)
 
-  def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
+def initializeWorker (meta : DocumentMeta) (i o e : FS.Stream) (initParams : InitializeParams) (opts : Options)
-      (gameDir : String) (gameWorkerState : GameWorkerState) : IO (WorkerContext × WorkerState) := do
+    (gameDir : String) (gameWorkerState : WorkerState) : IO (WorkerContext × Server.FileWorker.WorkerState) := do
   let clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
 
   let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
@@ -499,7 +545,7 @@ end Initialization
 
 section NotificationHandling
 
-  def handleDidChange (p : DidChangeTextDocumentParams) : GameWorkerM Unit := do
+def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
   let docId := p.textDocument
   let changes := p.contentChanges
   let oldDoc := (← StateT.lift get).doc
@@ -516,26 +562,39 @@ end NotificationHandling
 
 section MessageHandling
 
-  def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do
+
-    let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) =>
+/--
+Modified notification handler.
+
+Compare to `Lean.Server.FileWorker.handleNotification`.
+We use the modified `WorkerM` and use our custom `handleDidChange`.
+
+-/
+def handleNotification (method : String) (params : Json) : WorkerM Unit := do
+  let handle := fun paramType [FromJson paramType] (handler : paramType → WorkerM Unit) =>
     (StateT.lift <| parseParams paramType params) >>= handler
   match method with
+  -- Modified `textDocument/didChange`, using a custom `handleDidChange`
   | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
+  -- unmodified
   | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
-    | "$/setTrace"        => pure ()
+  -- unmodified
   | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
+  -- unmodified
   | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
+  -- New. TODO: What is this for?
+  | "$/setTrace"        => pure ()
   | _                        => throwServerError s!"Got unsupported notification method: {method}"
 
 end MessageHandling
 
 section MainLoop
-  partial def mainLoop : GameWorkerM Unit := do
+
-    let ctx ← read
+/--
-    let mut st ← StateT.lift get
+Erase finished tasks if there are no errors.
-    let msg ← ctx.hIn.readLspMessage
+-/
-    let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (task : Task (Except IO.Error Unit))
+private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
-        : IO PendingRequestMap := do
+    (task : Task (Except IO.Error Unit)) : IO PendingRequestMap := do
   if (← hasFinished task) then
     /- Handler tasks are constructed so that the only possible errors here
     are failures of writing a response into the stream. -/
@@ -543,9 +602,17 @@ section MainLoop
       throwServerError s!"Failed responding to request {id}: {e}"
     pure <| acc.erase id
   else pure acc
-    let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests
-    st := { st with pendingRequests }
 
+/--
+The main-loop.
+-/
+partial def mainLoop : WorkerM Unit := do
+  let ctx ← read
+  let mut st ← StateT.lift get
+  let msg ← ctx.hIn.readLspMessage
+  let pendingRequests ← st.pendingRequests.foldM (fun acc id task =>
+    filterFinishedTasks acc id task) st.pendingRequests
+  st := { st with pendingRequests }
   -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
   for (id, seshRef) in st.rpcSessions do
     let sesh ← seshRef.get
@@ -553,23 +620,30 @@ section MainLoop
       st := { st with rpcSessions := st.rpcSessions.erase id }
 
   set st
+
+  -- Process the RPC-message and restart main-loop.
   match msg with
+  | Message.request id "shutdown" none =>
+    ctx.hOut.writeLspResponse ⟨id, Json.null⟩
+    mainLoop
   | Message.request id method (some params) =>
+    -- Requests are handled by the unmodified lean server.
     handleRequest id method (toJson params)
     mainLoop
   | Message.notification "exit" none =>
     let doc := st.doc
     doc.cancelTk.set
     return ()
-    | Message.request id "shutdown" none =>
-      ctx.hOut.writeLspResponse ⟨id, Json.null⟩
-      mainLoop
   | Message.notification method (some params) =>
+    -- Custom notification handler
     handleNotification method (toJson params)
     mainLoop
-    | _ => throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
+  | _ =>
+    throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
+
 end MainLoop
 
+
 def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : IO UInt32 := do
   let i ← maybeTee "fwIn.txt" false i
   let o ← maybeTee "fwOut.txt" true o
@@ -608,12 +682,13 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
     let levelInfo ← loadLevelData gameDir levelId.world levelId.level
     let some initializationOptions := initRequest.param.initializationOptions?
       | throwServerError "no initialization options found"
-    let gameWorkerState : GameWorkerState:= {
+    let gameWorkerState : WorkerState := {
       inventory := initializationOptions.inventory
       difficulty := initializationOptions.difficulty
       levelInfo
     }
     let (ctx, st) ← initializeWorker meta i o e initParams opts gameDir gameWorkerState
+    -- Run the main loop
     let _ ← StateRefT'.run (s := st) <| ReaderT.run (r := ctx) <|
       StateT.run (s := gameWorkerState) <| (mainLoop)
     return (0 : UInt32)
@@ -625,6 +700,11 @@ def initAndRunWorker (i o e : FS.Stream) (opts : Options) (gameDir : String) : I
       message := e.toString }] o
     return (1 : UInt32)
 
+/--
+The main function. Simply wrapping `initAndRunWorker`.
+
+TODO: The first arg `args[0]` is always expected to be `--server`. We could drop this completely.
+-/
 def workerMain (opts : Options) (args : List String): IO UInt32 := do
   let i ← IO.getStdin
   let o ← IO.getStdout
@@ -632,8 +712,9 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
   try
     let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
     let exitCode ← initAndRunWorker i o e opts gameDir
-    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't
+    -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit,
-    -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code
+    -- but we definitely don't want to do that in the case of the worker processes,
+    -- which can produce non-terminating tasks evaluating user code.
     o.flush
     e.flush
     IO.Process.exit exitCode.toUInt8
@@ -641,4 +722,4 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
     e.putStrLn s!"worker initialization error: {err}"
     return (1 : UInt32)
 
-end MyServer.FileWorker
+end GameServer.FileWorker

server/lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "af7f36db6e7e9e395710a70635f915e8e3a0e69b",
+   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.4.0",
+   "inputRev": "v4.5.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "GameServer",

server/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.4.0
+leanprover/lean4:v4.5.0