From fc34cd2b8e3b338ac09820c7221adecf7b38cc23 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 22 Jul 2022 10:07:18 -0400 Subject: [PATCH] chore: convert doc/mod comments from `/-` to `/--`/`/-!` --- Lake/Build/Facets.lean | 6 +++--- Lake/Build/Index.lean | 4 ++-- Lake/Build/IndexTargets.lean | 8 ++++---- Lake/Build/Module.lean | 4 ++-- Lake/Build/Roots.lean | 6 +++--- Lake/Build/Target.lean | 4 ++-- Lake/Build/TargetTypes.lean | 6 +++--- Lake/Build/Targets.lean | 4 ++-- Lake/Build/Topological.lean | 4 ++-- Lake/Build/Trace.lean | 10 +++++----- Lake/CLI/Main.lean | 16 ++++++++-------- Lake/Config/ExternLib.lean | 2 +- Lake/Config/LeanExe.lean | 4 ++-- Lake/Config/LeanLib.lean | 4 ++-- Lake/Config/Module.lean | 2 +- Lake/Config/Monad.lean | 10 +++++----- Lake/Config/Package.lean | 18 +++++++++--------- Lake/DSL/Targets.lean | 4 ++-- Lake/Util/Async.lean | 20 ++++++++++---------- Lake/Util/Cli.lean | 4 ++-- Lake/Util/EvalTerm.lean | 2 +- Lake/Util/Log.lean | 4 ++-- Lake/Util/MainM.lean | 6 +++--- Lake/Util/Name.lean | 2 +- 24 files changed, 77 insertions(+), 77 deletions(-) diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 9fa87f79fd..b868a2875d 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -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 diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index dc85536c9c..4394a00fb0 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -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 diff --git a/Lake/Build/IndexTargets.lean b/Lake/Build/IndexTargets.lean index 992d631d8f..b3f2471e5d 100644 --- a/Lake/Build/IndexTargets.lean +++ b/Lake/Build/IndexTargets.lean @@ -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 diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 34a2925bf5..9c8f899610 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -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] diff --git a/Lake/Build/Roots.lean b/Lake/Build/Roots.lean index 9a5610c78b..9d91ac7ece 100644 --- a/Lake/Build/Roots.lean +++ b/Lake/Build/Roots.lean @@ -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 diff --git a/Lake/Build/Target.lean b/Lake/Build/Target.lean index 7f927125a3..4af72fa741 100644 --- a/Lake/Build/Target.lean +++ b/Lake/Build/Target.lean @@ -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 diff --git a/Lake/Build/TargetTypes.lean b/Lake/Build/TargetTypes.lean index 1db9fa2825..8d342604e1 100644 --- a/Lake/Build/TargetTypes.lean +++ b/Lake/Build/TargetTypes.lean @@ -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. -/ diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean index 08a78d92cd..1eb188ddbd 100644 --- a/Lake/Build/Targets.lean +++ b/Lake/Build/Targets.lean @@ -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 := diff --git a/Lake/Build/Topological.lean b/Lake/Build/Topological.lean index f51d76207e..7b80107f04 100644 --- a/Lake/Build/Topological.lean +++ b/Lake/Build/Topological.lean @@ -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] diff --git a/Lake/Build/Trace.lean b/Lake/Build/Trace.lean index 9164746e89..e655e9922c 100644 --- a/Lake/Build/Trace.lean +++ b/Lake/Build/Trace.lean @@ -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`. -/ diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index c317e72c06..63a6bffff5 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -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 diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean index c7ff5180c0..0ed452e76a 100644 --- a/Lake/Config/ExternLib.lean +++ b/Lake/Config/ExternLib.lean @@ -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 diff --git a/Lake/Config/LeanExe.lean b/Lake/Config/LeanExe.lean index d6ae0e1115..5bcd138af4 100644 --- a/Lake/Config/LeanExe.lean +++ b/Lake/Config/LeanExe.lean @@ -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 diff --git a/Lake/Config/LeanLib.lean b/Lake/Config/LeanLib.lean index c8f171bce2..73d77f5c65 100644 --- a/Lake/Config/LeanLib.lean +++ b/Lake/Config/LeanLib.lean @@ -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 diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index 3b39db2819..2e8325a9f6 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -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) diff --git a/Lake/Config/Monad.lean b/Lake/Config/Monad.lean index f91544c390..56abd391a9 100644 --- a/Lake/Config/Monad.lean +++ b/Lake/Config/Monad.lean @@ -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 := diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index b4d82507c2..d269b73087 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -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 diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean index 4740d773b5..d8f9ea85ca 100644 --- a/Lake/DSL/Targets.lean +++ b/Lake/DSL/Targets.lean @@ -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 := diff --git a/Lake/Util/Async.lean b/Lake/Util/Async.lean index 5b44bb0c43..3664a846c9 100644 --- a/Lake/Util/Async.lean +++ b/Lake/Util/Async.lean @@ -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] diff --git a/Lake/Util/Cli.lean b/Lake/Util/Cli.lean index cf683c05b4..9c05b85807 100644 --- a/Lake/Util/Cli.lean +++ b/Lake/Util/Cli.lean @@ -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] diff --git a/Lake/Util/EvalTerm.lean b/Lake/Util/EvalTerm.lean index ee3242fe0e..c38d20a68c 100644 --- a/Lake/Util/EvalTerm.lean +++ b/Lake/Util/EvalTerm.lean @@ -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) diff --git a/Lake/Util/Log.lean b/Lake/Util/Log.lean index 4b0fda4671..8813adf445 100644 --- a/Lake/Util/Log.lean +++ b/Lake/Util/Log.lean @@ -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 diff --git a/Lake/Util/MainM.lean b/Lake/Util/MainM.lean index 668eef89cb..f1416c6f76 100644 --- a/Lake/Util/MainM.lean +++ b/Lake/Util/MainM.lean @@ -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 diff --git a/Lake/Util/Name.lean b/Lake/Util/Name.lean index 8fd5fad59b..2afa4d9627 100644 --- a/Lake/Util/Name.lean +++ b/Lake/Util/Name.lean @@ -12,7 +12,7 @@ namespace Lake export Lean (Name NameMap) --- # Name Helpers +/-! # Name Helpers -/ namespace Name open Lean.Name