Merge branch 'dev'. Bump to v4.5.0

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 />
+            <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/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({ 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"])
+    }
 
-export function PreferencesPopup({ mobile, setMobile, lockMobile, setLockMobile, handleClose }: PreferencesPopupProps) {
     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'>
+                    <div className='preferences-item first leave-left-gap'>
                         <FormControlLabel
                             control={
-                            <Switch
+                                <Box sx={{ width: 300 }}>
-                                checked={mobile}
+                                    <Slider
-                                onChange={() => setMobile(!mobile)}
+                                        aria-label="Always visible"
-                                name="checked"
+                                        value={marks.find(item => item.key === layout).value}
-                                color="primary"
+                                        step={1}
-                            />
+                                        marks={marks}
+                                        max={2}
+                                        sx={{
+                                            '& .MuiSlider-track': { display: 'none', },
+                                        }}
+                                        onChange={handlerChangeLayout}
+                                    />
+                                </Box>
                             }
-                            label="Enable"
+                            label=""
-                            labelPlacement="start"
                         />
                     </div>
+                </div>
+
+                <div className='preferences-category tail-category'>
                     <div className='preferences-item'>
                         <FormControlLabel
                             control={
-                            <Switch
+                                <Switch
-                                checked={!lockMobile}
+                                    checked={isSavePreferences}
-                                onChange={() => setLockMobile(!lockMobile)}
+                                    onChange={() => setIsSavePreferences(!isSavePreferences)}
-                                name="checked"
+                                    name="checked"
-                                color="primary"
+                                    color="primary"
-                            />
+                                />
                             }
-                            label="Auto"
+                            label="Save my settings (in the browser store)"
-                            labelPlacement="start"
+                            labelPlacement="end"
                         />
                     </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/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

package-lock.json

@@ -32,7 +32,7 @@
         "express": "^4.18.2",
         "lean4-infoview": "https://gitpkg.now.sh/leanprover/vscode-lean4/lean4-infoview?de0062c",
         "lean4web": "github:hhu-adam/lean4web#b91645a7b88814675ba9f99817436d0a2ce3a0ec",
-        "octokit": "^2.0.14",
+        "octokit": "^3.1.2",
         "path-browserify": "^1.0.1",
         "react": "^18.2.0",
         "react-dom": "^18.2.0",
@@ -2843,341 +2843,335 @@
       }
     },
     "node_modules/@octokit/app": {
-      "version": "13.1.8",
+      "version": "14.0.2",
-      "resolved": "https://registry.npmjs.org/@octokit/app/-/app-13.1.8.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/app/-/app-14.0.2.tgz",
-      "integrity": "sha512-bCncePMguVyFpdBbnceFKfmPOuUD94T189GuQ0l00ZcQ+mX4hyPqnaWJlsXE2HSdA71eV7p8GPDZ+ErplTkzow==",
+      "integrity": "sha512-NCSCktSx+XmjuSUVn2dLfqQ9WIYePGP95SDJs4I9cn/0ZkeXcPkaoCLl64Us3dRKL2ozC7hArwze5Eu+/qt1tg==",
       "dependencies": {
-        "@octokit/auth-app": "^4.0.13",
+        "@octokit/auth-app": "^6.0.0",
-        "@octokit/auth-unauthenticated": "^3.0.0",
+        "@octokit/auth-unauthenticated": "^5.0.0",
-        "@octokit/core": "^4.0.0",
+        "@octokit/core": "^5.0.0",
-        "@octokit/oauth-app": "^4.0.7",
+        "@octokit/oauth-app": "^6.0.0",
-        "@octokit/plugin-paginate-rest": "^6.0.0",
+        "@octokit/plugin-paginate-rest": "^9.0.0",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
-        "@octokit/webhooks": "^10.0.0"
+        "@octokit/webhooks": "^12.0.4"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/auth-app": {
-      "version": "4.0.13",
+      "version": "6.0.3",
-      "resolved": "https://registry.npmjs.org/@octokit/auth-app/-/auth-app-4.0.13.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-app/-/auth-app-6.0.3.tgz",
-      "integrity": "sha512-NBQkmR/Zsc+8fWcVIFrwDgNXS7f4XDrkd9LHdi9DPQw1NdGHLviLzRO2ZBwTtepnwHXW5VTrVU9eFGijMUqllg==",
+      "integrity": "sha512-9N7IlBAKEJR3tJgPSubCxIDYGXSdc+2xbkjYpk9nCyqREnH8qEMoMhiEB1WgoA9yTFp91El92XNXAi+AjuKnfw==",
       "dependencies": {
-        "@octokit/auth-oauth-app": "^5.0.0",
+        "@octokit/auth-oauth-app": "^7.0.0",
-        "@octokit/auth-oauth-user": "^2.0.0",
+        "@octokit/auth-oauth-user": "^4.0.0",
-        "@octokit/request": "^6.0.0",
+        "@octokit/request": "^8.0.2",
-        "@octokit/request-error": "^3.0.0",
+        "@octokit/request-error": "^5.0.0",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "deprecation": "^2.3.1",
-        "lru-cache": "^9.0.0",
+        "lru-cache": "^10.0.0",
-        "universal-github-app-jwt": "^1.1.1",
+        "universal-github-app-jwt": "^1.1.2",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/auth-app/node_modules/lru-cache": {
-      "version": "9.1.2",
+      "version": "10.1.0",
-      "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-9.1.2.tgz",
+      "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-10.1.0.tgz",
-      "integrity": "sha512-ERJq3FOzJTxBbFjZ7iDs+NiK4VI9Wz+RdrrAB8dio1oV+YvdPzUEE4QNiT2VD51DkIbCYRUUzCRkssXCHqSnKQ==",
+      "integrity": "sha512-/1clY/ui8CzjKFyjdvwPWJUYKiFVXG2I2cY0ssG7h4+hwk+XOIX7ZSG9Q7TW8TW3Kp3BUSqgFWBLgL4PJ+Blag==",
       "engines": {
         "node": "14 || >=16.14"
       }
     },
     "node_modules/@octokit/auth-oauth-app": {
-      "version": "5.0.6",
+      "version": "7.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-app/-/auth-oauth-app-5.0.6.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-app/-/auth-oauth-app-7.0.1.tgz",
-      "integrity": "sha512-SxyfIBfeFcWd9Z/m1xa4LENTQ3l1y6Nrg31k2Dcb1jS5ov7pmwMJZ6OGX8q3K9slRgVpeAjNA1ipOAMHkieqyw==",
+      "integrity": "sha512-RE0KK0DCjCHXHlQBoubwlLijXEKfhMhKm9gO56xYvFmP1QTMb+vvwRPmQLLx0V+5AvV9N9I3lr1WyTzwL3rMDg==",
       "dependencies": {
-        "@octokit/auth-oauth-device": "^4.0.0",
+        "@octokit/auth-oauth-device": "^6.0.0",
-        "@octokit/auth-oauth-user": "^2.0.0",
+        "@octokit/auth-oauth-user": "^4.0.0",
-        "@octokit/request": "^6.0.0",
+        "@octokit/request": "^8.0.2",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "@types/btoa-lite": "^1.0.0",
         "btoa-lite": "^1.0.0",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/auth-oauth-device": {
-      "version": "4.0.5",
+      "version": "6.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-device/-/auth-oauth-device-4.0.5.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-device/-/auth-oauth-device-6.0.1.tgz",
-      "integrity": "sha512-XyhoWRTzf2ZX0aZ52a6Ew5S5VBAfwwx1QnC2Np6Et3MWQpZjlREIcbcvVZtkNuXp6Z9EeiSLSDUqm3C+aMEHzQ==",
+      "integrity": "sha512-yxU0rkL65QkjbqQedgVx3gmW7YM5fF+r5uaSj9tM/cQGVqloXcqP2xK90eTyYvl29arFVCW8Vz4H/t47mL0ELw==",
       "dependencies": {
-        "@octokit/oauth-methods": "^2.0.0",
+        "@octokit/oauth-methods": "^4.0.0",
-        "@octokit/request": "^6.0.0",
+        "@octokit/request": "^8.0.0",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/auth-oauth-user": {
-      "version": "2.1.2",
+      "version": "4.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-user/-/auth-oauth-user-2.1.2.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-oauth-user/-/auth-oauth-user-4.0.1.tgz",
-      "integrity": "sha512-kkRqNmFe7s5GQcojE3nSlF+AzYPpPv7kvP/xYEnE57584pixaFBH8Vovt+w5Y3E4zWUEOxjdLItmBTFAWECPAg==",
+      "integrity": "sha512-N94wWW09d0hleCnrO5wt5MxekatqEJ4zf+1vSe8MKMrhZ7gAXKFOKrDEZW2INltvBWJCyDUELgGRv8gfErH1Iw==",
       "dependencies": {
-        "@octokit/auth-oauth-device": "^4.0.0",
+        "@octokit/auth-oauth-device": "^6.0.0",
-        "@octokit/oauth-methods": "^2.0.0",
+        "@octokit/oauth-methods": "^4.0.0",
-        "@octokit/request": "^6.0.0",
+        "@octokit/request": "^8.0.2",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "btoa-lite": "^1.0.0",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/auth-token": {
-      "version": "3.0.4",
+      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/@octokit/auth-token/-/auth-token-3.0.4.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-token/-/auth-token-4.0.0.tgz",
-      "integrity": "sha512-TWFX7cZF2LXoCvdmJWY7XVPi74aSY0+FfBZNSXEXFkMpjcqsQwDSYVv5FhRFaI0V1ECnwbz4j59T/G+rXNWaIQ==",
+      "integrity": "sha512-tY/msAuJo6ARbK6SPIxZrPBms3xPbfwBrulZe0Wtr/DIY9lje2HeV1uoebShn6mx7SjCHif6EjMvoREj+gZ+SA==",
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/auth-unauthenticated": {
-      "version": "3.0.5",
+      "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/auth-unauthenticated/-/auth-unauthenticated-3.0.5.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/auth-unauthenticated/-/auth-unauthenticated-5.0.1.tgz",
-      "integrity": "sha512-yH2GPFcjrTvDWPwJWWCh0tPPtTL5SMgivgKPA+6v/XmYN6hGQkAto8JtZibSKOpf8ipmeYhLNWQ2UgW0GYILCw==",
+      "integrity": "sha512-oxeWzmBFxWd+XolxKTc4zr+h3mt+yofn4r7OfoIkR/Cj/o70eEGmPsFbueyJE2iBAGpjgTnEOKM3pnuEGVmiqg==",
       "dependencies": {
-        "@octokit/request-error": "^3.0.0",
+        "@octokit/request-error": "^5.0.0",
-        "@octokit/types": "^9.0.0"
+        "@octokit/types": "^12.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/core": {
-      "version": "4.2.4",
+      "version": "5.0.2",
-      "resolved": "https://registry.npmjs.org/@octokit/core/-/core-4.2.4.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/core/-/core-5.0.2.tgz",
-      "integrity": "sha512-rYKilwgzQ7/imScn3M9/pFfUf4I1AZEH3KhyJmtPdE2zfaXAn2mFfUy4FbKewzc2We5y/LlKLj36fWJLKC2SIQ==",
+      "integrity": "sha512-cZUy1gUvd4vttMic7C0lwPed8IYXWYp8kHIMatyhY8t8n3Cpw2ILczkV5pGMPqef7v0bLo0pOHrEHarsau2Ydg==",
       "dependencies": {
-        "@octokit/auth-token": "^3.0.0",
+        "@octokit/auth-token": "^4.0.0",
-        "@octokit/graphql": "^5.0.0",
+        "@octokit/graphql": "^7.0.0",
-        "@octokit/request": "^6.0.0",
+        "@octokit/request": "^8.0.2",
-        "@octokit/request-error": "^3.0.0",
+        "@octokit/request-error": "^5.0.0",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "before-after-hook": "^2.2.0",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/endpoint": {
-      "version": "7.0.6",
+      "version": "9.0.4",
-      "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-7.0.6.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-9.0.4.tgz",
-      "integrity": "sha512-5L4fseVRUsDFGR00tMWD/Trdeeihn999rTMGRMC1G/Ldi1uWlWJzI98H4Iak5DB/RVvQuyMYKqSK/R6mbSOQyg==",
+      "integrity": "sha512-DWPLtr1Kz3tv8L0UvXTDP1fNwM0S+z6EJpRcvH66orY6Eld4XBMCSYsaWp4xIm61jTWxK68BrR7ibO+vSDnZqw==",
       "dependencies": {
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
-        "is-plain-object": "^5.0.0",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/graphql": {
-      "version": "5.0.6",
+      "version": "7.0.2",
-      "resolved": "https://registry.npmjs.org/@octokit/graphql/-/graphql-5.0.6.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/graphql/-/graphql-7.0.2.tgz",
-      "integrity": "sha512-Fxyxdy/JH0MnIB5h+UQ3yCoh1FG4kWXfFKkpWqjZHw/p+Kc8Y44Hu/kCgNBT6nU1shNumEchmW/sUO1JuQnPcw==",
+      "integrity": "sha512-OJ2iGMtj5Tg3s6RaXH22cJcxXRi7Y3EBqbHTBRq+PQAqfaS8f/236fUrWhfSn8P4jovyzqucxme7/vWSSZBX2Q==",
       "dependencies": {
-        "@octokit/request": "^6.0.0",
+        "@octokit/request": "^8.0.1",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/oauth-app": {
-      "version": "4.2.4",
+      "version": "6.0.0",
-      "resolved": "https://registry.npmjs.org/@octokit/oauth-app/-/oauth-app-4.2.4.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/oauth-app/-/oauth-app-6.0.0.tgz",
-      "integrity": "sha512-iuOVFrmm5ZKNavRtYu5bZTtmlKLc5uVgpqTfMEqYYf2OkieV6VdxKZAb5qLVdEPL8LU2lMWcGpavPBV835cgoA==",
+      "integrity": "sha512-bNMkS+vJ6oz2hCyraT9ZfTpAQ8dZNqJJQVNaKjPLx4ue5RZiFdU1YWXguOPR8AaSHS+lKe+lR3abn2siGd+zow==",
       "dependencies": {
-        "@octokit/auth-oauth-app": "^5.0.0",
+        "@octokit/auth-oauth-app": "^7.0.0",
-        "@octokit/auth-oauth-user": "^2.0.0",
+        "@octokit/auth-oauth-user": "^4.0.0",
-        "@octokit/auth-unauthenticated": "^3.0.0",
+        "@octokit/auth-unauthenticated": "^5.0.0",
-        "@octokit/core": "^4.0.0",
+        "@octokit/core": "^5.0.0",
-        "@octokit/oauth-authorization-url": "^5.0.0",
+        "@octokit/oauth-authorization-url": "^6.0.2",
-        "@octokit/oauth-methods": "^2.0.0",
+        "@octokit/oauth-methods": "^4.0.0",
         "@types/aws-lambda": "^8.10.83",
-        "fromentries": "^1.3.1",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/oauth-authorization-url": {
-      "version": "5.0.0",
+      "version": "6.0.2",
-      "resolved": "https://registry.npmjs.org/@octokit/oauth-authorization-url/-/oauth-authorization-url-5.0.0.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/oauth-authorization-url/-/oauth-authorization-url-6.0.2.tgz",
-      "integrity": "sha512-y1WhN+ERDZTh0qZ4SR+zotgsQUE1ysKnvBt1hvDRB2WRzYtVKQjn97HEPzoehh66Fj9LwNdlZh+p6TJatT0zzg==",
+      "integrity": "sha512-CdoJukjXXxqLNK4y/VOiVzQVjibqoj/xHgInekviUJV73y/BSIcwvJ/4aNHPBPKcPWFnd4/lO9uqRV65jXhcLA==",
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/oauth-methods": {
-      "version": "2.0.6",
+      "version": "4.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/oauth-methods/-/oauth-methods-2.0.6.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/oauth-methods/-/oauth-methods-4.0.1.tgz",
-      "integrity": "sha512-l9Uml2iGN2aTWLZcm8hV+neBiFXAQ9+3sKiQe/sgumHlL6HDg0AQ8/l16xX/5jJvfxueqTW5CWbzd0MjnlfHZw==",
+      "integrity": "sha512-1NdTGCoBHyD6J0n2WGXg9+yDLZrRNZ0moTEex/LSPr49m530WNKcCfXDghofYptr3st3eTii+EHoG5k/o+vbtw==",
       "dependencies": {
-        "@octokit/oauth-authorization-url": "^5.0.0",
+        "@octokit/oauth-authorization-url": "^6.0.2",
-        "@octokit/request": "^6.2.3",
+        "@octokit/request": "^8.0.2",
-        "@octokit/request-error": "^3.0.3",
+        "@octokit/request-error": "^5.0.0",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "btoa-lite": "^1.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/openapi-types": {
-      "version": "18.1.1",
+      "version": "19.1.0",
-      "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-18.1.1.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-19.1.0.tgz",
-      "integrity": "sha512-VRaeH8nCDtF5aXWnjPuEMIYf1itK/s3JYyJcWFJT8X9pSNnBtriDf7wlEWsGuhPLl4QIH4xM8fqTXDwJ3Mu6sw=="
+      "integrity": "sha512-6G+ywGClliGQwRsjvqVYpklIfa7oRPA0vyhPQG/1Feh+B+wU0vGH1JiJ5T25d3g1JZYBHzR2qefLi9x8Gt+cpw=="
     },
-    "node_modules/@octokit/plugin-paginate-rest": {
+    "node_modules/@octokit/plugin-paginate-graphql": {
-      "version": "6.1.2",
+      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/@octokit/plugin-paginate-rest/-/plugin-paginate-rest-6.1.2.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/plugin-paginate-graphql/-/plugin-paginate-graphql-4.0.0.tgz",
-      "integrity": "sha512-qhrmtQeHU/IivxucOV1bbI/xZyC/iOBhclokv7Sut5vnejAIAEXVcGQeRpQlU39E0WwK9lNvJHphHri/DB6lbQ==",
+      "integrity": "sha512-7HcYW5tP7/Z6AETAPU14gp5H5KmCPT3hmJrS/5tO7HIgbwenYmgw4OY9Ma54FDySuxMwD+wsJlxtuGWwuZuItA==",
-      "dependencies": {
-        "@octokit/tsconfig": "^1.0.2",
-        "@octokit/types": "^9.2.3"
-      },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       },
       "peerDependencies": {
-        "@octokit/core": ">=4"
+        "@octokit/core": ">=5"
+      }
+    },
+    "node_modules/@octokit/plugin-paginate-rest": {
+      "version": "9.1.5",
+      "resolved": "https://registry.npmjs.org/@octokit/plugin-paginate-rest/-/plugin-paginate-rest-9.1.5.tgz",
+      "integrity": "sha512-WKTQXxK+bu49qzwv4qKbMMRXej1DU2gq017euWyKVudA6MldaSSQuxtz+vGbhxV4CjxpUxjZu6rM2wfc1FiWVg==",
+      "dependencies": {
+        "@octokit/types": "^12.4.0"
+      },
+      "engines": {
+        "node": ">= 18"
+      },
+      "peerDependencies": {
+        "@octokit/core": ">=5"
       }
     },
     "node_modules/@octokit/plugin-rest-endpoint-methods": {
-      "version": "7.2.3",
+      "version": "10.2.0",
-      "resolved": "https://registry.npmjs.org/@octokit/plugin-rest-endpoint-methods/-/plugin-rest-endpoint-methods-7.2.3.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/plugin-rest-endpoint-methods/-/plugin-rest-endpoint-methods-10.2.0.tgz",
-      "integrity": "sha512-I5Gml6kTAkzVlN7KCtjOM+Ruwe/rQppp0QU372K1GP7kNOYEKe8Xn5BW4sE62JAHdwpq95OQK/qGNyKQMUzVgA==",
+      "integrity": "sha512-ePbgBMYtGoRNXDyKGvr9cyHjQ163PbwD0y1MkDJCpkO2YH4OeXX40c4wYHKikHGZcpGPbcRLuy0unPUuafco8Q==",
       "dependencies": {
-        "@octokit/types": "^10.0.0"
+        "@octokit/types": "^12.3.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       },
       "peerDependencies": {
-        "@octokit/core": ">=3"
+        "@octokit/core": ">=5"
-      }
-    },
-    "node_modules/@octokit/plugin-rest-endpoint-methods/node_modules/@octokit/types": {
-      "version": "10.0.0",
-      "resolved": "https://registry.npmjs.org/@octokit/types/-/types-10.0.0.tgz",
-      "integrity": "sha512-Vm8IddVmhCgU1fxC1eyinpwqzXPEYu0NrYzD3YZjlGjyftdLBTeqNblRC0jmJmgxbJIsQlyogVeGnrNaaMVzIg==",
-      "dependencies": {
-        "@octokit/openapi-types": "^18.0.0"
       }
     },
     "node_modules/@octokit/plugin-retry": {
-      "version": "4.1.6",
+      "version": "6.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/plugin-retry/-/plugin-retry-4.1.6.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/plugin-retry/-/plugin-retry-6.0.1.tgz",
-      "integrity": "sha512-obkYzIgEC75r8+9Pnfiiqy3y/x1bc3QLE5B7qvv9wi9Kj0R5tGQFC6QMBg1154WQ9lAVypuQDGyp3hNpp15gQQ==",
+      "integrity": "sha512-SKs+Tz9oj0g4p28qkZwl/topGcb0k0qPNX/i7vBKmDsjoeqnVfFUquqrE/O9oJY7+oLzdCtkiWSXLpLjvl6uog==",
       "dependencies": {
-        "@octokit/types": "^9.0.0",
+        "@octokit/request-error": "^5.0.0",
+        "@octokit/types": "^12.0.0",
         "bottleneck": "^2.15.3"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       },
       "peerDependencies": {
-        "@octokit/core": ">=3"
+        "@octokit/core": ">=5"
       }
     },
     "node_modules/@octokit/plugin-throttling": {
-      "version": "5.2.3",
+      "version": "8.1.3",
-      "resolved": "https://registry.npmjs.org/@octokit/plugin-throttling/-/plugin-throttling-5.2.3.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/plugin-throttling/-/plugin-throttling-8.1.3.tgz",
-      "integrity": "sha512-C9CFg9mrf6cugneKiaI841iG8DOv6P5XXkjmiNNut+swePxQ7RWEdAZRp5rJoE1hjsIqiYcKa/ZkOQ+ujPI39Q==",
+      "integrity": "sha512-pfyqaqpc0EXh5Cn4HX9lWYsZ4gGbjnSmUILeu4u2gnuM50K/wIk9s1Pxt3lVeVwekmITgN/nJdoh43Ka+vye8A==",
       "dependencies": {
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.2.0",
         "bottleneck": "^2.15.3"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       },
       "peerDependencies": {
-        "@octokit/core": "^4.0.0"
+        "@octokit/core": "^5.0.0"
       }
     },
     "node_modules/@octokit/request": {
-      "version": "6.2.8",
+      "version": "8.1.6",
-      "resolved": "https://registry.npmjs.org/@octokit/request/-/request-6.2.8.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/request/-/request-8.1.6.tgz",
-      "integrity": "sha512-ow4+pkVQ+6XVVsekSYBzJC0VTVvh/FCTUUgTsboGq+DTeWdyIFV8WSCdo0RIxk6wSkBTHqIK1mYuY7nOBXOchw==",
+      "integrity": "sha512-YhPaGml3ncZC1NfXpP3WZ7iliL1ap6tLkAp6MvbK2fTTPytzVUyUesBBogcdMm86uRYO5rHaM1xIWxigWZ17MQ==",
       "dependencies": {
-        "@octokit/endpoint": "^7.0.0",
+        "@octokit/endpoint": "^9.0.0",
-        "@octokit/request-error": "^3.0.0",
+        "@octokit/request-error": "^5.0.0",
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
-        "is-plain-object": "^5.0.0",
-        "node-fetch": "^2.6.7",
         "universal-user-agent": "^6.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/request-error": {
-      "version": "3.0.3",
+      "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-3.0.3.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-5.0.1.tgz",
-      "integrity": "sha512-crqw3V5Iy2uOU5Np+8M/YexTlT8zxCfI+qu+LxUB7SZpje4Qmx3mub5DfEKSO8Ylyk0aogi6TYdf6kxzh2BguQ==",
+      "integrity": "sha512-X7pnyTMV7MgtGmiXBwmO6M5kIPrntOXdyKZLigNfQWSEQzVxR4a4vo49vJjTWX70mPndj8KhfT4Dx+2Ng3vnBQ==",
       "dependencies": {
-        "@octokit/types": "^9.0.0",
+        "@octokit/types": "^12.0.0",
         "deprecation": "^2.0.0",
         "once": "^1.4.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
-    "node_modules/@octokit/tsconfig": {
-      "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/@octokit/tsconfig/-/tsconfig-1.0.2.tgz",
-      "integrity": "sha512-I0vDR0rdtP8p2lGMzvsJzbhdOWy405HcGovrspJ8RRibHnyRgggUSNO5AIox5LmqiwmatHKYsvj6VGFHkqS7lA=="
-    },
     "node_modules/@octokit/types": {
-      "version": "9.3.2",
+      "version": "12.4.0",
-      "resolved": "https://registry.npmjs.org/@octokit/types/-/types-9.3.2.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/types/-/types-12.4.0.tgz",
-      "integrity": "sha512-D4iHGTdAnEEVsB8fl95m1hiz7D5YiRdQ9b/OEb3BYRVwbLsGHcRVPz+u+BgRLNk0Q0/4iZCBqDN96j2XNxfXrA==",
+      "integrity": "sha512-FLWs/AvZllw/AGVs+nJ+ELCDZZJk+kY0zMen118xhL2zD0s1etIUHm1odgjP7epxYU1ln7SZxEUWYop5bhsdgQ==",
       "dependencies": {
-        "@octokit/openapi-types": "^18.0.0"
+        "@octokit/openapi-types": "^19.1.0"
       }
     },
     "node_modules/@octokit/webhooks": {
-      "version": "10.9.1",
+      "version": "12.0.11",
-      "resolved": "https://registry.npmjs.org/@octokit/webhooks/-/webhooks-10.9.1.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/webhooks/-/webhooks-12.0.11.tgz",
-      "integrity": "sha512-5NXU4VfsNOo2VSU/SrLrpPH2Z1ZVDOWFcET4EpnEBX1uh/v8Uz65UVuHIRx5TZiXhnWyRE9AO1PXHa+M/iWwZA==",
+      "integrity": "sha512-YEQOb7v0TZ662nh5jsbY1CMgJyMajCEagKrHWC30LTCwCtnuIrLtEpE20vq4AtH0SuZI90+PtV66/Bnnw0jkvg==",
       "dependencies": {
-        "@octokit/request-error": "^3.0.0",
+        "@octokit/request-error": "^5.0.0",
-        "@octokit/webhooks-methods": "^3.0.0",
+        "@octokit/webhooks-methods": "^4.0.0",
-        "@octokit/webhooks-types": "6.11.0",
+        "@octokit/webhooks-types": "7.1.0",
         "aggregate-error": "^3.1.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/webhooks-methods": {
-      "version": "3.0.3",
+      "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/@octokit/webhooks-methods/-/webhooks-methods-3.0.3.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/webhooks-methods/-/webhooks-methods-4.0.0.tgz",
-      "integrity": "sha512-2vM+DCNTJ5vL62O5LagMru6XnYhV4fJslK+5YUkTa6rWlW2S+Tqs1lF9Wr9OGqHfVwpBj3TeztWfVON/eUoW1Q==",
+      "integrity": "sha512-M8mwmTXp+VeolOS/kfRvsDdW+IO0qJ8kYodM/sAysk093q6ApgmBXwK1ZlUvAwXVrp/YVHp6aArj4auAxUAOFw==",
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/@octokit/webhooks-types": {
-      "version": "6.11.0",
+      "version": "7.1.0",
-      "resolved": "https://registry.npmjs.org/@octokit/webhooks-types/-/webhooks-types-6.11.0.tgz",
+      "resolved": "https://registry.npmjs.org/@octokit/webhooks-types/-/webhooks-types-7.1.0.tgz",
-      "integrity": "sha512-AanzbulOHljrku1NGfafxdpTCfw2ENaWzH01N2vqQM+cUFbk868Cgh0xylz0JIM9BoKbfI++bdD6EYX0Q/UTEw=="
+      "integrity": "sha512-y92CpG4kFFtBBjni8LHoV12IegJ+KFxLgKRengrVjKmGE5XMeCuGvlfRe75lTRrgXaG6XIWJlFpIDTlkoJsU8w=="
     },
     "node_modules/@pmmmwh/react-refresh-webpack-plugin": {
       "version": "0.5.11",
@@ -4932,9 +4926,9 @@
       "dev": true
     },
     "node_modules/@types/aws-lambda": {
-      "version": "8.10.124",
+      "version": "8.10.131",
-      "resolved": "https://registry.npmjs.org/@types/aws-lambda/-/aws-lambda-8.10.124.tgz",
+      "resolved": "https://registry.npmjs.org/@types/aws-lambda/-/aws-lambda-8.10.131.tgz",
-      "integrity": "sha512-PHqK0SuAkFS3tZjceqRXecxxrWIN3VqTicuialtK2wZmvBy7H9WGc3u3+wOgaZB7N8SpSXDpWk9qa7eorpTStg=="
+      "integrity": "sha512-IWmFpqnVDvskYWnNSiu/qlRn80XlIOU0Gy5rKCl/NjhnI95pV8qIHs6L5b+bpHhyzuOSzjLgBcwgFSXrC1nZWA=="
     },
     "node_modules/@types/body-parser": {
       "version": "1.19.3",
@@ -4960,9 +4954,9 @@
       }
     },
     "node_modules/@types/btoa-lite": {
-      "version": "1.0.0",
+      "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/@types/btoa-lite/-/btoa-lite-1.0.0.tgz",
+      "resolved": "https://registry.npmjs.org/@types/btoa-lite/-/btoa-lite-1.0.2.tgz",
-      "integrity": "sha512-wJsiX1tosQ+J5+bY5LrSahHxr2wT+uME5UDwdN1kg4frt40euqA+wzECkmq4t5QbveHiJepfdThgQrPw6KiSlg=="
+      "integrity": "sha512-ZYbcE2x7yrvNFJiU7xJGrpF/ihpkM7zKgw8bha3LNJSesvTtUNxbpzaT7WXBIryf6jovisrxTBvymxMeLLj1Mg=="
     },
     "node_modules/@types/connect": {
       "version": "3.4.36",
@@ -5130,9 +5124,9 @@
       "dev": true
     },
     "node_modules/@types/jsonwebtoken": {
-      "version": "9.0.3",
+      "version": "9.0.5",
-      "resolved": "https://registry.npmjs.org/@types/jsonwebtoken/-/jsonwebtoken-9.0.3.tgz",
+      "resolved": "https://registry.npmjs.org/@types/jsonwebtoken/-/jsonwebtoken-9.0.5.tgz",
-      "integrity": "sha512-b0jGiOgHtZ2jqdPgPnP6WLCXZk1T8p06A/vPGzUvxpFGgKMbjXJDjC5m52ErqBnIuWZFgGoIJyRdeG5AyreJjA==",
+      "integrity": "sha512-VRLSGzik+Unrup6BsouBeHsf4d1hOEgYWTm/7Nmw1sXoN1+tRly/Gy/po3yeahnP4jfnQWWAhQAqcNfH7ngOkA==",
       "dependencies": {
         "@types/node": "*"
       }
@@ -8007,9 +8001,9 @@
       }
     },
     "node_modules/follow-redirects": {
-      "version": "1.15.3",
+      "version": "1.15.4",
-      "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.3.tgz",
+      "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.15.4.tgz",
-      "integrity": "sha512-1VzOtuEM8pC9SFU1E+8KfTjZyMztRsgEfwQl44z8A25uy13jSzTj6dyK2Df52iV0vgHCfBwLhDWevLn95w5v6Q==",
+      "integrity": "sha512-Cr4D/5wlrb0z9dgERpUL3LrmPKVDsETIJhaCMeDfuFYcqa5bldGV6wBsAN6X/vxlXQtFBMrXdXxdL8CbDTGniw==",
       "funding": [
         {
           "type": "individual",
@@ -8071,25 +8065,6 @@
         "node": ">= 0.6"
       }
     },
-    "node_modules/fromentries": {
-      "version": "1.3.2",
-      "resolved": "https://registry.npmjs.org/fromentries/-/fromentries-1.3.2.tgz",
-      "integrity": "sha512-cHEpEQHUg0f8XdtZCc2ZAhrHzKzT0MrFUTcvx+hfxYu7rGMDc5SKoXFh+n4YigxsHXRzc6OrCshdR1bWH6HHyg==",
-      "funding": [
-        {
-          "type": "github",
-          "url": "https://github.com/sponsors/feross"
-        },
-        {
-          "type": "patreon",
-          "url": "https://www.patreon.com/feross"
-        },
-        {
-          "type": "consulting",
-          "url": "https://feross.org/support"
-        }
-      ]
-    },
     "node_modules/fs-extra": {
       "version": "8.1.0",
       "resolved": "https://registry.npmjs.org/fs-extra/-/fs-extra-8.1.0.tgz",
@@ -9120,14 +9095,6 @@
         "url": "https://github.com/sponsors/sindresorhus"
       }
     },
-    "node_modules/is-plain-object": {
-      "version": "5.0.0",
-      "resolved": "https://registry.npmjs.org/is-plain-object/-/is-plain-object-5.0.0.tgz",
-      "integrity": "sha512-VRSzKkbMm5jMDoKLbltAkFQ5Qr7VDiTFGXxYFXXowVj387GeGNOCsOH6Msy00SGZ3Fp84b1Naa1psqgcCIEP5Q==",
-      "engines": {
-        "node": ">=0.10.0"
-      }
-    },
     "node_modules/is-regex": {
       "version": "1.1.4",
       "resolved": "https://registry.npmjs.org/is-regex/-/is-regex-1.1.4.tgz",
@@ -12581,22 +12548,23 @@
       "peer": true
     },
     "node_modules/octokit": {
-      "version": "2.1.0",
+      "version": "3.1.2",
-      "resolved": "https://registry.npmjs.org/octokit/-/octokit-2.1.0.tgz",
+      "resolved": "https://registry.npmjs.org/octokit/-/octokit-3.1.2.tgz",
-      "integrity": "sha512-Pxi6uKTjBRZWgAwsw1NgHdRlL+QASCN35OYS7X79o7PtBME0CLXEroZmPtEwlWZbPTP+iDbEy2wCbSOgm0uGIQ==",
+      "integrity": "sha512-MG5qmrTL5y8KYwFgE1A4JWmgfQBaIETE/lOlfwNYx1QOtCQHGVxkRJmdUJltFc1HVn73d61TlMhMyNTOtMl+ng==",
       "dependencies": {
-        "@octokit/app": "^13.1.5",
+        "@octokit/app": "^14.0.2",
-        "@octokit/core": "^4.2.1",
+        "@octokit/core": "^5.0.0",
-        "@octokit/oauth-app": "^4.2.1",
+        "@octokit/oauth-app": "^6.0.0",
-        "@octokit/plugin-paginate-rest": "^6.1.0",
+        "@octokit/plugin-paginate-graphql": "^4.0.0",
-        "@octokit/plugin-rest-endpoint-methods": "^7.1.1",
+        "@octokit/plugin-paginate-rest": "^9.0.0",
-        "@octokit/plugin-retry": "^4.1.3",
+        "@octokit/plugin-rest-endpoint-methods": "^10.0.0",
-        "@octokit/plugin-throttling": "^5.2.2",
+        "@octokit/plugin-retry": "^6.0.0",
-        "@octokit/request-error": "^v3.0.3",
+        "@octokit/plugin-throttling": "^8.0.0",
-        "@octokit/types": "^9.2.2"
+        "@octokit/request-error": "^5.0.0",
+        "@octokit/types": "^12.0.0"
       },
       "engines": {
-        "node": ">= 14"
+        "node": ">= 18"
       }
     },
     "node_modules/on-finished": {
@@ -15473,18 +15441,18 @@
       }
     },
     "node_modules/universal-github-app-jwt": {
-      "version": "1.1.1",
+      "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/universal-github-app-jwt/-/universal-github-app-jwt-1.1.1.tgz",
+      "resolved": "https://registry.npmjs.org/universal-github-app-jwt/-/universal-github-app-jwt-1.1.2.tgz",
-      "integrity": "sha512-G33RTLrIBMFmlDV4u4CBF7dh71eWwykck4XgaxaIVeZKOYZRAAxvcGMRFTUclVY6xoUPQvO4Ne5wKGxYm/Yy9w==",
+      "integrity": "sha512-t1iB2FmLFE+yyJY9+3wMx0ejB+MQpEVkH0gQv7dR6FZyltyq+ZZO0uDpbopxhrZ3SLEO4dCEkIujOMldEQ2iOA==",
       "dependencies": {
         "@types/jsonwebtoken": "^9.0.0",
-        "jsonwebtoken": "^9.0.0"
+        "jsonwebtoken": "^9.0.2"
       }
     },
     "node_modules/universal-user-agent": {
-      "version": "6.0.0",
+      "version": "6.0.1",
-      "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.0.tgz",
+      "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.1.tgz",
-      "integrity": "sha512-isyNax3wXoKaulPDZWHQqbmIx1k2tb9fb3GGDBRxCscfYV2Ch7WxPArBsFEG8s/safwXTT7H4QGhaIkTp9447w=="
+      "integrity": "sha512-yCzhz6FN2wU1NiiQRogkTQszlQSlpWaw8SvVegAc+bDxbzHgh1vX8uIe8OYyMH6DwH+sdTJsgMl36+mSMdRJIQ=="
     },
     "node_modules/universalify": {
       "version": "0.1.2",

package.json

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

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,103 +59,147 @@ 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
-      messages := st.messages.add {
+    messages := st.messages.add {
-        fileName := inputCtx.fileName
+      fileName := inputCtx.fileName
-        severity := MessageSeverity.error
+      severity := MessageSeverity.error
-        pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      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 =>
-      let ns ←
+    -- Try to resolve the name
-        try resolveGlobalConst (mkIdent val)
+    let ns ←
-        catch | _ => pure [] -- catch "unknown constant" error
+      try resolveGlobalConst (mkIdent val)
-      for n in ns do
+      -- Catch "unknown constant" error
-        let some (.thmInfo ..) := (← getEnv).find? n
+      catch | _ => pure []
-          | return () -- not a theorem -> ignore
+    for n in ns do
+      let some (.thmInfo ..) := (← getEnv).find? n
+        -- Not a theorem, no checks needed.
+        | return ()
+      if some n = levelInfo.statementName then
         -- Forbid the theorem we are proving currently
-        if some n = levelInfo.statementName then
+        addMessage info inputCtx (severity := .error)
-          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+          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,226 +396,254 @@ 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 s ← get
-    let ctx ← read
+  let ctx ← read
-    let oldDoc := (← StateT.lift get).doc
+  let oldDoc := (← StateT.lift get).doc
-    oldDoc.cancelTk.set
+  oldDoc.cancelTk.set
-    let initHeaderStx := (← StateT.lift get).initHeaderStx
+  let initHeaderStx := (← StateT.lift get).initHeaderStx
-    let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
+  let (newHeaderStx, newMpState, _) ← Parser.parseHeader newMeta.mkInputContext
-    let cancelTk ← CancelToken.new
+  let cancelTk ← CancelToken.new
-    let headSnapTask := oldDoc.cmdSnaps.waitHead?
+  let headSnapTask := oldDoc.cmdSnaps.waitHead?
-    let newSnaps ← if initHeaderStx != newHeaderStx then
+  let newSnaps ← if initHeaderStx != newHeaderStx then
-      EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
+    EIO.asTask (ε := ElabTaskError) (prio := .dedicated) do
-        IO.sleep ctx.initParams.editDelay.toUInt32
+      IO.sleep ctx.initParams.editDelay.toUInt32
-        cancelTk.check
+      cancelTk.check
-        IO.Process.exit 2
+      IO.Process.exit 2
-    else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
+  else EIO.mapTask (ε := ElabTaskError) (t := headSnapTask) (prio := .dedicated) fun headSnap?? => do
-      -- There is always at least one snapshot absent exceptions
+    -- There is always at least one snapshot absent exceptions
-      let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
+    let some headSnap ← MonadExcept.ofExcept headSnap?? | panic! "empty snapshots"
-      let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
+    let newHeaderSnap := { headSnap with stx := newHeaderStx, mpState := newMpState }
-      let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
+    let changePos := oldDoc.meta.text.source.firstDiffPos newMeta.text.source
-      -- Ignore exceptions, we are only interested in the successful snapshots
+    -- Ignore exceptions, we are only interested in the successful snapshots
-      let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
+    let (cmdSnaps, _) ← oldDoc.cmdSnaps.getFinishedPrefix
-      -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
+    -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only
-      -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
+    -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead.
-      let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
+    let mut validSnaps ← pure (cmdSnaps.takeWhile (fun s => s.endPos < changePos))
-      if h : validSnaps.length ≤ 1 then
+    if h : validSnaps.length ≤ 1 then
-        validSnaps := [newHeaderSnap]
+      validSnaps := [newHeaderSnap]
-      else
+    else
-        /- When at least one valid non-header snap exists, it may happen that a change does not fall
+      /- When at least one valid non-header snap exists, it may happen that a change does not fall
-           within the syntactic range of that last snap but still modifies it by appending tokens.
+          within the syntactic range of that last snap but still modifies it by appending tokens.
-           We check for this here. We do not currently handle crazy grammars in which an appended
+          We check for this here. We do not currently handle crazy grammars in which an appended
-           token can merge two or more previous commands into one. To do so would require reparsing
+          token can merge two or more previous commands into one. To do so would require reparsing
-           the entire file. -/
+          the entire file. -/
-        have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
+      have : validSnaps.length ≥ 2 := Nat.gt_of_not_le h
-        let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
+      let mut lastSnap := validSnaps.getLast (by subst ·; simp at h)
-        let preLastSnap :=
+      let preLastSnap :=
-          have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
+        have : 0 < validSnaps.length := Nat.lt_of_lt_of_le (by decide) this
-          have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
+        have : validSnaps.length - 2 < validSnaps.length := Nat.sub_lt this (by decide)
-          validSnaps[validSnaps.length - 2]
+        validSnaps[validSnaps.length - 2]
-        let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
+      let newLastStx ← parseNextCmd newMeta.mkInputContext preLastSnap
-        if newLastStx != lastSnap.stx then
+      if newLastStx != lastSnap.stx then
-          validSnaps := validSnaps.dropLast
+        validSnaps := validSnaps.dropLast
-      -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
+    -- wait for a bit, giving the initial `cancelTk.check` in `nextCmdSnap` time to trigger
-      -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
+    -- before kicking off any expensive elaboration (TODO: make expensive elaboration cancelable)
-      unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
+    unfoldSnaps newMeta validSnaps.toArray cancelTk s ctx
-        (startAfterMs := ctx.initParams.editDelay.toUInt32)
+      (startAfterMs := ctx.initParams.editDelay.toUInt32)
-    StateT.lift <| modify fun st => { st with
+  StateT.lift <| modify fun st => { st with
-      doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
+    doc := { meta := newMeta, cmdSnaps := AsyncList.delayed newSnaps, cancelTk }}
 
 end Updates
 
 section Initialization
 
-  def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
+def DocumentMeta.mkInputContext (doc : DocumentMeta) : Parser.InputContext where
-    input    := "" -- No header!
+  input    := "" -- No header!
-    fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
+  fileName := (System.Uri.fileUriToPath? doc.uri).getD doc.uri |>.toString
-    fileMap  := default
+  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):
+    (gameDir : String) (module : Name):
-      IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
+    IO (Syntax × Task (Except Error (Snapshot × SearchPath))) := do
-    -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
+  -- Determine search paths of the game project by running `lake env printenv LEAN_PATH`.
-    let out ← IO.Process.output
+  let out ← IO.Process.output
-      { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
+    { cwd := gameDir, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
-    if out.exitCode != 0 then
+  if out.exitCode != 0 then
-      throwServerError s!"Error while running Lake: {out.stderr}"
+    throwServerError s!"Error while running Lake: {out.stderr}"
 
-    -- Make the paths relative to the current directory
+  -- Make the paths relative to the current directory
-    let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
+  let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
-    let currentDir ← IO.currentDir
+  let currentDir ← IO.currentDir
-    let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
+  let paths := paths.map fun p => currentDir / (gameDir : System.FilePath) / p
 
-    -- Set the search path
+  -- Set the search path
-    Lean.searchPathRef.set paths
+  Lean.searchPathRef.set paths
 
-    let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
+  let env ← importModules' #[{ module := `Init : Import }, { module := module : Import }]
 
-    -- use empty header
+  -- use empty header
-    let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
+  let (headerStx, headerParserState, msgLog) ← Parser.parseHeader
-      {m.mkInputContext with
+    {m.mkInputContext with
-        input := ""
+      input := ""
-        fileMap := FileMap.ofString ""}
+      fileMap := FileMap.ofString ""}
-    (headerStx, ·) <$> EIO.asTask do
+  (headerStx, ·) <$> EIO.asTask do
-      let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
+    let mut srcSearchPath : SearchPath := paths --← initSrcSearchPath (← getBuildDir)
-      let headerEnv := env
+    let headerEnv := env
-      let mut headerEnv := headerEnv
+    let mut headerEnv := headerEnv
-      try
+    try
-        if let some path := System.Uri.fileUriToPath? m.uri then
+      if let some path := System.Uri.fileUriToPath? m.uri then
-          headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
+        headerEnv := headerEnv.setMainModule (← moduleNameOfFileName path none)
-      catch _ => pure ()
+    catch _ => pure ()
-      let cmdState := Elab.Command.mkState headerEnv {} opts
+    let cmdState := Elab.Command.mkState headerEnv {} opts
-      let cmdState := { cmdState with infoState := {
+    let cmdState := { cmdState with infoState := {
-        enabled := true
+      enabled := true
-        trees := #[Elab.InfoTree.context ({
+      trees := #[Elab.InfoTree.context ({
-          env     := headerEnv
+        env     := headerEnv
-          fileMap := m.text
+        fileMap := m.text
-          ngen    := { namePrefix := `_worker }
+        ngen    := { namePrefix := `_worker }
-        }) (Elab.InfoTree.node
+      }) (Elab.InfoTree.node
-            (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
+          (Elab.Info.ofCommandInfo { elaborator := `header, stx := headerStx })
-            (headerStx[1].getArgs.toList.map (fun importStx =>
+          (headerStx[1].getArgs.toList.map (fun importStx =>
-              Elab.InfoTree.node (Elab.Info.ofCommandInfo {
+            Elab.InfoTree.node (Elab.Info.ofCommandInfo {
-                elaborator := `import
+              elaborator := `import
-                stx := importStx
+              stx := importStx
-              }) #[].toPArray'
+            }) #[].toPArray'
-            )).toPArray'
+          )).toPArray'
-        )].toPArray'
+      )].toPArray'
-      }}
+    }}
-      let headerSnap := {
+    let headerSnap := {
-        beginPos := 0
+      beginPos := 0
-        stx := headerStx
+      stx := headerStx
-        mpState := {}
+      mpState := {}
-        cmdState := cmdState
+      cmdState := cmdState
-        interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
+      interactiveDiags := ← cmdState.messages.msgs.mapM (Widget.msgToInteractiveDiagnostic m.text · hasWidgets)
-        tacticCache := (← IO.mkRef {})
+      tacticCache := (← IO.mkRef {})
-      }
+    }
-      publishDiagnostics m headerSnap.diagnostics.toArray hOut
+    publishDiagnostics m headerSnap.diagnostics.toArray hOut
-      return (headerSnap, srcSearchPath)
+    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 clientHasWidgets := initParams.initializationOptions?.bind (·.hasWidgets?) |>.getD false
 
-    let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
+  let (headerStx, headerTask) ← compileHeader meta o opts (hasWidgets := clientHasWidgets)
-      gameDir gameWorkerState.levelInfo.module
+    gameDir gameWorkerState.levelInfo.module
-    let cancelTk ← CancelToken.new
+  let cancelTk ← CancelToken.new
-    let ctx :=
+  let ctx :=
-      { hIn  := i
+    { hIn  := i
-        hOut := o
+      hOut := o
-        hLog := e
+      hLog := e
-        headerTask
+      headerTask
-        initParams
+      initParams
-        clientHasWidgets
+      clientHasWidgets
-      }
+    }
-    let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
+  let cmdSnaps ← EIO.mapTask (t := headerTask) (match · with
-      | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
+    | Except.ok (s, _) => unfoldSnaps meta #[s] cancelTk gameWorkerState ctx (startAfterMs := 0)
-      | Except.error e   => throw (e : ElabTaskError))
+    | Except.error e   => throw (e : ElabTaskError))
-    let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
+  let doc : EditableDocument := { meta, cmdSnaps := AsyncList.delayed cmdSnaps, cancelTk }
-    return (ctx,
+  return (ctx,
-    { doc             := doc
+  { doc             := doc
-      initHeaderStx   := headerStx
+    initHeaderStx   := headerStx
-      currHeaderStx      := headerStx
+    currHeaderStx      := headerStx
-      importCachingTask? := none
+    importCachingTask? := none
-      pendingRequests := RBMap.empty
+    pendingRequests := RBMap.empty
-      rpcSessions     := RBMap.empty
+    rpcSessions     := RBMap.empty
-    })
+  })
 
 end Initialization
 
 section NotificationHandling
 
-  def handleDidChange (p : DidChangeTextDocumentParams) : GameWorkerM Unit := do
+def handleDidChange (p : DidChangeTextDocumentParams) : WorkerM Unit := do
-    let docId := p.textDocument
+  let docId := p.textDocument
-    let changes := p.contentChanges
+  let changes := p.contentChanges
-    let oldDoc := (← StateT.lift get).doc
+  let oldDoc := (← StateT.lift get).doc
-    let some newVersion ← pure docId.version?
+  let some newVersion ← pure docId.version?
-      | throwServerError "Expected version number"
+    | throwServerError "Expected version number"
-    if newVersion ≤ oldDoc.meta.version then
+  if newVersion ≤ oldDoc.meta.version then
-      -- TODO(WN): This happens on restart sometimes.
+    -- TODO(WN): This happens on restart sometimes.
-      IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
+    IO.eprintln s!"Got outdated version number: {newVersion} ≤ {oldDoc.meta.version}"
-    else if ¬ changes.isEmpty then
+  else if ¬ changes.isEmpty then
-      let newDocText := foldDocumentChanges changes oldDoc.meta.text
+    let newDocText := foldDocumentChanges changes oldDoc.meta.text
-      updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
+    updateDocument ⟨docId.uri, newVersion, newDocText, .always⟩
 
 end NotificationHandling
 
 section MessageHandling
 
-  def handleNotification (method : String) (params : Json) : GameWorkerM Unit := do
+
-    let handle := fun paramType [FromJson paramType] (handler : paramType → GameWorkerM Unit) =>
+/--
-      (StateT.lift <| parseParams paramType params) >>= handler
+Modified notification handler.
-    match method with
+
-    | "textDocument/didChange" => handle DidChangeTextDocumentParams (handleDidChange)
+Compare to `Lean.Server.FileWorker.handleNotification`.
-    | "$/cancelRequest"        => handle CancelParams (handleCancelRequest ·)
+We use the modified `WorkerM` and use our custom `handleDidChange`.
-    | "$/setTrace"        => pure ()
+
-    | "$/lean/rpc/release"     => handle RpcReleaseParams (handleRpcRelease ·)
+-/
-    | "$/lean/rpc/keepAlive"   => handle RpcKeepAliveParams (handleRpcKeepAlive ·)
+def handleNotification (method : String) (params : Json) : WorkerM Unit := do
-    | _                        => throwServerError s!"Got unsupported notification method: {method}"
+  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 ·)
+  -- 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
-    let msg ← ctx.hIn.readLspMessage
-    let filterFinishedTasks (acc : PendingRequestMap) (id : RequestID) (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. -/
-        if let Except.error e := task.get then
-          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 }
 
-    -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired.
+/--
-    for (id, seshRef) in st.rpcSessions do
+Erase finished tasks if there are no errors.
-      let sesh ← seshRef.get
+-/
-      if (← sesh.hasExpired) then
+private def filterFinishedTasks (acc : PendingRequestMap) (id : RequestID)
-        st := { st with rpcSessions := st.rpcSessions.erase id }
+    (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. -/
+    if let Except.error e := task.get then
+      throwServerError s!"Failed responding to request {id}: {e}"
+    pure <| acc.erase id
+  else pure acc
+
+/--
+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
+    if (← sesh.hasExpired) then
+      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.notification method (some params) =>
+    -- Custom notification handler
+    handleNotification method (toJson params)
+    mainLoop
+  | _ =>
+    throwServerError s!"Got invalid JSON-RPC message: {toJson msg}"
 
-    set st
-    match msg with
-    | Message.request id method (some params) =>
-      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) =>
-      handleNotification method (toJson params)
-      mainLoop
-    | _ => 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