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

chore: convert doc/mod comments from /- to /--//-!

Browse source
This commit is contained in:
Mario Carneiro 2022-07-22 10:07:18 -04:00 • committed by Mac
parent 6caea9306c
commit fc34cd2b8e
24 changed files with 77 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
Lake/Build/Facets.lean
View file

@ -17,7 +17,7 @@ import said configurations for `BuildInfo`.
namespace Lake
-- ## Module Facets
/-! ## Module Facets -/
/-- A module facet name along with proof of its data type. -/
structure ModuleFacet (α) where
@ -65,12 +65,12 @@ module_data lean.o : ActiveFileTarget
/-- Shared library for `--load-dynlib` -/
module_data dynlib : ActiveFileTarget
-- ## Package Facets
/-! ## Package Facets -/
/-- The package's `extraDepTarget`. -/
package_data extraDep : ActiveOpaqueTarget
-- ## Target Facets
/-! ## Target Facets -/
abbrev LeanLib.staticFacet := `leanLib.static
abbrev LeanLib.sharedFacet := `leanLib.shared

4
Lake/Build/Index.lean
View file

@ -195,12 +195,12 @@ and a topological / suspending scheduler and return the dynamic result.
end
/- Build the given Lake target using the given Lake build store. -/
/-- Build the given Lake target using the given Lake build store. -/
@[inline] def BuildInfo.buildIn (store : BuildStore) (self : BuildInfo)
[FamilyDef BuildData self.key α] : BuildM α := do
failOnBuildCycle <| ← EStateT.run' (m := BuildM) store <| buildIndexTop self
/- Build the given Lake target in a fresh build store. -/
/-- Build the given Lake target in a fresh build store. -/
@[inline] def BuildInfo.build (self : BuildInfo) [FamilyDef BuildData self.key α] : BuildM α :=
buildIn BuildStore.empty self

8
Lake/Build/IndexTargets.lean
View file

@ -10,7 +10,7 @@ open Lean hiding SearchPath
namespace Lake
-- # Module Facet Targets
/-! # Module Facet Targets -/
@[inline] def Module.facetTarget (facet : Name) (self : Module)
[FamilyDef ModuleData facet (ActiveBuildTarget α)] : OpaqueTarget :=
@ -28,7 +28,7 @@ namespace Lake
@[inline] def Module.oTarget (self : Module) : FileTarget :=
self.facetTarget oFacet |>.withInfo self.oFile
-- # Pure Lean Lib Targets
/-! # Pure Lean Lib Targets -/
/--
Build the `extraDepTarget` of a package and its (transitive) dependencies
@ -50,7 +50,7 @@ def LeanLib.buildModules (self : LeanLib) (facet : Name)
@[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget :=
self.builtinLib.leanTarget
-- # Native Lean Lib Targets
/-! # Native Lean Lib Targets -/
@[inline] protected def LeanLib.staticLibTarget (self : LeanLib) : FileTarget :=
self.static.target.withInfo self.sharedLibFile
@ -64,7 +64,7 @@ def LeanLib.buildModules (self : LeanLib) (facet : Name)
@[inline] protected def Package.sharedLibTarget (self : Package) : FileTarget :=
self.builtinLib.sharedLibTarget
-- # Lean Executable Targets
/-! # Lean Executable Targets -/
@[inline] protected def LeanExe.build (self : LeanExe) : BuildM ActiveFileTarget :=
self.exe.build

4
Lake/Build/Module.lean
View file

@ -12,7 +12,7 @@ open System
namespace Lake
-- # Solo Module Targets
/-! # Solo Module Targets -/
def Module.soloTarget (mod : Module) (dynlibs : Array String)
(dynlibPath : SearchPath) (depTarget : BuildTarget x) (leanOnly : Bool) : OpaqueTarget :=
@ -62,7 +62,7 @@ def Module.mkDynlibTarget (self : Module) (linkTargets : Array FileTarget)
let args := links.map toString ++ libDirs.map (s!"-L{·}") ++ libFiles.map (s!"-l{·}")
compileSharedLib self.dynlibFile args (← getLeanc)
-- # Recursive Building
/-! # Recursive Building -/
section
variable [Monad m] [MonadBuildStore m]

6
Lake/Build/Roots.lean
View file

@ -11,7 +11,7 @@ namespace Lake
variable [Monad m] [MonadLiftT BuildM m] [MonadBuildStore m]
-- # Build Static Lib
/-! # Build Static Lib -/
/-- Build and collect the specified facet of the library's local modules. -/
@[specialize] def LeanLib.recBuildLocalModules
@ -37,7 +37,7 @@ def LeanLib.recBuildStatic (self : LeanLib) : IndexT m ActiveFileTarget := do
let oTargets := (← self.recBuildLocalModules self.nativeFacets).map Target.active
staticLibTarget self.staticLibFile oTargets |>.activate
-- # Build Shared Lib
/-! # Build Shared Lib -/
/--
Build and collect the local object files and external libraries
@ -78,7 +78,7 @@ def LeanLib.recBuildShared (self : LeanLib) : IndexT m ActiveFileTarget := do
let linkTargets := (← self.recBuildLinks self.nativeFacets).map Target.active
leanSharedLibTarget self.sharedLibFile linkTargets self.linkArgs |>.activate
-- # Build Executable
/-! # Build Executable -/
@[specialize] protected
def LeanExe.recBuild (self : LeanExe) : IndexT m ActiveFileTarget := do

4
Lake/Build/Target.lean
View file

@ -10,7 +10,7 @@ open System
namespace Lake
--------------------------------------------------------------------------------
-- # Active Targets
/-! # Active Targets -/
--------------------------------------------------------------------------------
structure ActiveTarget.{u,v,w} (i : Type u) (k : Type v → Type w) (t : Type v) where
@ -93,7 +93,7 @@ end
end ActiveTarget
--------------------------------------------------------------------------------
-- # Inactive Target
/-! # Inactive Target -/
--------------------------------------------------------------------------------
structure Target.{u,v,v',w} (i : Type u) (n : Type v → Type w) (k : Type v' → Type v) (t : Type v') where

6
Lake/Build/TargetTypes.lean
View file

@ -10,7 +10,7 @@ open System
namespace Lake
--------------------------------------------------------------------------------
-- # Build Targets
/-! # Build Targets -/
--------------------------------------------------------------------------------
/-- A Lake build target. -/
@ -49,7 +49,7 @@ abbrev bindOpaqueSync (self : ActiveBuildTarget i) (f : BuildTrace → BuildM β
end ActiveBuildTarget
--------------------------------------------------------------------------------
-- # File Targets
/-! # File Targets -/
--------------------------------------------------------------------------------
/-- A `BuildTarget` that produces a file. -/
@ -59,7 +59,7 @@ abbrev FileTarget := BuildTarget FilePath
abbrev ActiveFileTarget := ActiveBuildTarget FilePath
--------------------------------------------------------------------------------
-- # Opaque Targets
/-! # Opaque Targets -/
--------------------------------------------------------------------------------
/-- A `BuildTarget` with no artifact information. -/

4
Lake/Build/Targets.lean
View file

@ -9,7 +9,7 @@ import Lake.Build.TargetTypes
open System
namespace Lake
-- # General Utilities
/-! # General Utilities -/
def inputFileTarget (path : FilePath) : FileTarget :=
Target.mk path <| async (m := BuildM) <| computeTrace path
@ -42,7 +42,7 @@ def fileTargetWithDepArray (file : FilePath) (depTargets : Array (BuildTarget i)
(build : Array i → BuildM PUnit) (extraDepTrace : BuildM _ := pure BuildTrace.nil) : FileTarget :=
fileTargetWithDep file (Target.collectArray depTargets) build extraDepTrace
-- # Specific Targets
/-! # Specific Targets -/
def oFileTarget (oFile : FilePath) (srcTarget : FileTarget)
(args : Array String := #[]) (compiler : FilePath := "c++") : FileTarget :=

4
Lake/Build/Topological.lean
View file

@ -19,7 +19,7 @@ This is called a suspending scheduler in *Build systems à la carte*.
open Std
namespace Lake
-- ## Abstractions
/-! ## Abstractions -/
/-- A dependently typed object builder. -/
abbrev DBuildFn.{u,v,w} (ι : Type u) (β : ι → Type v) (m : Type v → Type w) :=
@ -36,7 +36,7 @@ abbrev RecBuildFn ι α m := DRecBuildFn ι (fun _ => α) m
abbrev CycleT (κ) :=
ExceptT (List κ)
-- ## Algorithm
/-! ## Algorithm -/
/-- Auxiliary function for `buildTop`. -/
@[specialize] partial def buildTopCore [BEq κ] [Monad m] [MonadDStore κ β m]

10
Lake/Build/Trace.lean
View file

@ -8,7 +8,7 @@ open System
namespace Lake
--------------------------------------------------------------------------------
-- # Utilities
/-! # Utilities -/
--------------------------------------------------------------------------------
class CheckExists.{u} (i : Type u) where
@ -21,7 +21,7 @@ instance : CheckExists FilePath where
checkExists := FilePath.pathExists
--------------------------------------------------------------------------------
-- # Trace Abstraction
/-! # Trace Abstraction -/
--------------------------------------------------------------------------------
class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t : Type v) where
@ -71,7 +71,7 @@ instance [Monad m] : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩
end
--------------------------------------------------------------------------------
-- # Hash Trace
/-! # Hash Trace -/
--------------------------------------------------------------------------------
/--
@ -135,7 +135,7 @@ instance [ComputeHash α m] [Monad m] : ComputeHash (Array α) m where
computeHash ar := ar.foldlM (fun b a => Hash.mix b <$> computeHash a) Hash.nil
--------------------------------------------------------------------------------
-- # Modification Time (MTime) Trace
/-! # Modification Time (MTime) Trace -/
--------------------------------------------------------------------------------
open IO.FS (SystemTime)
@ -175,7 +175,7 @@ def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : IO Bool := do
try pure ((← getMTime info) >= depMTime) catch _ => pure false
--------------------------------------------------------------------------------
-- # Lake Build Trace (Hash + MTIme)
/-! # Lake Build Trace (Hash + MTIme) -/
--------------------------------------------------------------------------------
/-- Trace used for common Lake targets. Combines `Hash` and `MTime`. -/

16
Lake/CLI/Main.lean
View file

@ -19,7 +19,7 @@ open Lean (Json toJson fromJson?)
namespace Lake
-- ## General options for top-level `lake`
/-! ## General options for top-level `lake` -/
structure LakeOptions where
rootDir : FilePath := "."
@ -64,7 +64,7 @@ def LakeOptions.mkLoadConfig
export LakeOptions (mkLoadConfig)
-- ## Monad
/-! ## Monad -/
abbrev CliMainM := ExceptT CliError MainM
abbrev CliStateM := StateT LakeOptions CliMainM
@ -76,7 +76,7 @@ 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
-- ## Argument Parsing
/-! ## Argument Parsing -/
def takeArg (arg : String) : CliM String := do
match (← takeArg?) with
@ -97,7 +97,7 @@ def noArgsRem (act : CliStateM α) : CliM α := do
if args.isEmpty then act else
throw <| CliError.unexpectedArguments args
-- ## Option Parsing
/-! ## Option Parsing -/
def getWantsHelp : CliStateM Bool :=
(·.wantsHelp) <$> get
@ -138,7 +138,7 @@ def lakeOption :=
longShort := shortOptionWithArg lakeShortOption
}
-- ## Actions
/-! ## Actions -/
/-- Verify the Lean version Lake was built with matches that of the give Lean installation. -/
def verifyLeanVersion (leanInstall : LeanInstall) : Except CliError PUnit := do
@ -222,11 +222,11 @@ def parseTemplateSpec (spec : String) : Except CliError InitTemplate :=
else
throw <| CliError.unknownTemplate spec
-- ## Commands
/-! ## Commands -/
namespace lake
-- ### `lake script` CLI
/-! ### `lake script` CLI -/
namespace script
@ -280,7 +280,7 @@ def scriptCli : (cmd : String) → CliM PUnit
| "help" => script.help
| cmd => throw <| CliError.unknownCommand cmd
-- ### `lake` CLI
/-! ### `lake` CLI -/
protected def new : CliM PUnit := do
processOptions lakeOption

2
Lake/Config/ExternLib.lean
View file

@ -25,7 +25,7 @@ structure ExternLib where
namespace ExternLib
/- The library's well-formed name. -/
/-- The library's well-formed name. -/
@[inline] def name (self : ExternLib) : Name :=
self.config.name

4
Lake/Config/LeanExe.lean
View file

@ -40,7 +40,7 @@ def LeanExeConfig.toLeanLibConfig (self : LeanExeConfig) : LeanLibConfig where
namespace LeanExe
/- The executable's well-formed name. -/
/-- The executable's well-formed name. -/
@[inline] def name (self : LeanExe) : Name :=
self.config.name
@ -54,7 +54,7 @@ namespace LeanExe
name := self.config.root
keyName := self.pkg.name ++ self.config.root
/- Return the the root module if the name matches, otherwise return none. -/
/-- Return the the root module if the name matches, otherwise return none. -/
def isRoot? (name : Name) (self : LeanExe) : Option Module :=
if name == self.config.root then some self.root else none

4
Lake/Config/LeanLib.lean
View file

@ -30,11 +30,11 @@ structure LeanLib where
namespace LeanLib
/- The library's well-formed name. -/
/-- The library's well-formed name. -/
@[inline] def name (self : LeanLib) : Name :=
self.config.name
/- The package's `srcDir` joined with the library's `srcDir`. -/
/-- The package's `srcDir` joined with the library's `srcDir`. -/
@[inline] def srcDir (self : LeanLib) : FilePath :=
self.pkg.srcDir / self.config.srcDir

2
Lake/Config/Module.lean
View file

@ -106,7 +106,7 @@ abbrev pkg (self : Module) : Package :=
@[inline] def isLeanOnly (self : Module) : Bool :=
self.pkg.isLeanOnly && !self.shouldPrecompile
-- ## Trace Helpers
/-! ## Trace Helpers -/
protected def getMTime (self : Module) : IO MTime := do
return mixTrace (← getMTime self.oleanFile) (← getMTime self.ileanFile)

10
Lake/Config/Monad.lean
View file

@ -38,7 +38,7 @@ variable [MonadWorkspace m] [Functor m]
instance : MonadLakeEnv m where
read := (·.lakeEnv) <$> read
/- ## Workspace Helpers -/
/-! ## Workspace Helpers -/
@[inline] def getWorkspace : m Workspace :=
read
@ -91,12 +91,12 @@ end
section
variable [MonadLakeEnv m] [Functor m]
/- ## Environment Helpers -/
/-! ## Environment Helpers -/
@[inline] def getLakeEnv : m Lake.Env :=
read
/- ### Lean Install Helpers -/
/-! ### Lean Install Helpers -/
@[inline] def getLeanInstall : m LeanInstall :=
(·.lean) <$> getLakeEnv
@ -135,7 +135,7 @@ variable [MonadLakeEnv m] [Functor m]
@[inline] def getLeanCc? : m (Option String) :=
(·.leanCc?) <$> getLeanInstall
/- ### Lake Install Helpers -/
/-! ### Lake Install Helpers -/
@[inline] def getLakeInstall : m LakeInstall :=
(·.lake) <$> getLakeEnv
@ -152,7 +152,7 @@ variable [MonadLakeEnv m] [Functor m]
@[inline] def getLake : m FilePath :=
(·.lake) <$> getLakeInstall
/- ### Search Path Helpers -/
/-! ### Search Path Helpers -/
/-- Get the detected `LEAN_PATH` value of the Lake environment. -/
@[inline] def getEnvLeanPath : m SearchPath :=

18
Lake/Config/Package.lean
View file

@ -17,7 +17,7 @@ open Std System Lean
namespace Lake
--------------------------------------------------------------------------------
-- # Defaults
/-! # Defaults -/
--------------------------------------------------------------------------------
/-- The default setting for a `PackageConfig`'s `buildDir` option. -/
@ -39,10 +39,10 @@ def defaultIrDir : FilePath := "ir"
def defaultBinRoot : Name := `Main
--------------------------------------------------------------------------------
-- # PackageFacet
/-! # PackageFacet -/
--------------------------------------------------------------------------------
/- A buildable component of a `Package`. -/
/-- A buildable component of a `Package`. -/
inductive PackageFacet
| /-- The package's binary executable. -/ exe
| /-- The package's static library. -/ staticLib
@ -53,7 +53,7 @@ deriving BEq, DecidableEq, Repr
instance : Inhabited PackageFacet := ⟨PackageFacet.exe⟩
--------------------------------------------------------------------------------
-- # PackageConfig
/-! # PackageConfig -/
--------------------------------------------------------------------------------
/-- A `Package`'s declarative configuration. -/
@ -235,7 +235,7 @@ def toLeanExeConfig (self : PackageConfig) : LeanExeConfig where
end PackageConfig
--------------------------------------------------------------------------------
-- # Package
/-! # Package -/
--------------------------------------------------------------------------------
abbrev DNameMap α := DRBMap Name α Lean.Name.quickCmp
@ -250,7 +250,7 @@ structure Package where
configEnv : Environment
/-- The Lean `Options` the package configuration was elaborated with. -/
leanOpts : Options
/- (Opaque references to) the package's direct dependencies. -/
/-- (Opaque references to) the package's direct dependencies. -/
opaqueDeps : Array OpaquePackage := #[]
/-- Lean library configurations for the package. -/
leanLibConfigs : NameMap LeanLibConfig := {}
@ -284,7 +284,7 @@ namespace Package
@[inline] def name (self : Package) : Name :=
self.config.name
/- An `Array` of the package's direct dependencies. -/
/-- An `Array` of the package's direct dependencies. -/
@[inline] def deps (self : Package) : Array Package :=
self.opaqueDeps.map (·.get)
@ -324,7 +324,7 @@ namespace Package
@[inline] def oleanDir (self : Package) : FilePath :=
self.buildDir / self.config.oleanDir
/- The package's `buildType` configuration. -/
/-- The package's `buildType` configuration. -/
@[inline] def buildType (self : Package) : BuildType :=
self.config.buildType
@ -332,7 +332,7 @@ namespace Package
@[inline] def moreLeanArgs (self : Package) : Array String :=
self.config.moreLeanArgs
/- The package's `moreLeancArgs` configuration. -/
/-- The package's `moreLeancArgs` configuration. -/
@[inline] def moreLeancArgs (self : Package) : Array String :=
self.config.moreLeancArgs

4
Lake/DSL/Targets.lean
View file

@ -13,7 +13,7 @@ namespace Lake.DSL
open Lean Parser Command
--------------------------------------------------------------------------------
-- # Lean Library & Executable Targets
/-! # Lean Library & Executable Targets -/
--------------------------------------------------------------------------------
/--
@ -57,7 +57,7 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
mkConfigStructDecl none doc? attrs ty sig
--------------------------------------------------------------------------------
-- # External Library Target
/-! # External Library Target -/
--------------------------------------------------------------------------------
syntax externLibDeclSpec :=

20
Lake/Util/Async.lean
View file

@ -22,28 +22,28 @@ between these monads and combining them in different ways.
namespace Lake
--------------------------------------------------------------------------------
-- # Async / Await Abstraction
/-! # Async / Await Abstraction -/
--------------------------------------------------------------------------------
class Sync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
/- Run the monadic action as a synchronous task. -/
/-- Run the monadic action as a synchronous task. -/
sync : m α → n (k α)
export Sync (sync)
class Async (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
/- Run the monadic action as an asynchronous task. -/
/-- Run the monadic action as an asynchronous task. -/
async : m α → n (k α)
export Async (async)
class Await (k : Type u → Type v) (m : outParam $ Type u → Type w) where
/- Wait for an (a)synchronous task to finish. -/
/-- Wait for an (a)synchronous task to finish. -/
await : k α → m α
export Await (await)
-- ## Standard Instances
/-! ## Standard Instances -/
instance : Sync Id Id Task := ⟨Task.pure⟩
instance : Sync BaseIO BaseIO BaseIOTask := ⟨Functor.map Task.pure⟩
@ -96,7 +96,7 @@ instance [Await k m] : Await (OptionT k) (OptionT m) where
await x := OptionT.mk <| await x.run
--------------------------------------------------------------------------------
-- # Combinators
/-! # Combinators -/
--------------------------------------------------------------------------------
class BindSync (m : Type u → Type v) (n : outParam $ Type u' → Type w) (k : outParam $ Type u → Type u') where
@ -141,7 +141,7 @@ extends SeqAsync n k, SeqLeftAsync n k, SeqRightAsync n k, SeqWithAsync n k wher
seqLeftAsync := seqWithAsync fun a _ => a
seqRightAsync := seqWithAsync fun _ b => b
-- ## Standard Instances
/-! ## Standard Instances -/
instance : BindSync Id Id Task := ⟨flip Task.map⟩
instance : BindSync BaseIO BaseIO BaseIOTask := ⟨flip BaseIO.mapTask⟩
@ -212,10 +212,10 @@ instance [ApplicativeAsync n k] : ApplicativeAsync n (OptionT k) where
cast (by delta OptionT; rfl) <| seqWithAsync (n := n) h ka kb
--------------------------------------------------------------------------------
-- # List/Array Utilities
/-! # List/Array Utilities -/
--------------------------------------------------------------------------------
-- ## Sequencing (A)synchronous Tasks
/-! ## Sequencing (A)synchronous Tasks -/
/-- Combine all (a)synchronous tasks in a `List` from right to left into a single task ending `last`. -/
def seqLeftList1Async [SeqLeftAsync n k] [Monad n] (last : (k α)) : (tasks : List (k α)) → n (k α)
@ -246,7 +246,7 @@ def seqRightArrayAsync [SeqRightAsync n k] [Monad n] [Pure k] (tasks : Array (k
else
return (pure ())
-- ## Folding (A)synchronous Tasks
/-! ## Folding (A)synchronous Tasks -/
variable [SeqWithAsync n k] [Monad n] [Pure k]

4
Lake/Util/Cli.lean
View file

@ -10,7 +10,7 @@ namespace Lake
Defines the abstract CLI interface for Lake.
-/
-- # Types
/-! # Types -/
def ArgList := List String
@ -33,7 +33,7 @@ structure OptionHandlers (m : Type u → Type v) (α : Type u) where
/-- Process a long short option (ex. `-long`, `-xarg`, `-xyz`). -/
longShort : String → m α
-- # Utilities
/-! # Utilities -/
variable [Monad m] [MonadStateOf ArgList m]

2
Lake/Util/EvalTerm.lean
View file

@ -40,7 +40,7 @@ unsafe def unsafeEvalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α := do
@[implementedBy unsafeEvalTerm]
opaque evalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α
-- ## ToExpr Instances
/-! ## ToExpr Instances -/
instance : ToExpr System.FilePath where
toExpr p := mkApp (mkConst ``System.FilePath.mk) (toExpr p.toString)

4
Lake/Util/Log.lean
View file

@ -12,7 +12,7 @@ inductive LogLevel
| warning
| error
-- # Class
/-! # Class -/
class MonadLog (m : Type u → Type v) where
log (message : String) (level : LogLevel) : m PUnit
@ -58,7 +58,7 @@ protected def error [Alternative m] [MonadLog m] (msg : String) : m α :=
end MonadLog
-- # Transformers
/-! # Transformers -/
abbrev MonadLogT (m : Type u → Type v) (n : Type v → Type w) :=
ReaderT (MonadLog m) n

6
Lake/Util/MainM.lean
View file

@ -21,7 +21,7 @@ instance : MonadLift BaseIO MainM := inferInstanceAs (MonadLift BaseIO (EIO Exit
namespace MainM
-- # Basics
/-! # Basics -/
@[inline] protected def mk (x : EIO ExitCode α) : MainM α :=
x
@ -35,7 +35,7 @@ namespace MainM
protected def run (self : MainM α) : BaseIO ExitCode :=
self.toBaseIO.map fun | Except.ok _ => 0 | Except.error rc => rc
-- # Exits
/-! # Exits -/
/-- Exit with given return code. -/
protected def exit (rc : ExitCode) : MainM α :=
@ -63,7 +63,7 @@ instance : Alternative MainM where
failure := MainM.failure
orElse := MainM.orElse
-- # Logging and IO
/-! # Logging and IO -/
instance : MonadLog MainM := MonadLog.eio

2
Lake/Util/Name.lean
View file

@ -12,7 +12,7 @@ namespace Lake
export Lean (Name NameMap)
-- # Name Helpers
/-! # Name Helpers -/
namespace Name
open Lean.Name