From 67341f478d3fe5308cc116fffd8ae8afdbbd6dde Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Sat, 24 Jul 2021 07:36:58 -0400
Subject: [PATCH] refactor:: move some magic constants into defs

---
 Lake/Init.lean       |  9 ++++++---
 Lake/LeanConfig.lean | 12 +++++++-----
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/Lake/Init.lean b/Lake/Init.lean
index 62450083bc..a7192d2ee1 100644
--- a/Lake/Init.lean
+++ b/Lake/Init.lean
@@ -12,12 +12,15 @@ def initGitignoreContents :=
 "/build
 "
 
+def mainFileName (pkgName : String) : System.FilePath :=
+  s!"{pkgName.capitalize}.lean"
+
 def mainFileContents :=
 "def main : IO Unit :=
   IO.println \"Hello, world!\"
 "
 
-def leanPkgFileContents (pkgName : String) :=
+def pkgFileContents (pkgName : String) :=
 s!"import Lake.Package
 
 def package : Lake.PackageConfig := \{
@@ -30,8 +33,8 @@ def package : Lake.PackageConfig := \{
 open Git System
 
 def initPkg (dir : FilePath) (pkgName : String) : IO PUnit := do
-  IO.FS.writeFile (dir / leanPkgFile) (leanPkgFileContents pkgName)
-  IO.FS.writeFile (dir / s!"{pkgName.capitalize}.lean") mainFileContents
+  IO.FS.writeFile (dir / pkgFileName) (pkgFileContents pkgName)
+  IO.FS.writeFile (dir / mainFileName pkgName) mainFileContents
   let h ← IO.FS.Handle.mk (dir / ".gitignore") IO.FS.Mode.append (bin := false)
   h.putStr initGitignoreContents
   unless ← FilePath.isDir (dir /".git") do
diff --git a/Lake/LeanConfig.lean b/Lake/LeanConfig.lean
index 9de4e609ac..1948721e1f 100644
--- a/Lake/LeanConfig.lean
+++ b/Lake/LeanConfig.lean
@@ -10,7 +10,9 @@ open Lean System
 
 namespace Lake
 
-def leanPkgFile : FilePath := "package.lean"
+def pkgModName : Name := `package
+def pkgDefName : Name := `package
+def pkgFileName : FilePath := "package.lean"
 
 namespace Package
 
@@ -18,15 +20,15 @@ unsafe def fromLeanFileUnsafe
 (path : FilePath) (root : FilePath) (args : List String := [])
 : IO Package := do
   let input ← IO.FS.readFile path
-  let (env, ok) ← Elab.runFrontend input Options.empty path.toString `package
+  let (env, ok) ← Elab.runFrontend input Options.empty path.toString pkgModName
   if ok then
     let packagerE := Id.run <| ExceptT.run <|
-        env.evalConstCheck Packager Options.empty ``Packager `package
+        env.evalConstCheck Packager Options.empty ``Packager pkgDefName
     match packagerE with
     | Except.ok packager => Package.mk root (← packager root args)
     | Except.error error =>
       let configE := Id.run <| ExceptT.run <|
-        env.evalConstCheck PackageConfig Options.empty ``PackageConfig `package
+        env.evalConstCheck PackageConfig Options.empty ``PackageConfig pkgDefName
       match configE with
       | Except.ok config => Package.mk root config
       | Except.error error => throw <| IO.userError <|
@@ -36,7 +38,7 @@ unsafe def fromLeanFileUnsafe
 
 unsafe def fromDirUnsafe
 (path : FilePath) (args : List String := []) : IO Package :=
-  fromLeanFileUnsafe (path / leanPkgFile) path args
+  fromLeanFileUnsafe (path / pkgFileName) path args
 
 @[implementedBy fromDirUnsafe]
 constant fromDir (path : FilePath) (args : List String := []) : IO Package