wip

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 \

server/nng/.gitignore

@@ -1 +1,2 @@
-build
+build/
+lake-packages/

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 ℕ :=
 -- {

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 
 

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,

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"