diff --git a/client/src/components/app_bar.tsx b/client/src/components/app_bar.tsx
index 175caeb..530636e 100644
--- a/client/src/components/app_bar.tsx
+++ b/client/src/components/app_bar.tsx
@@ -8,7 +8,7 @@ import { useAppDispatch, useAppSelector } from '../hooks'
import { Button } from './button'
import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
import { faDownload, faUpload, faEraser, faBook, faBookOpen, faGlobe, faHome, faArrowRight, faArrowLeft, faXmark, faBars, faCode, faCircleInfo, faTerminal } from '@fortawesome/free-solid-svg-icons'
-import { PrivacyPolicyPopup } from './privacy_policy'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
import { WorldSelectionMenu, downloadFile } from './world_tree'
/** navigation to switch between pages on mobile */
diff --git a/client/src/components/landing_page.tsx b/client/src/components/landing_page.tsx
index 2d20ab3..b395c89 100644
--- a/client/src/components/landing_page.tsx
+++ b/client/src/components/landing_page.tsx
@@ -11,7 +11,7 @@ import coverRobo from '../assets/covers/formaloversum.png'
import bgImage from '../assets/bg.jpg'
import Markdown from './markdown';
-import {PrivacyPolicyPopup} from './privacy_policy'
+import {PrivacyPolicyPopup} from './popup/privacy_policy'
const flag = {
'Dutch': '🇳🇱',
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 6e5c475..bcbafd9 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -33,7 +33,7 @@ import { DeletedChatContext, InputModeContext, MobileContext, MonacoEditorContex
import { DualEditor } from './infoview/main'
import { GameHint } from './infoview/rpc_api'
import { DeletedHints, Hint, Hints } from './hints'
-import { PrivacyPolicyPopup } from './privacy_policy'
+import { PrivacyPolicyPopup } from './popup/privacy_policy'
import '@fontsource/roboto/300.css'
import '@fontsource/roboto/400.css'
diff --git a/client/src/components/popup/erase.tsx b/client/src/components/popup/erase.tsx
new file mode 100644
index 0000000..73088f8
--- /dev/null
+++ b/client/src/components/popup/erase.tsx
@@ -0,0 +1,60 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { useSelector } from 'react-redux'
+import { GameIdContext } from '../../app'
+import { useAppDispatch } from '../../hooks'
+import { deleteProgress, selectProgress } from '../../state/progress'
+import { downloadFile } from '../world_tree'
+import { Button } from '../button'
+
+
+/** Pop-up to delete game progress.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function ErasePopup ({handleClose}) {
+ const gameId = React.useContext(GameIdContext)
+ const gameProgress = useSelector(selectProgress(gameId))
+ const dispatch = useAppDispatch()
+
+ /** Download the current progress (i.e. what's saved in the browser store) */
+ const downloadProgress = (e) => {
+ e.preventDefault()
+ downloadFile({
+ data: JSON.stringify(gameProgress, null, 2),
+ fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+ fileType: 'text/json',
+ })
+ }
+
+ const eraseProgress = () => {
+ dispatch(deleteProgress({game: gameId}))
+ handleClose()
+ }
+
+ const downloadAndErase = (e) => {
+ downloadProgress(e)
+ eraseProgress()
+ }
+
+ return
+
+
+
+
Delete Progress?
+
+
Do you want to delete your saved progress irreversibly?
+
+ (This deletes your proofs and your collected inventory.
+ Saves from other games are not deleted.)
+
+
+
+
+
+
+
+}
diff --git a/client/src/components/popup/game_info.tsx b/client/src/components/popup/game_info.tsx
new file mode 100644
index 0000000..6d1898c
--- /dev/null
+++ b/client/src/components/popup/game_info.tsx
@@ -0,0 +1,23 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { Typography } from '@mui/material'
+import Markdown from '../markdown'
+
+/** Pop-up that is displaying the Game Info.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function InfoPopup ({info, handleClose}: {info: string, handleClose: () => void}) {
+ return
+
+
+
+
+ {info}
+
+
+
+}
diff --git a/client/src/components/privacy_policy.tsx b/client/src/components/popup/privacy_policy.tsx
similarity index 100%
rename from client/src/components/privacy_policy.tsx
rename to client/src/components/popup/privacy_policy.tsx
diff --git a/client/src/components/popup/rules_help.tsx b/client/src/components/popup/rules_help.tsx
new file mode 100644
index 0000000..e4ed1cd
--- /dev/null
+++ b/client/src/components/popup/rules_help.tsx
@@ -0,0 +1,55 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+
+/** Pop-up that is displayed when opening the help explaining the game rules.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function RulesHelpPopup ({handleClose}: {handleClose: () => void}) {
+ return
+
+
+
+
Game Rules
+
+ Game rules determine if it is allowed to skip levels and if the games runs checks to only
+ allow unlocked tactics and theorems in proofs.
+
+
+ Note: "Unlocked" tactics (or theorems) are determined by two things: The set of minimal
+ tactics needed to solve a level, plus any tactics you unlocked in another level. That means
+ if you unlock simp in a level, you can use it henceforth in any level.
+
+
The options are:
+
+
+
+
+
levels
+
tactics
+
+
+
+
+
regular
+
🔐
+
🔐
+
+
+
relaxed
+
🔓
+
🔐
+
+
+
none
+
🔓
+
🔓
+
+
+
+
+
+}
diff --git a/client/src/components/popup/upload.tsx b/client/src/components/popup/upload.tsx
new file mode 100644
index 0000000..cfaae8b
--- /dev/null
+++ b/client/src/components/popup/upload.tsx
@@ -0,0 +1,70 @@
+/**
+ * @fileOverview
+*/
+import * as React from 'react'
+import { useSelector } from 'react-redux'
+import { GameIdContext } from '../../app'
+import { useAppDispatch } from '../../hooks'
+import { GameProgressState, loadProgress, selectProgress } from '../../state/progress'
+import { downloadFile } from '../world_tree'
+import { Button } from '../button'
+
+/** Pop-up that is displaying the Game Info.
+ *
+ * `handleClose` is the function to close it again because it's open/closed state is
+ * controlled by the containing element.
+ */
+export function UploadPopup ({handleClose}) {
+ const [file, setFile] = React.useState();
+ const gameId = React.useContext(GameIdContext)
+ const gameProgress = useSelector(selectProgress(gameId))
+ const dispatch = useAppDispatch()
+
+ const handleFileChange = (e) => {
+ if (e.target.files) {
+ setFile(e.target.files[0])
+ }
+ }
+
+ /** Upload progress from a */
+ const uploadProgress = (e) => {
+ if (!file) {return}
+ const fileReader = new FileReader()
+ fileReader.readAsText(file, "UTF-8")
+ fileReader.onload = (e) => {
+ const data = JSON.parse(e.target.result.toString()) as GameProgressState
+ console.debug("Json Data", data)
+ dispatch(loadProgress({game: gameId, data: data}))
+ }
+ handleClose()
+ }
+
+ /** Download the current progress (i.e. what's saved in the browser store) */
+ const downloadProgress = (e) => {
+ e.preventDefault()
+ downloadFile({
+ data: JSON.stringify(gameProgress, null, 2),
+ fileName: `lean4game-${gameId}-${new Date().toLocaleDateString()}.json`,
+ fileType: 'text/json',
+ })
+ }
+
+
+ return
+
+
+
+
Upload Saved Progress
+
+
Select a JSON file with the saved game progress to load your progress.