max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor:: move some magic constants into defs

Browse source
This commit is contained in:
tydeu 2021-07-24 07:36:58 -04:00
parent 53b95fb455
commit 67341f478d
2 changed files with 13 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
Lake/Init.lean
View file

@ -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

12
Lake/LeanConfig.lean
View file

@ -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