14 month time-skip

2025-08-06 00:25:53 +02:00
parent 4e8b2e1c15
commit 3d9d4f1d54
8 changed files with 2786 additions and 3275 deletions
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -31,15 +31,11 @@ jobs:
          # We've been seeing many failures at this step recently because of network errors.
          # As a band-aid, we try twice.
          # The 'sleep 1' is small pause to let the network recover.
-          lake exe cache get || (sleep 1; lake exe cache get)
+          lake exe cache get Game || (sleep 1; lake exe cache get Game)

      - name: create timestamp file
        run: touch tmp_timestamp

-        # Note: this would also happen in the lake post-update-hook
-      - name: build gameserver executable
-        run: env LEAN_ABORT_ON_PANIC=1 lake build gameserver
-
      - name: building game
        run: env LEAN_ABORT_ON_PANIC=1 lake build

--- a/.github/workflows/build_non_main.yml
+++ b/.github/workflows/build_non_main.yml
@@ -31,7 +31,7 @@ jobs:
          # We've been seeing many failures at this step recently because of network errors.
          # As a band-aid, we try twice.
          # The 'sleep 1' is small pause to let the network recover.
-          lake exe cache get || (sleep 1; lake exe cache get)
+          lake exe cache get Game || (sleep 1; lake exe cache get Game)

      - name: building game
        run: env LEAN_ABORT_ON_PANIC=1 lake build
--- a/.i18n/en/Game.pot
+++ b/.i18n/en/Game.pot
--- a/Game/Tactic/Cases.lean
+++ b/Game/Tactic/Cases.lean
@@ -29,9 +29,9 @@ Usage: `cases n with d` if `n : ℕ`; `cases h with h1 h2` if `h : P ∨ Q`; `ca

 *(This implementation mimics the `cases'` from mathlib. The actual `cases` tactic in mathlib has a more complex syntax)*
 -/
-elab (name := cases) "cases " tgts:(Parser.Tactic.casesTarget,+) usingArg:((" using " ident)?)
-    withArg:((" with" (ppSpace colGt binderIdent)+)?) : tactic => do
-  let (targets, toTag) ← elabCasesTargets tgts.1.getSepArgs
+elab (name := cases) "cases " tgts:(Parser.Tactic.elimTarget,+) usingArg:((" using " ident)?)
+  withArg:((" with" (ppSpace colGt binderIdent)+)?) : tactic => do
+  let (targets, toTag) ← elabElimTargets tgts.1.getSepArgs
  let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
  g.withContext do
    let elimInfo ← getElimNameInfo usingArg targets (induction := false)
--- a/Game/Tactic/Induction.lean
+++ b/Game/Tactic/Induction.lean
@@ -1,7 +1,7 @@
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.Induction
-import Std.Tactic.OpenPrivate
-import Std.Data.List.Basic
+import Batteries.Tactic.OpenPrivate
+import Batteries.Data.List.Basic
 import Game.MyNat.Definition
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Tactic.Cases
@@ -35,7 +35,7 @@ open Lean Parser Tactic
 open Meta Elab Elab.Tactic
 open Mathlib.Tactic

-open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in
+open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction

 /--
 Modified `induction` tactic for this game.
@@ -44,11 +44,11 @@ Usage: `induction n with d hd`.

 *(The actual `induction` tactic has a more complex `with`-argument that works differently)*
 -/
-elab (name := MyNat.induction) "induction " tgts:(Parser.Tactic.casesTarget,+)
+elab (name := MyNat.induction) "induction " tgts:(Parser.Tactic.elimTarget,+)
    usingArg:((" using " ident)?)
    withArg:((" with" (ppSpace colGt binderIdent)+)?)
    genArg:((" generalizing" (ppSpace colGt ident)+)?) : tactic => do
-  let (targets, toTag) ← elabCasesTargets tgts.1.getSepArgs
+  let (targets, toTag) ← elabElimTargets tgts.1.getSepArgs
  let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
  g.withContext do
    let elimInfo ← getElimNameInfo usingArg targets (induction := true)
@@ -67,7 +67,7 @@ elab (name := MyNat.induction) "induction " tgts:(Parser.Tactic.casesTarget,+)
    | _ => pure elimInfo

    let targets ← addImplicitTargets elimInfo targets
-    evalInduction.checkTargets targets
+    checkInductionTargets targets
    let targetFVarIds := targets.map (·.fvarId!)
    g.withContext do
      let genArgs ← if genArg.1.isNone then pure #[] else getFVarIds genArg.1[1].getArgs
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,86 +1,115 @@
-{"version": 7,
+{"version": "1.1.0",
 "packagesDir": ".lake/packages",
 "packages":
- [{"url": "https://github.com/leanprover/std4.git",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
   "type": "git",
   "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
-   "name": "std",
+   "scope": "leanprover-community",
+   "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/mhuisi/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hhu-adam/lean-i18n.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "7550f08140c59c9a604bbcc23ab7830c103a3e39",
-   "name": "i18n",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph",
-   "type": "git",
-   "subDir": null,
-   "rev": "ac07367cbdd57440e6fe78e5be13b41f9cb0f896",
-   "name": "importGraph",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
-   "inherited": true,
+   "inputRev": "v4.21.0",
+   "inherited": false,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/lean4game.git",
   "type": "git",
   "subDir": "server",
-   "rev": "66aa8e688ec6d684bc2ad37c7eee46627a0481b2",
+   "scope": "hhu-adam",
+   "rev": "6df74ebfc845e4c287238ad1cbf652c20605c2a6",
   "name": "GameServer",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.21.0",
   "inherited": false,
   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/quote4",
+  {"url": "https://github.com/leanprover-community/plausible",
   "type": "git",
   "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
-   "name": "Qq",
+   "scope": "leanprover-community",
+   "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+   "name": "plausible",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.62",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/aesop",
   "type": "git",
   "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "scope": "leanprover-community",
+   "rev": "8ff27701d003456fd59f13a9212431239d902aef",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
   "type": "git",
   "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
-   "name": "proofwidgets",
+   "scope": "leanprover-community",
+   "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+   "name": "Qq",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "master",
   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
   "type": "git",
   "subDir": null,
-   "rev": "a45ae63747140c1b2cbad9d46f518015c047047a",
-   "name": "mathlib",
+   "scope": "leanprover-community",
+   "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+   "name": "batteries",
   "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
-   "inherited": false,
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/hhu-adam/lean-i18n.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "7dc27b87606f94ad0931a09f63330028d653d325",
+   "name": "i18n",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.21.0",
+   "inherited": true,
   "configFile": "lakefile.lean"}],
 "name": "Game",
 "lakeDir": ".lake"}
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,13 +6,18 @@ def leanVersion : String := s!"v{Lean.versionString}"

 def LocalGameServer : Dependency := {
  name := `GameServer
-  src := Source.path "../lean4game/server"
+  scope := "hhu-adam"
+  src? := DependencySrc.path "../lean4game/server"
+  version? := none
+  opts := ∅
 }

 def RemoteGameServer : Dependency := {
  name := `GameServer
-  -- TODO: change back to stable version
-  src := Source.git "https://github.com/leanprover-community/lean4game.git" leanVersion "server"
+  scope := "hhu-adam"
+  src? := DependencySrc.git "https://github.com/leanprover-community/lean4game.git" leanVersion "server"
+  version? := s!"git#{leanVersion}"
+  opts := ∅
 }

 /- Choose GameServer dependency depending on the environment variable `LEAN4GAME`. -/
@@ -33,7 +38,7 @@ you can use `require mathlib from git "[URL]" @ leanVersion`



-require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ leanVersion
+require "leanprover-community" / mathlib @ s!"git#{leanVersion}"



@@ -46,10 +51,12 @@ package Game where
  moreLeanArgs := #[
    "-Dtactic.hygienic=false",
    "-Dlinter.unusedVariables.funArgs=false",
+    "-Dweak.linter.unusedTactic=false",
    "-Dtrace.debug=false"]
  moreServerOptions := #[
    ⟨`tactic.hygienic, false⟩,
    ⟨`linter.unusedVariables.funArgs, true⟩,
+    ⟨`weak.linter.unusedTactic, false⟩,
    ⟨`trace.debug, true⟩]
  weakLeanArgs := #[]

--- a/2
+++ b/2
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.21.0