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

Assorted code cleanup and reogranization

Browse source
This commit is contained in:
Mac Malone 2021-05-29 12:38:29 -04:00
parent ea9382643e
commit 44b9ad2a30
10 changed files with 218 additions and 195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

108
Leanpkg2/Build.lean
View file

@ -3,35 +3,125 @@ 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 Lean.Data.Name
import Lean.Elab.Import
import Leanpkg2.Resolve
import Leanpkg2.BuildCore
import Leanpkg2.Manifest
import Leanpkg2.BuildConfig
import Leanpkg2.Configure
import Leanpkg2.Make
import Leanpkg2.Proc
open System
open Lean System
namespace Leanpkg2
def buildImports (manifest : Manifest) (imports : List String) (leanArgs : List String) : IO Unit := do
let cfg ← configure manifest
structure BuildContext extends BuildConfig where
parents : List Name := []
moreDepsMTime : IO.FS.SystemTime
manifest : Manifest
deriving instance Inhabited for IO.FS.SystemTime
deriving instance Inhabited for Task
structure Result where
maxMTime : IO.FS.SystemTime
task : Task (Except IO.Error Unit)
deriving Inhabited
structure State where
modTasks : NameMap Result := ∅
abbrev BuildM := ReaderT BuildContext <| StateT State IO
partial def buildModule (mod : Name) : BuildM Result := do
let ctx ← read
if ctx.parents.contains mod then
-- cyclic import
let cycle := ctx.parents.dropWhile (· != mod) ++ [mod]
let cycle := cycle.reverse.map (s!" {·}")
throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
if let some r := (← get).modTasks.find? mod then
-- already visited
return r
let srcPath := ctx.manifest.effectivePath
let leanFile := modToFilePath srcPath mod "lean"
let leanMData ← leanFile.metadata
-- recursively build dependencies and calculate transitive `maxMTime`
let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
let localImports := imports.filter (·.module.getRoot == ctx.pkg)
let deps ← localImports.mapM (buildModule ·.module)
let depMTimes ← deps.mapM (·.maxMTime)
let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-- check whether we have an up-to-date .olean
let oleanFile := modToFilePath (srcPath / buildPath) mod "olean"
try
if (← oleanFile.metadata).modified >= maxMTime then
let r := { maxMTime, task := Task.pure (Except.ok ()) }
modify fun st => { st with modTasks := st.modTasks.insert mod r }
return r
catch
| IO.Error.noFileOrDirectory .. => pure ()
| e => throw e
let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do
if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
-- propagate failure
throw e
try
let cFile := modToFilePath (srcPath / tempBuildPath) mod "c"
IO.createDirAll oleanFile.parent.get!
IO.createDirAll cFile.parent.get!
execCmd {
cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString
args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
env := #[("LEAN_PATH", ctx.leanPath)]
}
catch e =>
-- print errors early
IO.eprintln e
throw e
let r := { maxMTime, task := task }
modify fun st => { st with modTasks := st.modTasks.insert mod r }
return r
def buildModules (manifest : Manifest) (cfg : BuildConfig) (mods : List Name) : IO Unit := do
let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
let rs ← mods.mapM buildModule |>.run { toBuildConfig := cfg, moreDepsMTime, manifest } |>.run' {}
for r in rs do
if let Except.error _ ← IO.wait r.task then
-- actual error has already been printed above
throw <| IO.userError "Build failed."
def buildImports (manifest : Manifest) (cfg : Configuration) (imports leanArgs : List String := []) : IO Unit := do
let imports := imports.map (·.toName)
let root ← getRootPart <| manifest.effectivePath
let localImports := imports.filter (·.getRoot == root)
if localImports != [] then
let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps }
let buildCfg : BuildConfig := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps }
if ← FilePath.pathExists "Makefile" then
let oleans := localImports.map fun i => Lean.modToFilePath "build" i "olean" |>.toString
let oleans := localImports.map fun i =>
Lean.modToFilePath (manifest.effectivePath / buildPath) i "olean" |>.toString
execMake manifest oleans buildCfg
else
Build.buildModules manifest buildCfg localImports
buildModules manifest buildCfg localImports
def printPaths (manifest : Manifest) (imports leanArgs : List String := []) : IO Unit := do
let cfg ← configure manifest
buildImports manifest cfg imports leanArgs
IO.println cfg.leanPath
IO.println cfg.leanSrcPath
def build (manifest : Manifest) (makeArgs leanArgs : List String := []) : IO Unit := do
let cfg ← configure manifest
let root ← getRootPart <| manifest.effectivePath
let buildCfg : Build.Config := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps }
let buildCfg : BuildConfig := { pkg := root, leanArgs, leanPath := cfg.leanPath, moreDeps := cfg.moreDeps }
if makeArgs != [] || (← FilePath.pathExists "Makefile") then
execMake manifest makeArgs buildCfg
else
Build.buildModules manifest buildCfg [root]
buildModules manifest buildCfg [root]

24
Leanpkg2/BuildConfig.lean Normal file
View file

@ -0,0 +1,24 @@
/-
Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Data.Name
import Lean.Elab.Import
import Leanpkg2.Manifest
import Leanpkg2.Proc
open Lean
open System
namespace Leanpkg2
def buildPath : FilePath := "build"
def tempBuildPath := buildPath / "temp"
structure BuildConfig where
pkg : Name
leanArgs : List String
leanPath : String
-- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
moreDeps : List FilePath

106
Leanpkg2/BuildCore.lean
View file

@ -1,106 +0,0 @@
/-
Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
import Lean.Data.Name
import Lean.Elab.Import
import Leanpkg2.Manifest
import Leanpkg2.Proc
open Lean
open System
namespace Leanpkg2.Build
def buildPath : FilePath := "build"
def tempBuildPath := buildPath / "temp"
structure Config where
pkg : Name
leanArgs : List String
leanPath : String
-- things like `leanpkg.toml` and olean roots of dependencies that should also trigger rebuilds
moreDeps : List FilePath
structure Context extends Config where
parents : List Name := []
moreDepsMTime : IO.FS.SystemTime
manifest : Manifest
deriving instance Inhabited for IO.FS.SystemTime
deriving instance Inhabited for Task
structure Result where
maxMTime : IO.FS.SystemTime
task : Task (Except IO.Error Unit)
deriving Inhabited
structure State where
modTasks : NameMap Result := ∅
abbrev BuildM := ReaderT Context <| StateT State IO
partial def buildModule (mod : Name) : BuildM Result := do
let ctx ← read
if ctx.parents.contains mod then
-- cyclic import
let cycle := ctx.parents.dropWhile (· != mod) ++ [mod]
let cycle := cycle.reverse.map (s!" {·}")
throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
if let some r := (← get).modTasks.find? mod then
-- already visited
return r
let srcPath := ctx.manifest.effectivePath
let leanFile := modToFilePath srcPath mod "lean"
let leanMData ← leanFile.metadata
-- recursively build dependencies and calculate transitive `maxMTime`
let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
let localImports := imports.filter (·.module.getRoot == ctx.pkg)
let deps ← localImports.mapM (buildModule ·.module)
let depMTimes ← deps.mapM (·.maxMTime)
let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-- check whether we have an up-to-date .olean
let oleanFile := modToFilePath (srcPath / buildPath) mod "olean"
try
if (← oleanFile.metadata).modified >= maxMTime then
let r := { maxMTime, task := Task.pure (Except.ok ()) }
modify fun st => { st with modTasks := st.modTasks.insert mod r }
return r
catch
| IO.Error.noFileOrDirectory .. => pure ()
| e => throw e
let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do
if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
-- propagate failure
throw e
try
let cFile := modToFilePath (srcPath / tempBuildPath) mod "c"
IO.createDirAll oleanFile.parent.get!
IO.createDirAll cFile.parent.get!
execCmd {
cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString
args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
env := #[("LEAN_PATH", ctx.leanPath)]
}
catch e =>
-- print errors early
IO.eprintln e
throw e
let r := { maxMTime, task := task }
modify fun st => { st with modTasks := st.modTasks.insert mod r }
return r
def buildModules (manifest : Manifest) (cfg : Config) (mods : List Name) : IO Unit := do
let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
let rs ← mods.mapM buildModule |>.run { toConfig := cfg, moreDepsMTime, manifest } |>.run' {}
for r in rs do
if let Except.error _ ← IO.wait r.task then
-- actual error has already been printed above
throw <| IO.userError "Build failed."

4
Leanpkg2/Cli.lean
View file

@ -7,7 +7,7 @@ import Leanpkg2.Init
import Leanpkg2.Configure
import Leanpkg2.Make
import Leanpkg2.Build
import Leanpkg2.Manifest
import Leanpkg2.TomlManifest
namespace Leanpkg2
@ -66,7 +66,7 @@ directory."
def cli : (cmd : String) → (leanpkgArgs leanArgs : List String) → IO Unit
| "init", [name], [] => init name
| "configure", [], [] => discard do configure (← readManifest)
| "print-paths", leanpkgArgs, leanArgs => do buildImports (← readManifest) leanpkgArgs leanArgs
| "print-paths", imports, leanArgs => do printPaths (← readManifest) imports leanArgs
| "build", makeArgs, leanArgs => do build (← readManifest) makeArgs leanArgs
| "help", ["init"], [] => IO.println helpInit
| "help", ["configure"], [] => IO.println helpConfigure

12
Leanpkg2/Configure.lean
View file

@ -3,7 +3,7 @@ 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.BuildCore
import Leanpkg2.BuildConfig
import Leanpkg2.Resolve
open System
@ -27,19 +27,19 @@ def configure (manifest : Manifest) : IO Configuration := do
"configuring " ++ manifest.name ++ " " ++ manifest.version
let paths ← solveDeps manifest
let mut moreDeps := []
for (pkgpath, srcpath) in paths do
unless pkgpath == "." do
for (pkgPath, srcPath) in paths do
unless pkgPath == "." do
-- build recursively
-- TODO: share build of common dependencies
execCmd {
cmd := (← IO.appPath).toString
cwd := pkgpath
cwd := pkgPath
args := #["build"]
}
let pkgRoot := srcpath / Build.buildPath / (← getRootPart srcpath).toString
let pkgRoot := srcPath / buildPath / (← getRootPart srcPath).toString
moreDeps := pkgRoot.withExtension "olean" :: moreDeps
return {
leanPath := SearchPath.toString <| paths.map (·.2 / Build.buildPath)
leanPath := SearchPath.toString <| paths.map (·.2 / buildPath)
leanSrcPath := SearchPath.toString <| paths.map (·.2)
moreDeps
}

4
Leanpkg2/Init.lean
View file

@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
-/
import Leanpkg2.Git
import Leanpkg2.Proc
import Leanpkg2.Manifest
import Leanpkg2.TomlManifest
namespace Leanpkg2
@ -26,7 +26,7 @@ lean_version = \"{leanVersionString}\"
"
def initPkg (pkgName : String) (fromNew : Bool) : IO Unit := do
IO.FS.writeFile leanpkgTomlFn (leanpkgFileContents pkgName)
IO.FS.writeFile leanpkgToml (leanpkgFileContents pkgName)
IO.FS.writeFile ⟨s!"{pkgName.capitalize}.lean"⟩ mainFileContents
let h ← IO.FS.Handle.mk ⟨".gitignore"⟩ IO.FS.Mode.append (bin := false)
h.putStr initGitignoreContents

6
Leanpkg2/Make.lean
View file

@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
-/
import Leanpkg2.Manifest
import Leanpkg2.BuildCore
import Leanpkg2.BuildConfig
open System
namespace Leanpkg2
def lockFileName : System.FilePath := ⟨".leanpkg-lock"⟩
def lockFileName : System.FilePath := ".leanpkg-lock"
partial def withLockFile (x : IO α) : IO α := do
acquire
@ -39,7 +39,7 @@ partial def withLockFile (x : IO α) : IO α := do
acquire (firstTime := false)
| e => throw e
def execMake (manifest : Manifest) (makeArgs : List String) (cfg : Build.Config) : IO Unit := withLockFile do
def execMake (manifest : Manifest) (makeArgs : List String) (cfg : BuildConfig) : IO Unit := withLockFile do
let timeoutArgs :=
match manifest.timeout with
| some t => ["-T", toString t]

64
Leanpkg2/Manifest.lean
View file

@ -3,7 +3,6 @@ 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.Toml
import Leanpkg2.LeanVersion
open System
@ -11,30 +10,9 @@ open System
namespace Leanpkg2
inductive Source where
| path (dir : System.FilePath) : Source
| path (dir : FilePath) : Source
| git (url rev : String) (branch : Option String) : Source
namespace Source
def fromToml (v : Toml.Value) : Option Source :=
(do let Toml.Value.str dir ← v.lookup "path" | none
path ⟨dir⟩) <|>
(do let Toml.Value.str url ← v.lookup "git" | none
let Toml.Value.str rev ← v.lookup "rev" | none
match v.lookup "branch" with
| none => git url rev none
| some (Toml.Value.str branch) => git url rev (some branch)
| _ => none)
def toToml : Source → Toml.Value
| path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)]
| git url rev none =>
Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)]
| git url rev (some branch) =>
Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)]
end Source
structure Dependency where
name : String
src : Source
@ -52,44 +30,4 @@ namespace Manifest
def effectivePath (m : Manifest) : FilePath :=
m.path.getD ⟨"."⟩
def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do
let pkg ← t.lookup "package"
let Toml.Value.str n ← pkg.lookup "name" | none
let Toml.Value.str ver ← pkg.lookup "version" | none
let leanVer ← match pkg.lookup "lean_version" with
| some (Toml.Value.str leanVer) => some leanVer
| none => some leanVersionString
| _ => none
let tm ← match pkg.lookup "timeout" with
| some (Toml.Value.nat timeout) => some (some timeout)
| none => some none
| _ => none
let path ← match pkg.lookup "path" with
| some (Toml.Value.str path) => some (some ⟨path⟩)
| none => some none
| _ => none
let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none
let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src)
return { name := n, version := ver, leanVersion := leanVer,
path := path, dependencies := deps, timeout := tm }
def fromFile (fn : System.FilePath) : IO Manifest := do
let cnts ← IO.FS.readFile fn
let toml ← Toml.parse cnts
let some manifest ← pure (fromToml toml)
| throw <| IO.userError s!"cannot read manifest from {fn}"
manifest
end Manifest
def leanpkgTomlFn : System.FilePath := ⟨"leanpkg.toml"⟩
def readManifest : IO Manifest := do
let m ← Manifest.fromFile leanpkgTomlFn
if m.leanVersion ≠ leanVersionString then
IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
++ ", but package requires " ++ m.leanVersion ++ "\n"
return m
def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do
IO.FS.writeFile fn manifest.reprint.get!

8
Leanpkg2/Resolve.lean
View file

@ -3,9 +3,9 @@ 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.Proc
import Leanpkg2.Git
import Leanpkg2.Proc
import Leanpkg2.TomlManifest
open System
@ -65,13 +65,13 @@ def solveDepsCore (relPath : FilePath) (d : Manifest) : (maxDepth : Nat) → Sol
deps.forM (materialize relPath)
for dep in deps do
let p ← resolvedPath dep.name
let d' ← Manifest.fromFile $ p / "leanpkg.toml"
let d' ← Manifest.fromTomlFile <| p / "leanpkg.toml"
unless d'.name = dep.name do
throw <| IO.userError s!"{d.name} (in {relPath}) depends on {d'.name}, but resolved dependency has name {dep.name} (in {p})"
solveDepsCore p d' maxDepth
def constructPath (depname : String) (dirname : FilePath) : IO (FilePath × FilePath) := do
let path ← Manifest.effectivePath (← Manifest.fromFile <| dirname / leanpkgTomlFn)
let path ← Manifest.effectivePath (← Manifest.fromTomlFile <| dirname / leanpkgToml)
(dirname, dirname / path)
def solveDeps (d : Manifest) : IO (List (FilePath × FilePath)) := do

77
Leanpkg2/TomlManifest.lean Normal file
View file

@ -0,0 +1,77 @@
/-
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.Toml
import Leanpkg2.LeanVersion
import Leanpkg2.Manifest
open System
namespace Leanpkg2
namespace Source
def fromToml (v : Toml.Value) : Option Source :=
(do let Toml.Value.str dir ← v.lookup "path" | none
path ⟨dir⟩) <|>
(do let Toml.Value.str url ← v.lookup "git" | none
let Toml.Value.str rev ← v.lookup "rev" | none
match v.lookup "branch" with
| none => git url rev none
| some (Toml.Value.str branch) => git url rev (some branch)
| _ => none)
def toToml : Source → Toml.Value
| path dir => Toml.Value.table [("path", Toml.Value.str dir.toString)]
| git url rev none =>
Toml.Value.table [("git", Toml.Value.str url), ("rev", Toml.Value.str rev)]
| git url rev (some branch) =>
Toml.Value.table [("git", Toml.Value.str url), ("branch", Toml.Value.str branch), ("rev", Toml.Value.str rev)]
end Source
namespace Manifest
def fromToml (t : Toml.Value) : Option Manifest := OptionM.run do
let pkg ← t.lookup "package"
let Toml.Value.str n ← pkg.lookup "name" | none
let Toml.Value.str ver ← pkg.lookup "version" | none
let leanVer ← match pkg.lookup "lean_version" with
| some (Toml.Value.str leanVer) => some leanVer
| none => some leanVersionString
| _ => none
let tm ← match pkg.lookup "timeout" with
| some (Toml.Value.nat timeout) => some (some timeout)
| none => some none
| _ => none
let path ← match pkg.lookup "path" with
| some (Toml.Value.str path) => some (some ⟨path⟩)
| none => some none
| _ => none
let Toml.Value.table deps ← t.lookup "dependencies" <|> some (Toml.Value.table []) | none
let deps ← deps.mapM fun ⟨n, src⟩ => do Dependency.mk n (← Source.fromToml src)
return { name := n, version := ver, leanVersion := leanVer,
path := path, dependencies := deps, timeout := tm }
def fromTomlFile (fn : System.FilePath) : IO Manifest := do
let cnts ← IO.FS.readFile fn
let toml ← Toml.parse cnts
let some manifest ← pure (fromToml toml)
| throw <| IO.userError s!"cannot read manifest from {fn}"
manifest
end Manifest
def leanpkgToml : System.FilePath := "leanpkg.toml"
def readManifest : IO Manifest := do
let m ← Manifest.fromTomlFile leanpkgToml
if m.leanVersion ≠ leanVersionString then
IO.eprintln $ "\nWARNING: Lean version mismatch: installed version is " ++ leanVersionString
++ ", but package requires " ++ m.leanVersion ++ "\n"
return m
def writeManifest (manifest : Lean.Syntax) (fn : FilePath) : IO Unit := do
IO.FS.writeFile fn manifest.reprint.get!