diff --git a/src/lake/.envrc b/src/lake/.envrc new file mode 100644 index 0000000000..3550a30f2d --- /dev/null +++ b/src/lake/.envrc @@ -0,0 +1 @@ +use flake diff --git a/src/lake/.gitattributes b/src/lake/.gitattributes new file mode 100644 index 0000000000..dfdb8b771c --- /dev/null +++ b/src/lake/.gitattributes @@ -0,0 +1 @@ +*.sh text eol=lf diff --git a/src/lake/.github/workflows/ci.yml b/src/lake/.github/workflows/ci.yml new file mode 100644 index 0000000000..104ea27992 --- /dev/null +++ b/src/lake/.github/workflows/ci.yml @@ -0,0 +1,72 @@ +name: CI + +on: [ push, pull_request ] + +jobs: + skip_check: + name: Skip Check + continue-on-error: true + runs-on: ubuntu-latest + outputs: + should_skip: ${{ steps.skip_check.outputs.should_skip }} + steps: + - id: skip_check + uses: fkirc/skip-duplicate-actions@v4 + with: + concurrent_skipping: 'same_content_newer' + paths_ignore: '["README.md", "LICENSE"]' + + build: + needs: skip_check + name: ${{ matrix.name || 'Build' }} + if: ${{ needs.skip_check.outputs.should_skip != 'true' }} + runs-on: ${{ matrix.os }} + defaults: + run: + shell: ${{ matrix.shell || 'sh' }} + strategy: + matrix: + include: + - name: Ubuntu + os: ubuntu-latest + - name: MacOS + os: macos-latest + - name: Windows + os: windows-latest + shell: msys2 {0} + # complete all jobs + fail-fast: false + steps: + - name: Install MSYS2 (Windows) + if: matrix.os == 'windows-latest' + uses: msys2/setup-msys2@v2 + with: + path-type: inherit + install: curl unzip make diffutils mingw-w64-x86_64-gcc mingw-w64-x86_64-gmp + - name: Install Elan + shell: bash -euo pipefail {0} + run: | + curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none + echo "$HOME/.elan/bin" >> $GITHUB_PATH + - name: Checkout + uses: actions/checkout@v2 + - name: Check Lean + run: lean --version + - name: Build & Time + run: ./time.sh -j4 + - name: Upload Build + continue-on-error: true + uses: actions/upload-artifact@v2 + with: + name: ${{ matrix.os }} + path: build + - name: Check Lake + run: make check-lake + - name: Test Lake + run: make test-ci + - name: Time Bootstrap + run: make time-bootstrap + - name: Check Bootstrap + run: make check-bootstrap + - name: Test Bootstrapped Lake + run: make test-bootstrapped -j4 diff --git a/src/lake/.gitignore b/src/lake/.gitignore new file mode 100644 index 0000000000..59ebc302c5 --- /dev/null +++ b/src/lake/.gitignore @@ -0,0 +1,5 @@ +/build +produced.out +result* +# Do not commit the flake lockfile to avoid having to maintain it +flake.lock diff --git a/src/lake/LICENSE b/src/lake/LICENSE new file mode 100644 index 0000000000..4c3f8ab0fb --- /dev/null +++ b/src/lake/LICENSE @@ -0,0 +1,70 @@ +Apache License 2.0 (Apache) +Apache License +Version 2.0, January 2004 +http://www.apache.org/licenses/ + +TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + +1. Definitions. + +"License" shall mean the terms and conditions for use, reproduction, and distribution as defined by Sections 1 through 9 of this document. + +"Licensor" shall mean the copyright owner or entity authorized by the copyright owner that is granting the License. + +"Legal Entity" shall mean the union of the acting entity and all other entities that control, are controlled by, or are under common control with that entity. For the purposes of this definition, "control" means (i) the power, direct or indirect, to cause the direction or management of such entity, whether by contract or otherwise, or (ii) ownership of fifty percent (50%) or more of the outstanding shares, or (iii) beneficial ownership of such entity. + +"You" (or "Your") shall mean an individual or Legal Entity exercising permissions granted by this License. + +"Source" form shall mean the preferred form for making modifications, including but not limited to software source code, documentation source, and configuration files. + +"Object" form shall mean any form resulting from mechanical transformation or translation of a Source form, including but not limited to compiled object code, generated documentation, and conversions to other media types. + +"Work" shall mean the work of authorship, whether in Source or Object form, made available under the License, as indicated by a copyright notice that is included in or attached to the work (an example is provided in the Appendix below). + +"Derivative Works" shall mean any work, whether in Source or Object form, that is based on (or derived from) the Work and for which the editorial revisions, annotations, elaborations, or other modifications represent, as a whole, an original work of authorship. For the purposes of this License, Derivative Works shall not include works that remain separable from, or merely link (or bind by name) to the interfaces of, the Work and Derivative Works thereof. + +"Contribution" shall mean any work of authorship, including the original version of the Work and any modifications or additions to that Work or Derivative Works thereof, that is intentionally submitted to Licensor for inclusion in the Work by the copyright owner or by an individual or Legal Entity authorized to submit on behalf of the copyright owner. For the purposes of this definition, "submitted" means any form of electronic, verbal, or written communication sent to the Licensor or its representatives, including but not limited to communication on electronic mailing lists, source code control systems, and issue tracking systems that are managed by, or on behalf of, the Licensor for the purpose of discussing and improving the Work, but excluding communication that is conspicuously marked or otherwise designated in writing by the copyright owner as "Not a Contribution." + +"Contributor" shall mean Licensor and any individual or Legal Entity on behalf of whom a Contribution has been received by Licensor and subsequently incorporated within the Work. + +2. Grant of Copyright License. + +Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable copyright license to reproduce, prepare Derivative Works of, publicly display, publicly perform, sublicense, and distribute the Work and such Derivative Works in Source or Object form. + +3. Grant of Patent License. + +Subject to the terms and conditions of this License, each Contributor hereby grants to You a perpetual, worldwide, non-exclusive, no-charge, royalty-free, irrevocable (except as stated in this section) patent license to make, have made, use, offer to sell, sell, import, and otherwise transfer the Work, where such license applies only to those patent claims licensable by such Contributor that are necessarily infringed by their Contribution(s) alone or by combination of their Contribution(s) with the Work to which such Contribution(s) was submitted. If You institute patent litigation against any entity (including a cross-claim or counterclaim in a lawsuit) alleging that the Work or a Contribution incorporated within the Work constitutes direct or contributory patent infringement, then any patent licenses granted to You under this License for that Work shall terminate as of the date such litigation is filed. + +4. Redistribution. + +You may reproduce and distribute copies of the Work or Derivative Works thereof in any medium, with or without modifications, and in Source or Object form, provided that You meet the following conditions: + +1. You must give any other recipients of the Work or Derivative Works a copy of this License; and + +2. You must cause any modified files to carry prominent notices stating that You changed the files; and + +3. You must retain, in the Source form of any Derivative Works that You distribute, all copyright, patent, trademark, and attribution notices from the Source form of the Work, excluding those notices that do not pertain to any part of the Derivative Works; and + +4. If the Work includes a "NOTICE" text file as part of its distribution, then any Derivative Works that You distribute must include a readable copy of the attribution notices contained within such NOTICE file, excluding those notices that do not pertain to any part of the Derivative Works, in at least one of the following places: within a NOTICE text file distributed as part of the Derivative Works; within the Source form or documentation, if provided along with the Derivative Works; or, within a display generated by the Derivative Works, if and wherever such third-party notices normally appear. The contents of the NOTICE file are for informational purposes only and do not modify the License. You may add Your own attribution notices within Derivative Works that You distribute, alongside or as an addendum to the NOTICE text from the Work, provided that such additional attribution notices cannot be construed as modifying the License. + +You may add Your own copyright statement to Your modifications and may provide additional or different license terms and conditions for use, reproduction, or distribution of Your modifications, or for any such Derivative Works as a whole, provided Your use, reproduction, and distribution of the Work otherwise complies with the conditions stated in this License. + +5. Submission of Contributions. + +Unless You explicitly state otherwise, any Contribution intentionally submitted for inclusion in the Work by You to the Licensor shall be under the terms and conditions of this License, without any additional terms or conditions. Notwithstanding the above, nothing herein shall supersede or modify the terms of any separate license agreement you may have executed with Licensor regarding such Contributions. + +6. Trademarks. + +This License does not grant permission to use the trade names, trademarks, service marks, or product names of the Licensor, except as required for reasonable and customary use in describing the origin of the Work and reproducing the content of the NOTICE file. + +7. Disclaimer of Warranty. + +Unless required by applicable law or agreed to in writing, Licensor provides the Work (and each Contributor provides its Contributions) on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied, including, without limitation, any warranties or conditions of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A PARTICULAR PURPOSE. You are solely responsible for determining the appropriateness of using or redistributing the Work and assume any risks associated with Your exercise of permissions under this License. + +8. Limitation of Liability. + +In no event and under no legal theory, whether in tort (including negligence), contract, or otherwise, unless required by applicable law (such as deliberate and grossly negligent acts) or agreed to in writing, shall any Contributor be liable to You for damages, including any direct, indirect, special, incidental, or consequential damages of any character arising as a result of this License or out of the use or inability to use the Work (including but not limited to damages for loss of goodwill, work stoppage, computer failure or malfunction, or any and all other commercial damages or losses), even if such Contributor has been advised of the possibility of such damages. + +9. Accepting Warranty or Additional Liability. + +While redistributing the Work or Derivative Works thereof, You may choose to offer, and charge a fee for, acceptance of support, warranty, indemnity, or other liability obligations and/or rights consistent with this License. However, in accepting such obligations, You may act only on Your own behalf and on Your sole responsibility, not on behalf of any other Contributor, and only if You agree to indemnify, defend, and hold each Contributor harmless for any liability incurred by, or claims asserted against, such Contributor by reason of your accepting any such warranty or additional liability. diff --git a/src/lake/Lake.lean b/src/lake/Lake.lean new file mode 100644 index 0000000000..2c05f7a86d --- /dev/null +++ b/src/lake/Lake.lean @@ -0,0 +1,10 @@ +/- +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.Build +import Lake.Config +import Lake.DSL +import Lake.Version +import Lake.CLI.Actions diff --git a/src/lake/Lake/Build.lean b/src/lake/Lake/Build.lean new file mode 100644 index 0000000000..446f79716e --- /dev/null +++ b/src/lake/Lake/Build.lean @@ -0,0 +1,12 @@ +/- +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.Build.Monad +import Lake.Build.Actions +import Lake.Build.Index +import Lake.Build.Module +import Lake.Build.Package +import Lake.Build.Library +import Lake.Build.Imports diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean new file mode 100644 index 0000000000..e83b69828d --- /dev/null +++ b/src/lake/Lake/Build/Actions.lean @@ -0,0 +1,123 @@ +/- +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 Lake.Util.Proc +import Lake.Util.NativeLib +import Lake.Build.Context + +namespace Lake +open System + +def createParentDirs (path : FilePath) : IO Unit := do + if let some dir := path.parent then IO.FS.createDirAll dir + +def compileLeanModule (name : String) (leanFile : FilePath) +(oleanFile? ileanFile? cFile? : Option FilePath) +(leanPath : SearchPath := []) (rootDir : FilePath := ".") +(dynlibs : Array FilePath := #[]) (dynlibPath : SearchPath := {}) +(leanArgs : Array String := #[]) (lean : FilePath := "lean") +: BuildM Unit := do + logStep s!"Building {name}" + let mut args := leanArgs ++ + #[leanFile.toString, "-R", rootDir.toString] + if let some oleanFile := oleanFile? then + createParentDirs oleanFile + args := args ++ #["-o", oleanFile.toString] + if let some ileanFile := ileanFile? then + createParentDirs ileanFile + args := args ++ #["-i", ileanFile.toString] + if let some cFile := cFile? then + createParentDirs cFile + args := args ++ #["-c", cFile.toString] + for dynlib in dynlibs do + args := args.push s!"--load-dynlib={dynlib}" + proc { + args + cmd := lean.toString + env := #[ + ("LEAN_PATH", leanPath.toString), + (sharedLibPathEnvVar, (← getSearchPath sharedLibPathEnvVar) ++ dynlibPath |>.toString) + ] + } + +def compileO (name : String) (oFile srcFile : FilePath) +(moreArgs : Array String := #[]) (compiler : FilePath := "cc") : BuildM Unit := do + logStep s!"Compiling {name}" + createParentDirs oFile + proc { + cmd := compiler.toString + args := #["-c", "-o", oFile.toString, srcFile.toString] ++ moreArgs + } + +def compileStaticLib (name : String) (libFile : FilePath) +(oFiles : Array FilePath) (ar : FilePath := "ar") : BuildM Unit := do + logStep s!"Creating {name}" + createParentDirs libFile + proc { + cmd := ar.toString + args := #["rcs", libFile.toString] ++ oFiles.map toString + } + +def compileSharedLib (name : String) (libFile : FilePath) +(linkArgs : Array String) (linker : FilePath := "cc") : BuildM Unit := do + logStep s!"Linking {name}" + createParentDirs libFile + proc { + cmd := linker.toString + args := #["-shared", "-o", libFile.toString] ++ linkArgs + } + +def compileExe (name : String) (binFile : FilePath) (linkFiles : Array FilePath) +(linkArgs : Array String := #[]) (linker : FilePath := "cc") : BuildM Unit := do + logStep s!"Linking {name}" + createParentDirs binFile + proc { + cmd := linker.toString + args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs + } + +/-- Download a file using `curl`, clobbering any existing file. -/ +def download (name : String) (url : String) (file : FilePath) : LogIO PUnit := do + logInfo s!"Downloading {name}" + if (← file.pathExists) then + IO.FS.removeFile file + else + createParentDirs file + let args := + if (← getIsVerbose) then #[] else #["-s"] + proc (quiet := true) { + cmd := "curl" + args := args ++ #["-f", "-o", file.toString, "-L", url] + } + +/-- Unpack an archive `file` using `tar` into the directory `dir`. -/ +def untar (name : String) (file : FilePath) (dir : FilePath) (gzip := true) : LogIO PUnit := do + logInfo s!"Unpacking {name}" + let mut opts := "-x" + if (← getIsVerbose) then + opts := opts.push 'v' + if gzip then + opts := opts.push 'z' + proc { + cmd := "tar", + args := #[opts, "-f", file.toString, "-C", dir.toString] + } + +/-- Pack a directory `dir` using `tar` into the archive `file`. -/ +def tar (name : String) (dir : FilePath) (file : FilePath) +(gzip := true) (excludePaths : Array FilePath := #[]) : LogIO PUnit := do + logInfo s!"Packing {name}" + createParentDirs file + let mut args := #["-c"] + if gzip then + args := args.push "-z" + if (← getIsVerbose) then + args := args.push "-v" + for path in excludePaths do + args := args.push s!"--exclude={path}" + proc { + cmd := "tar" + args := args ++ #["-f", file.toString, "-C", dir.toString, "."] + } diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean new file mode 100644 index 0000000000..7b46d09fbe --- /dev/null +++ b/src/lake/Lake/Build/Common.lean @@ -0,0 +1,118 @@ +/- +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.Build.Job +import Lake.Build.Actions +import Lake.Build.Monad + +open System +namespace Lake + +/-! # General Utilities -/ + +@[inline] def inputFile (path : FilePath) : SchedulerM (BuildJob FilePath) := + Job.async <| (path, ·) <$> computeTrace path + +@[inline] def buildUnlessUpToDate [CheckExists ι] [GetMTime ι] (info : ι) +(depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit) : JobM PUnit := do + let isOldMode ← getIsOldMode + let upToDate ← + if isOldMode then + depTrace.checkAgainstTime info + else + depTrace.checkAgainstFile info traceFile + unless upToDate do + build + unless isOldMode do + depTrace.writeToFile traceFile + +@[inline] def buildFileUnlessUpToDate (file : FilePath) +(depTrace : BuildTrace) (build : BuildM PUnit) : BuildM BuildTrace := do + let traceFile := FilePath.mk <| file.toString ++ ".trace" + buildUnlessUpToDate file depTrace traceFile build + computeTrace file + +@[inline] def buildFileAfterDep +(file : FilePath) (dep : BuildJob α) (build : α → BuildM PUnit) +(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := + dep.bindSync fun depInfo depTrace => do + let depTrace := depTrace.mix (← extraDepTrace) + let trace ← buildFileUnlessUpToDate file depTrace <| build depInfo + return (file, trace) + +@[inline] def buildFileAfterDepList +(file : FilePath) (deps : List (BuildJob α)) (build : List α → BuildM PUnit) +(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do + buildFileAfterDep file (← BuildJob.collectList deps) build extraDepTrace + +@[inline] def buildFileAfterDepArray +(file : FilePath) (deps : Array (BuildJob α)) (build : Array α → BuildM PUnit) +(extraDepTrace : BuildM _ := pure BuildTrace.nil) : SchedulerM (BuildJob FilePath) := do + buildFileAfterDep file (← BuildJob.collectArray deps) build extraDepTrace + +/-! # Common Builds -/ + +def buildO (name : String) +(oFile : FilePath) (srcJob : BuildJob FilePath) +(args : Array String := #[]) (compiler : FilePath := "cc") : SchedulerM (BuildJob FilePath) := + buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do + compileO name oFile srcFile args compiler + +def buildLeanO (name : String) +(oFile : FilePath) (srcJob : BuildJob FilePath) +(args : Array String := #[]) : SchedulerM (BuildJob FilePath) := + buildFileAfterDep oFile srcJob (extraDepTrace := computeHash args) fun srcFile => do + compileO name oFile srcFile args (← getLeanc) + +def buildStaticLib (libFile : FilePath) +(oFileJobs : Array (BuildJob FilePath)) : SchedulerM (BuildJob FilePath) := + let name := libFile.fileName.getD libFile.toString + buildFileAfterDepArray libFile oFileJobs fun oFiles => do + compileStaticLib name libFile oFiles (← getLeanAr) + +def buildLeanSharedLib +(libFile : FilePath) (linkJobs : Array (BuildJob FilePath)) +(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) := + let name := libFile.fileName.getD libFile.toString + buildFileAfterDepArray libFile linkJobs + (extraDepTrace := computeHash linkArgs) fun links => do + compileSharedLib name libFile (links.map toString ++ linkArgs) (← getLeanc) + +def buildLeanExe +(exeFile : FilePath) (linkJobs : Array (BuildJob FilePath)) +(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) := + let name := exeFile.fileName.getD exeFile.toString + buildFileAfterDepArray exeFile linkJobs + (extraDepTrace := computeHash linkArgs) fun links => do + compileExe name exeFile links linkArgs (← getLeanc) + +def buildLeanSharedLibOfStatic (staticLibJob : BuildJob FilePath) +(linkArgs : Array String := #[]) : SchedulerM (BuildJob FilePath) := + staticLibJob.bindSync fun staticLib staticTrace => do + let dynlib := staticLib.withExtension sharedLibExt + let baseArgs := + if System.Platform.isOSX then + #[s!"-Wl,-force_load,{staticLib}"] + else + #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"] + let args := baseArgs ++ linkArgs + let depTrace := staticTrace.mix (← computeHash args) + let trace ← buildFileUnlessUpToDate dynlib depTrace do + let name := dynlib.fileName.getD dynlib.toString + compileSharedLib name dynlib args (← getLeanc) + return (dynlib, trace) + +def computeDynlibOfShared +(sharedLibTarget : BuildJob FilePath) : SchedulerM (BuildJob Dynlib) := + sharedLibTarget.bindSync fun sharedLib trace => do + if let some stem := sharedLib.fileStem then + if Platform.isWindows then + return ({path := sharedLib, name := stem}, trace) + else if stem.startsWith "lib" then + return ({path := sharedLib, name := stem.drop 3}, trace) + else + error s!"shared library `{sharedLib}` does not start with `lib`; this is not supported on Unix" + else + error s!"shared library `{sharedLib}` has no file name" diff --git a/src/lake/Lake/Build/Context.lean b/src/lake/Lake/Build/Context.lean new file mode 100644 index 0000000000..dc10a84932 --- /dev/null +++ b/src/lake/Lake/Build/Context.lean @@ -0,0 +1,58 @@ +/- +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.Log +import Lake.Util.Task +import Lake.Util.Error +import Lake.Util.OptionIO +import Lake.Config.Context +import Lake.Build.Trace +import Lake.Build.Store +import Lake.Build.Topological + +open System +namespace Lake + +/-- A Lake context with some additional caching for builds. -/ +structure BuildContext extends Context where + leanTrace : BuildTrace + oldMode : Bool := false + startedBuilds : IO.Ref Nat + finishedBuilds : IO.Ref Nat + +/-- A transformer to equip a monad with a `BuildContext`. -/ +abbrev BuildT := ReaderT BuildContext + +/-- The monad for the Lake build manager. -/ +abbrev SchedulerM := BuildT <| LogT BaseIO + +/-- The core monad for Lake builds. -/ +abbrev BuildM := BuildT LogIO + +/-- A transformer to equip a monad with a Lake build store. -/ +abbrev BuildStoreT := StateT BuildStore + +/-- A Lake build cycle. -/ +abbrev BuildCycle := Cycle BuildKey + +/-- A transformer for monads that may encounter a build cycle. -/ +abbrev BuildCycleT := CycleT BuildKey + +/-- A recursive build of a Lake build store that may encounter a cycle. -/ +abbrev RecBuildM := BuildCycleT <| BuildStoreT BuildM + +instance [Pure m] : MonadLift LakeM (BuildT m) where + monadLift x := fun ctx => pure <| x.run ctx.toContext + +@[inline] def BuildM.run (ctx : BuildContext) (self : BuildM α) : LogIO α := + self ctx + +def BuildM.catchFailure (f : Unit → BaseIO α) (self : BuildM α) : SchedulerM α := + fun ctx logMethods => self ctx logMethods |>.catchFailure f + +def logStep (message : String) : BuildM Unit := do + let done ← (← read).finishedBuilds.get + let started ← (← read).startedBuilds.get + logInfo s!"[{done}/{started}] {message}" diff --git a/src/lake/Lake/Build/Data.lean b/src/lake/Lake/Build/Data.lean new file mode 100644 index 0000000000..79d2579ef4 --- /dev/null +++ b/src/lake/Lake/Build/Data.lean @@ -0,0 +1,131 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Key +import Lake.Util.Family + +open Lean +namespace Lake + +-------------------------------------------------------------------------------- +/-! ## Build Data Subtypes -/ +-------------------------------------------------------------------------------- + +/-- +The open type family which maps a module facet's name to its build data +in the Lake build store. For example, a transitive × direct import pair +for the `lean.imports` facet or an active build target for `lean.c`. + +It is an open type, meaning additional mappings can be add lazily +as needed (via `module_data`). +-/ +opaque ModuleData (facet : Name) : Type + +/-- +The open type family which maps a package facet's name to its build data +in the Lake build store. For example, a transitive dependencies of the package +for the facet `deps`. + +It is an open type, meaning additional mappings can be add lazily +as needed (via `package_data`). +-/ +opaque PackageData (facet : Name) : Type + +/-- +The open type family which maps a (builtin) Lake target's (e.g., `extern_lib`) +facet to its associated build data. For example, an active build target for +the `externLib.static` facet. + +It is an open type, meaning additional mappings can be add lazily +as needed (via `target_data`). +-/ +opaque TargetData (facet : Name) : Type + +/- +The open type family which maps a library facet's name to its build data +in the Lake build store. For example, an active build target for the `static` +facet. + +It is an open type, meaning additional mappings can be add lazily +as needed (via `library_data`). +-/ +abbrev LibraryData (facet : Name) := TargetData (`leanLib ++ facet) + +instance [h : FamilyOut LibraryData facet α] : FamilyDef TargetData (`leanLib ++ facet) α := + ⟨by simp [h.family_key_eq_type]⟩ + +instance [h : FamilyOut TargetData (`leanLib ++ facet) α] : FamilyDef LibraryData facet α := + ⟨h.family_key_eq_type⟩ + +/-- +The open type family which maps a custom target (package × target name) to +its build data in the Lake build store. + +It is an open type, meaning additional mappings can be add lazily +as needed (via `custom_data`). +-/ +opaque CustomData (target : Name × Name) : Type + +-------------------------------------------------------------------------------- +/-! ## Build Data -/ +-------------------------------------------------------------------------------- + +/-- +A mapping between a build key and its associated build data in the store. +It is a simple type function composed of the separate open type families for +modules facets, package facets, Lake target facets, and custom targets. +-/ +abbrev BuildData : BuildKey → Type +| .moduleFacet _ f => ModuleData f +| .packageFacet _ f => PackageData f +| .targetFacet _ _ f => TargetData f +| .customTarget p t => CustomData (p, t) + +instance (priority := low) : FamilyDef BuildData (.moduleFacet m f) (ModuleData f) := ⟨rfl⟩ +instance (priority := low) : FamilyDef BuildData (.packageFacet p f) (PackageData f) := ⟨rfl⟩ +instance (priority := low) : FamilyDef BuildData (.targetFacet p t f) (TargetData f) := ⟨rfl⟩ +instance (priority := low) : FamilyDef BuildData (.customTarget p t) (CustomData (p,t)) := ⟨rfl⟩ + +-------------------------------------------------------------------------------- +/-! ## Macros for Declaring Build Data -/ +-------------------------------------------------------------------------------- + +/-- Macro for declaring new `PackageData`. -/ +scoped macro (name := packageDataDecl) doc?:optional(Parser.Command.docComment) +"package_data " id:ident " : " ty:term : command => do + let dty := mkCIdentFrom (← getRef) ``PackageData + let key := Name.quoteFrom id id.getId + `($[$doc?]? family_def $id : $dty $key := $ty) + +/-- Macro for declaring new `ModuleData`. -/ +scoped macro (name := moduleDataDecl) doc?:optional(Parser.Command.docComment) +"module_data " id:ident " : " ty:term : command => do + let dty := mkCIdentFrom (← getRef) ``ModuleData + let key := Name.quoteFrom id id.getId + `($[$doc?]? family_def $id : $dty $key := $ty) + +/-- Macro for declaring new `TargetData` for libraries. -/ +scoped macro (name := libraryDataDecl) doc?:optional(Parser.Command.docComment) +"library_data " id:ident " : " ty:term : command => do + let dty := mkCIdentFrom (← getRef) ``TargetData + let key := Name.quoteFrom id id.getId + let id := mkIdentFrom id <| id.getId.modifyBase (`leanLib ++ ·) + `($[$doc?]? family_def $id : $dty (`leanLib ++ $key) := $ty) + +/-- Macro for declaring new `TargetData`. -/ +scoped macro (name := targetDataDecl) doc?:optional(Parser.Command.docComment) +"target_data " id:ident " : " ty:term : command => do + let dty := mkCIdentFrom (← getRef) ``TargetData + let key := Name.quoteFrom id id.getId + `($[$doc?]? family_def $id : $dty $key := $ty) + +/-- Macro for declaring new `CustomData`. -/ +scoped macro (name := customDataDecl) doc?:optional(Parser.Command.docComment) +"custom_data " pkg:ident tgt:ident " : " ty:term : command => do + let dty := mkCIdentFrom (← getRef) ``CustomData + let id := mkIdentFrom tgt (pkg.getId ++ tgt.getId) + let pkg := Name.quoteFrom pkg pkg.getId + let tgt := Name.quoteFrom pkg tgt.getId + `($[$doc?]? family_def $id : $dty ($pkg, $tgt) := $ty) diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean new file mode 100644 index 0000000000..8a5f81d6ec --- /dev/null +++ b/src/lake/Lake/Build/Executable.lean @@ -0,0 +1,34 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Common + +namespace Lake + +/-- Get the Lean executable in the workspace with the configuration's name. -/ +@[inline] def LeanExeConfig.get (self : LeanExeConfig) +[Monad m] [MonadError m] [MonadLake m] : m LeanExe := do + let some exe ← findLeanExe? self.name + | error "Lean executable '{self.name}' does not exist in the workspace" + return exe + + +/-- Fetch the build of the Lean executable. -/ +@[inline] def LeanExeConfig.fetch +(self : LeanExeConfig) : IndexBuildM (BuildJob FilePath) := do + (← self.get).exe.fetch + +/-! # Build Executable -/ + +protected def LeanExe.recBuildExe +(self : LeanExe) : IndexBuildM (BuildJob FilePath) := do + let imports ← self.root.transImports.fetch + let mut linkJobs := #[← self.root.o.fetch] + for mod in imports do for facet in mod.nativeFacets do + linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name + let deps := (← fetch <| self.pkg.facet `deps).push self.pkg + for dep in deps do for lib in dep.externLibs do + linkJobs := linkJobs.push <| ← lib.static.fetch + buildLeanExe self.file linkJobs self.linkArgs diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean new file mode 100644 index 0000000000..9072086acd --- /dev/null +++ b/src/lake/Lake/Build/Facets.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Job +import Lake.Build.Data + +/-! +# Simple Builtin Facet Declarations + +This module contains the definitions of most of the builtin facets. +The others are defined `Build.Info`. The facets there require configuration +definitions (e.g., `Module`), and some of the facets here are used in said +definitions. +-/ + +namespace Lake +export System (SearchPath FilePath) + +/-- A dynamic/shared library for linking. -/ +structure Dynlib where + /-- Library file path. -/ + path : FilePath + /-- Library name without platform-specific prefix/suffix (for `-l`). -/ + name : String + +/-- Optional library directory (for `-L`). -/ +def Dynlib.dir? (self : Dynlib) : Option FilePath := + self.path.parent + +/-! ## Module Facets -/ + +/-- A module facet name along with proof of its data type. -/ +structure ModuleFacet (α) where + /-- The name of the module facet. -/ + name : Name + /-- Proof that module's facet build result is of type α. -/ + data_eq : ModuleData name = α + deriving Repr + +instance (facet : ModuleFacet α) : FamilyDef ModuleData facet.name α := + ⟨facet.data_eq⟩ + +instance [FamilyOut ModuleData facet α] : CoeDep Name facet (ModuleFacet α) := + ⟨facet, FamilyOut.family_key_eq_type⟩ + +/-- +The facet which builds all of a module's dependencies +(i.e., transitive local imports and `--load-dynlib` shared libraries). +Returns the list of shared libraries to load along with their search path. +-/ +abbrev Module.depsFacet := `deps +module_data deps : BuildJob (SearchPath × Array FilePath) + +/-- +The core compilation / elaboration of the Lean file via `lean`, +which produce the Lean binaries of the module (i.e., `olean`, `ilean`, `c`). +Its trace just includes its dependencies. +-/ +abbrev Module.leanBinFacet := `bin +module_data bin : BuildJob Unit + +/-- +The `leanBinFacet` combined with the module's trace +(i.e., the trace of its `olean` and `ilean`). +It is the facet used for building a Lean import of a module. +-/ +abbrev Module.importBinFacet := `importBin +module_data importBin : BuildJob Unit + +/-- The `olean` file produced by `lean` -/ +abbrev Module.oleanFacet := `olean +module_data olean : BuildJob FilePath + +/-- The `ilean` file produced by `lean` -/ +abbrev Module.ileanFacet := `ilean +module_data ilean : BuildJob FilePath + +/-- The C file built from the Lean file via `lean` -/ +abbrev Module.cFacet := `c +module_data c : BuildJob FilePath + +/-- The object file built from `lean.c` -/ +abbrev Module.oFacet := `o +module_data o : BuildJob FilePath + +/-! ## Package Facets -/ + +/-- The package's cloud build release. -/ +abbrev Package.releaseFacet := `release +package_data release : BuildJob Unit + +/-- The package's `extraDepTarget` mixed with its transitive dependencies'. -/ +abbrev Package.extraDepFacet := `extraDep +package_data extraDep : BuildJob Unit + +/-! ## Target Facets -/ + +/-- A Lean library's Lean libraries. -/ +abbrev LeanLib.leanFacet := `lean +library_data lean : BuildJob Unit + +/-- A Lean library's static binary. -/ +abbrev LeanLib.staticFacet := `static +library_data static : BuildJob FilePath + +/-- A Lean library's shared binary. -/ +abbrev LeanLib.sharedFacet := `shared +library_data shared : BuildJob FilePath + +/-- A Lean binary executable. -/ +abbrev LeanExe.exeFacet := `leanExe +target_data leanExe : BuildJob FilePath + +/-- A external library's static binary. -/ +abbrev ExternLib.staticFacet := `externLib.static +target_data externLib.static : BuildJob FilePath + +/-- A external library's shared binary. -/ +abbrev ExternLib.sharedFacet := `externLib.shared +target_data externLib.shared : BuildJob FilePath + +/-- A external library's dynlib. -/ +abbrev ExternLib.dynlibFacet := `externLib.dynlib +target_data externLib.dynlib : BuildJob Dynlib diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean new file mode 100644 index 0000000000..392b162770 --- /dev/null +++ b/src/lake/Lake/Build/Imports.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Index + +/-! +Definitions to support `lake print-paths` builds. +-/ + +open System +namespace Lake + +/-- +Construct an `Array` of `Module`s for the workspace-local modules of +a `List` of import strings. +-/ +def Workspace.processImportList +(imports : List String) (self : Workspace) : Array Module := Id.run do + let mut localImports := #[] + for imp in imports do + if let some mod := self.findModule? imp.toName then + localImports := localImports.push mod + return localImports + +/-- +Recursively build a set of imported modules and return their build jobs, +the build jobs of their precompiled modules and the build jobs of said modules' +external libraries. +-/ +def recBuildImports (imports : Array Module) +: IndexBuildM (Array (BuildJob Unit) × Array (BuildJob Dynlib) × Array (BuildJob Dynlib)) := do + let mut modJobs := #[] + let mut precompileImports := OrdModuleSet.empty + for mod in imports do + if mod.shouldPrecompile then + precompileImports := precompileImports.appendArray (← mod.transImports.fetch) |>.insert mod + else + precompileImports := precompileImports.appendArray (← mod.precompileImports.fetch) + modJobs := modJobs.push <| ← mod.leanBin.fetch + let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray + let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.dynlib.fetch)) + let precompileJobs ← precompileImports.toArray.mapM (·.dynlib.fetch) + return (modJobs, precompileJobs, externJobs) + +/-- +Builds the workspace-local modules of list of imports. +Used by `lake print-paths` to build modules for the Lean server. +Returns the set of module dynlibs built (so they can be loaded by the server). + +Builds only module `.olean` and `.ilean` files if the package is configured +as "Lean-only". Otherwise, also builds `.c` files. +-/ +def buildImportsAndDeps (imports : List String) : BuildM (Array FilePath) := do + let ws ← getWorkspace + if imports.isEmpty then + -- build the package's (and its dependencies') `extraDepTarget` + ws.root.extraDep.build >>= (·.materialize) + return #[] + else + -- build local imports from list + let mods := ws.processImportList imports + let (modJobs, precompileJobs, externLibJobs) ← + recBuildImports mods |>.run.run + modJobs.forM (·.await) + let modLibs ← precompileJobs.mapM (·.await <&> (·.path)) + let externLibs ← externLibJobs.mapM (·.await <&> (·.path)) + -- NOTE: Lean wants the external library symbols before module symbols + return externLibs ++ modLibs diff --git a/src/lake/Lake/Build/Index.lean b/src/lake/Lake/Build/Index.lean new file mode 100644 index 0000000000..c065840cf5 --- /dev/null +++ b/src/lake/Lake/Build/Index.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Executable +import Lake.Build.Topological + +/-! +# The Lake Build Index + +The Lake build index is the complete map of Lake build keys to +Lake build functions, which is used by Lake to build any Lake build info. + +This module leverages the index to perform topologically-based recursive builds. +-/ + +open Lean +namespace Lake + +/-- +Converts a conveniently typed target facet build function into its +dynamically typed equivalent. +-/ +@[macro_inline] def mkTargetFacetBuild (facet : Name) (build : IndexBuildM α) +[h : FamilyOut TargetData facet α] : IndexBuildM (TargetData facet) := + cast (by rw [← h.family_key_eq_type]) build + +def ExternLib.recBuildStatic (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do + lib.config.getJob <$> fetch (lib.pkg.target lib.staticTargetName) + +def ExternLib.recBuildShared (lib : ExternLib) : IndexBuildM (BuildJob FilePath) := do + buildLeanSharedLibOfStatic (← lib.static.fetch) lib.linkArgs + +def ExternLib.recComputeDynlib (lib : ExternLib) : IndexBuildM (BuildJob Dynlib) := do + computeDynlibOfShared (← lib.shared.fetch) + +/-! +## Topologically-based Recursive Build Using the Index +-/ + +/-- Recursive build function for anything in the Lake build index. -/ +def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key) +| .moduleFacet mod facet => do + if let some config := (← getWorkspace).findModuleFacetConfig? facet then + config.build mod + else + error s!"do not know how to build module facet `{facet}`" +| .packageFacet pkg facet => do + if let some config := (← getWorkspace).findPackageFacetConfig? facet then + config.build pkg + else + error s!"do not know how to build package facet `{facet}`" +| .target pkg target => + if let some config := pkg.findTargetConfig? target then + config.build pkg + else + error s!"could not build `{target}` of `{pkg.name}` -- target not found" +| .libraryFacet lib facet => do + if let some config := (← getWorkspace).findLibraryFacetConfig? facet then + config.build lib + else + error s!"do not know how to build library facet `{facet}`" +| .leanExe exe => + mkTargetFacetBuild LeanExe.exeFacet exe.recBuildExe +| .staticExternLib lib => + mkTargetFacetBuild ExternLib.staticFacet lib.recBuildStatic +| .sharedExternLib lib => + mkTargetFacetBuild ExternLib.sharedFacet lib.recBuildShared +| .dynlibExternLib lib => + mkTargetFacetBuild ExternLib.dynlibFacet lib.recComputeDynlib + +/-- +Run the given recursive build using the Lake build index +and a topological / suspending scheduler. +-/ +def IndexBuildM.run (build : IndexBuildM α) : RecBuildM α := + build <| recFetchMemoize BuildInfo.key recBuildWithIndex + +/-- +Recursively build the given info using the Lake build index +and a topological / suspending scheduler. +-/ +def buildIndexTop' (info : BuildInfo) : RecBuildM (BuildData info.key) := + recFetchMemoize BuildInfo.key recBuildWithIndex info + +/-- +Recursively build the given info using the Lake build index +and a topological / suspending scheduler and return the dynamic result. +-/ +@[macro_inline] def buildIndexTop (info : BuildInfo) +[FamilyOut BuildData info.key α] : RecBuildM α := do + cast (by simp) <| buildIndexTop' info + +/-- Build the given Lake target in a fresh build store. -/ +@[inline] def BuildInfo.build +(self : BuildInfo) [FamilyOut BuildData self.key α] : BuildM α := + buildIndexTop self |>.run + +export BuildInfo (build) + +/-! ### Lean Executable Builds -/ + +@[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) := + self.exe.build + +@[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) := + self.exe.fetch diff --git a/src/lake/Lake/Build/Info.lean b/src/lake/Lake/Build/Info.lean new file mode 100644 index 0000000000..562dc0d031 --- /dev/null +++ b/src/lake/Lake/Build/Info.lean @@ -0,0 +1,269 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Config.LeanExe +import Lake.Config.ExternLib +import Lake.Build.Facets +import Lake.Util.EquipT + +/-! +# Build Info + +This module defines the Lake build info type and related utilities. +Build info is what is the data passed to a Lake build function to facilitate +the build. +-/ + +namespace Lake + +/-- The type of Lake's build info. -/ +inductive BuildInfo +| moduleFacet (module : Module) (facet : Name) +| packageFacet (package : Package) (facet : Name) +| libraryFacet (lib : LeanLib) (facet : Name) +| leanExe (exe : LeanExe) +| staticExternLib (lib : ExternLib) +| sharedExternLib (lib : ExternLib) +| dynlibExternLib (lib : ExternLib) +| target (package : Package) (target : Name) + +-------------------------------------------------------------------------------- +/-! ## Build Info & Keys -/ +-------------------------------------------------------------------------------- + +/-! ### Build Key Helper Constructors -/ + +abbrev Module.facetBuildKey (facet : Name) (self : Module) : BuildKey := + .moduleFacet self.keyName facet + +abbrev Package.facetBuildKey (facet : Name) (self : Package) : BuildKey := + .packageFacet self.name facet + +abbrev Package.targetBuildKey (target : Name) (self : Package) : BuildKey := + .customTarget self.name target + +abbrev LeanLib.facetBuildKey (self : LeanLib) (facet : Name) : BuildKey := + .targetFacet self.pkg.name self.name (`leanLib ++ facet) + +abbrev LeanExe.buildKey (self : LeanExe) : BuildKey := + .targetFacet self.pkg.name self.name exeFacet + +abbrev ExternLib.staticBuildKey (self : ExternLib) : BuildKey := + .targetFacet self.pkg.name self.name staticFacet + +abbrev ExternLib.sharedBuildKey (self : ExternLib) : BuildKey := + .targetFacet self.pkg.name self.name sharedFacet + +abbrev ExternLib.dynlibBuildKey (self : ExternLib) : BuildKey := + .targetFacet self.pkg.name self.name dynlibFacet + +/-! ### Build Info to Key -/ + +/-- The key that identifies the build in the Lake build store. -/ +abbrev BuildInfo.key : (self : BuildInfo) → BuildKey +| moduleFacet m f => m.facetBuildKey f +| packageFacet p f => p.facetBuildKey f +| libraryFacet l f => l.facetBuildKey f +| leanExe x => x.buildKey +| staticExternLib l => l.staticBuildKey +| sharedExternLib l => l.sharedBuildKey +| dynlibExternLib l => l.dynlibBuildKey +| target p t => p.targetBuildKey t + +/-! ### Instances for deducing data types of `BuildInfo` keys -/ + +instance [FamilyOut ModuleData f α] +: FamilyDef BuildData (BuildInfo.key (.moduleFacet m f)) α where + family_key_eq_type := by unfold BuildData; simp + +instance [FamilyOut PackageData f α] +: FamilyDef BuildData (BuildInfo.key (.packageFacet p f)) α where + family_key_eq_type := by unfold BuildData; simp + +instance (priority := low) {p : NPackage n} : FamilyDef BuildData + (.customTarget p.toPackage.name t) (CustomData (n,t)) := ⟨by simp⟩ + +instance {p : NPackage n} [FamilyOut CustomData (n, t) α] +: FamilyDef BuildData (BuildInfo.key (.target p.toPackage t)) α where + family_key_eq_type := by unfold BuildData; simp + +instance [FamilyOut TargetData (`leanLib ++ f) α] +: FamilyDef BuildData (BuildInfo.key (.libraryFacet l f)) α where + family_key_eq_type := by unfold BuildData; simp + +instance [FamilyOut TargetData LeanExe.exeFacet α] +: FamilyDef BuildData (BuildInfo.key (.leanExe x)) α where + family_key_eq_type := by unfold BuildData; simp + +instance [FamilyOut TargetData ExternLib.staticFacet α] +: FamilyDef BuildData (BuildInfo.key (.staticExternLib l)) α where + family_key_eq_type := by unfold BuildData; simp + +instance [FamilyOut TargetData ExternLib.sharedFacet α] +: FamilyDef BuildData (BuildInfo.key (.sharedExternLib l)) α where + family_key_eq_type := by unfold BuildData; simp + +instance [FamilyOut TargetData ExternLib.dynlibFacet α] +: FamilyDef BuildData (BuildInfo.key (.dynlibExternLib l)) α where + family_key_eq_type := by unfold BuildData; simp + +-------------------------------------------------------------------------------- +/-! ## Recursive Building -/ +-------------------------------------------------------------------------------- + +/-- A build function for any element of the Lake build index. -/ +abbrev IndexBuildFn (m : Type → Type v) := + -- `DBuildFn BuildInfo (BuildData ·.key) m` with less imports + (info : BuildInfo) → m (BuildData info.key) + +/-- A transformer to equip a monad with a build function for the Lake index. -/ +abbrev IndexT (m : Type → Type v) := EquipT (IndexBuildFn m) m + +/-- The monad for build functions that are part of the index. -/ +abbrev IndexBuildM := IndexT RecBuildM + +/-- Fetch the result associated with the info using the Lake build index. -/ +@[inline] def BuildInfo.fetch (self : BuildInfo) [FamilyOut BuildData self.key α] : IndexBuildM α := + fun build => cast (by simp) <| build self + +export BuildInfo (fetch) + +-------------------------------------------------------------------------------- +/-! ## Build Info & Facets -/ +-------------------------------------------------------------------------------- + +/-! +### Complex Builtin Facet Declarations + +Additional builtin facets missing from `Build.Facets`. +These are defined here because they need configuration definitions +(e.g., `Module`), whereas the facets there are needed by the configuration +definitions. +-/ + +/-- The direct local imports of the Lean module. -/ +abbrev Module.importsFacet := `lean.imports +module_data lean.imports : Array Module + +/-- The transitive local imports of the Lean module. -/ +abbrev Module.transImportsFacet := `lean.transImports +module_data lean.transImports : Array Module + +/-- The transitive local imports of the Lean module. -/ +abbrev Module.precompileImportsFacet := `lean.precompileImports +module_data lean.precompileImports : Array Module + +/-- Shared library for `--load-dynlib`. -/ +abbrev Module.dynlibFacet := `dynlib +module_data dynlib : BuildJob Dynlib + +/-- A Lean library's Lean modules. -/ +abbrev LeanLib.modulesFacet := `modules +library_data modules : Array Module + +/-- The package's complete array of transitive dependencies. -/ +abbrev Package.depsFacet := `deps +package_data deps : Array Package + + +/-! +### Facet Build Info Helper Constructors + +Definitions to easily construct `BuildInfo` values for module, package, +and target facets. +-/ + +namespace Module + +/-- Build info for the module's specified facet. -/ +abbrev facet (facet : Name) (self : Module) : BuildInfo := + .moduleFacet self facet + +@[inherit_doc importsFacet] abbrev imports (self : Module) := + self.facet importsFacet + +@[inherit_doc transImportsFacet] abbrev transImports (self : Module) := + self.facet transImportsFacet + +@[inherit_doc precompileImportsFacet] abbrev precompileImports (self : Module) := + self.facet precompileImportsFacet + +@[inherit_doc depsFacet] abbrev deps (self : Module) := + self.facet depsFacet + +@[inherit_doc leanBinFacet] abbrev leanBin (self : Module) := + self.facet leanBinFacet + +@[inherit_doc importBinFacet] abbrev importBin (self : Module) := + self.facet importBinFacet + +@[inherit_doc oleanFacet] abbrev olean (self : Module) := + self.facet oleanFacet + +@[inherit_doc ileanFacet] abbrev ilean (self : Module) := + self.facet ileanFacet + +@[inherit_doc cFacet] abbrev c (self : Module) := + self.facet cFacet + +@[inherit_doc oFacet] abbrev o (self : Module) := + self.facet oFacet + +@[inherit_doc dynlibFacet] abbrev dynlib (self : Module) := + self.facet dynlibFacet + +end Module + +/-- Build info for the package's specified facet. -/ +abbrev Package.facet (facet : Name) (self : Package) : BuildInfo := + .packageFacet self facet + +@[inherit_doc releaseFacet] +abbrev Package.release (self : Package) : BuildInfo := + self.facet releaseFacet + +@[inherit_doc extraDepFacet] +abbrev Package.extraDep (self : Package) : BuildInfo := + self.facet extraDepFacet + +/-- Build info for a custom package target. -/ +abbrev Package.target (target : Name) (self : Package) : BuildInfo := + .target self target + +/-- Build info of the Lean library's Lean binaries. -/ +abbrev LeanLib.facet (self : LeanLib) (facet : Name) : BuildInfo := + .libraryFacet self facet + +@[inherit_doc modulesFacet] +abbrev LeanLib.modules (self : LeanLib) : BuildInfo := + self.facet modulesFacet + +@[inherit_doc leanFacet] +abbrev LeanLib.lean (self : LeanLib) : BuildInfo := + self.facet leanFacet + +@[inherit_doc staticFacet] +abbrev LeanLib.static (self : LeanLib) : BuildInfo := + self.facet staticFacet + +@[inherit_doc sharedFacet] +abbrev LeanLib.shared (self : LeanLib) : BuildInfo := + self.facet sharedFacet + +/-- Build info of the Lean executable. -/ +abbrev LeanExe.exe (self : LeanExe) : BuildInfo := + .leanExe self + +/-- Build info of the external library's static binary. -/ +abbrev ExternLib.static (self : ExternLib) : BuildInfo := + .staticExternLib self + +/-- Build info of the external library's shared binary. -/ +abbrev ExternLib.shared (self : ExternLib) : BuildInfo := + .sharedExternLib self + +/-- Build info of the external library's dynlib. -/ +abbrev ExternLib.dynlib (self : ExternLib) : BuildInfo := + .dynlibExternLib self diff --git a/src/lake/Lake/Build/Job.lean b/src/lake/Lake/Build/Job.lean new file mode 100644 index 0000000000..31eca9a5ea --- /dev/null +++ b/src/lake/Lake/Build/Job.lean @@ -0,0 +1,112 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Util.Async +import Lake.Build.Trace +import Lake.Build.Context + +open System +namespace Lake + +/-- A Lake job. -/ +abbrev Job α := OptionIOTask α + +/-- The monad of Lake jobs. -/ +abbrev JobM := BuildM + +/-- The monad of a finished Lake job. -/ +abbrev ResultM := OptionIO + +namespace Job + +@[inline] def nil : Job Unit := + pure () + +@[inline] protected def async (act : JobM α) : SchedulerM (Job α) := + async act + +@[inline] protected def await (self : Job α) : ResultM α := + await self + +@[inline] protected def bindSync +(self : Job α) (f : α → JobM β) (prio := Task.Priority.default) : SchedulerM (Job β) := + bindSync prio self f + +@[inline] protected def bindAsync +(self : Job α) (f : α → SchedulerM (Job β)) : SchedulerM (Job β) := + bindAsync self f + +end Job + +/-- A Lake build job. -/ +abbrev BuildJob α := Job (α × BuildTrace) + +namespace BuildJob + +@[inline] def mk (job : Job (α × BuildTrace)) : BuildJob α := + job + +@[inline] def ofJob (self : Job BuildTrace) : BuildJob Unit := + mk <| ((), ·) <$> self + +@[inline] def toJob (self : BuildJob α) : Job (α × BuildTrace) := + self + +@[inline] def nil : BuildJob Unit := + mk <| pure ((), nilTrace) + +@[inline] protected def pure (a : α) : BuildJob α := + mk <| pure (a, nilTrace) + +instance : Pure BuildJob := ⟨BuildJob.pure⟩ + +@[inline] protected def map (f : α → β) (self : BuildJob α) : BuildJob β := + mk <| (fun (a,t) => (f a,t)) <$> self.toJob + +instance : Functor BuildJob where + map := BuildJob.map + +@[inline] def mapWithTrace (f : α → BuildTrace → β × BuildTrace) (self : BuildJob α) : BuildJob β := + mk <| (fun (a,t) => f a t) <$> self.toJob + +@[inline] protected def bindSync +(self : BuildJob α) (f : α → BuildTrace → JobM β) +(prio : Task.Priority := .default) : SchedulerM (Job β) := + self.toJob.bindSync (prio := prio) fun (a, t) => f a t + +@[inline] protected def bindAsync +(self : BuildJob α) (f : α → BuildTrace → SchedulerM (Job β)) : SchedulerM (Job β) := + self.toJob.bindAsync fun (a, t) => f a t + +@[inline] protected def await (self : BuildJob α) : ResultM α := + (·.1) <$> await self.toJob + +instance : Await BuildJob ResultM := ⟨BuildJob.await⟩ + +@[inline] def materialize (self : BuildJob α) : ResultM Unit := + discard <| await self.toJob + +def mix (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob Unit) := + mk <$> seqWithAsync (fun (_,t) (_,t') => ((), mixTrace t t')) t1.toJob t2.toJob + +def mixList (jobs : List (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do + jobs.foldrM (init := pure nilTrace) fun j a => + seqWithAsync (fun (_,t') t => mixTrace t t') j.toJob a + +def mixArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob Unit) := ofJob <$> do + jobs.foldlM (init := pure nilTrace) fun a j => + seqWithAsync (fun t (_,t') => mixTrace t t') a j.toJob + +protected def seqWithAsync +(f : α → β → γ) (t1 : BuildJob α) (t2 : BuildJob β) : BaseIO (BuildJob γ) := + mk <$> seqWithAsync (fun (a,t) (b,t') => (f a b, mixTrace t t')) t1.toJob t2.toJob + +instance : SeqWithAsync BaseIO BuildJob := ⟨BuildJob.seqWithAsync⟩ + +def collectList (jobs : List (BuildJob α)) : BaseIO (BuildJob (List α)) := + jobs.foldrM (seqWithAsync List.cons) (pure []) + +def collectArray (jobs : Array (BuildJob α)) : BaseIO (BuildJob (Array α)) := + jobs.foldlM (seqWithAsync Array.push) (pure #[]) diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean new file mode 100644 index 0000000000..6b1ebd9377 --- /dev/null +++ b/src/lake/Lake/Build/Key.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Util.Name + +namespace Lake + +/-- The type of keys in the Lake build store. -/ +inductive BuildKey +| moduleFacet (module : Name) (facet : Name) +| packageFacet (package : Name) (facet : Name) +| targetFacet (package : Name) (target : Name) (facet : Name) +| customTarget (package : Name) (target : Name) +deriving Inhabited, Repr, DecidableEq, Hashable + +namespace BuildKey + +def toString : (self : BuildKey) → String +| moduleFacet m f => s!"+{m}:{f}" +| packageFacet p f => s!"@{p}:{f}" +| targetFacet p t f => s!"{p}/{t}:{f}" +| customTarget p t => s!"{p}/{t}" + +instance : ToString BuildKey := ⟨(·.toString)⟩ + +def quickCmp (k k' : BuildKey) : Ordering := + match k with + | moduleFacet m f => + match k' with + | moduleFacet m' f' => + match m.quickCmp m' with + | .eq => f.quickCmp f' + | ord => ord + | _ => .lt + | packageFacet p f => + match k' with + | moduleFacet .. => .gt + | packageFacet p' f' => + match p.quickCmp p' with + | .eq => f.quickCmp f' + | ord => ord + | _ => .lt + | targetFacet p t f => + match k' with + | customTarget .. => .lt + | targetFacet p' t' f' => + match p.quickCmp p' with + | .eq => + match t.quickCmp t' with + | .eq => f.quickCmp f' + | ord => ord + | ord => ord + | _=> .gt + | customTarget p t => + match k' with + | customTarget p' t' => + match p.quickCmp p' with + | .eq => t.quickCmp t' + | ord => ord + | _ => .gt + +theorem eq_of_quickCmp {k k' : BuildKey} : +quickCmp k k' = Ordering.eq → k = k' := by + unfold quickCmp + cases k with + | moduleFacet m f => + cases k' + case moduleFacet m' f' => + dsimp only; split + next m_eq => intro f_eq; rw [eq_of_cmp m_eq, eq_of_cmp f_eq] + next => intro; contradiction + all_goals (intro; contradiction) + | packageFacet p f => + cases k' + case packageFacet p' f' => + dsimp only; split + next p_eq => intro f_eq; rw [eq_of_cmp p_eq, eq_of_cmp f_eq] + next => intro; contradiction + all_goals (intro; contradiction) + | targetFacet p t f => + cases k' + case targetFacet p' t' f' => + dsimp only; split + next p_eq => + split + next t_eq => + intro f_eq + rw [eq_of_cmp p_eq, eq_of_cmp t_eq, eq_of_cmp f_eq] + next => intro; contradiction + next => intro; contradiction + all_goals (intro; contradiction) + | customTarget p t => + cases k' + case customTarget p' t' => + dsimp only; split + next p_eq => intro t_eq; rw [eq_of_cmp p_eq, eq_of_cmp t_eq] + next => intro; contradiction + all_goals (intro; contradiction) + +instance : LawfulCmpEq BuildKey quickCmp where + eq_of_cmp := eq_of_quickCmp + cmp_rfl {k} := by cases k <;> simp [quickCmp] diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean new file mode 100644 index 0000000000..123d377288 --- /dev/null +++ b/src/lake/Lake/Build/Library.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Common + +namespace Lake + +/-- Get the Lean library in the workspace with the configuration's name. -/ +@[inline] def LeanLibConfig.get (self : LeanLibConfig) +[Monad m] [MonadError m] [MonadLake m] : m LeanLib := do + let some lib ← findLeanLib? self.name + | error "Lean library '{self.name}' does not exist in the workspace" + return lib + +/-- Fetch the build result of a library facet. -/ +@[inline] protected def LibraryFacetDecl.fetch (lib : LeanLib) +(self : LibraryFacetDecl) [FamilyOut LibraryData self.name α] : IndexBuildM α := do + fetch <| lib.facet self.name + +/-- Fetch the build job of a library facet. -/ +def LibraryFacetConfig.fetchJob (lib : LeanLib) +(self : LibraryFacetConfig name) : IndexBuildM (BuildJob Unit) := do + let some getJob := self.getJob? + | error "library facet '{self.name}' has no associated build job" + return getJob <| ← fetch <| lib.facet self.name + +/-- Fetch the build job of a library facet. -/ +def LeanLib.fetchFacetJob +(name : Name) (self : LeanLib) : IndexBuildM (BuildJob Unit) := do + let some config := (← getWorkspace).libraryFacetConfigs.find? name + | error "library facet '{name}' does not exist in workspace" + inline <| config.fetchJob self + +/-! # Build Lean & Static Lib -/ + +/-- +Collect the local modules of a library. +That is, the modules from `getModuleArray` plus their local transitive imports. +-/ +partial def LeanLib.recCollectLocalModules (self : LeanLib) : IndexBuildM (Array Module) := do + let mut mods := #[] + let mut modSet := ModuleSet.empty + for mod in (← self.getModuleArray) do + (mods, modSet) ← go mod mods modSet + return mods +where + go root mods modSet := do + let mut mods := mods + let mut modSet := modSet + unless modSet.contains root do + modSet := modSet.insert root + let imps ← root.imports.fetch + for mod in imps do + if self.isLocalModule mod.name then + (mods, modSet) ← go mod mods modSet + mods := mods.push root + return (mods, modSet) + +/-- The `LibraryFacetConfig` for the builtin `modulesFacet`. -/ +def LeanLib.modulesFacetConfig : LibraryFacetConfig modulesFacet := + mkFacetConfig LeanLib.recCollectLocalModules + +protected def LeanLib.recBuildLean +(self : LeanLib) : IndexBuildM (BuildJob Unit) := do + let mods ← self.modules.fetch + mods.foldlM (init := BuildJob.nil) fun job mod => do + job.mix <| ← mod.leanBin.fetch + +/-- The `LibraryFacetConfig` for the builtin `leanFacet`. -/ +def LeanLib.leanFacetConfig : LibraryFacetConfig leanFacet := + mkFacetJobConfigSmall LeanLib.recBuildLean + +protected def LeanLib.recBuildStatic +(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do + let mods ← self.modules.fetch + let oJobs ← mods.concatMapM fun mod => + mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name + buildStaticLib self.staticLibFile oJobs + +/-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/ +def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet := + mkFacetJobConfig LeanLib.recBuildStatic + +/-! # Build Shared Lib -/ + +protected def LeanLib.recBuildShared +(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do + let mods ← self.modules.fetch + let oJobs ← mods.concatMapM fun mod => + mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name + let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray + let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch)) + buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.linkArgs + +/-- The `LibraryFacetConfig` for the builtin `sharedFacet`. -/ +def LeanLib.sharedFacetConfig : LibraryFacetConfig sharedFacet := + mkFacetJobConfig LeanLib.recBuildShared + +open LeanLib in +/-- +A library facet name to build function map that contains builders for +the initial set of Lake library facets (e.g., `lean`, `static`, and `shared`). +-/ +def initLibraryFacetConfigs : DNameMap LibraryFacetConfig := + DNameMap.empty + |>.insert modulesFacet modulesFacetConfig + |>.insert leanFacet leanFacetConfig + |>.insert staticFacet staticFacetConfig + |>.insert sharedFacet sharedFacetConfig diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean new file mode 100644 index 0000000000..3f86b4e91a --- /dev/null +++ b/src/lake/Lake/Build/Module.lean @@ -0,0 +1,255 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich, Mac Malone +-/ +import Lake.Util.OrdHashSet +import Lean.Elab.ParseImportsFast +import Lake.Build.Common + +open System + +namespace Lake + +/-- Fetch the build result of a module facet. -/ +@[inline] protected def ModuleFacetDecl.fetch (mod : Module) +(self : ModuleFacetDecl) [FamilyOut ModuleData self.name α] : IndexBuildM α := do + fetch <| mod.facet self.name + +/-- Fetch the build job of a module facet. -/ +def ModuleFacetConfig.fetchJob (mod : Module) +(self : ModuleFacetConfig name) : IndexBuildM (BuildJob Unit) := do + let some getJob := self.getJob? + | error "module facet '{self.name}' has no associated build job" + return getJob <| ← fetch <| mod.facet self.name + +/-- Fetch the build job of a module facet. -/ +def Module.fetchFacetJob +(name : Name) (self : Module) : IndexBuildM (BuildJob Unit) := do + let some config := (← getWorkspace).moduleFacetConfigs.find? name + | error "library facet '{name}' does not exist in workspace" + inline <| config.fetchJob self + +def Module.buildUnlessUpToDate (mod : Module) +(dynlibPath : SearchPath) (dynlibs : Array FilePath) +(depTrace : BuildTrace) : BuildM PUnit := do + let isOldMode ← getIsOldMode + let argTrace : BuildTrace := pureHash mod.leanArgs + let srcTrace : BuildTrace ← computeTrace { path := mod.leanFile : TextFilePath } + let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace + let modUpToDate ← do + if isOldMode then + srcTrace.checkAgainstTime mod + else + modTrace.checkAgainstFile mod mod.traceFile + let name := mod.name.toString + unless modUpToDate do + compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile + (← getLeanPath) mod.rootDir dynlibs dynlibPath (mod.leanArgs ++ mod.weakLeanArgs) (← getLean) + unless isOldMode do + modTrace.writeToFile mod.traceFile + +/-- Compute library directories and build external library Jobs of the given packages. -/ +def recBuildExternDynlibs (pkgs : Array Package) +: IndexBuildM (Array (BuildJob Dynlib) × Array FilePath) := do + let mut libDirs := #[] + let mut jobs : Array (BuildJob Dynlib) := #[] + for pkg in pkgs do + libDirs := libDirs.push pkg.nativeLibDir + jobs := jobs.append <| ← pkg.externLibs.mapM (·.dynlib.fetch) + return (jobs, libDirs) + +/-- +Build the dynlibs of the transitive imports that want precompilation +and the dynlibs of *their* imports. +-/ +partial def recBuildPrecompileDynlibs (imports : Array Module) +: IndexBuildM (Array (BuildJob Dynlib) × Array (BuildJob Dynlib) × Array FilePath) := do + let (pkgs, _, jobs) ← + go imports OrdPackageSet.empty ModuleSet.empty #[] false + return (jobs, ← recBuildExternDynlibs pkgs.toArray) +where + go imports pkgs modSet jobs shouldPrecompile := do + let mut pkgs := pkgs + let mut modSet := modSet + let mut jobs := jobs + for mod in imports do + if modSet.contains mod then + continue + modSet := modSet.insert mod + let shouldPrecompile := shouldPrecompile || mod.shouldPrecompile + if shouldPrecompile then + pkgs := pkgs.insert mod.pkg + jobs := jobs.push <| (← mod.dynlib.fetch) + let recImports ← mod.imports.fetch + (pkgs, modSet, jobs) ← go recImports pkgs modSet jobs shouldPrecompile + return (pkgs, modSet, jobs) + +variable [MonadLiftT BuildM m] + +/-- +Recursively parse the Lean files of a module and its imports +building an `Array` product of its direct local imports. +-/ +def Module.recParseImports (mod : Module) : IndexBuildM (Array Module) := do + let contents ← IO.FS.readFile mod.leanFile + let imports ← Lean.parseImports' contents mod.leanFile.toString + let mods ← imports.foldlM (init := OrdModuleSet.empty) fun set imp => + findModule? imp.module <&> fun | some mod => set.insert mod | none => set + return mods.toArray + +/-- The `ModuleFacetConfig` for the builtin `importsFacet`. -/ +def Module.importsFacetConfig : ModuleFacetConfig importsFacet := + mkFacetConfig (·.recParseImports) + +/-- Recursively compute a module's transitive imports. -/ +def Module.recComputeTransImports (mod : Module) : IndexBuildM (Array Module) := do + (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do + return set.appendArray (← imp.transImports.fetch) |>.insert imp + +/-- The `ModuleFacetConfig` for the builtin `transImportsFacet`. -/ +def Module.transImportsFacetConfig : ModuleFacetConfig transImportsFacet := + mkFacetConfig (·.recComputeTransImports) + +/-- Recursively compute a module's precompiled imports. -/ +def Module.recComputePrecompileImports (mod : Module) : IndexBuildM (Array Module) := do + (·.toArray) <$> (← mod.imports.fetch).foldlM (init := OrdModuleSet.empty) fun set imp => do + if imp.shouldPrecompile then + return set.appendArray (← imp.transImports.fetch) |>.insert imp + else + return set.appendArray (← imp.precompileImports.fetch) + +/-- The `ModuleFacetConfig` for the builtin `precompileImportsFacet`. -/ +def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFacet := + mkFacetConfig (·.recComputePrecompileImports) + +/-- Recursively build a module's transitive local imports and shared library dependencies. -/ +def Module.recBuildDeps (mod : Module) : IndexBuildM (BuildJob (SearchPath × Array FilePath)) := do + let imports ← mod.imports.fetch + let extraDepJob ← mod.pkg.extraDep.fetch + let precompileImports ← mod.precompileImports.fetch + let modJobs ← precompileImports.mapM (·.dynlib.fetch) + let pkgs := precompileImports.foldl (·.insert ·.pkg) + OrdPackageSet.empty |>.insert mod.pkg |>.toArray + let (externJobs, libDirs) ← recBuildExternDynlibs pkgs + let importJob ← BuildJob.mixArray <| ← imports.mapM (·.importBin.fetch) + let externDynlibsJob ← BuildJob.collectArray externJobs + let modDynlibsJob ← BuildJob.collectArray modJobs + + extraDepJob.bindAsync fun _ _ => do + importJob.bindAsync fun _ importTrace => do + modDynlibsJob.bindAsync fun modDynlibs modTrace => do + return externDynlibsJob.mapWithTrace fun externDynlibs externTrace => + let depTrace := importTrace.mix <| modTrace.mix externTrace + /- + Requirements: + * Lean wants the external library symbols before module symbols. + * Unix requires the file extension of the dynlib. + * For some reason, building from the Lean server requires full paths. + Everything else loads fine with just the augmented library path. + * Linux still needs the augmented path to resolve nested dependencies in dynlibs. + -/ + let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList + let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path) + ((dynlibPath, dynlibs), depTrace) + +/-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/ +def Module.depsFacetConfig : ModuleFacetConfig depsFacet := + mkFacetJobConfigSmall (·.recBuildDeps) + +/-- Recursively build a module and its dependencies. -/ +def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) := do + (← mod.deps.fetch).bindSync fun (dynlibPath, dynlibs) depTrace => do + mod.buildUnlessUpToDate dynlibPath dynlibs depTrace + return ((), depTrace) + +/-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/ +def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet := + mkFacetJobConfig (·.recBuildLeanCore) + +/-- The `ModuleFacetConfig` for the builtin `importBinFacet`. -/ +def Module.importBinFacetConfig : ModuleFacetConfig importBinFacet := + mkFacetJobConfigSmall fun mod => do + (← mod.leanBin.fetch).bindSync fun _ depTrace => + return ((), mixTrace (← computeTrace mod) depTrace) + +/-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/ +def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet := + mkFacetJobConfigSmall fun mod => do + (← mod.leanBin.fetch).bindSync fun _ depTrace => + return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace) + +/-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/ +def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet := + mkFacetJobConfigSmall fun mod => do + (← mod.leanBin.fetch).bindSync fun _ depTrace => + return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace) + +/-- The `ModuleFacetConfig` for the builtin `cFacet`. -/ +def Module.cFacetConfig : ModuleFacetConfig cFacet := + mkFacetJobConfigSmall fun mod => do + (← mod.leanBin.fetch).bindSync fun _ _ => + -- do content-aware hashing so that we avoid recompiling unchanged C files + return (mod.cFile, ← computeTrace mod.cFile) + +/-- Recursively build the module's object file from its C file produced by `lean`. -/ +def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do + buildLeanO self.name.toString self.oFile (← self.c.fetch) self.leancArgs + +/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/ +def Module.oFacetConfig : ModuleFacetConfig oFacet := + mkFacetJobConfig Module.recBuildLeanO + +-- TODO: Return `BuildJob OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib` +/-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/ +def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do + + -- Compute dependencies + let transImports ← mod.transImports.fetch + let modJobs ← transImports.mapM (·.dynlib.fetch) + let pkgs := transImports.foldl (·.insert ·.pkg) + OrdPackageSet.empty |>.insert mod.pkg |>.toArray + let (externJobs, pkgLibDirs) ← recBuildExternDynlibs pkgs + let linkJobs ← mod.nativeFacets.mapM (fetch <| mod.facet ·.name) + + -- Collect Jobs + let linksJob ← BuildJob.collectArray linkJobs + let modDynlibsJob ← BuildJob.collectArray modJobs + let externDynlibsJob ← BuildJob.collectArray externJobs + + -- Build dynlib + show SchedulerM _ from do + linksJob.bindAsync fun links oTrace => do + modDynlibsJob.bindAsync fun modDynlibs libTrace => do + externDynlibsJob.bindSync fun externDynlibs externTrace => do + let libNames := modDynlibs.map (·.name) ++ externDynlibs.map (·.name) + let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.dir?) + let depTrace := oTrace.mix <| libTrace.mix externTrace + let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do + let args := links.map toString ++ + libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}") + compileSharedLib mod.name.toString mod.dynlibFile args (← getLeanc) + return (⟨mod.dynlibFile, mod.dynlibName⟩, trace) + +/-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/ +def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet := + mkFacetJobConfig Module.recBuildDynlib + +open Module in +/-- +A name-configuration map for the initial set of +Lake module facets (e.g., `lean.{imports, c, o, dynlib]`). +-/ +def initModuleFacetConfigs : DNameMap ModuleFacetConfig := + DNameMap.empty + |>.insert importsFacet importsFacetConfig + |>.insert transImportsFacet transImportsFacetConfig + |>.insert precompileImportsFacet precompileImportsFacetConfig + |>.insert depsFacet depsFacetConfig + |>.insert leanBinFacet leanBinFacetConfig + |>.insert importBinFacet importBinFacetConfig + |>.insert oleanFacet oleanFacetConfig + |>.insert ileanFacet ileanFacetConfig + |>.insert cFacet cFacetConfig + |>.insert oFacet oFacetConfig + |>.insert dynlibFacet dynlibFacetConfig diff --git a/src/lake/Lake/Build/Monad.lean b/src/lake/Lake/Build/Monad.lean new file mode 100644 index 0000000000..ab94ee1f38 --- /dev/null +++ b/src/lake/Lake/Build/Monad.lean @@ -0,0 +1,57 @@ +/- +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.Config.Monad +import Lake.Build.Context +import Lake.Util.EStateT + +open System + +namespace Lake + +def mkBuildContext (ws : Workspace) (oldMode : Bool) : IO BuildContext := do + let lean := ws.lakeEnv.lean + let leanTrace := Hash.ofString lean.githash + return { + opaqueWs := ws, leanTrace, oldMode + startedBuilds := ← IO.mkRef 0 + finishedBuilds := ← IO.mkRef 0 + } + +@[inline] def getLeanTrace : BuildM BuildTrace := + (·.leanTrace) <$> readThe BuildContext + +@[inline] def getIsOldMode : BuildM Bool := + (·.oldMode) <$> readThe BuildContext + +def failOnBuildCycle [ToString k] : Except (List k) α → BuildM α +| Except.ok a => pure a +| Except.error cycle => do + let cycle := cycle.map (s!" {·}") + error s!"build cycle detected:\n{"\n".intercalate cycle}" + +/-- +Run the recursive build in the given build store. +If a cycle is encountered, log it and then fail. +-/ +@[inline] def RecBuildM.runIn (store : BuildStore) (build : RecBuildM α) : BuildM (α × BuildStore) := do + let (res, store) ← EStateT.run store <| ReaderT.run build [] + return (← failOnBuildCycle res, store) + +/-- +Run the recursive build in a fresh build store. +If a cycle is encountered, log it and then fail. +-/ +@[inline] def RecBuildM.run (build : RecBuildM α) : BuildM α := do + (·.1) <$> build.runIn {} + +/-- Run the given build function in the Workspace's context. -/ +@[inline] def Workspace.runBuild (ws : Workspace) (build : BuildM α) (oldMode := false) : LogIO α := do + let ctx ← mkBuildContext ws oldMode + build.run ctx + +/-- Run the given build function in the Lake monad's workspace. -/ +@[inline] def runBuild (build : BuildM α) (oldMode := false) : LakeT LogIO α := do + (← getWorkspace).runBuild build oldMode diff --git a/src/lake/Lake/Build/Package.lean b/src/lake/Lake/Build/Package.lean new file mode 100644 index 0000000000..f95595dd59 --- /dev/null +++ b/src/lake/Lake/Build/Package.lean @@ -0,0 +1,122 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Util.Sugar +import Lake.Build.Common + +open System +namespace Lake + +/-- Fetch the build job of the specified package target. -/ +def Package.fetchTargetJob (self : Package) +(target : Name) : IndexBuildM (Option (BuildJob Unit)) := do + let some config := self.findTargetConfig? target + | error s!"package '{self.name}' has no target '{target}'" + return config.getJob (← fetch <| self.target target) + +/-- Fetch the build result of a target. -/ +protected def TargetDecl.fetch (self : TargetDecl) +[FamilyDef CustomData (self.pkg, self.name) α] : IndexBuildM α := do + let some pkg ← findPackage? self.pkg + | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace" + fetch <| pkg.target self.name + +/-- Fetch the build job of the target. -/ +def TargetDecl.fetchJob (self : TargetDecl) : IndexBuildM (BuildJob Unit) := do + let some pkg ← findPackage? self.pkg + | error s!"package '{self.pkg}' of target '{self.name}' does not exist in workspace" + return self.config.getJob (← fetch <| pkg.target self.name) + +/-- Fetch the build result of a package facet. -/ +@[inline] protected def PackageFacetDecl.fetch (pkg : Package) +(self : PackageFacetDecl) [FamilyOut PackageData self.name α] : IndexBuildM α := do + fetch <| pkg.facet self.name + +/-- Fetch the build job of a package facet. -/ +def PackageFacetConfig.fetchJob (pkg : Package) +(self : PackageFacetConfig name) : IndexBuildM (BuildJob Unit) := do + let some getJob := self.getJob? + | error "package facet '{pkg.name}' has no associated build job" + return getJob <| ← fetch <| pkg.facet self.name + +/-- Fetch the build job of a library facet. -/ +def Package.fetchFacetJob +(name : Name) (self : Package) : IndexBuildM (BuildJob Unit) := do + let some config := (← getWorkspace).packageFacetConfigs.find? name + | error "package facet '{name}' does not exist in workspace" + inline <| config.fetchJob self + +/-- Compute a topological ordering of the package's transitive dependencies. -/ +def Package.recComputeDeps (self : Package) : IndexBuildM (Array Package) := do + let mut deps := #[] + let mut depSet := PackageSet.empty + for dep in self.deps do + for depDep in (← fetch <| dep.facet `deps) do + unless depSet.contains depDep do + deps := deps.push depDep + depSet := depSet.insert depDep + unless depSet.contains dep do + deps := deps.push dep + depSet := depSet.insert dep + return deps + +/-- The `PackageFacetConfig` for the builtin `depsFacet`. -/ +def Package.depsFacetConfig : PackageFacetConfig depsFacet := + mkFacetConfig Package.recComputeDeps + +/-- +Build the `extraDepTarget` for the package and its transitive dependencies. +Also fetch pre-built releases for the package's' dependencies. +-/ +def Package.recBuildExtraDepTargets (self : Package) : IndexBuildM (BuildJob Unit) := do + let mut job := BuildJob.nil + -- Build dependencies' extra dep targets + for dep in self.deps do + job ← job.mix <| ← dep.extraDep.fetch + -- Fetch pre-built release if desired and this package is a dependency + if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then + job ← job.mix <| ← self.release.fetch + -- Build this package's extra dep targets + for target in self.extraDepTargets do + if let some config := self.findTargetConfig? target then + job ← job.mix <| config.getJob <| ← fetch <| self.target target + else + error s!"unknown target `{target}`" + return job + +/-- The `PackageFacetConfig` for the builtin `dynlibFacet`. -/ +def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet := + mkFacetJobConfigSmall Package.recBuildExtraDepTargets + +/-- Download and unpack the package's prebuilt release archive (from GitHub). -/ +def Package.fetchRelease (self : Package) : SchedulerM (BuildJob Unit) := Job.async do + let some (repoUrl, tag) := self.release? | do + logWarning "wanted prebuilt release, but release repository and tag was not known" + return ((), .nil) + let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}" + let logName := s!"{self.name}/{tag}/{self.buildArchive}" + try + let depTrace := Hash.ofString url + let trace ← buildFileUnlessUpToDate self.buildArchiveFile depTrace do + download logName url self.buildArchiveFile + untar logName self.buildArchiveFile self.buildDir + return ((), trace) + else + return ((), .nil) + +/-- The `PackageFacetConfig` for the builtin `releaseFacet`. -/ +def Package.releaseFacetConfig : PackageFacetConfig releaseFacet := + mkFacetJobConfig (·.fetchRelease) + +open Package in +/-- +A package facet name to build function map that contains builders for +the initial set of Lake package facets (e.g., `extraDep`). +-/ +def initPackageFacetConfigs : DNameMap PackageFacetConfig := + DNameMap.empty + |>.insert depsFacet depsFacetConfig + |>.insert extraDepFacet extraDepFacetConfig + |>.insert releaseFacet releaseFacetConfig diff --git a/src/lake/Lake/Build/Store.lean b/src/lake/Lake/Build/Store.lean new file mode 100644 index 0000000000..63cf94ed12 --- /dev/null +++ b/src/lake/Lake/Build/Store.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Data +import Lake.Util.StoreInsts + +/-! +# The Lake Build Store + +The Lake build store is the map of Lake build keys to build task and/or +build results that is slowly filled during a recursive build (e.g., via +topological-based build of an initial key's dependencies). +-/ + +namespace Lake + +/-- A monad equipped with a Lake build store. -/ +abbrev MonadBuildStore (m) := MonadDStore BuildKey BuildData m + +/-- The type of the Lake build store. -/ +abbrev BuildStore := + DRBMap BuildKey BuildData BuildKey.quickCmp + +@[inline] def BuildStore.empty : BuildStore := DRBMap.empty + +namespace BuildStore + +-- Linter reports false positives on the `v` variables below +set_option linter.unusedVariables false + +/-- Derive an array of built module facets from the store. -/ +def collectModuleFacetArray (self : BuildStore) +(facet : Name) [FamilyOut ModuleData facet α] : Array α := Id.run do + let mut res : Array α := #[] + for ⟨k, v⟩ in self do + match k with + | .moduleFacet m f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h] + res := res.push <| cast of_data v + | _ => pure () + return res + +/-- Derive a map of module names to built facets from the store. -/ +def collectModuleFacetMap (self : BuildStore) +(facet : Name) [FamilyOut ModuleData facet α] : NameMap α := Id.run do + let mut res := Lean.mkNameMap α + for ⟨k, v⟩ in self do + match k with + | .moduleFacet m f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h] + res := res.insert m <| cast of_data v + | _ => pure () + return res + +/-- Derive an array of built package facets from the store. -/ +def collectPackageFacetArray (self : BuildStore) +(facet : Name) [FamilyOut PackageData facet α] : Array α := Id.run do + let mut res : Array α := #[] + for ⟨k, v⟩ in self do + match k with + | .packageFacet _ f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h] + res := res.push <| cast of_data v + | _ => pure () + return res + +/-- Derive an array of built target facets from the store. -/ +def collectTargetFacetArray (self : BuildStore) +(facet : Name) [FamilyOut TargetData facet α] : Array α := Id.run do + let mut res : Array α := #[] + for ⟨k, v⟩ in self do + match k with + | .targetFacet _ _ f => + if h : f = facet then + have of_data := by unfold BuildData; simp [h] + res := res.push <| cast of_data v + | _ => pure () + return res + +/-- Derive an array of built external shared libraries from the store. -/ +def collectSharedExternLibs (self : BuildStore) +[FamilyOut TargetData `externLib.shared α] : Array α := + self.collectTargetFacetArray `externLib.shared diff --git a/src/lake/Lake/Build/Topological.lean b/src/lake/Lake/Build/Topological.lean new file mode 100644 index 0000000000..90faeb3370 --- /dev/null +++ b/src/lake/Lake/Build/Topological.lean @@ -0,0 +1,139 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Util.Cycle +import Lake.Util.Store +import Lake.Util.EquipT + +/-! +# Topological / Suspending Recursive Builder + +This module defines a recursive build function that topologically +(ι.e., via a depth-first search with memoization) builds the elements of +a build store. + +This is called a suspending scheduler in *Build systems à la carte*. +-/ + +namespace Lake + +/-! +## Recursive Fetching + +In this section, we define the primitives that make up a builder. +-/ + +/-- +A dependently typed monadic *fetch* function. + +That is, a function within the monad `m` and takes an input `a : α` +describing what to fetch and and produces some output `b : β a` (dependently +typed) or `b : B` (not) describing what was fetched. All build functions are +fetch functions, but not all fetch functions need build something. +-/ +abbrev DFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) := + (a : α) → m (β a) + +/-! +In order to nest builds / fetches within one another, +we equip the monad `m` with a fetch function of its own. +-/ + +/-- A transformer that equips a monad with a `DFetchFn`. -/ +abbrev DFetchT (α : Type u) (β : α → Type v) (m : Type v → Type w) := + EquipT (DFetchFn α β m) m + +/-- A `DFetchT` that is not dependently typed. -/ +abbrev FetchT (α : Type u) (β : Type v) (m : Type v → Type w) := + DFetchT α (fun _ => β) m + +/-! +We can then use the such a monad as the basis for a fetch function itself. +-/ + +/- +A `DFetchFn` that utilizes another `DFetchFn` equipped to the monad to +fetch values. It is thus usually implemented recursively via some variation +of the `recFetch` function below, hence the "rec" in both names. +-/ +abbrev DRecFetchFn (α : Type u) (β : α → Type v) (m : Type v → Type w) := + DFetchFn α β (DFetchT α β m) + +/-- A `DRecFetchFn` that is not dependently typed. -/ +abbrev RecFetchFn (α : Type u) (β : Type v) (m : Type v → Type w) := + α → FetchT α β m β + +/-- A `DFetchFn` that provides its base `DRecFetchFn` with itself. -/ +@[specialize] partial def recFetch +[(α : Type u) → Nonempty (m α)] (fetch : DRecFetchFn α β m) : DFetchFn α β m := + fun a => fetch a (recFetch fetch) + +/-! +The basic `recFetch` can fail to terminate in a variety of ways, +it can even cycle (i.e., `a` fetches `b` which fetches `a`). Thus, we +define the `acyclicRecFetch` below to guard against such cases. +-/ + +/-- +A `recFetch` augmented by a `CycleT` to guard against recursive cycles. +If the set of visited keys is finite, this function should provably terminate. + +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] +(keyOf : α → κ) (fetch : DRecFetchFn α β (CycleT κ m)) : DFetchFn α β (CycleT κ m) := + recFetch fun a recurse => + /- + NOTE: We provide the stack directly to `recurse` rather than + get it through `ReaderT` to prevent it being overridden by the `fetch` + function (and thereby potentially produce a cycle). + -/ + guardCycle (keyOf a) fun stack => fetch a (recurse · stack) stack + +/-! +When building, we usually do not want to build the same thing twice during +a single build pass. At the same time, separate builds may both wish to fetch +the same thing. Thus, we need to store past build results to return them upon +future fetches. This is what `recFetchMemoize` below does. +-/ + +/-- +`recFetchAcyclic` augmented with a `MonadDStore` to +memoize fetch results and thus avoid computing the same result twice. +-/ +@[inline] def recFetchMemoize [BEq κ] [Monad m] [MonadDStore κ β m] +(keyOf : α → κ) (fetch : DRecFetchFn α (fun a => β (keyOf a)) (CycleT κ m)) +: 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 new file mode 100644 index 0000000000..0c63b1345d --- /dev/null +++ b/src/lake/Lake/Build/Trace.lean @@ -0,0 +1,273 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ + +open System +namespace Lake + +-------------------------------------------------------------------------------- +/-! # Utilities -/ +-------------------------------------------------------------------------------- + +class CheckExists.{u} (i : Type u) where + /-- Check whether there already exists an artifact for the given target info. -/ + checkExists : i → BaseIO Bool + +export CheckExists (checkExists) + +instance : CheckExists FilePath where + checkExists := FilePath.pathExists + +-------------------------------------------------------------------------------- +/-! # Trace Abstraction -/ +-------------------------------------------------------------------------------- + +class ComputeTrace.{u,v,w} (i : Type u) (m : outParam $ Type v → Type w) (t : Type v) where + /-- Compute the trace of some target info using information from the monadic context. -/ + computeTrace : i → m t + +def computeTrace [ComputeTrace i m t] [MonadLiftT m n] (info : i) : n t := + liftM <| ComputeTrace.computeTrace info + +class NilTrace.{u} (t : Type u) where + /-- The nil trace. Should not unduly clash with a proper trace. -/ + nilTrace : t + +export NilTrace (nilTrace) + +instance [NilTrace t] : Inhabited t := ⟨nilTrace⟩ + +class MixTrace.{u} (t : Type u) where + /-- Combine two traces. The result should be dirty if either of the inputs is dirty. -/ + mixTrace : t → t → t + +export MixTrace (mixTrace) + +def mixTraceM [MixTrace t] [Pure m] (t1 t2 : t) : m t := + pure <| mixTrace t1 t2 + +section +variable [MixTrace t] [NilTrace t] + +def mixTraceList (traces : List t) : t := + traces.foldl mixTrace nilTrace + +def mixTraceArray (traces : Array t) : t := + traces.foldl mixTrace nilTrace + +variable [ComputeTrace i m t] + +def computeListTrace [MonadLiftT m n] [Monad n] (artifacts : List i) : n t := + mixTraceList <$> artifacts.mapM computeTrace + +instance [Monad m] : ComputeTrace (List i) m t := ⟨computeListTrace⟩ + +def computeArrayTrace [MonadLiftT m n] [Monad n] (artifacts : Array i) : n t := + mixTraceArray <$> artifacts.mapM computeTrace + +instance [Monad m] : ComputeTrace (Array i) m t := ⟨computeArrayTrace⟩ +end + +-------------------------------------------------------------------------------- +/-! # Hash Trace -/ +-------------------------------------------------------------------------------- + +/-- +A content hash. +TODO: Use a secure hash rather than the builtin Lean hash function. +-/ +structure Hash where + val : UInt64 + deriving BEq, DecidableEq, Repr + +namespace Hash + +def ofNat (n : Nat) := + mk n.toUInt64 + +def loadFromFile (hashFile : FilePath) : IO (Option Hash) := + return (← IO.FS.readFile hashFile).toNat?.map ofNat + +def nil : Hash := + mk <| 1723 -- same as Name.anonymous + +instance : NilTrace Hash := ⟨nil⟩ + +def mix (h1 h2 : Hash) : Hash := + mk <| mixHash h1.val h2.val + +instance : MixTrace Hash := ⟨mix⟩ + +protected def toString (self : Hash) : String := + toString self.val + +instance : ToString Hash := ⟨Hash.toString⟩ + +def ofString (str : String) := + mix nil <| mk <| hash str -- same as Name.mkSimple + +def ofByteArray (bytes : ByteArray) : Hash := + ⟨hash bytes⟩ + +end Hash + +class ComputeHash (α : Type u) (m : outParam $ Type → Type v) where + computeHash : α → m Hash + +instance [ComputeHash α m] : ComputeTrace α m Hash := ⟨ComputeHash.computeHash⟩ + +def pureHash [ComputeHash α Id] (a : α) : Hash := + ComputeHash.computeHash a + +def computeHash [ComputeHash α m] [MonadLiftT m n] (a : α) : n Hash := + liftM <| ComputeHash.computeHash a + +instance : ComputeHash String Id := ⟨Hash.ofString⟩ + +def computeFileHash (file : FilePath) : IO Hash := + Hash.ofByteArray <$> IO.FS.readBinFile file + +instance : ComputeHash FilePath IO := ⟨computeFileHash⟩ + +/-- + A wrapper around `FilePath` that adjusts its `ComputeHash` implementation + to normalize `\r\n` sequences to `\n` for cross-platform compatibility. -/ +structure TextFilePath where + path : FilePath + +instance : ComputeHash TextFilePath IO where + computeHash file := do + let text ← IO.FS.readFile file.path + let text := text.replace "\r\n" "\n" + return Hash.ofString text + +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 -/ +-------------------------------------------------------------------------------- + +open IO.FS (SystemTime) + +/-- A modification time. -/ +def MTime := SystemTime + +namespace MTime + +instance : OfNat MTime (nat_lit 0) := ⟨⟨0,0⟩⟩ + +instance : BEq MTime := inferInstanceAs (BEq SystemTime) +instance : Repr MTime := inferInstanceAs (Repr SystemTime) + +instance : Ord MTime := inferInstanceAs (Ord SystemTime) +instance : LT MTime := ltOfOrd +instance : LE MTime := leOfOrd +instance : Min MTime := minOfLe +instance : Max MTime := maxOfLe + +instance : NilTrace MTime := ⟨0⟩ +instance : MixTrace MTime := ⟨max⟩ + +end MTime + +class GetMTime (α) where + getMTime : α → IO MTime + +export GetMTime (getMTime) +instance [GetMTime α] : ComputeTrace α IO MTime := ⟨getMTime⟩ + +def getFileMTime (file : FilePath) : IO MTime := + return (← file.metadata).modified + +instance : GetMTime FilePath := ⟨getFileMTime⟩ +instance : GetMTime TextFilePath := ⟨(getFileMTime ·.path)⟩ + +/-- Check if the info's `MTIme` is at least `depMTime`. -/ +def checkIfNewer [GetMTime i] (info : i) (depMTime : MTime) : BaseIO Bool := + (do pure ((← getMTime info) >= depMTime : Bool)).catchExceptions fun _ => pure false + +-------------------------------------------------------------------------------- +/-! # Lake Build Trace (Hash + MTIme) -/ +-------------------------------------------------------------------------------- + +/-- Trace used for common Lake targets. Combines `Hash` and `MTime`. -/ +structure BuildTrace where + hash : Hash + mtime : MTime + deriving Repr + +namespace BuildTrace + +def withHash (hash : Hash) (self : BuildTrace) : BuildTrace := + {self with hash} + +def withoutHash (self : BuildTrace) : BuildTrace := + {self with hash := Hash.nil} + +def withMTime (mtime : MTime) (self : BuildTrace) : BuildTrace := + {self with mtime} + +def withoutMTime (self : BuildTrace) : BuildTrace := + {self with mtime := 0} + +def fromHash (hash : Hash) : BuildTrace := + mk hash 0 + +instance : Coe Hash BuildTrace := ⟨fromHash⟩ + +def fromMTime (mtime : MTime) : BuildTrace := + mk Hash.nil mtime + +instance : Coe MTime BuildTrace := ⟨fromMTime⟩ + +def nil : BuildTrace := + mk Hash.nil 0 + +instance : NilTrace BuildTrace := ⟨nil⟩ + +def compute [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] (info : i) : IO BuildTrace := + return mk (← computeHash info) (← getMTime info) + +instance [ComputeHash i m] [MonadLiftT m IO] [GetMTime i] : ComputeTrace i IO BuildTrace := ⟨compute⟩ + +def mix (t1 t2 : BuildTrace) : BuildTrace := + mk (Hash.mix t1.hash t2.hash) (max t1.mtime t2.mtime) + +instance : MixTrace BuildTrace := ⟨mix⟩ + +/-- +Check the build trace against the given target info and hash +to see if the target is up-to-date. +-/ +def checkAgainstHash [CheckExists i] +(info : i) (hash : Hash) (self : BuildTrace) : BaseIO Bool := + pure (hash == self.hash) <&&> checkExists info + +/-- +Check the build trace against the given target info and its modification time +to see if the target is up-to-date. +-/ +def checkAgainstTime [CheckExists i] [GetMTime i] +(info : i) (self : BuildTrace) : BaseIO Bool := + checkIfNewer info self.mtime + +/-- +Check the build trace against the given target info and its trace file +to see if the target is up-to-date. +-/ +def checkAgainstFile [CheckExists i] [GetMTime i] +(info : i) (traceFile : FilePath) (self : BuildTrace) : BaseIO Bool := do + let act : IO _ := do + if let some hash ← Hash.loadFromFile traceFile then + self.checkAgainstHash info hash + else + return self.mtime < (← getMTime info) + act.catchExceptions fun _ => pure false + +def writeToFile (traceFile : FilePath) (self : BuildTrace) : IO PUnit := + IO.FS.writeFile traceFile self.hash.toString + +end BuildTrace diff --git a/src/lake/Lake/CLI.lean b/src/lake/Lake/CLI.lean new file mode 100644 index 0000000000..2695b6a4cf --- /dev/null +++ b/src/lake/Lake/CLI.lean @@ -0,0 +1,6 @@ +/- +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.CLI.Main diff --git a/src/lake/Lake/CLI/Actions.lean b/src/lake/Lake/CLI/Actions.lean new file mode 100644 index 0000000000..c638330a6c --- /dev/null +++ b/src/lake/Lake/CLI/Actions.lean @@ -0,0 +1,29 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lake.Build.Index + +namespace Lake + +def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do + IO.Process.spawn {cmd, args, env := ← getAugmentedEnv} >>= (·.wait) + +def exe (name : Name) (args : Array String := #[]) (oldMode := false) : LakeT LogIO UInt32 := do + let ws ← getWorkspace + if let some exe := ws.findLeanExe? name then + let exeFile ← ws.runBuild (exe.build >>= (·.await)) oldMode + env exeFile.toString args + else + error s!"unknown executable `{name}`" + +def uploadRelease (pkg : Package) (tag : String) : LogIO Unit := do + let mut args := + #["release", "upload", tag, pkg.buildArchiveFile.toString, "--clobber"] + if let some repo := pkg.releaseRepo? then + args := args.append #["-R", repo] + tar pkg.buildArchive pkg.buildDir pkg.buildArchiveFile + (excludePaths := #["*.tar.gz", "*.tar.gz.trace"]) + logInfo s!"Uploading {tag}/{pkg.buildArchive}" + proc {cmd := "gh", args} diff --git a/src/lake/Lake/CLI/Build.lean b/src/lake/Lake/CLI/Build.lean new file mode 100644 index 0000000000..0f57189588 --- /dev/null +++ b/src/lake/Lake/CLI/Build.lean @@ -0,0 +1,187 @@ +/- +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.Build.Index +import Lake.CLI.Error + +namespace Lake + +/-! ## Build Target Specifiers -/ + +structure BuildSpec where + info : BuildInfo + getBuildJob : BuildData info.key → BuildJob Unit + +@[inline] def BuildSpec.getJob (self : BuildSpec) (data : BuildData self.info.key) : Job Unit := + discard <| self.getBuildJob data + +@[inline] def BuildData.toBuildJob +[FamilyOut BuildData k (BuildJob α)] (data : BuildData k) : BuildJob Unit := + discard <| ofFamily data + +@[inline] def mkBuildSpec (info : BuildInfo) +[FamilyOut BuildData info.key (BuildJob α)] : BuildSpec := + {info, getBuildJob := BuildData.toBuildJob} + +@[inline] def mkConfigBuildSpec (facetType : String) +(info : BuildInfo) (config : FacetConfig Fam ι facet) (h : BuildData info.key = Fam facet) +: Except CliError BuildSpec := do + let some getJob := config.getJob? + | throw <| CliError.nonCliFacet facetType facet + return {info, getBuildJob := h ▸ getJob} + +def BuildSpec.build (self : BuildSpec) : RecBuildM (Job Unit) := + self.getJob <$> buildIndexTop' self.info + +def buildSpecs (specs : Array BuildSpec) : BuildM PUnit := do + let jobs ← RecBuildM.run do specs.mapM (·.build) + jobs.forM (discard <| ·.await) + +/-! ## Parsing CLI Build Target Specifiers -/ + +def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package := + if spec.isEmpty then + return ws.root + else + match ws.findPackage? <| stringToLegalOrSimpleName spec with + | some pkg => return pkg + | none => throw <| CliError.unknownPackage spec + +open Module in +def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : Name) : Except CliError BuildSpec := + if facet.isAnonymous then + return mkBuildSpec <| mod.facet leanBinFacet + else if let some config := ws.findModuleFacetConfig? facet then do + mkConfigBuildSpec "module" (mod.facet facet) config rfl + else + throw <| CliError.unknownFacet "module" facet + +def resolveLibTarget (ws : Workspace) (lib : LeanLib) (facet : Name) : Except CliError (Array BuildSpec) := + if facet.isAnonymous then + lib.defaultFacets.mapM (resolveFacet ·) + else + Array.singleton <$> resolveFacet facet +where + resolveFacet facet := + if let some config := ws.findLibraryFacetConfig? facet then do + mkConfigBuildSpec "library" (lib.facet facet) config rfl + else + throw <| CliError.unknownFacet "library" facet + +def resolveExeTarget (exe : LeanExe) (facet : Name) : Except CliError BuildSpec := + if facet.isAnonymous || facet == `exe then + return mkBuildSpec exe.exe + else + throw <| CliError.unknownFacet "executable" facet + +def resolveExternLibTarget (lib : ExternLib) (facet : Name) : Except CliError BuildSpec := + if facet.isAnonymous || facet = `static then + return mkBuildSpec lib.static + else if facet = `shared then + return mkBuildSpec lib.shared + else + throw <| CliError.unknownFacet "external library" facet + +def resolveCustomTarget (pkg : Package) +(name facet : Name) (config : TargetConfig pkg.name name) : Except CliError BuildSpec := + if !facet.isAnonymous then + throw <| CliError.invalidFacet name facet + else do + let info := pkg.target name + have h : BuildData info.key = CustomData (pkg.name, name) := rfl + return {info, getBuildJob := h ▸ config.getJob} + +def resolveTargetInPackage (ws : Workspace) +(pkg : Package) (target facet : Name) : Except CliError (Array BuildSpec) := + if let some config := pkg.findTargetConfig? target then + Array.singleton <$> resolveCustomTarget pkg target facet config + else if let some exe := pkg.findLeanExe? target then + Array.singleton <$> resolveExeTarget exe facet + else if let some lib := pkg.findExternLib? target then + Array.singleton <$> resolveExternLibTarget lib facet + else if let some lib := pkg.findLeanLib? target then + resolveLibTarget ws lib facet + else if let some mod := pkg.findModule? target then + Array.singleton <$> resolveModuleTarget ws mod facet + else + throw <| CliError.missingTarget pkg.name (target.toString false) + +def resolveDefaultPackageTarget (ws : Workspace) (pkg : Package) : Except CliError (Array BuildSpec) := + pkg.defaultTargets.concatMapM (resolveTargetInPackage ws pkg · .anonymous) + +def resolvePackageTarget (ws : Workspace) (pkg : Package) (facet : Name) : Except CliError (Array BuildSpec) := + if facet.isAnonymous then + resolveDefaultPackageTarget ws pkg + else if let some config := ws.findPackageFacetConfig? facet then do + Array.singleton <$> mkConfigBuildSpec "package" (pkg.facet facet) config rfl + else + throw <| CliError.unknownFacet "package" facet + +def resolveTargetInWorkspace (ws : Workspace) +(target : Name) (facet : Name) : Except CliError (Array BuildSpec) := + if let some ⟨pkg, config⟩ := ws.findTargetConfig? target then + Array.singleton <$> resolveCustomTarget pkg target facet config + else if let some exe := ws.findLeanExe? target then + Array.singleton <$> resolveExeTarget exe facet + else if let some lib := ws.findExternLib? target then + Array.singleton <$> resolveExternLibTarget lib facet + else if let some lib := ws.findLeanLib? target then + resolveLibTarget ws lib facet + else if let some pkg := ws.findPackage? target then + resolvePackageTarget ws pkg facet + else if let some mod := ws.findModule? target then + Array.singleton <$> resolveModuleTarget ws mod facet + else + throw <| CliError.unknownTarget target + +def resolveTargetBaseSpec +(ws : Workspace) (spec : String) (facet : Name) : Except CliError (Array BuildSpec) := do + match spec.splitOn "/" with + | [spec] => + if spec.isEmpty then + resolvePackageTarget ws ws.root facet + else if spec.startsWith "@" then + let pkg ← parsePackageSpec ws <| spec.drop 1 + resolvePackageTarget ws pkg facet + else if spec.startsWith "+" then + let mod := spec.drop 1 |>.toName + if let some mod := ws.findModule? mod then + Array.singleton <$> resolveModuleTarget ws mod facet + else + throw <| CliError.unknownModule mod + else + resolveTargetInWorkspace ws (stringToLegalOrSimpleName spec) facet + | [pkgSpec, targetSpec] => + let pkgSpec := if pkgSpec.startsWith "@" then pkgSpec.drop 1 else pkgSpec + let pkg ← parsePackageSpec ws pkgSpec + if targetSpec.isEmpty then + resolvePackageTarget ws pkg facet + else if targetSpec.startsWith "+" then + let mod := targetSpec.drop 1 |>.toName + if let some mod := pkg.findModule? mod then + Array.singleton <$> resolveModuleTarget ws mod facet + else + throw <| CliError.unknownModule mod + else + resolveTargetInPackage ws pkg targetSpec facet + | _ => + throw <| CliError.invalidTargetSpec spec '/' + +def parseTargetSpec (ws : Workspace) (spec : String) : Except CliError (Array BuildSpec) := do + match spec.splitOn ":" with + | [spec] => + resolveTargetBaseSpec ws spec .anonymous + | [rootSpec, facet] => + resolveTargetBaseSpec ws rootSpec facet.toName + | _ => + throw <| CliError.invalidTargetSpec spec ':' + +def parseTargetSpecs (ws : Workspace) (specs : List String) : Except CliError (Array BuildSpec) := do + let mut results := #[] + for spec in specs do + results := results ++ (← parseTargetSpec ws spec) + if results.isEmpty then + results ← resolveDefaultPackageTarget ws ws.root + return results diff --git a/src/lake/Lake/CLI/Error.lean b/src/lake/Lake/CLI/Error.lean new file mode 100644 index 0000000000..c4d1ed614b --- /dev/null +++ b/src/lake/Lake/CLI/Error.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ + +namespace Lake +open Lean (Name) + +inductive CliError +/- CLI Errors -/ +| missingCommand +| unknownCommand (cmd : String) +| missingArg (arg : String) +| missingOptArg (opt arg : String) +| unknownShortOption (opt : Char) +| unknownLongOption (opt : String) +| unexpectedArguments (args : List String) +/- Init CLI Errors -/ +| unknownTemplate (spec : String) +/- Build CLI Errors -/ +| unknownModule (mod : Name) +| unknownPackage (spec : String) +| unknownFacet (type : String) (facet : Name) +| unknownTarget (target : Name) +| missingModule (pkg : Name) (mod : Name) +| missingTarget (pkg : Name) (spec : String) +| nonCliTarget (target : Name) +| nonCliFacet (type : String) (facet : Name) +| invalidTargetSpec (spec : String) (tooMany : Char) +| invalidFacet (target : Name) (facet : Name) +/- Script CLI Error -/ +| unknownScript (script : String) +| missingScriptDoc (script : String) +| invalidScriptSpec (spec : String) +/- Config Errors -/ +| unknownLeanInstall +| unknownLakeInstall +| leanRevMismatch (expected actual : String) +deriving Inhabited, Repr + +namespace CliError + +def toString : CliError → String +| missingCommand => "missing command" +| unknownCommand cmd => s!"unknown command '{cmd}'" +| missingArg arg => s!"missing {arg}" +| missingOptArg opt arg => s!"missing {arg} after {opt}" +| unknownShortOption opt => s!"unknown short option '-{opt}'" +| unknownLongOption opt => s!"unknown long option '{opt}'" +| unexpectedArguments as => s!"unexpected arguments: {" ".intercalate as}" +| unknownTemplate spec => s!"unknown package template `{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}`" +| unknownTarget t => s!"unknown target `{t.toString false}`" +| missingModule pkg mod => s!"package '{pkg.toString false}' has no module '{mod.toString false}'" +| missingTarget pkg spec => s!"package '{pkg.toString false}' has no target '{spec}'" +| nonCliTarget t => s!"target `{t.toString false}` is not a buildable via `lake`" +| nonCliFacet t f => s!"{t} facet `{f.toString false}` is not a buildable via `lake`" +| invalidTargetSpec s c => s!"invalid script spec '{s}' (too many '{c}')" +| invalidFacet t f => s!"invalid facet `{f.toString false}`; target {t.toString false} has no facets" +| unknownScript s => s!"unknown script {s}" +| missingScriptDoc s => s!"no documentation provided for `{s}`" +| invalidScriptSpec s => s!"invalid script spec '{s}' (too many '/')" +| 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}" + +instance : ToString CliError := ⟨toString⟩ diff --git a/src/lake/Lake/CLI/Help.lean b/src/lake/Lake/CLI/Help.lean new file mode 100644 index 0000000000..0955b69bef --- /dev/null +++ b/src/lake/Lake/CLI/Help.lean @@ -0,0 +1,242 @@ +/- +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 Lake.Version + +namespace Lake + +def usage := +uiVersionString ++ " + +USAGE: + lake [OPTIONS] + +OPTIONS: + --version print version and exit + --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 + --old only rebuild modified modules (ignore transitive deps) + --update, -U update manifest before building + +COMMANDS: + new [] create a Lean package in a new directory + init [] create a Lean package in the current directory + build [...] build targets + update update dependencies + upload upload build artifacts to a GitHub release + clean remove build outputs + script manage and run workspace scripts + scripts shorthand for `lake script list` + run