feat: verbosity options for logging + neater build progress
This commit is contained in:
Mario Carneiro
GitHub
parent
2d2bed90aa
commit
a0400cbe97
16 changed files with 101 additions and 58 deletions
|
|
@ -16,7 +16,7 @@ def proc (args : IO.Process.SpawnArgs) : JobM Unit := do
|
|||
let envStr := String.join <| args.env.toList.filterMap fun (k, v) =>
|
||||
if k == "PATH" then none else some s!"{k}={v.getD ""} " -- PATH too big
|
||||
let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
|
||||
logInfo <| "> " ++ envStr ++
|
||||
logVerbose <| "> " ++ envStr ++
|
||||
match args.cwd with
|
||||
| some cwd => s!"{cmdStr} # in directory {cwd}"
|
||||
| none => cmdStr
|
||||
|
|
@ -33,12 +33,13 @@ def proc (args : IO.Process.SpawnArgs) : JobM Unit := do
|
|||
logError s!"external command {args.cmd} exited with status {out.exitCode}"
|
||||
failure
|
||||
|
||||
def compileLeanModule (leanFile : FilePath)
|
||||
def compileLeanModule (name : Name) (leanFile : FilePath)
|
||||
(oleanFile? ileanFile? cFile? : Option FilePath)
|
||||
(leanPath : SearchPath := []) (rootDir : FilePath := ".")
|
||||
(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {})
|
||||
(leanArgs : Array String := #[]) (lean : FilePath := "lean")
|
||||
: JobM PUnit := do
|
||||
logAuxInfo s!"Building {name}"
|
||||
let mut args := leanArgs ++
|
||||
#[leanFile.toString, "-R", rootDir.toString]
|
||||
if let some oleanFile := oleanFile? then
|
||||
|
|
@ -61,32 +62,36 @@ def compileLeanModule (leanFile : FilePath)
|
|||
]
|
||||
}
|
||||
|
||||
def compileO (oFile srcFile : FilePath)
|
||||
def compileO (name : Name) (oFile srcFile : FilePath)
|
||||
(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : JobM Unit := do
|
||||
logAuxInfo s!"Compiling {name}"
|
||||
createParentDirs oFile
|
||||
proc {
|
||||
cmd := compiler.toString
|
||||
args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs
|
||||
}
|
||||
|
||||
def compileStaticLib (libFile : FilePath)
|
||||
def compileStaticLib (name : Name) (libFile : FilePath)
|
||||
(oFiles : Array FilePath) (ar : FilePath := "ar") : JobM Unit := do
|
||||
logAuxInfo s!"Linking {name}"
|
||||
createParentDirs libFile
|
||||
proc {
|
||||
cmd := ar.toString
|
||||
args := #["rcs", libFile.toString] ++ oFiles.map toString
|
||||
}
|
||||
|
||||
def compileSharedLib (libFile : FilePath)
|
||||
def compileSharedLib (name : Name) (libFile : FilePath)
|
||||
(linkArgs : Array String) (linker : FilePath := "cc") : JobM Unit := do
|
||||
logAuxInfo s!"Linking {name}"
|
||||
createParentDirs libFile
|
||||
proc {
|
||||
cmd := linker.toString
|
||||
args := #["-shared", "-o", libFile.toString] ++ linkArgs
|
||||
}
|
||||
|
||||
def compileExe (binFile : FilePath) (linkFiles : Array FilePath)
|
||||
def compileExe (name : Name) (binFile : FilePath) (linkFiles : Array FilePath)
|
||||
(linkArgs : Array String := #[]) (linker : FilePath := "cc") : JobM Unit := do
|
||||
logAuxInfo s!"Linking {name}"
|
||||
createParentDirs binFile
|
||||
proc {
|
||||
cmd := linker.toString
|
||||
|
|
|
|||
|
|
@ -21,4 +21,4 @@ protected def LeanExe.recBuildExe
|
|||
let deps := (← recBuild <| self.pkg.facet `deps).push self.pkg
|
||||
for dep in deps do for lib in dep.externLibs do
|
||||
linkTargets := linkTargets.push <| Target.active <| ← lib.static.recBuild
|
||||
leanExeTarget self.file linkTargets self.linkArgs |>.activate
|
||||
leanExeTarget self.name self.file linkTargets self.linkArgs |>.activate
|
||||
|
|
|
|||
|
|
@ -59,7 +59,7 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
|
|||
| .sharedExternLib lib =>
|
||||
mkTargetFacetBuild ExternLib.sharedFacet do
|
||||
let staticTarget := Target.active <| ← lib.static.recBuild
|
||||
staticToLeanSharedLibTarget staticTarget |>.activate
|
||||
staticToLeanSharedLibTarget lib.name staticTarget |>.activate
|
||||
| .dynlibExternLib lib =>
|
||||
mkTargetFacetBuild ExternLib.dynlibFacet do
|
||||
let sharedTarget := Target.active <| ← lib.shared.recBuild
|
||||
|
|
|
|||
|
|
@ -37,7 +37,7 @@ def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet :=
|
|||
protected def LeanLib.recBuildStatic
|
||||
(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
|
||||
let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active
|
||||
staticLibTarget self.staticLibFile oTargets |>.activate
|
||||
staticLibTarget self.name self.staticLibFile oTargets |>.activate
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
|
||||
def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
|
||||
|
|
@ -79,7 +79,7 @@ def LeanLib.recBuildLinks
|
|||
protected def LeanLib.recBuildShared
|
||||
(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
|
||||
let linkJobs := (← self.recBuildLinks).map Target.active
|
||||
leanSharedLibTarget self.sharedLibFile linkJobs self.linkArgs |>.activate
|
||||
leanSharedLibTarget self.name self.sharedLibFile linkJobs self.linkArgs |>.activate
|
||||
|
||||
/-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/
|
||||
def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet :=
|
||||
|
|
|
|||
|
|
@ -19,12 +19,12 @@ def Module.buildUnlessUpToDate (mod : Module)
|
|||
let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile
|
||||
if leanOnly then
|
||||
unless modUpToDate do
|
||||
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none
|
||||
compileLeanModule mod.name mod.leanFile mod.oleanFile mod.ileanFile none
|
||||
(← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
|
||||
else
|
||||
let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile
|
||||
unless modUpToDate && cUpToDate do
|
||||
compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
|
||||
compileLeanModule mod.name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile
|
||||
(← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean)
|
||||
modTrace.writeToFile mod.cTraceFile
|
||||
modTrace.writeToFile mod.traceFile
|
||||
|
|
@ -143,7 +143,7 @@ def Module.cFacetConfig : ModuleFacetConfig cFacet :=
|
|||
/-- Recursively build the module's object file from its C file produced by `lean`. -/
|
||||
def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do
|
||||
let cJob := Target.active (← self.c.recBuild)
|
||||
leanOFileTarget self.oFile cJob self.leancArgs |>.activate
|
||||
leanOFileTarget self.name self.oFile cJob self.leancArgs |>.activate
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
|
||||
def Module.oFacetConfig : ModuleFacetConfig oFacet :=
|
||||
|
|
@ -215,7 +215,7 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob String) := do
|
|||
let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
|
||||
let args := links.map toString ++
|
||||
libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}")
|
||||
compileSharedLib mod.dynlibFile args (← getLeanc)
|
||||
compileSharedLib mod.name mod.dynlibFile args (← getLeanc)
|
||||
return (mod.dynlibName, trace)
|
||||
|
||||
/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/
|
||||
|
|
|
|||
|
|
@ -47,44 +47,44 @@ def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget ι
|
|||
|
||||
/-! # Specific Targets -/
|
||||
|
||||
def oFileTarget (oFile : FilePath) (srcTarget : FileTarget)
|
||||
def oFileTarget (name : Name) (oFile : FilePath) (srcTarget : FileTarget)
|
||||
(args : Array String := #[]) (compiler : FilePath := "c++") : FileTarget :=
|
||||
fileTargetWithDep oFile srcTarget (extraDepTrace := computeHash args) fun srcFile => do
|
||||
compileO oFile srcFile args compiler
|
||||
compileO name oFile srcFile args compiler
|
||||
|
||||
def leanOFileTarget (oFile : FilePath)
|
||||
def leanOFileTarget (name : Name) (oFile : FilePath)
|
||||
(srcTarget : FileTarget) (args : Array String := #[]) : FileTarget :=
|
||||
fileTargetWithDep oFile srcTarget (extraDepTrace := computeHash args) fun srcFile => do
|
||||
compileO oFile srcFile args (← getLeanc)
|
||||
compileO name oFile srcFile args (← getLeanc)
|
||||
|
||||
def staticLibTarget (libFile : FilePath)
|
||||
def staticLibTarget (name : Name) (libFile : FilePath)
|
||||
(oFileTargets : Array FileTarget) (ar : Option FilePath := none) : FileTarget :=
|
||||
fileTargetWithDepArray libFile oFileTargets fun oFiles => do
|
||||
compileStaticLib libFile oFiles (ar.getD (← getLeanAr))
|
||||
compileStaticLib name libFile oFiles (ar.getD (← getLeanAr))
|
||||
|
||||
def cSharedLibTarget (libFile : FilePath)
|
||||
def cSharedLibTarget (name : Name) (libFile : FilePath)
|
||||
(linkTargets : Array FileTarget) (linkArgs : Array String := #[])
|
||||
(linker : FilePath := "cc"): FileTarget :=
|
||||
fileTargetWithDepArray libFile linkTargets fun links => do
|
||||
compileSharedLib libFile (links.map toString ++ linkArgs) linker
|
||||
compileSharedLib name libFile (links.map toString ++ linkArgs) linker
|
||||
|
||||
def leanSharedLibTarget (libFile : FilePath)
|
||||
def leanSharedLibTarget (name : Name) (libFile : FilePath)
|
||||
(linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
|
||||
fileTargetWithDepArray libFile linkTargets fun links => do
|
||||
compileSharedLib libFile (links.map toString ++ linkArgs) (← getLeanc)
|
||||
compileSharedLib name libFile (links.map toString ++ linkArgs) (← getLeanc)
|
||||
|
||||
def cExeTarget (exeFile : FilePath) (linkTargets : Array FileTarget)
|
||||
def cExeTarget (name : Name) (exeFile : FilePath) (linkTargets : Array FileTarget)
|
||||
(linkArgs : Array String := #[]) (linker : FilePath := "cc") : FileTarget :=
|
||||
fileTargetWithDepArray exeFile linkTargets (extraDepTrace := computeHash linkArgs) fun links => do
|
||||
compileExe exeFile links linkArgs linker
|
||||
compileExe name exeFile links linkArgs linker
|
||||
|
||||
def leanExeTarget (exeFile : FilePath)
|
||||
def leanExeTarget (name : Name) (exeFile : FilePath)
|
||||
(linkTargets : Array FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
|
||||
fileTargetWithDepArray exeFile linkTargets
|
||||
(extraDepTrace := getLeanTrace <&> (·.mix <| pureHash linkArgs)) fun links => do
|
||||
compileExe exeFile links linkArgs (← getLeanc)
|
||||
compileExe name exeFile links linkArgs (← getLeanc)
|
||||
|
||||
def staticToLeanSharedLibTarget (staticLibTarget : FileTarget) : FileTarget :=
|
||||
def staticToLeanSharedLibTarget (name : Name) (staticLibTarget : FileTarget) : FileTarget :=
|
||||
.mk <| staticLibTarget.bindSync fun staticLib staticTrace => do
|
||||
let dynlib := staticLib.withExtension sharedLibExt
|
||||
let trace ← buildFileUnlessUpToDate dynlib staticTrace do
|
||||
|
|
@ -93,7 +93,7 @@ def staticToLeanSharedLibTarget (staticLibTarget : FileTarget) : FileTarget :=
|
|||
#[s!"-Wl,-force_load,{staticLib}"]
|
||||
else
|
||||
#["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
|
||||
compileSharedLib dynlib args (← getLeanc)
|
||||
compileSharedLib name dynlib args (← getLeanc)
|
||||
return (dynlib, trace)
|
||||
|
||||
def sharedToLeanDynlibTarget (sharedLibTarget : FileTarget) : DynlibTarget :=
|
||||
|
|
|
|||
|
|
@ -18,6 +18,8 @@ OPTIONS:
|
|||
--help, -h print help of the program or a command and exit
|
||||
--dir, -d=file use the package configuration in a specific directory
|
||||
--file, -f=file use a specific file for the package configuration
|
||||
--quiet, -q hide progress messages
|
||||
--verbose, -v show verbose information (command invocations)
|
||||
--lean=cmd specify the `lean` command used by Lake
|
||||
-K key[=value] set the configuration file option named key
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,7 @@ structure LakeOptions where
|
|||
configOpts : NameMap String := {}
|
||||
subArgs : List String := []
|
||||
wantsHelp : Bool := false
|
||||
verbosity : Verbosity := .normal
|
||||
|
||||
/-- Get the Lean installation. Error if missing. -/
|
||||
def LakeOptions.getLeanInstall (opts : LakeOptions) : Except CliError LeanInstall :=
|
||||
|
|
@ -60,6 +61,7 @@ def LakeOptions.mkLoadConfig
|
|||
configFile := opts.rootDir / opts.configFile
|
||||
configOpts := opts.configOpts
|
||||
leanOpts := Lean.Options.empty
|
||||
verbosity := opts.verbosity
|
||||
updateDeps
|
||||
}
|
||||
|
||||
|
|
@ -77,6 +79,9 @@ def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do
|
|||
let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString
|
||||
main.run
|
||||
|
||||
instance : MonadLift LogIO CliStateM :=
|
||||
⟨fun x => do MainM.runLogIO x (← get).verbosity⟩
|
||||
|
||||
/-! ## Argument Parsing -/
|
||||
|
||||
def takeArg (arg : String) : CliM String := do
|
||||
|
|
@ -119,18 +124,22 @@ def setConfigOpt (kvPair : String) : CliM PUnit :=
|
|||
|
||||
def lakeShortOption : (opt : Char) → CliM PUnit
|
||||
| 'h' => modifyThe LakeOptions ({· with wantsHelp := true})
|
||||
| 'q' => modifyThe LakeOptions ({· with verbosity := .quiet})
|
||||
| 'v' => modifyThe LakeOptions ({· with verbosity := .verbose})
|
||||
| 'd' => do let rootDir ← takeOptArg "-d" "path"; modifyThe LakeOptions ({· with rootDir})
|
||||
| 'f' => do let configFile ← takeOptArg "-f" "path"; modifyThe LakeOptions ({· with configFile})
|
||||
| 'K' => do setConfigOpt <| ← takeOptArg "-K" "key-value pair"
|
||||
| opt => throw <| CliError.unknownShortOption opt
|
||||
|
||||
def lakeLongOption : (opt : String) → CliM PUnit
|
||||
| "--help" => modifyThe LakeOptions ({· with wantsHelp := true})
|
||||
| "--dir" => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
|
||||
| "--file" => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
|
||||
| "--lean" => do setLean <| ← takeOptArg "--lean" "path or command"
|
||||
| "--" => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
|
||||
| opt => throw <| CliError.unknownLongOption opt
|
||||
| "--help" => modifyThe LakeOptions ({· with wantsHelp := true})
|
||||
| "--quiet" => modifyThe LakeOptions ({· with verbosity := .quiet})
|
||||
| "--verbose" => modifyThe LakeOptions ({· with verbosity := .verbose})
|
||||
| "--dir" => do let rootDir ← takeOptArg "--dir" "path"; modifyThe LakeOptions ({· with rootDir})
|
||||
| "--file" => do let configFile ← takeOptArg "--file" "path"; modifyThe LakeOptions ({· with configFile})
|
||||
| "--lean" => do setLean <| ← takeOptArg "--lean" "path or command"
|
||||
| "--" => do let subArgs ← takeArgs; modifyThe LakeOptions ({· with subArgs})
|
||||
| opt => throw <| CliError.unknownLongOption opt
|
||||
|
||||
def lakeOption :=
|
||||
option {
|
||||
|
|
@ -175,9 +184,9 @@ def printPaths (config : LoadConfig) (imports : List String := []) : MainM PUnit
|
|||
if (← IO.getEnv invalidConfigEnvVar) matches some .. then
|
||||
IO.eprintln s!"Error parsing '{configFile}'. Please restart the lean server after fixing the Lake configuration file."
|
||||
exit 1
|
||||
let ws ← loadWorkspace config
|
||||
let ws ← MainM.runLogIO (loadWorkspace config) config.verbosity
|
||||
let ctx ← mkBuildContext ws
|
||||
let dynlibs ← ws.root.buildImportsAndDeps imports |>.run MonadLog.eio ctx
|
||||
let dynlibs ← ws.root.buildImportsAndDeps imports |>.run (MonadLog.eio config.verbosity) ctx
|
||||
IO.println <| Json.compress <| toJson {ws.leanPaths with loadDynlibPaths := dynlibs}
|
||||
else
|
||||
exit noConfigFileCode
|
||||
|
|
@ -200,11 +209,11 @@ def serve (config : LoadConfig) (args : Array String) : LogIO UInt32 := do
|
|||
env := extraEnv
|
||||
}).wait
|
||||
|
||||
def exe (name : Name) (args : Array String := #[]) : LakeT IO UInt32 := do
|
||||
def exe (name : Name) (args : Array String := #[]) (verbosity : Verbosity) : LakeT IO UInt32 := do
|
||||
let ws ← getWorkspace
|
||||
if let some exe := ws.findLeanExe? name then
|
||||
let ctx ← mkBuildContext ws
|
||||
let exeFile ← (exe.build >>= (·.await)).run MonadLog.eio ctx
|
||||
let exeFile ← (exe.build >>= (·.await)).run (MonadLog.eio verbosity) ctx
|
||||
env exeFile.toString args
|
||||
else
|
||||
error s!"unknown executable `{name}`"
|
||||
|
|
@ -287,13 +296,13 @@ protected def new : CliM PUnit := do
|
|||
processOptions lakeOption
|
||||
let pkgName ← takeArg "package name"
|
||||
let template ← parseTemplateSpec <| (← takeArg?).getD ""
|
||||
noArgsRem <| new pkgName template
|
||||
noArgsRem <| MainM.runLogIO (new pkgName template) (← getThe LakeOptions).verbosity
|
||||
|
||||
protected def init : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
let pkgName ← takeArg "package name"
|
||||
let template ← parseTemplateSpec <| (← takeArg?).getD ""
|
||||
noArgsRem <| init pkgName template
|
||||
noArgsRem <| MainM.runLogIO (init pkgName template) (← getThe LakeOptions).verbosity
|
||||
|
||||
protected def build : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
|
|
@ -303,7 +312,7 @@ protected def build : CliM PUnit := do
|
|||
let targetSpecs ← takeArgs
|
||||
let specs ← parseTargetSpecs ws targetSpecs
|
||||
let ctx ← mkBuildContext ws
|
||||
BuildM.run MonadLog.io ctx <| buildSpecs specs
|
||||
BuildM.run (MonadLog.io config.verbosity) ctx <| buildSpecs specs
|
||||
|
||||
protected def update : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
|
|
@ -349,7 +358,7 @@ protected def exe : CliM PUnit := do
|
|||
let config ← mkLoadConfig (← getThe LakeOptions)
|
||||
let ws ← loadWorkspace config
|
||||
let ctx := mkLakeContext ws
|
||||
exit <| ← (exe exeName args.toArray).run ctx
|
||||
exit <| ← (exe exeName args.toArray config.verbosity).run ctx
|
||||
|
||||
protected def selfCheck : CliM PUnit := do
|
||||
processOptions lakeOption
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ import Lean.Util.Paths
|
|||
import Lake.Config.FacetConfig
|
||||
import Lake.Config.TargetConfig
|
||||
import Lake.Config.Env
|
||||
import Lake.Util.Log
|
||||
|
||||
open System
|
||||
open Lean (LeanPaths)
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Mac Malone
|
|||
import Lean.Data.Name
|
||||
import Lean.Data.Options
|
||||
import Lake.Config.Env
|
||||
import Lake.Util.Log
|
||||
|
||||
namespace Lake
|
||||
open System Lean
|
||||
|
|
@ -25,6 +26,8 @@ structure LoadConfig where
|
|||
configOpts : NameMap String := {}
|
||||
/-- The Lean options with which to elaborate the configuration file. -/
|
||||
leanOpts : Options := {}
|
||||
/-- The verbosity setting for logging messages. -/
|
||||
verbosity : Verbosity := .normal
|
||||
/--
|
||||
Whether to update dependencies during resolution
|
||||
or fallback to the ones listed in the manifest.
|
||||
|
|
|
|||
|
|
@ -12,13 +12,28 @@ inductive LogLevel
|
|||
| warning
|
||||
| error
|
||||
|
||||
inductive Verbosity
|
||||
| quiet
|
||||
| normal
|
||||
| verbose
|
||||
deriving BEq
|
||||
|
||||
instance : Inhabited Verbosity := ⟨.normal⟩
|
||||
|
||||
/-! # Class -/
|
||||
|
||||
class MonadLog (m : Type u → Type v) where
|
||||
verbosity : m (ULift Verbosity)
|
||||
log (message : String) (level : LogLevel) : m PUnit
|
||||
|
||||
export MonadLog (log)
|
||||
|
||||
abbrev logVerbose [Monad m] [MonadLog m] (message : String) : m PUnit := do
|
||||
if (← MonadLog.verbosity (m := m)).1 == .verbose then log message .info
|
||||
|
||||
abbrev logAuxInfo [Monad m] [MonadLog m] (message : String) : m PUnit := do
|
||||
if (← MonadLog.verbosity (m := m)).1 != .quiet then log message .info
|
||||
|
||||
abbrev logInfo [MonadLog m] (message : String) : m PUnit :=
|
||||
log message .info
|
||||
|
||||
|
|
@ -31,26 +46,29 @@ abbrev logError [MonadLog m] (message : String) : m PUnit :=
|
|||
namespace MonadLog
|
||||
|
||||
def nop [Pure m] : MonadLog m :=
|
||||
⟨fun _ _ => pure ()⟩
|
||||
⟨pure ⟨.normal⟩, fun _ _ => pure ()⟩
|
||||
|
||||
instance [Pure m] : Inhabited (MonadLog m) := ⟨MonadLog.nop⟩
|
||||
|
||||
def io [MonadLiftT BaseIO m] : MonadLog m where
|
||||
def io [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
verbosity := (pure ⟨verbosity⟩ : BaseIO _)
|
||||
log msg
|
||||
| .info => IO.println msg.trim |>.catchExceptions fun _ => pure ()
|
||||
| .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
|
||||
def eio [MonadLiftT BaseIO m] : MonadLog m where
|
||||
def eio [MonadLiftT BaseIO m] (verbosity := Verbosity.normal) : MonadLog m where
|
||||
verbosity := (pure ⟨verbosity⟩ : BaseIO _)
|
||||
log msg
|
||||
| .info => IO.eprintln s!"info: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .info => IO.eprintln s!"info: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .warning => IO.eprintln s!"warning: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
| .error => IO.eprintln s!"error: {msg.trim}" |>.catchExceptions fun _ => pure ()
|
||||
|
||||
def lift [MonadLiftT m n] (self : MonadLog m) : MonadLog n where
|
||||
verbosity := liftM <| self.verbosity
|
||||
log msg lv := liftM <| self.log msg lv
|
||||
|
||||
instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
|
||||
instance [MonadLift m n] [methods : MonadLog m] : MonadLog n := lift methods
|
||||
|
||||
/-- Log the given error message and then fail. -/
|
||||
protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
|
||||
|
|
@ -67,6 +85,7 @@ instance [Pure n] [Inhabited α] : Inhabited (MonadLogT m n α) :=
|
|||
⟨fun _ => pure Inhabited.default⟩
|
||||
|
||||
instance [Monad n] [MonadLiftT m n] : MonadLog (MonadLogT m n) where
|
||||
verbosity := do (← read).verbosity
|
||||
log msg lv := do (← read).log msg lv
|
||||
|
||||
namespace MonadLogT
|
||||
|
|
|
|||
|
|
@ -75,4 +75,8 @@ protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
|
|||
instance : MonadError MainM := ⟨MainM.error⟩
|
||||
instance [ToString ε] : MonadLift (EIO ε) MainM := ⟨MonadError.runEIO⟩
|
||||
instance : MonadLift IO MainM := inferInstance -- necessary, but don't know why
|
||||
instance : MonadLift LogIO MainM := ⟨fun x => liftM <| x.run MonadLog.eio⟩
|
||||
|
||||
def runLogIO (x : LogIO α) (verbosity := Verbosity.normal) : MainM α :=
|
||||
liftM <| MonadLogT.run (MonadLog.eio verbosity) x
|
||||
|
||||
instance : MonadLift LogIO MainM := ⟨runLogIO⟩
|
||||
|
|
|
|||
|
|
@ -20,8 +20,8 @@ def ffiOTarget : FileTarget :=
|
|||
let oFile := cBuildDir / "ffi.o"
|
||||
let srcTarget := inputFileTarget <| cSrcDir / "ffi.cpp"
|
||||
fileTargetWithDep oFile srcTarget fun srcFile => do
|
||||
compileO oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC"] "c++"
|
||||
compileO `ffi oFile srcFile #["-I", (← getLeanIncludeDir).toString, "-fPIC"] "c++"
|
||||
|
||||
extern_lib cLib :=
|
||||
let libFile := cBuildDir / nameToStaticLib "leanffi"
|
||||
staticLibTarget libFile #[ffiOTarget]
|
||||
staticLibTarget `leanffi libFile #[ffiOTarget]
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ LAKE=${LAKE:-../../../build/bin/lake}
|
|||
|
||||
cd foo
|
||||
rm -rf build
|
||||
${LAKE} build -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m2 foo.c
|
||||
${LAKE} build -KleanArgs=-Dhygiene=false -K leancArgs=-DBAZ | grep -m2 foo.c
|
||||
${LAKE} build -KleanArgs=-Dhygiene=false -K leancArgs=-DBAR | grep -m1 foo.o
|
||||
${LAKE} build -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m1 foo.olean
|
||||
${LAKE} build -v -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m2 foo.c
|
||||
${LAKE} build -v -KleanArgs=-Dhygiene=false -K leancArgs=-DBAZ | grep -m2 foo.c
|
||||
${LAKE} build -v -KleanArgs=-Dhygiene=false -K leancArgs=-DBAR | grep -m1 foo.o
|
||||
${LAKE} build -v -KleanArgs=-Dhygiene=true -K leancArgs=-DBAR | grep -m1 foo.olean
|
||||
|
|
|
|||
|
|
@ -9,4 +9,4 @@ lake +leanprover/lean4:nightly-2022-06-30 new foo
|
|||
cd foo
|
||||
lake +leanprover/lean4:nightly-2022-06-30 build | grep -m1 foo
|
||||
cp ../../../lean-toolchain lean-toolchain
|
||||
${LAKE:-../../../build/bin/lake} build | grep -m1 foo
|
||||
${LAKE:-../../../build/bin/lake} build -v | grep -m1 foo
|
||||
|
|
|
|||
|
|
@ -32,6 +32,6 @@ git commit -am 'second commit in a'
|
|||
popd
|
||||
|
||||
pushd b
|
||||
$LAKE1 update
|
||||
$LAKE1 update -v
|
||||
git diff | grep -m1 manifest
|
||||
popd
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue