From f2041789b7383a260948bdd8085c19c6bd0ee796 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Wed, 2 Jun 2021 16:02:22 -0400
Subject: [PATCH] Renamed `Manifest.lean` to `Pakcage.lean`

---
 Leanpkg2/Build.lean                      |  2 +-
 Leanpkg2/BuildConfig.lean                | 17 +----------------
 Leanpkg2/Make.lean                       |  6 +++---
 Leanpkg2/{Manifest.lean => Package.lean} | 10 ++++++++++
 Leanpkg2/Resolve.lean                    |  2 --
 Leanpkg2/TomlManifest.lean               |  2 +-
 examples/hello/Package.lean              |  1 -
 examples/helloDeps/a/Package.lean        |  1 -
 examples/helloDeps/b/Package.lean        |  1 -
 9 files changed, 16 insertions(+), 26 deletions(-)
 rename Leanpkg2/{Manifest.lean => Package.lean} (82%)

diff --git a/Leanpkg2/Build.lean b/Leanpkg2/Build.lean
index 854f58964d..c60606ad63 100644
--- a/Leanpkg2/Build.lean
+++ b/Leanpkg2/Build.lean
@@ -6,7 +6,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 import Lean.Data.Name
 import Lean.Elab.Import
 import Leanpkg2.Resolve
-import Leanpkg2.Manifest
+import Leanpkg2.Package
 import Leanpkg2.BuildConfig
 import Leanpkg2.Make
 import Leanpkg2.Proc
diff --git a/Leanpkg2/BuildConfig.lean b/Leanpkg2/BuildConfig.lean
index 6e123cb813..de71b456fc 100644
--- a/Leanpkg2/BuildConfig.lean
+++ b/Leanpkg2/BuildConfig.lean
@@ -5,7 +5,7 @@ Authors: Sebastian Ullrich
 -/
 import Lean.Data.Name
 import Lean.Elab.Import
-import Leanpkg2.Manifest
+import Leanpkg2.Package
 import Leanpkg2.Proc
 
 open Lean
@@ -13,19 +13,6 @@ open System
 
 namespace Leanpkg2
 
-def buildPath : FilePath := "build"
-def tempBuildPath := buildPath / "temp"
-
-namespace Package
-
-def buildDir (self : Package) : FilePath :=
-  self.dir / Leanpkg2.buildPath
-
-def buildRoot (self : Package)  : FilePath :=
-  self.buildDir / self.manifest.module
-
-end Package
-
 structure BuildConfig where
   module   : Name
   leanArgs : List String
@@ -40,5 +27,3 @@ def fromPackages (module : Name) (leanArgs : List String) (pkgs : List Package)
   leanPath := SearchPath.toString <| pkgs.map (·.buildDir)
   moreDeps := pkgs.filter (·.dir.toString != ".") |>.map (·.buildRoot.withExtension "olean")
 }
-
-end BuildConfig
diff --git a/Leanpkg2/Make.lean b/Leanpkg2/Make.lean
index 37954aeb57..26ab4bfb30 100644
--- a/Leanpkg2/Make.lean
+++ b/Leanpkg2/Make.lean
@@ -3,14 +3,14 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Leanpkg2.Manifest
+import Leanpkg2.Package
 import Leanpkg2.BuildConfig
 
 open System
 
 namespace Leanpkg2
 
-def lockFileName : System.FilePath := ".leanpkg-lock"
+def lockFileName : FilePath := ".leanpkg-lock"
 
 partial def withLockFile (x : IO α) : IO α := do
   acquire
@@ -22,7 +22,7 @@ partial def withLockFile (x : IO α) : IO α := do
     acquire (firstTime := true) :=
       try
         -- TODO: lock file should ideally contain PID
-        if !System.Platform.isWindows then
+        if !Platform.isWindows then
           discard <| IO.Prim.Handle.mk lockFileName "wx"
         else
           -- `x` mode doesn't seem to work on Windows even though it's listed at
diff --git a/Leanpkg2/Manifest.lean b/Leanpkg2/Package.lean
similarity index 82%
rename from Leanpkg2/Manifest.lean
rename to Leanpkg2/Package.lean
index f7195eca4c..cce75d61b5 100644
--- a/Leanpkg2/Manifest.lean
+++ b/Leanpkg2/Package.lean
@@ -10,6 +10,10 @@ open Lean System
 
 namespace Leanpkg2
 
+def buildPath : FilePath := "build"
+def tempBuildPath := buildPath / "temp"
+def depsPath := buildPath / "deps"
+
 inductive Source where
   | path (dir : FilePath) : Source
   | git (url rev : String) (branch : Option String) : Source
@@ -54,4 +58,10 @@ def sourceDir (self : Package) : FilePath :=
 def sourceRoot (self : Package)  : FilePath :=
   self.sourceDir / self.manifest.module
 
+def buildDir (self : Package) : FilePath :=
+  self.dir / Leanpkg2.buildPath
+
+def buildRoot (self : Package)  : FilePath :=
+  self.buildDir / self.manifest.module
+
 end Package
diff --git a/Leanpkg2/Resolve.lean b/Leanpkg2/Resolve.lean
index 6ed62180b7..f4152b5d0f 100644
--- a/Leanpkg2/Resolve.lean
+++ b/Leanpkg2/Resolve.lean
@@ -12,8 +12,6 @@ open System
 
 namespace Leanpkg2
 
-def depsPath := buildPath / "deps"
-
 def Assignment := List (String × Package)
 
 namespace Assignment
diff --git a/Leanpkg2/TomlManifest.lean b/Leanpkg2/TomlManifest.lean
index 4e04111987..99dce01964 100644
--- a/Leanpkg2/TomlManifest.lean
+++ b/Leanpkg2/TomlManifest.lean
@@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Leanpkg2.Toml
 import Leanpkg2.LeanVersion
-import Leanpkg2.Manifest
+import Leanpkg2.Package
 
 open System
 
diff --git a/examples/hello/Package.lean b/examples/hello/Package.lean
index 294b023114..5de8e84f0b 100644
--- a/examples/hello/Package.lean
+++ b/examples/hello/Package.lean
@@ -1,5 +1,4 @@
 import Leanpkg2.Build
-import Leanpkg2.Manifest
 
 open Leanpkg2
 
diff --git a/examples/helloDeps/a/Package.lean b/examples/helloDeps/a/Package.lean
index c1c41dd810..11d316b818 100644
--- a/examples/helloDeps/a/Package.lean
+++ b/examples/helloDeps/a/Package.lean
@@ -1,5 +1,4 @@
 import Leanpkg2.Build
-import Leanpkg2.Manifest
 
 open Leanpkg2
 
diff --git a/examples/helloDeps/b/Package.lean b/examples/helloDeps/b/Package.lean
index dc7902dd08..b5e24b0fc5 100644
--- a/examples/helloDeps/b/Package.lean
+++ b/examples/helloDeps/b/Package.lean
@@ -1,5 +1,4 @@
 import Leanpkg2.Build
-import Leanpkg2.Manifest
 
 open Leanpkg2 System