diff --git a/Lake/CLI/Init.lean b/Lake/CLI/Init.lean index f573382a82..91dd4ee887 100644 --- a/Lake/CLI/Init.lean +++ b/Lake/CLI/Init.lean @@ -30,7 +30,7 @@ def libFileContents := def mainFileName : FilePath := s!"{defaultExeRoot}.lean" -def mainFileContents (libRoot : Name) := +def mainFileContents (libRoot : String) := s!"import {libRoot} def main : IO Unit := @@ -42,7 +42,7 @@ s!"def main : IO Unit := IO.println s!\"Hello, world!\" " -def stdConfigFileContents (pkgName : Name) (root : Name) := +def stdConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL @@ -50,7 +50,7 @@ package {pkgName} \{ -- add package configuration options here } -lean_lib {root} \{ +lean_lib {libRoot} \{ -- add library configuration options here } @@ -60,7 +60,7 @@ lean_exe {pkgName} \{ } " -def exeConfigFileContents (pkgName : Name) (exeRoot : Name) := +def exeConfigFileContents (pkgName exeRoot : String) := s!"import Lake open Lake DSL @@ -74,7 +74,7 @@ lean_exe {exeRoot} \{ } " -def libConfigFileContents (pkgName : Name) (libRoot : Name) := +def libConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL @@ -88,7 +88,7 @@ lean_lib {libRoot} \{ } " -def mathConfigFileContents (pkgName : Name) (libRoot : Name) := +def mathConfigFileContents (pkgName libRoot : String) := s!"import Lake open Lake DSL @@ -110,6 +110,8 @@ inductive InitTemplate | std | exe | lib | math deriving Repr, DecidableEq +instance : Inhabited InitTemplate := ⟨.std⟩ + def InitTemplate.parse? : String → Option InitTemplate | "std" => some .std | "exe" => some .exe @@ -117,13 +119,19 @@ def InitTemplate.parse? : String → Option InitTemplate | "math" => some .math | _ => none -def InitTemplate.configFileContents (pkgName root : Name) : InitTemplate → String +def InitTemplate.configFileContents (pkgName root : String) : InitTemplate → String | .std => stdConfigFileContents pkgName root | .lib => libConfigFileContents pkgName root | .exe => exeConfigFileContents pkgName root | .math => mathConfigFileContents pkgName root -instance : Inhabited InitTemplate := ⟨.std⟩ +def escapeName! : Name → String +| .anonymous => "[anonymous]" +| .str .anonymous s => escape s +| .str n s => escapeName! n ++ "." ++ escape s +| _ => unreachable! +where + escape s := Lean.idBeginEscape.toString ++ s ++ Lean.idEndEscape.toString /-- Initialize a new Lake package in the given directory with the given name. -/ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit := do @@ -146,7 +154,9 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit let configFile := dir / defaultConfigFile if (← configFile.pathExists) then error "package already initialized" - IO.FS.writeFile configFile <| tmp.configFileContents pkgName root + let rootNameStr := escapeName! root + let contents := tmp.configFileContents (escapeName! pkgName) rootNameStr + IO.FS.writeFile configFile contents -- write example code if the files do not already exist if tmp = .exe then @@ -159,7 +169,7 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit if tmp = .std then let mainFile := dir / mainFileName unless (← mainFile.pathExists) do - IO.FS.writeFile mainFile <| mainFileContents root + IO.FS.writeFile mainFile <| mainFileContents rootNameStr -- write Lean's toolchain to file (if it has one) for `elan` if Lean.toolchain ≠ "" then diff --git a/README.md b/README.md index 5aff43456b..4b8dcf60fb 100644 --- a/README.md +++ b/README.md @@ -64,7 +64,7 @@ def hello := "world" **Main.lean** ```lean -import Hello +import «Hello» def main : IO Unit := IO.println s!"Hello, {hello}!" @@ -78,16 +78,16 @@ Lake also creates a basic `lakefile.lean` for the package along with a `lean-too import Lake open Lake DSL -package hello { +package «hello» { -- add package configuration options here } -lean_lib Hello { +lean_lib «Hello» { -- add library configuration options here } @[default_target] -lean_exe hello { +lean_exe «hello» { root := `Main } ``` diff --git a/examples/init/.gitignore b/examples/init/.gitignore index 66d4cb4a17..dfc4a5b1ba 100644 --- a/examples/init/.gitignore +++ b/examples/init/.gitignore @@ -1,2 +1,3 @@ /hello_world /hello-world +/meta diff --git a/examples/init/clean.sh b/examples/init/clean.sh index b096e8abc2..4d901c168d 100755 --- a/examples/init/clean.sh +++ b/examples/init/clean.sh @@ -1,2 +1,3 @@ rm -rf hello-world rm -rf hello_world +rm -rf meta diff --git a/examples/init/test.sh b/examples/init/test.sh index 70bd28f07e..fb079daeb9 100755 --- a/examples/init/test.sh +++ b/examples/init/test.sh @@ -16,6 +16,12 @@ $LAKE new hello.world $LAKE -d hello-world build hello-world/build/bin/hello-world +# Test issue 128 + +$LAKE new meta +$LAKE -d meta build +meta/build/bin/meta + # Test `init` mkdir hello_world