diff --git a/src/lake/.gitignore b/src/lake/.gitignore index 3f78e1de4a..b58912d59c 100644 --- a/src/lake/.gitignore +++ b/src/lake/.gitignore @@ -1,3 +1,3 @@ .lake lake-manifest.json -*produced.out +*produced.* diff --git a/src/lake/Lake.lean b/src/lake/Lake.lean index 2c05f7a86d..09633bb524 100644 --- a/src/lake/Lake.lean +++ b/src/lake/Lake.lean @@ -8,3 +8,4 @@ import Lake.Config import Lake.DSL import Lake.Version import Lake.CLI.Actions +import Lake.Toml diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean index 90faeb3370..5fb2d3c4cb 100644 --- a/src/lake/Lake/Build/Topological.lean +++ b/src/lake/Lake/Build/Topological.lean @@ -84,7 +84,7 @@ We use `keyOf` to the derive the unique key of a fetch from its descriptor `a : α`. We do this because descriptors may not be comparable and/or contain more information than necessary to determine uniqueness. -/ -@[inline] partial def recFetchAcyclic [BEq κ] [Monad m] +@[inline] def recFetchAcyclic [BEq κ] [Monad m] (keyOf : α → κ) (fetch : DRecFetchFn α β (CycleT κ m)) : DFetchFn α β (CycleT κ m) := recFetch fun a recurse => /- @@ -110,30 +110,3 @@ memoize fetch results and thus avoid computing the same result twice. : DFetchFn α (fun a => β (keyOf a)) (CycleT κ m) := recFetchAcyclic keyOf fun a recurse => fetchOrCreate (keyOf a) do fetch a recurse - -/-! -## Building - -In this section, we use the abstractions we have just created to define -the desired topological recursive build function (a.k.a. a suspending scheduler). --/ - -/-- Recursively builds objects for the keys `κ`, avoiding cycles. -/ -@[inline] def buildAcyclic [BEq κ] [Monad m] -(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β := - recFetchAcyclic (β := fun _ => β) keyOf build a [] - -/-- Dependently typed version of `buildTop`. -/ -@[inline] def buildDTop (β) [BEq κ] [Monad m] [MonadDStore κ β m] -(keyOf : α → κ) (a : α) (build : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m)) -: ExceptT (Cycle κ) m (β (keyOf a)) := - recFetchMemoize keyOf build a [] - -/-- -Recursively fills a `MonadStore` of key-object pairs by -building objects topologically (ι.e., depth-first with memoization). -If a cycle is detected, the list of keys traversed is thrown. --/ -@[inline] def buildTop [BEq κ] [Monad m] [MonadStore κ β m] -(keyOf : α → κ) (a : α) (build : RecFetchFn α β (CycleT κ m)) : ExceptT (Cycle κ) m β := - recFetchMemoize (β := fun _ => β) keyOf build a [] diff --git a/src/lake/Lake/Build/Trace.lean b/src/lake/Lake/Build/Trace.lean index 8191536372..68b6321fa0 100644 --- a/src/lake/Lake/Build/Trace.lean +++ b/src/lake/Lake/Build/Trace.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Mac Malone. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ +import Lake.Util.Newline open System namespace Lake @@ -128,23 +129,6 @@ def computeFileHash (file : FilePath) : IO Hash := instance : ComputeHash FilePath IO := ⟨computeFileHash⟩ -/-- This is the same as `String.replace text "\r\n" "\n"`, but more efficient. -/ -@[inline] partial def crlf2lf (text : String) : String := - go "" 0 0 -where - go (acc : String) (accStop pos : String.Pos) : String := - if h : text.atEnd pos then - -- note: if accStop = 0 then acc is empty - if accStop = 0 then text else acc ++ text.extract accStop pos - else - let c := text.get' pos h - let pos' := text.next' pos h - if c == '\r' && text.get pos' == '\n' then - let acc := acc ++ text.extract accStop pos - go acc pos' (text.next pos') - else - go acc accStop pos' - def computeTextFileHash (file : FilePath) : IO Hash := do let text ← IO.FS.readFile file let text := crlf2lf text diff --git a/src/lake/Lake/CLI/Error.lean b/src/lake/Lake/CLI/Error.lean index 6061244cfa..d2899bf05e 100644 --- a/src/lake/Lake/CLI/Error.lean +++ b/src/lake/Lake/CLI/Error.lean @@ -18,6 +18,7 @@ inductive CliError | unexpectedArguments (args : List String) /- Init CLI Errors -/ | unknownTemplate (spec : String) +| unknownConfigLang (spec : String) /- Build CLI Errors -/ | unknownModule (mod : Name) | unknownPackage (spec : String) @@ -31,10 +32,12 @@ inductive CliError | invalidFacet (target : Name) (facet : Name) /- Executable CLI Errors -/ | unknownExe (spec : String) -/- Script CLI Error -/ +/- Script CLI Error -/ | unknownScript (script : String) | missingScriptDoc (script : String) | invalidScriptSpec (spec : String) +/-- Translate Errors -/ +| outputConfigExists (path : System.FilePath) /- Config Errors -/ | unknownLeanInstall | unknownLakeInstall @@ -53,6 +56,7 @@ def toString : CliError → String | unknownLongOption opt => s!"unknown long option '{opt}'" | unexpectedArguments as => s!"unexpected arguments: {" ".intercalate as}" | unknownTemplate spec => s!"unknown package template `{spec}`" +| unknownConfigLang spec => s!"unknown configuration language `{spec}`" | unknownModule mod => s!"unknown module `{mod.toString false}`" | unknownPackage spec => s!"unknown package `{spec}`" | unknownFacet ty f => s!"unknown {ty} facet `{f.toString false}`" @@ -67,6 +71,7 @@ def toString : CliError → String | unknownScript s => s!"unknown script {s}" | missingScriptDoc s => s!"no documentation provided for `{s}`" | invalidScriptSpec s => s!"invalid script spec '{s}' (too many '/')" +| outputConfigExists f => s!"output configuration file already exists: {f}" | unknownLeanInstall => "could not detect a Lean installation" | unknownLakeInstall => "could not detect the configuration of the Lake installation" | leanRevMismatch e a => s!"expected Lean commit {e}, but got {if a.isEmpty then "nothing" else a}" diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean index c33050c41d..6729f43995 100644 --- a/src/lake/Lake/CLI/Help.lean +++ b/src/lake/Lake/CLI/Help.lean @@ -25,6 +25,7 @@ COMMANDS: script manage and run workspace scripts scripts shorthand for `lake script list` run