From 99d458c646e00fa76868edda68534bda6781beb2 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Sun, 6 Jun 2021 21:56:58 -0400
Subject: [PATCH] Update init to produce `package.lean`

---
 Leanpkg2/Cli.lean                 |  2 +-
 Leanpkg2/Init.lean                | 21 +++++++++++----------
 Leanpkg2/LeanConfig.lean          |  2 +-
 Leanpkg2/Resolve.lean             |  2 +-
 examples/hello/package.lean       |  4 ++--
 examples/helloDeps/a/package.lean |  4 ++--
 examples/helloDeps/b/package.lean |  4 ++--
 7 files changed, 20 insertions(+), 19 deletions(-)

diff --git a/Leanpkg2/Cli.lean b/Leanpkg2/Cli.lean
index 7d92337ea0..e153100ee4 100644
--- a/Leanpkg2/Cli.lean
+++ b/Leanpkg2/Cli.lean
@@ -62,7 +62,7 @@ This command creates a new Lean package with the given name in the current
 directory."
 
 def getRootPkg : IO Package := do
-  let cfg ← PackageConfig.fromLeanFile leanConfigFile
+  let cfg ← PackageConfig.fromLeanFile leanPkgFile
   if cfg.leanVersion ≠ leanVersionString then
     IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++
       leanVersionString ++ ", but package requires " ++ cfg.leanVersion ++ "\n"
diff --git a/Leanpkg2/Init.lean b/Leanpkg2/Init.lean
index b08495b872..e7877486ff 100644
--- a/Leanpkg2/Init.lean
+++ b/Leanpkg2/Init.lean
@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Git
 import Leanpkg2.Proc
-import Leanpkg2.TomlConfig
+import Leanpkg2.LeanConfig
 
 namespace Leanpkg2
 
@@ -18,16 +18,19 @@ def mainFileContents :=
   IO.println \"Hello, world!\"
 "
 
-def leanpkgFileContents (pkgName : String) :=
-s!"[package]
-name = \"{pkgName}\"
-version = \"0.1\"
-lean_version = \"{leanVersionString}\"
+def leanPkgFileContents (pkgName : String) :=
+s!"import Leanpkg2.Package
+
+def package : Leanpkg2.PackageConfig := \{
+  name := \"{pkgName}\"
+  version := \"0.1\"
+  leanVersion := \"{leanVersionString}\"
+}
 "
 
 open Git in
-def initPkg (pkgName : String) (fromNew : Bool) : IO Unit := do
-  IO.FS.writeFile leanpkgToml (leanpkgFileContents pkgName)
+def init (pkgName : String) : IO Unit := do
+  IO.FS.writeFile leanPkgFile (leanPkgFileContents pkgName)
   IO.FS.writeFile ⟨s!"{pkgName.capitalize}.lean"⟩ mainFileContents
   let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false)
   h.putStr initGitignoreContents
@@ -38,5 +41,3 @@ def initPkg (pkgName : String) (fromNew : Bool) : IO Unit := do
         checkoutBranch upstreamBranch
     ) <|>
       IO.eprintln "WARNING: failed to initialize git repository"
-
-def init (pkgName : String) := initPkg pkgName false
diff --git a/Leanpkg2/LeanConfig.lean b/Leanpkg2/LeanConfig.lean
index 7a1f4b17c7..2430f1e6bf 100644
--- a/Leanpkg2/LeanConfig.lean
+++ b/Leanpkg2/LeanConfig.lean
@@ -11,7 +11,7 @@ open Lean Elab System
 
 namespace Leanpkg2
 
-def leanConfigFile : FilePath := "package.lean"
+def leanPkgFile : FilePath := "package.lean"
 
 namespace PackageConfig
 
diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean
index 5e16ad2dca..9dce9f2c15 100644
--- a/Leanpkg2/Resolve.lean
+++ b/Leanpkg2/Resolve.lean
@@ -69,7 +69,7 @@ def solveDepsCore (pkg : Package) : (maxDepth : Nat) → Solver Unit
     let newDeps ← pkg.dependencies.filterM (notYetAssigned ·.name)
     for dep in newDeps do
       let dir ← materialize pkg.dir dep
-      let cfg ← PackageConfig.fromLeanFile <| dir / leanConfigFile
+      let cfg ← PackageConfig.fromLeanFile <| dir / leanPkgFile
       modify (·.insert dep.name ⟨dir, cfg⟩)
     for dep in newDeps do
       let depPkg ← resolvedPackage dep.name
diff --git a/examples/hello/package.lean b/examples/hello/package.lean
index 9d65d2aca1..16c26d7ec4 100644
--- a/examples/hello/package.lean
+++ b/examples/hello/package.lean
@@ -1,6 +1,6 @@
 import Leanpkg2.Package
 
 def package : Leanpkg2.PackageConfig := {
-  name := "hello",
-  version := "1.0",
+  name := "hello"
+  version := "1.0"
 }
diff --git a/examples/helloDeps/a/package.lean b/examples/helloDeps/a/package.lean
index 7e697633cb..db385e4029 100644
--- a/examples/helloDeps/a/package.lean
+++ b/examples/helloDeps/a/package.lean
@@ -1,6 +1,6 @@
 import Leanpkg2.Package
 
 def package : Leanpkg2.PackageConfig := {
-  name := "a",
-  version := "1.0",
+  name := "a"
+  version := "1.0"
 }
diff --git a/examples/helloDeps/b/package.lean b/examples/helloDeps/b/package.lean
index 8e6bc14eb9..0c84296a53 100644
--- a/examples/helloDeps/b/package.lean
+++ b/examples/helloDeps/b/package.lean
@@ -3,8 +3,8 @@ import Leanpkg2.Build
 open Leanpkg2 System
 
 def package : PackageConfig := {
-  name := "b",
-  version := "1.0",
+  name := "b"
+  version := "1.0"
   dependencies := [
     { name := "a", src := Source.path (FilePath.mk ".." / "a") }
   ]