From b94632cf0bf08eb26302e6f5659c3bd702ef6d36 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 25 Apr 2023 20:17:14 +0200
Subject: [PATCH] wip

---
 server/build.sh                         | 15 ++++++++++++++-
 server/nng/.gitignore                   |  3 ++-
 server/nng/NNG/MyNat/AddCommMonoid.lean |  8 ++++++++
 server/nng/NNG/MyNat/LE.lean            |  6 +++++-
 server/nng/lake-manifest.json           |  7 ++++++-
 server/nng/lakefile.lean                |  3 ++-
 6 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/server/build.sh b/server/build.sh
index 21941ea..9051276 100755
--- a/server/build.sh
+++ b/server/build.sh
@@ -14,7 +14,20 @@ docker build \
   --rm -f server.Dockerfile -t adam:latest .
 
 # Build NNG
-(cd nng && lake build)
+
+(
+  if [ ! -d nng ]
+  then
+    git clone https://github.com/hhu-adam/NNG4 nng/
+    cd nng
+  else
+    cd nng
+    git pull
+  fi
+  lake exe cache get
+  lake build
+)
+
 docker rmi nng:latest || true
 docker build \
   --build-arg GAME_DIR=nng \
diff --git a/server/nng/.gitignore b/server/nng/.gitignore
index 378eac2..8105d0d 100644
--- a/server/nng/.gitignore
+++ b/server/nng/.gitignore
@@ -1 +1,2 @@
-build
+build/
+lake-packages/
diff --git a/server/nng/NNG/MyNat/AddCommMonoid.lean b/server/nng/NNG/MyNat/AddCommMonoid.lean
index 27c36c3..b2d08f7 100644
--- a/server/nng/NNG/MyNat/AddCommMonoid.lean
+++ b/server/nng/NNG/MyNat/AddCommMonoid.lean
@@ -4,6 +4,14 @@ import NNG.MyNat.Addition
 namespace MyNat
 
 -- TODO: Do we need these instances?
+-- (kmb) I wanted to introduce these instances as "collectibles" as
+-- one went through the "main route" from addition world to power
+-- world. If you could make some extra window with those collectibles
+-- in, and whenever you have an instance sorry-free it awards you
+-- the collectible, that would be great! These things were just
+-- precisely the oddball (to my eyes) classes which nat was an instance of,
+-- but I think they would make great collectibles.
+
 
 -- instance addSemigroup : AddSemigroup ℕ :=
 -- {
diff --git a/server/nng/NNG/MyNat/LE.lean b/server/nng/NNG/MyNat/LE.lean
index 0e30011..c96d79d 100644
--- a/server/nng/NNG/MyNat/LE.lean
+++ b/server/nng/NNG/MyNat/LE.lean
@@ -4,7 +4,11 @@ namespace MyNat
 
 def le (a b : ℕ) :=  ∃ (c : ℕ), b = a + c
 
--- Another choice is to define it recursively: 
+-- Another choice is to define it recursively:
+-- (kb) note: I didn't choose this option because tests showed
+-- that mathematicians found it a lot more confusing than
+-- the existence definition.
+
 -- | le 0 _
 -- | le (succ a) (succ b) = le ab 
 
diff --git a/server/nng/lake-manifest.json b/server/nng/lake-manifest.json
index 7534416..cc199bf 100644
--- a/server/nng/lake-manifest.json
+++ b/server/nng/lake-manifest.json
@@ -19,7 +19,12 @@
     "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
     "name": "aesop",
     "inputRev?": "master"}},
-  {"path": {"name": "GameServer", "dir": "./../leanserver"}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/lean4game.git",
+    "subDir?": "server/leanserver",
+    "rev": "9fa94ecc5ca1c398479fb6026b03fcac46928bd7",
+    "name": "GameServer",
+    "inputRev?": "main"}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean
index 82868bf..d1adbdc 100644
--- a/server/nng/lakefile.lean
+++ b/server/nng/lakefile.lean
@@ -1,7 +1,8 @@
 import Lake
 open Lake DSL
 
-require GameServer from ".."/"leanserver"
+require GameServer from  git
+  "https://github.com/leanprover-community/lean4game.git"@"main"/"server"/"leanserver"
 
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git" @ "fc4a489c2af75f687338fe85c8901335360f8541"