From 9f90c9bb66842ede6ba32afb7be47eeb63b7d1b9 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Fri, 17 Sep 2021 16:26:25 -0400
Subject: [PATCH] feat: don't overwite existing files on init + test

closes leanprover/lake#10
---
 Lake/Init.lean        | 26 ++++++++++++++++++++++----
 examples/init/test.sh |  7 ++++++-
 2 files changed, 28 insertions(+), 5 deletions(-)

diff --git a/Lake/Init.lean b/Lake/Init.lean
index 75ef514588..c97be67d05 100644
--- a/Lake/Init.lean
+++ b/Lake/Init.lean
@@ -10,6 +10,7 @@ import Lake.LeanConfig
 namespace Lake
 open Git System
 
+/-- `elan` toolchain file name -/
 def toolchainFileName : FilePath :=
 "lean-toolchain"
 
@@ -33,13 +34,30 @@ def package : Lake.PackageConfig := \{
 }
 "
 
-def initPkg (dir : FilePath) (pkgName : String) : IO PUnit := do
-  IO.FS.writeFile (dir / pkgFileName) (pkgFileContents pkgName)
-  IO.FS.writeFile (dir / mainFileName pkgName) mainFileContents
+/-- Initialize a new Lake package in the given directory with the given name. -/
+def initPkg (dir : FilePath) (name : String) : IO PUnit := do
+
+  -- write default configuration file
+  let pkgFile := dir / pkgFileName
+  if (← pkgFile.pathExists) then
+    -- error if package already has a `package.lean`
+    throw <| IO.userError "package already initialized"
+  IO.FS.writeFile pkgFile (pkgFileContents name)
+
+  -- write example main module if none exists
+  let mainFile := dir / mainFileName name
+  unless (← mainFile.pathExists) do
+    IO.FS.writeFile mainFile mainFileContents
+
+  -- write current toolchain to file for `elan`
   IO.FS.writeFile (dir / toolchainFileName) <| leanVersionString ++ "\n"
+
+  -- update `.gitignore`
   let h ← IO.FS.Handle.mk (dir / ".gitignore") IO.FS.Mode.append (bin := false)
   h.putStr gitignoreContents
-  unless ← FilePath.isDir (dir /".git") do
+
+  -- initialize a `.git` repository if none already
+  unless (← FilePath.isDir <| dir / ".git") do
     try
       quietInit dir
       unless upstreamBranch = "master" do
diff --git a/examples/init/test.sh b/examples/init/test.sh
index ab8080d346..3cef006fd4 100755
--- a/examples/init/test.sh
+++ b/examples/init/test.sh
@@ -7,6 +7,7 @@ set -ex
 ../../build/bin/lake new helloNew
 
 cd helloNew
+test -f lean-toolchain
 ../../../build/bin/lake build-bin
 ./build/bin/helloNew
 cd ..
@@ -14,8 +15,12 @@ cd ..
 # Test `init`
 
 mkdir helloInit
+
 cd helloInit
 ../../../build/bin/lake init helloInit
-
 ../../../build/bin/lake build-bin
 ./build/bin/helloInit
+
+# Test `init` on existing package (should error)
+
+../../../build/bin/lake init helloInit && exit 1 || true