Merge branch 'main' of github.com:leanprover-community/lean4game

client/src/components/Level.tsx

@@ -44,8 +44,15 @@ export const MonacoEditorContext = React.createContext<monaco.editor.IStandalone
 
 export const InputModeContext = React.createContext<{
   commandLineMode: boolean,
-  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>
+  setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
-}>({commandLineMode: true, setCommandLineMode: () => {}});
+  commandLineInput: string,
+  setCommandLineInput: React.Dispatch<React.SetStateAction<string>>
+}>({
+  commandLineMode: true,
+  setCommandLineMode: () => {},
+  commandLineInput: "",
+  setCommandLineInput: () => {},
+});
 
 function Level() {
 
@@ -56,9 +63,12 @@ function Level() {
   const codeviewRef = useRef<HTMLDivElement>(null)
   const introductionPanelRef = useRef<HTMLDivElement>(null)
 
+  const initialCode = useSelector(selectCode(worldId, levelId))
+
   const [commandLineMode, setCommandLineMode] = useState(true)
+  const [commandLineInput, setCommandLineInput] = useState("")
   const [showSidePanel, setShowSidePanel] = useState(true)
-  const [canUndo, setCanUndo] = useState(true)
+  const [canUndo, setCanUndo] = useState(initialCode.trim() !== "")
 
   const toggleSidePanel = () => {
     setShowSidePanel(!showSidePanel)
@@ -119,7 +129,6 @@ function Level() {
     setCanUndo(code.trim() !== "")
   }
 
-  const initialCode = useSelector(selectCode(worldId, levelId))
 
   const {editor, infoProvider, editorConnection} =
     useLevelEditor(worldId, levelId, codeviewRef, initialCode, onDidChangeContent)
@@ -168,7 +177,7 @@ function Level() {
 
         <EditorContext.Provider value={editorConnection}>
           <MonacoEditorContext.Provider value={editor}>
-            <InputModeContext.Provider value={{commandLineMode, setCommandLineMode}}>
+            <InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
               {editorConnection && <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />}
             </InputModeContext.Provider>
           </MonacoEditorContext.Provider>

client/src/components/infoview/CommandLine.tsx

@@ -1,5 +1,5 @@
 import * as React from 'react'
-import { useRef, useState } from 'react'
+import { useRef, useState, useEffect } from 'react'
 import { LspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
 import { useServerNotificationEffect } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
@@ -8,69 +8,204 @@ import { InputModeContext, MonacoEditorContext } from '../Level'
 
 import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'
 import { faWandMagicSparkles } from '@fortawesome/free-solid-svg-icons'
+import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter';
+import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider';
 
+import { Registry } from 'monaco-textmate' // peer dependency
+import { wireTmGrammars } from 'monaco-editor-textmate'
+import * as lightPlusTheme from 'lean4web/client/src/lightPlus.json'
+import * as leanSyntax from 'lean4web/client/src/syntaxes/lean.json'
+import * as leanMarkdownSyntax from 'lean4web/client/src/syntaxes/lean-markdown.json'
+import * as codeblockSyntax from 'lean4web/client/src/syntaxes/codeblock.json'
+import languageConfig from 'lean4/language-configuration.json';
 
-function hasErrorsOrWarnings(diags) {
+
-  return diags.some(
+/* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */
-    (d) =>
+
-      !d.message.startsWith("unsolved goals") &&
+// register Monaco languages
-      (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
+monaco.languages.register({
-  )
+  id: 'lean4cmd',
-}
+  extensions: ['.leancmd']
+})
+
+// map of monaco "language id's" to TextMate scopeNames
+const grammars = new Map()
+grammars.set('lean4', 'source.lean')
+grammars.set('lean4cmd', 'source.lean')
+
+const registry = new Registry({
+  getGrammarDefinition: async (scopeName) => {
+    if (scopeName === 'source.lean') {
+      return {
+          format: 'json',
+          content: JSON.stringify(leanSyntax)
+      }
+    } else if (scopeName === 'source.lean.markdown') {
+      return {
+          format: 'json',
+          content: JSON.stringify(leanMarkdownSyntax)
+      }
+    } else {
+      return {
+          format: 'json',
+          content: JSON.stringify(codeblockSyntax)
+      }
+    }
+  }
+});
+
+wireTmGrammars(monaco, registry, grammars)
+
+let config: any = { ...languageConfig }
+config.autoClosingPairs = config.autoClosingPairs.map(
+  pair => { return {'open': pair[0], 'close': pair[1]} }
+)
+monaco.languages.setLanguageConfiguration('lean4cmd', config);
 
 export function CommandLine() {
 
+  /** Reference to the hidden multi-line editor */
   const editor = React.useContext(MonacoEditorContext)
-  const commandInput = useRef<HTMLInputElement>()
+  const [oneLineEditor, setOneLineEditor] = useState<monaco.editor.IStandaloneCodeEditor>(null)
   const [processing, setProcessing] = useState(false)
 
-  const { commandLineMode } = React.useContext(InputModeContext)
+  const { commandLineMode, commandLineInput, setCommandLineInput } = React.useContext(InputModeContext)
-  const allDiags = React.useContext(LspDiagnosticsContext)
-  const diags = allDiags.get(editor.getModel().uri.toString())
 
-  React.useEffect(() => {
+  const inputRef = useRef()
-    if (commandLineMode) {
-      const endPos = editor.getModel().getFullModelRange().getEndPosition()
-      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
-        editor.executeEdits("command-line", [{
-          range: monaco.Selection.fromPositions(endPos, endPos),
-          text: "\n",
-          forceMoveMarkers: false
-        }]);
-      }
-      editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
-    }
-  }, [commandLineMode])
 
-  const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
+  // Run the command
-    ev.preventDefault()
+  const runCommand = React.useCallback(() => {
+    if (processing) return;
     const pos = editor.getPosition()
     editor.executeEdits("command-line", [{
       range: monaco.Selection.fromPositions(
         pos,
         editor.getModel().getFullModelRange().getEndPosition()
       ),
-      text: commandInput.current!.value + "\n",
+      text: commandLineInput + "\n",
       forceMoveMarkers: false
     }]);
     editor.setPosition(pos)
     setProcessing(true)
-  }
+  }, [commandLineInput, editor])
+
+  useEffect(() => {
+    if (oneLineEditor && oneLineEditor.getValue() !== commandLineInput) {
+      oneLineEditor.setValue(commandLineInput)
+    }
+  }, [commandLineInput])
 
+  // React when answer from the server comes back
   useServerNotificationEffect('textDocument/publishDiagnostics', (params: PublishDiagnosticsParams) => {
     if (params.uri == editor.getModel().uri.toString()) {
       setProcessing(false)
       if (!hasErrorsOrWarnings(params.diagnostics)) {
-        commandInput.current!.value = "";
+        setCommandLineInput("")
         editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
       }
     }
   }, []);
 
+  useEffect(() => {
+    const myEditor = monaco.editor.create(inputRef.current!, {
+      value: commandLineInput,
+      language: "lean4cmd",
+      quickSuggestions: false,
+      lightbulb: {
+        enabled: true
+      },
+      unicodeHighlight: {
+          ambiguousCharacters: false,
+      },
+      automaticLayout: true,
+      minimap: {
+        enabled: false
+      },
+      lineNumbers: 'off',
+      glyphMargin: false,
+      folding: false,
+      lineDecorationsWidth: 0,
+      lineNumbersMinChars: 0,
+      'semanticHighlighting.enabled': true,
+      overviewRulerLanes: 0,
+      hideCursorInOverviewRuler: true,
+      scrollbar: {
+        vertical: 'hidden',
+        horizontalScrollbarSize: 3
+      },
+      overviewRulerBorder: false,
+      theme: 'vs-code-theme-converted',
+      contextmenu: false
+    })
+
+    setOneLineEditor(myEditor)
+
+    const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), myEditor.getModel(), myEditor)
+
+    return () => {abbrevRewriter.dispose(); myEditor.dispose()}
+  }, [])
+
+  useEffect(() => {
+    if (!oneLineEditor) return
+    // Ensure that our one-line editor can only have a single line
+    const l = oneLineEditor.getModel().onDidChangeContent((e) => {
+      const value = oneLineEditor.getValue()
+      setCommandLineInput(value)
+      const newValue = value.replace(/[\n\r]/g, '')
+      if (value != newValue) {
+        oneLineEditor.setValue(newValue)
+      }
+    })
+    return () => { l.dispose() }
+  }, [oneLineEditor, setCommandLineInput])
+
+  useEffect(() => {
+    if (!oneLineEditor) return
+    // Run command when pressing enter
+    const l = oneLineEditor.onKeyUp((ev) => {
+      if (ev.code === "Enter") {
+        runCommand()
+      }
+    })
+    return () => { l.dispose() }
+  }, [oneLineEditor, runCommand])
+
+  // Effect when command line mode gets enabled
+  useEffect(() => {
+    if (commandLineMode) {
+      const endPos = editor.getModel().getFullModelRange().getEndPosition()
+      if (editor.getModel().getLineContent(endPos.lineNumber).trim() !== "") {
+        editor.executeEdits("command-line", [{
+          range: monaco.Selection.fromPositions(endPos, endPos),
+          text: commandLineInput + "\n",
+          forceMoveMarkers: false
+        }]);
+      }
+      editor.setPosition(editor.getModel().getFullModelRange().getEndPosition())
+    }
+  }, [commandLineMode])
+
+  const handleSubmit : React.FormEventHandler<HTMLFormElement> = (ev) => {
+    ev.preventDefault()
+    runCommand()
+  }
+
   return <div className="command-line">
       <form onSubmit={handleSubmit}>
-        <input type="text" ref={commandInput} disabled={processing} />
+        <div className="command-line-input-wrapper">
+          <div ref={inputRef} className="command-line-input" />
+        </div>
         <button type="submit" disabled={processing} className="btn btn-inverted"><FontAwesomeIcon icon={faWandMagicSparkles} /> Run</button>
       </form>
     </div>
 }
+
+/** Checks whether the diagnostics contain any errors or warnings to check whether the level has
+   been completed.*/
+function hasErrorsOrWarnings(diags) {
+  return diags.some(
+    (d) =>
+      !d.message.startsWith("unsolved goals") &&
+      (d.severity == DiagnosticSeverity.Error || d.severity == DiagnosticSeverity.Warning)
+  )
+}

client/src/components/infoview/goals.tsx

@@ -118,13 +118,14 @@ interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
     showHints?: boolean
+    commandLine: boolean
 }
 
 /**
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter, showHints } = props
+    const { goal, filter, showHints, commandLine } = props
 
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
     const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
@@ -159,7 +160,7 @@ export const Goal = React.memo((props: GoalProps) => {
         { assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Assumptions:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {commandLineMode && <CommandLine />}
+        {commandLine && commandLineMode && <CommandLine />}
         {!filter.reverse && goalLi}
         {showHints && hints}
     </div>
@@ -175,7 +176,7 @@ export function Goals({ goals, filter }: GoalsProps) {
         return <>No goals</>
     } else {
         return <>
-            {goals.goals.map((g, i) => <Goal key={i} goal={g} filter={filter} />)}
+            {goals.goals.map((g, i) => <Goal commandLine={false} key={i} goal={g} filter={filter} />)}
         </>
     }
 }

client/src/components/infoview/info.tsx

@@ -16,6 +16,7 @@ import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/
 import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions';
 import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
+import { Troubleshoot } from '@mui/icons-material';
 
 type InfoStatus = 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
@@ -123,7 +124,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             <div className="goals-section">
                 { goals && goals.goals.length > 0
                   ? <><div className="goals-section-title">Main Goal</div>
-                    <Goal filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
+                    <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
                   : <div className="goals-section-title">No Goals</div> }
             </div>
         </LocationsContext.Provider>
@@ -149,7 +150,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     <div className="goals-section-title">Other Goals</div>
 
                     {goals.goals.slice(1).map((goal, i) =>
-                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal filter={goalFilter} goal={goal} /></details>)}
+                        <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal commandLine={false} filter={goalFilter} goal={goal} /></details>)}
                 </div>}
         </LocationsContext.Provider>
     </>

client/src/components/infoview/infoview.css

@@ -44,10 +44,6 @@
   margin: 0.2em 0;
 }
 
-.command-line input[type="text"] {
-  font-family: var(--vscode-editor-font-family);
-}
-
 .command-line form {
   display: flex;
 }
@@ -56,8 +52,21 @@
   display: block;
 }
 
-.command-line form>input[type="text"]{
+.command-line .command-line-input-wrapper{
   flex: 1;
-  padding: 0.2em .6em;
+  padding: 0.4em .6em 0;
   font-size: 1rem;
+  background: white;
+}
+
+.command-line .command-line-input{
+  height: 1.2em;
+}
+
+/* Turn off some monaco decorations: */
+.command-line-input .monaco-editor .view-overlays .current-line {
+  border: 0;
+}
+.command-line-input .monaco-editor .scroll-decoration {
+  box-shadow: none;
 }

client/src/components/level.css

@@ -117,6 +117,27 @@ td code  {
   white-space:nowrap;
 }
 
+/* Styling in the editor while typing abbreviations such as "\alpha" */
+.abbreviation {
+  text-decoration: underline;
+}
+
+/* Styling in the left margin of the editor when processing */
+.processing {
+  background: linear-gradient(
+    to right,
+    rgba(255, 165, 0, 1) 0%,
+    rgba(255, 165, 0, 1) 30%,
+    transparent 30%,
+    transparent  100%
+  );
+}
+
+/* Styling in the left margin of the editor on error */
+.glyph-margin-error {
+  background: rgba(255, 0, 0, 1);
+}
+
 /***************************************/
 /* TODO: For development purposes only */
 /***************************************/

server/leanserver/GameServer/Commands.lean

@@ -184,41 +184,20 @@ elab "TacticDoc" name:ident content:str : command =>
     name := name.getId,
     content := content.getString })
 
-/-- Declare a set of tactic documentation entries.
-Expect an identifier used as the set name then `:=` and a
-space separated list of identifiers.
--/
-elab "TacticSet" name:ident ":=" args:ident* : command => do
-  let docs := tacticDocExt.getState (← getEnv)
-  let mut entries : Array TacticDocEntry := #[]
-  for arg in args do
-    let name := arg.getId
-    match docs.find? (·.name = name) with
-    | some doc => entries := entries.push doc
-    | none => throwError "Documentation for tactic {name} wasn't found."
-  modifyEnv (tacticSetExt.addEntry · {
-    name := name.getId,
-    tactics := entries })
-
 instance : Quote TacticDocEntry `term :=
 ⟨λ entry => Syntax.mkCApp ``TacticDocEntry.mk #[quote entry.name, quote entry.content]⟩
 
-/-- Declare the list of tactics that will be displayed in the current level.
+/-- Declare tactics that are introduced by this level. -/
-Expects a space separated list of identifiers that refer to either a tactic doc
+elab "NewTactics" args:ident* : command => do
-entry or a tactic doc set. -/
+  modifyCurLevel fun level => pure {level with newTactics := args.map (·.getId)}
-elab "Tactics" args:ident* : command => do
+
-  let env ← getEnv
+/-- Declare tactics that are temporarily disabled in this level -/
-  let docs := tacticDocExt.getState env
+elab "DisabledTactics" args:ident* : command => do
-  let sets := tacticSetExt.getState env
+  modifyCurLevel fun level => pure {level with disabledTactics := args.map (·.getId)}
-  let mut tactics : Array TacticDocEntry := #[]
+
-  for arg in args do
+/-- Temporarily disable all tactics except the ones declared here -/
-    let name := arg.getId
+elab "OnlyTactics" args:ident* : command => do
-    match docs.find? (·.name = name) with
+  modifyCurLevel fun level => pure {level with onlyTactics := args.map (·.getId)}
-    | some entry => tactics := tactics.push entry
-    | none => match sets.find? (·.name = name) with
-              | some entry => tactics := tactics ++ entry.tactics
-              | none => throwError "Tactic doc or tactic set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with tactics := tactics}
 
 /-! ## Lemmas -/
 
@@ -238,11 +217,11 @@ Expect an identifier used as the set name then `:=` and a
 space separated list of identifiers. -/
 elab "LemmaSet" name:ident ":" title:str ":=" args:ident* : command => do
   let docs := lemmaDocExt.getState (← getEnv)
-  let mut entries : Array LemmaDocEntry := #[]
+  let mut entries : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some doc => entries := entries.push doc
+    | some doc => entries := entries.push name
     | none => throwError "Lemma doc {name} wasn't found."
   modifyEnv (lemmaSetExt.addEntry · {
     name := name.getId,
@@ -255,16 +234,60 @@ instance : Quote LemmaDocEntry `term :=
 /-- Declare the list of lemmas that will be displayed in the current level.
 Expects a space separated list of identifiers that refer to either a lemma doc
 entry or a lemma doc set. -/
-elab "Lemmas" args:ident* : command => do
+elab "NewLemmas" args:ident* : command => do
   let env ← getEnv
   let docs := lemmaDocExt.getState env
   let sets := lemmaSetExt.getState env
-  let mut lemmas : Array LemmaDocEntry := #[]
+  let mut lemmas : Array Name := #[]
   for arg in args do
     let name := arg.getId
     match docs.find? (·.userName = name) with
-    | some entry => lemmas := lemmas.push entry
+    | some entry => lemmas := lemmas.push name
     | none => match sets.find? (·.name = name) with
               | some entry => lemmas := lemmas ++ entry.lemmas
               | none => throwError "Lemma doc or lemma set {name} wasn't found."
-  modifyCurLevel fun level => pure {level with lemmas := lemmas}
+  modifyCurLevel fun level => pure {level with newLemmas := lemmas}
+
+/-! ## Make Game -/
+
+def getTacticDoc! (tac : Name) : CommandElabM TacticDocEntry := do
+  match (tacticDocExt.getState (← getEnv)).find? (·.name = tac) with
+  | some doc => return doc
+  | none => throwError "Tactic documentation not found: {tac}"
+
+/-- Make the final Game. This command will precompute various things about the game, such as which
+tactics are available in each level etc. -/
+elab "MakeGame" : command => do
+  let game ← getCurGame
+
+  -- Check for loops in world graph
+  if game.worlds.hasLoops then
+    throwError "World graph has loops!"
+
+  -- Compute which tactics are available in which level:
+  let mut newTacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut newTactics : HashSet Name:= {}
+    for (_, level) in world.levels.toArray do
+      newTactics := newTactics.insertMany level.newTactics
+    newTacticsInWorld := newTacticsInWorld.insert worldId newTactics
+
+  let mut tacticsInWorld : HashMap Name (HashSet Name) := {}
+  for (worldId, _) in game.worlds.nodes.toArray do
+    let mut tactics : HashSet Name:= {}
+    let predecessors := game.worlds.predecessors worldId
+    for predWorldId in predecessors do
+      tactics := tactics.insertMany (newTacticsInWorld.find! predWorldId)
+    tacticsInWorld := tacticsInWorld.insert worldId tactics
+
+  for (worldId, world) in game.worlds.nodes.toArray do
+    let mut tactics := tacticsInWorld.find! worldId
+    logInfo m!"{tactics.toArray}"
+
+    let levels := world.levels.toArray.insertionSort fun a b => a.1 < b.1
+
+    for (levelId, level) in levels do
+      tactics := tactics.insertMany level.newTactics
+
+      modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
+        return {level with tactics := ← tactics.toArray.mapM getTacticDoc!}

server/leanserver/GameServer/EnvExtensions.lean

@@ -1,4 +1,6 @@
 import Lean
+import GameServer.Graph
+
 /-! # Environment extensions
 
 The game framework stores almost all its game building data in environment extensions
@@ -45,25 +47,6 @@ elab "#print_tactic_doc" : command => do
   for entry in tacticDocExt.getState (← getEnv) do
     dbg_trace "{entry.name} : {entry.content}"
 
-structure TacticSetEntry where
-  name : Name
-  tactics : Array TacticDocEntry
-  deriving ToJson, Repr
-
-/-- Environment extension for tactic sets. -/
-initialize tacticSetExt : SimplePersistentEnvExtension TacticSetEntry (Array TacticSetEntry) ←
-  registerSimplePersistentEnvExtension {
-    name := `tactic_set
-    addEntryFn := Array.push
-    addImportedFn := Array.concatMap id
-  }
-
-open Elab Command in
-/-- Print all registered tactic sets for debugging purposes. -/
-elab "#print_tactic_set" : command => do
-  for entry in tacticSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.tactics.map TacticDocEntry.name}"
-
 /-! ## Lemma documentation -/
 
 structure LemmaDocEntry where
@@ -90,7 +73,7 @@ elab "#print_lemma_doc" : command => do
 structure LemmaSetEntry where
   name : Name
   title : String
-  lemmas : Array LemmaDocEntry
+  lemmas : Array Name
   deriving ToJson, Repr
 
 /-- Environment extension for lemma sets. -/
@@ -105,26 +88,8 @@ open Elab Command in
 /-- Print all registered lemma sets for debugging purposes. -/
 elab "#print_lemma_set" : command => do
   for entry in lemmaSetExt.getState (← getEnv) do
-    dbg_trace "{entry.name} : {entry.lemmas.map LemmaDocEntry.name}"
+    dbg_trace "{entry.name} : {entry.lemmas}"
-
-/-! ## Graph -/
-
-structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
-  nodes: HashMap α β := {}
-  edges: Array (α × α) := {}
-deriving Inhabited
-
-instance [ToJson β] : ToJson (Graph Name β) := {
-  toJson := fun graph => Json.mkObj [
-    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
-    ("edges", toJson graph.edges)
-  ]
-}
-
-instance [inst : BEq α] [inst : Hashable α] : EmptyCollection (Graph α β) := ⟨default⟩
 
-def Graph.insertNode [inst : BEq α] [inst : Hashable α] (g : Graph α β) (a : α) (b : β) :=
-  {g with nodes := g.nodes.insert a b}
 
 /-! ## Environment extensions for game specification-/
 
@@ -198,7 +163,21 @@ structure GameLevel where
   introduction: String := default
   description: String := default
   conclusion: String := default
+  -- new tactics introduces by this level:
+  newTactics: Array Name := default
+  -- tactics exceptionally forbidden in this level:
+  disabledTactics: Array Name := default
+  -- only these tactics are allowed in this level (ignore if empty):
+  onlyTactics: Array Name := default
+  -- tactics in this level (computed by `MakeGame`):
   tactics: Array TacticDocEntry := default
+  -- new lemmas introduces by this level:
+  newLemmas: Array Name := default
+  -- lemmas exceptionally forbidden in this level:
+  disabledLemmas: Array Name := default
+  -- only these lemmas are allowed in this level (ignore if empty):
+  onlyLemmas: Array Name := default
+  -- lemmas in this level (computed by `MakeGame`):
   lemmas: Array LemmaDocEntry := default
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
@@ -329,3 +308,15 @@ def modifyCurLevel (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := d
   modifyCurWorld fun world => do
     let level ← getCurLevel
     return {world with levels := world.levels.insert level.index (← fn level)}
+
+def modifyLevel (levelId : LevelId) (fn : GameLevel → m GameLevel) [MonadError m] : m Unit := do
+  let some game ← getGame? levelId.game
+    | throwError m!"Game {levelId.game} does not exist"
+  let some world := (← getCurGame).worlds.nodes.find? levelId.world
+    | throwError m!"World {levelId.world} does not exist"
+  let some level := world.levels.find? levelId.level
+    | throwError m!"Level {levelId.level} does not exist"
+  let level' ← fn level
+  let world' := {world with levels := world.levels.insert levelId.level level'}
+  let game' := {game with worlds := game.worlds.insertNode levelId.world world'}
+  insertGame levelId.game game'

server/leanserver/GameServer/FileWorker.lean

@@ -17,7 +17,7 @@ private def mkErrorMessage (c : InputContext) (pos : String.Pos) (errorMsg : Str
 
 private def mkEOI (pos : String.Pos) : Syntax :=
   let atom := mkAtom (SourceInfo.original "".toSubstring pos "".toSubstring pos) ""
-  mkNode `Lean.Parser.Module.eoi #[atom]
+  mkNode ``Command.eoi #[atom]
 
 partial def parseTactic (inputCtx : InputContext) (pmctx : ParserModuleContext)
   (mps : ModuleParserState) (messages : MessageLog) (couldBeEndSnap : Bool) :
@@ -64,6 +64,35 @@ open JsonRpc
 
 section Elab
 
+-- TODO: use HashSet for allowed tactics?
+/-- Find all tactics in syntax object that are forbidden according to a
+set `allowed` of allowed tactics. -/
+partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameLevel) (stx : Syntax)
+  : Elab.Command.CommandElabM Unit := do
+  match stx with
+  | .missing => return ()
+  | .node info kind args =>
+    for arg in args do
+      findForbiddenTactics inputCtx level arg
+  | .atom info val =>
+    -- ignore syntax elements that do not start with a letter
+    if 0 < val.length ∧ val.data[0]!.isAlpha then
+      if ¬ ((level.tactics.map (·.name.toString))).contains val then
+        addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
+      else if level.disabledTactics.contains val
+        ∨ (¬ level.onlyTactics.isEmpty ∧ ¬ level.onlyTactics.contains val)then
+        addErrorMessage info s!"The tactic '{val}' is disabled in this level!"
+  | .ident info rawVal val preresolved => return ()
+where addErrorMessage (info : SourceInfo) (s : MessageData) :=
+  modify fun st => { st with
+    messages := st.messages.add {
+      fileName := inputCtx.fileName
+      severity := MessageSeverity.error
+      pos      := inputCtx.fileMap.toPosition (info.getPos?.getD 0)
+      data     := s
+    }
+  }
+
 open Elab Meta Expr in
 def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets : Bool) (couldBeEndSnap : Bool) : IO Snapshot := do
   let cmdState := snap.cmdState
@@ -98,15 +127,20 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
       Elab.Command.catchExceptions
         (getResetInfoTrees *> do
           let level ← GameServer.getLevelByFileName inputCtx.fileName
+
+          -- Check for forbidden tactics
+          findForbiddenTactics inputCtx level tacticStx
+
           -- Insert invisible `skip` command to make sure we always display the initial goal
           let skip := Syntax.node (.original default 0 default endOfWhitespace) ``Lean.Parser.Tactic.skip #[]
           -- Insert final `done` command to display unsolved goal error in the end
           let done := Syntax.node (.synthetic cmdParserState.pos cmdParserState.pos) ``Lean.Parser.Tactic.done #[]
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
+
           let cmdStx ← `(command|
             set_option tactic.hygienic false in
-            theorem my_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post
@@ -122,6 +156,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           data     := output
         }
       }
+
     let postCmdSnap : Snapshot := {
       beginPos := cmdPos
       stx := tacticStx

server/leanserver/GameServer/Graph.lean

@@ -0,0 +1,69 @@
+import Lean
+
+open Lean Meta
+
+/-! ## Graph -/
+
+variable [inst : BEq α] [inst : Hashable α]
+
+structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
+  nodes: HashMap α β := {}
+  edges: Array (α × α) := {}
+deriving Inhabited
+
+instance [ToJson β] : ToJson (Graph Name β) := {
+  toJson := fun graph => Json.mkObj [
+    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
+    ("edges", toJson graph.edges)
+  ]
+}
+
+instance  : EmptyCollection (Graph α β) := ⟨default⟩
+
+def Graph.insertNode (g : Graph α β) (a : α) (b : β) :=
+  {g with nodes := g.nodes.insert a b}
+
+/-- Check if graph contains loops -/
+partial def Graph.hasLoops (g : Graph α β) (visited0 : HashSet α := {}): Bool := Id.run do
+  let mut visited : HashSet α := visited0
+  let all : Array α := g.nodes.toArray.map (·.1)
+
+  -- find some node that we haven't visited
+  let some x := all.find? fun x => ¬ visited.contains x
+    | return false -- We have visted all nodes and found no loops
+  visited := visited.insert x
+
+  match visitSuccessors x x visited with -- visit all recursive successors of x
+  | some visited' => visited := visited'
+  | none => return true -- none means a loop has been found
+
+  g.hasLoops visited -- continue looking for unvisited nodes
+
+where
+  visitSuccessors (x : α) (x0 : α) (visited0 : HashSet α) : Option (HashSet α) := Id.run do
+    let mut visited : HashSet α := visited0
+
+    let directSuccessors := (g.edges.filter (·.1 == x)).map (·.2)
+    for y in directSuccessors do
+      if y == x0 then
+        return none -- loop found
+      if visited.contains y then
+        continue -- no loop possible here because the visited nodes do not lead to x0
+      visited := visited.insert y
+      match visitSuccessors y x0 visited with
+      | some visited' => visited := visited'
+      | none => return none
+
+    return some visited
+
+-- #eval Graph.hasLoops ⟨HashMap.ofList [(2,2), (1,1)], #[(2,1)]⟩
+
+partial def Graph.predecessors (g : Graph α β) (x : α) (acc : HashSet α := {}) : HashSet α := Id.run do
+  let mut res := acc
+  let directPredecessors := (g.edges.filter (·.2 == x)).map (·.1)
+  for y in directPredecessors do
+    if ¬ res.contains y then
+      res := res.insert y
+      res := g.predecessors y res
+
+  return res

server/testgame/TestGame.lean

@@ -39,9 +39,12 @@ Conclusion
 
 
 Path Proposition → Implication → Predicate → Contradiction → LeanStuff
---Path Predicate → Prime
+-- Path Predicate → Prime
 Path Predicate → Induction → LeanStuff → Function → SetFunction
 
 Path LeanStuff → SetTheory → SetFunction
 
 Path SetTheory → SetTheory2
+
+
+MakeGame

server/testgame/TestGame/Levels/Contradiction/L01_Have.lean

@@ -63,6 +63,6 @@ have k : ¬ B
 
 Conclusion ""
 
-Tactics contradiction rcases haveₓ assumption apply
+NewTactics contradiction rcases haveₓ assumption apply
 
-Lemmas Even Odd not_even not_odd
+NewLemmas Even Odd not_even not_odd

server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean

@@ -60,6 +60,6 @@ Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False =>
 
 Conclusion ""
 
-Tactics contradiction apply assumption rcases sufficesₓ
+NewTactics contradiction apply assumption rcases sufficesₓ
 
-Lemmas Even Odd not_even not_odd
+NewLemmas Even Odd not_even not_odd

server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean

@@ -52,4 +52,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
 
 Conclusion ""
 
-Tactics by_contra sufficesₓ haveₓ contradiction apply assumption
+NewTactics by_contra sufficesₓ haveₓ contradiction apply assumption

server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean

@@ -46,4 +46,4 @@ HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>
 
 Conclusion ""
 
-Tactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption
+NewTactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption

server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean

@@ -61,5 +61,5 @@ Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) =>
 Hint (n : ℕ) : Even n → Even (n ^ 2) =>
 "Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek."
 
-Tactics contrapose rw apply
+NewTactics contrapose rw apply
-Lemmas Even Odd not_even not_odd even_square
+NewLemmas Even Odd not_even not_odd even_square

server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean

@@ -71,6 +71,6 @@ HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
 "Probiers mit `apply ...`"
 
 
-Tactics contradiction by_contra rw apply assumption -- TODO: suffices, have
+NewTactics contradiction by_contra rw apply assumption -- TODO: suffices, have
 
-Lemmas Odd Even not_odd not_even even_square
+NewLemmas Odd Even not_odd not_even even_square

server/testgame/TestGame/Levels/Function/L01_xxx.lean

@@ -23,4 +23,4 @@ Statement
     : True := by
   trivial
 
-Tactics rw
+NewTactics rw

server/testgame/TestGame/Levels/Implication/L01_Intro.lean

@@ -37,4 +37,4 @@ HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
 Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) =>
 "Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden."
 
-Tactics intro constructor assumption
+NewTactics intro constructor assumption

server/testgame/TestGame/Levels/Implication/L02_Revert.lean

@@ -39,4 +39,4 @@ dass $B$ wahr ist."
 HiddenHint (A : Prop) (B : Prop) (ha : A) (h : A → B): B =>
 "Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen."
 
-Tactics revert assumption
+NewTactics revert assumption

server/testgame/TestGame/Levels/Implication/L03_Apply.lean

@@ -32,7 +32,7 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
 "Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch $A$ zeigen,
 dafür hast du bereits einen Beweis in den Annahmen."
 
-Tactics apply assumption
+NewTactics apply assumption
 
 -- Katex notes
 -- `\\(    \\)` or `$   $` for inline

server/testgame/TestGame/Levels/Implication/L04_Apply.lean

@@ -32,4 +32,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C)
 "Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
 diese mit `apply` an."
 
-Tactics intro apply assumption revert
+NewTactics intro apply assumption revert

server/testgame/TestGame/Levels/Implication/L05_Apply.lean

@@ -48,6 +48,6 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
     (i : D → E) (k : E → F) (m : C → F) : D =>
 "Sackgasse. Probier doch einen anderen Weg."
 
-Tactics apply assumption revert intro
+NewTactics apply assumption revert intro
 
 -- https://www.jmilne.org/not/Mamscd.pdf

server/testgame/TestGame/Levels/Implication/L06_Iff.lean

@@ -38,6 +38,6 @@ aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean,
 ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
 "
 
-Tactics constructor assumption
+NewTactics constructor assumption
 
 -- TODO : `case mpr =>` ist mathematisch noch sinnvoll.

server/testgame/TestGame/Levels/Implication/L07_Rw.lean

@@ -71,4 +71,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔
 "Das ist nicht der optimale Weg..."
 
 
-Tactics rw assumption
+NewTactics rw assumption

server/testgame/TestGame/Levels/Implication/L08_Iff.lean

@@ -41,4 +41,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =
 
 Conclusion "Im nächsten Level findest du die zweite Option."
 
-Tactics apply assumption
+NewTactics apply assumption

server/testgame/TestGame/Levels/Implication/L09_Iff.lean

@@ -36,7 +36,7 @@ Conclusion
 "
 "
 
-Tactics intro apply rcases assumption
+NewTactics intro apply rcases assumption
 
 -- -- TODO: The new `cases` works differntly. There is also `cases'`
 -- example (A B : Prop) : (A ↔ B) → (A → B) := by

server/testgame/TestGame/Levels/Implication/L10_Apply.lean

@@ -50,6 +50,6 @@ Conclusion
 "
 "
 
-Tactics apply left right assumption
+NewTactics apply left right assumption
 
-Lemmas not_or_of_imp
+NewLemmas not_or_of_imp

server/testgame/TestGame/Levels/Implication/L11_Rw.lean

@@ -34,6 +34,6 @@ Conclusion
 `rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet.
 "
 
-Tactics rw
+NewTactics rw
 
-Lemmas not_not not_or_of_imp
+NewLemmas not_not not_or_of_imp

server/testgame/TestGame/Levels/Implication/L12_Summary.lean

@@ -76,6 +76,6 @@ HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B =>
 HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B =>
 "Findest du einen Widerspruch?"
 
-Tactics rfl assumption trivial left right constructor rcases
+NewTactics rfl assumption trivial left right constructor rcases
 
-Lemmas not_not not_or_of_imp
+NewLemmas not_not not_or_of_imp

server/testgame/TestGame/Levels/Induction/L01_Simp.lean

@@ -43,4 +43,4 @@ Statement
     (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
   simp
 
-Tactics simp
+NewTactics simp

server/testgame/TestGame/Levels/Induction/L02_Sum.lean

@@ -34,4 +34,4 @@ Statement
   simp
   ring
 
-Tactics rw simp ring
+NewTactics rw simp ring

server/testgame/TestGame/Levels/Induction/L03_Induction.lean

@@ -42,4 +42,4 @@ Statement arithmetic_sum
   simp_rw [Nat.succ_eq_one_add]
   ring
 
-Tactics ring
+NewTactics ring

server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean

@@ -27,4 +27,4 @@ $\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
   rw [hn, Nat.succ_eq_add_one]
   ring
 
-Tactics ring
+NewTactics ring

server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean

@@ -44,4 +44,4 @@ Statement
   -- rw [mul_add, hn]
   -- ring
 
-Tactics ring
+NewTactics ring

server/testgame/TestGame/Levels/Induction/T00_Sum.lean

@@ -44,4 +44,4 @@ Statement
     rw [hn]
 
 
-Tactics ring
+NewTactics ring

server/testgame/TestGame/Levels/Induction/T01_Induction.lean

@@ -29,4 +29,4 @@ example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n
   sorry
 | n + 5  => by sorry
 
-Tactics rw simp ring
+NewTactics rw simp ring

server/testgame/TestGame/Levels/Induction/T02_Induction.lean

@@ -23,10 +23,4 @@ Statement
   sorry
   sorry
 
-Tactics rw simp ring
+NewTactics rw simp ring
-
--- example (n : ℕ) : (n - 1) * (n + 1) = (n ^ 2 - 1) := by
---   induction' n with n hn
---   ring
---   rw [Nat.succ_eq_one_add]
---   rw []

server/testgame/TestGame/Levels/Induction/T03_SumComm.lean

@@ -21,7 +21,7 @@ Statement
     (n : ℕ) : True := by
   trivial
 
-Tactics simp
+NewTactics simp
 
 
 -- Σ_i Σ_j ... = Σ_j Σ_i ...

server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean

@@ -29,4 +29,4 @@ Statement
     "TODO" : True := by
   trivial
 
-Tactics rw
+NewTactics rw

server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean

@@ -67,4 +67,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
 Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
 "Ein UND im Goal kann mit `constructor` aufgeteilt werden."
 
-Tactics left right assumption constructor rcases
+NewTactics left right assumption constructor rcases

server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean

@@ -20,4 +20,4 @@ Conclusion
 "
 "
 
-Tactics ring
+NewTactics ring

server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean

@@ -20,4 +20,4 @@ Conclusion
 "
 "
 
-Tactics ring
+NewTactics ring

server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean

@@ -58,4 +58,4 @@ Hint (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even
 "`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
 `(x : ℕ) → `"
 
-Tactics ring intro unfold
+NewTactics ring intro unfold

server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean

@@ -22,4 +22,4 @@ Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
 
 Conclusion ""
 
-Tactics use simp
+NewTactics use simp

server/testgame/TestGame/Levels/Predicate/L01_Ring.lean

@@ -39,6 +39,6 @@ Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
 (erst `ℤ` ist ein Ring).
 "
 
-Tactics ring
+NewTactics ring
 
 #eval 4 / 6

server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean

@@ -67,4 +67,4 @@ Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃
 
 Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
 
-Tactics assumption rw
+NewTactics assumption rw

server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean

@@ -37,4 +37,4 @@ Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1
 Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
 dem Goal umschreiben."
 
-Tactics assumption rw
+NewTactics assumption rw

server/testgame/TestGame/Levels/Predicate/L04_Ring.lean

@@ -30,4 +30,4 @@ Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
 
 Conclusion ""
 
-Tactics ring rw
+NewTactics ring rw

server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean

@@ -28,4 +28,4 @@ Conclusion
 aufzurufen, deshalb brauchst du das nur noch selten.
 "
 
-Tactics rfl
+NewTactics rfl

server/testgame/TestGame/Levels/Predicate/L06_Exists.lean

@@ -67,5 +67,5 @@ Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
 Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
 "Die Taktik `ring` löst solche Gleichungen."
 
-Tactics unfold rcases use rw ring
+NewTactics unfold rcases use rw ring
-Lemmas Even Odd
+NewLemmas Even Odd

server/testgame/TestGame/Levels/Predicate/L07_Forall.lean

@@ -50,4 +50,4 @@ Hint (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even
 Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
 praktisch gleich. Mehr dazu später."
 
-Tactics ring intro unfold
+NewTactics ring intro unfold

server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean

@@ -62,6 +62,6 @@ Hint (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
 
 Conclusion ""
 
-Tactics push_neg intro use rw unfold ring
+NewTactics push_neg intro use rw unfold ring
 
-Lemmas Even Odd not_even not_odd not_exists not_forall
+NewLemmas Even Odd not_even not_odd not_exists not_forall

server/testgame/TestGame/Levels/Predicate/L09_Summary.lean

@@ -50,6 +50,6 @@ Statement
 
 Conclusion ""
 
-Tactics push_neg intro use rw unfold ring
+NewTactics push_neg intro use rw unfold ring
 
-Lemmas Even Odd not_even not_odd not_exists not_forall
+NewLemmas Even Odd not_even not_odd not_exists not_forall

server/testgame/TestGame/Levels/Prime/L01_Prime.lean

@@ -36,6 +36,6 @@ example : True := by
 
 Conclusion ""
 
-Tactics
+NewTactics
 
-Lemmas
+NewLemmas

server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean

@@ -48,4 +48,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B))
 
 Conclusion ""
 
-Tactics tauto
+NewTactics tauto

server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean

@@ -27,4 +27,5 @@ HiddenHint : 42 = 42 =>
 
 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
 
-Tactics rfl
+NewTactics rfl
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean

@@ -32,4 +32,5 @@ HiddenHint (n : ℕ) (h : 1 < n) : 1 < n =>
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean

@@ -27,4 +27,5 @@ HiddenHint (A : Prop) (hA : A) : A =>
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L04_True.lean

@@ -33,4 +33,5 @@ True := by
 
 Conclusion ""
 
-Tactics trivial
+NewTactics trivial
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L05_Not.lean

@@ -21,4 +21,5 @@ Statement
 
 Conclusion ""
 
-Tactics trivial
+NewTactics trivial
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L06_False.lean

@@ -27,4 +27,5 @@ HiddenHint (A : Prop) (h : False) : A =>
 "Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen,
 unabhängig davon, was das Goal ist."
 
-Tactics contradiction
+NewTactics contradiction
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean

@@ -26,4 +26,5 @@ Conclusion
 "
 "
 
-Tactics contradiction
+NewTactics contradiction
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L08_Contra.lean

@@ -29,4 +29,5 @@ Conclusion
 "
 "
 
-Tactics contradiction
+NewTactics contradiction
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L09_And.lean

@@ -32,7 +32,8 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-Tactics constructor assumption
+NewTactics constructor assumption
+DisabledTactics tauto
 
 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."

server/testgame/TestGame/Levels/Proposition/L10_And.lean

@@ -33,7 +33,8 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-Tactics constructor assumption
+NewTactics constructor assumption
+DisabledTactics tauto
 
 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."

server/testgame/TestGame/Levels/Proposition/L11_Or.lean

@@ -30,4 +30,5 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) =>
 Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
 "Sackgasse. Probier's nochmals."
 
-Tactics left right assumption
+NewTactics left right assumption
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L12_Or.lean

@@ -44,4 +44,5 @@ HiddenHint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A =>
 Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
 "Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
 
-Tactics assumption rcases
+NewTactics assumption rcases
+DisabledTactics tauto

server/testgame/TestGame/Levels/Proposition/L13_Summary.lean

@@ -122,4 +122,5 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
 HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
 "`left` oder `right`?"
 
-Tactics left right assumption constructor rcases rfl contradiction trivial
+NewTactics left right assumption constructor rcases rfl contradiction trivial
+DisabledTactics tauto

server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean

@@ -21,4 +21,4 @@ Statement
     : True := by
   trivial
 
-Tactics rw
+NewTactics rw

server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean

@@ -39,4 +39,4 @@ Statement mem_univ
   trivial
   -- tauto
 
-Tactics tauto trivial
+NewTactics tauto trivial

server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean

@@ -39,7 +39,7 @@ Statement subset_empty_iff
   intro h hA
   apply mem_univ -- or `trivial`.
 
-Tactics intro trivial apply
+NewTactics intro trivial apply
 -- blocked: tauto simp
 
 end MySet

server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean

@@ -54,8 +54,8 @@ Statement subset_empty_iff
   rcases a with ⟨h₁, h₂⟩
   assumption
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
 
 end MySet

server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean

@@ -45,8 +45,8 @@ Statement eq_empty_iff_forall_not_mem
   rw [←subset_empty_iff]
   rfl -- This is quite a miracle :)
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset
 
 end MySet

server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean

@@ -30,6 +30,6 @@ Statement nonempty_iff_ne_empty
   push_neg
   rfl
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean

@@ -26,6 +26,6 @@ Statement
 "" (A B : Set ℕ) : (A ∪ ∅) ∩ B = A ∩ (univ ∩ B) := by
   simp
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean

@@ -30,6 +30,6 @@ Statement
   rw [←union_diff_distrib]
   rw [univ_union]
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean

@@ -30,6 +30,6 @@ Statement
   rw [←not_mem_compl_iff]
   exact h4
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean

@@ -22,7 +22,7 @@ man die de-Morganschen Regeln einfach selber beweisen könnten.
 
 
 Die meisten Aufgaben über Mengen sind eine Kombination von `rw` und `simp_rw` verschiedenster
-Lemmas in `import Mathlib.Data.Set`.
+NewLemmas in `import Mathlib.Data.Set`.
 
 Die Taktik `simp_rw` funktioniert ähnlich wie `rw`, aber sie versucht jedes Lemma so oft
 wie möglich anzuwenden. Wir kennen also 4 etwas verwandte Optionen um Lemmas und Theoreme zu
@@ -52,7 +52,7 @@ Statement
   rw [diff_eq_compl_inter]
   rw [inter_comm]
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
 -- TODOs
 -- Lemmas compl_union compl_inter mem_compl_iff

server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean

@@ -33,6 +33,6 @@ Statement
   rw [Set.mem_diff]
   exact hx
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean

@@ -32,6 +32,6 @@ Statement
     ({4, 9} : Set ℕ) = Set.insert 4 {9} := by
   rfl
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean

@@ -35,5 +35,5 @@ Statement
   simp_rw [mem_insert_iff, mem_singleton_iff] at *
   tauto
 
-Tactics simp_rw intro tauto rw
+NewTactics simp_rw intro tauto rw
 --Lemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean

@@ -32,6 +32,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean

@@ -37,6 +37,6 @@ Statement
   assumption
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean

@@ -36,6 +36,6 @@ Statement
   ring
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean

@@ -34,6 +34,6 @@ Statement
   ring
 
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean

@@ -28,6 +28,6 @@ Statement
     { x ∈ (S : Set ℤ) | 0 ≤ x} ⊆ S := by
   library_search
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean

@@ -23,6 +23,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean

@@ -22,6 +22,6 @@ open Set
 Statement
 "" : True := sorry
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean

@@ -23,6 +23,6 @@ Statement
   use 1
   ring
 
-Tactics constructor intro rw assumption rcases simp tauto trivial
+NewTactics constructor intro rw assumption rcases simp tauto trivial
 
-Lemmas Subset.antisymm_iff empty_subset
+NewLemmas Subset.antisymm_iff empty_subset

server/testgame/TestGame/Levels/SetTheory/T01_Set.lean

@@ -54,8 +54,7 @@ Statement
   rw [←Set.union_diff_distrib]
   rw [Set.univ_union]
 
-Tactics rw
+NewTactics rw
-
 
 example : 4 ∈ (univ : Set ℕ) := by
   trivial

server/testgame/TestGame/Levels/StatementTest.lean

@@ -35,4 +35,4 @@ lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c
 
 Conclusion ""
 
-Tactics assumption
+NewTactics assumption

server/testgame/TestGame/TacticDocs.lean

@@ -258,5 +258,3 @@ Prove:
 
 TacticDoc intro
 "Useful to introduce stuff"
-
-TacticSet basics := rfl induction_on intro rewrite