namespace

Main.lean

@@ -1,4 +1,4 @@
 import TenCert
 
 def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+  IO.println s!"Hello, {TenCert.hello}!"

TenCert.lean

@@ -1,3 +1,6 @@
 -- This module serves as the root of the `TenCert` library.
 -- Import modules here that should be built as part of the library.
-import TenCert.Basic
+import TenCert.Basic
+import SHerLOC.Basic
+import ANPU.Basic
+import TensorLib.Basic

TenCert/Basic.lean

@@ -1 +1,5 @@
-def hello := "world"
+namespace TenCert
+
+def hello := "world"
+
+namespace TenCert

lake-manifest.json

@@ -1,5 +1,35 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover/SHerLOC.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3e2777320ce9326f0f212acac583ffa864dafe89",
+   "name": "SHerLOC",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/ANPU.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e989420b95f2c7c091bdb99459d87fdfdcd90898",
+   "name": "ANPU",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/TensorLib.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "8103ee2345c79143153213030ee2ebae7b809fe8",
+   "name": "TensorLib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "TenCert",
  "lakeDir": ".lake"}

lakefile.lean

@@ -4,6 +4,15 @@ open Lake DSL
 package "TenCert" where
   -- add package configuration options here
 
+require SHerLOC from git
+  "https://github.com/leanprover/SHerLOC.git" @ "main"
+
+require ANPU from git
+  "https://github.com/leanprover/ANPU.git" @ "main"
+
+require TensorLib from git
+  "https://github.com/leanprover/TensorLib.git" @ "main"
+
 lean_lib «TenCert» where
   -- add library configuration options here