From 7992cffa265bef90332cb3d9c3a51d81515c7819 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 23 Mar 2023 15:23:12 +0100
Subject: [PATCH] add minimal NNG dummy

---
 server/nng/.gitignore         |  1 +
 server/nng/NNG.lean           |  9 +++++++++
 server/nng/lake-manifest.json |  3 +++
 server/nng/lakefile.lean      | 11 +++++++++++
 server/nng/lean-toolchain     |  1 +
 5 files changed, 25 insertions(+)
 create mode 100644 server/nng/.gitignore
 create mode 100644 server/nng/NNG.lean
 create mode 100644 server/nng/lake-manifest.json
 create mode 100644 server/nng/lakefile.lean
 create mode 100644 server/nng/lean-toolchain

diff --git a/server/nng/.gitignore b/server/nng/.gitignore
new file mode 100644
index 0000000..c795b05
--- /dev/null
+++ b/server/nng/.gitignore
@@ -0,0 +1 @@
+build
\ No newline at end of file
diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean
new file mode 100644
index 0000000..88032ba
--- /dev/null
+++ b/server/nng/NNG.lean
@@ -0,0 +1,9 @@
+import GameServer.Commands
+
+Game "NNG"
+World "HelloWorld"
+Level 1
+
+Statement : 1 + 1 = 2 := rfl
+
+MakeGame
\ No newline at end of file
diff --git a/server/nng/lake-manifest.json b/server/nng/lake-manifest.json
new file mode 100644
index 0000000..fee354b
--- /dev/null
+++ b/server/nng/lake-manifest.json
@@ -0,0 +1,3 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages": [{"path": {"name": "GameServer", "dir": "./../leanserver"}}]}
diff --git a/server/nng/lakefile.lean b/server/nng/lakefile.lean
new file mode 100644
index 0000000..9ff2130
--- /dev/null
+++ b/server/nng/lakefile.lean
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+require GameServer from ".."/"leanserver"
+
+package NNG
+
+@[default_target]
+lean_lib NNG {
+  moreLeanArgs := #["-DautoImplicit=false"]
+}
diff --git a/server/nng/lean-toolchain b/server/nng/lean-toolchain
new file mode 100644
index 0000000..7f0fd43
--- /dev/null
+++ b/server/nng/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-03-09