From c3ff4334cdc63c9e771a10dd5a288f02ce5090e2 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sun, 6 Apr 2025 13:41:08 -0400 Subject: [PATCH] fix: lake: library load & link order (#7809) This PR fixes the order of libraries when loading them via `--load-dynlib` or `--plugin` in `lean` and when linking them into a shared library or executable. A `Dynlib` now tracks its dependencies and they are topologically sorted before being passed to either linking or loading. Closes #7790. --- src/lake/Lake/Build/Common.lean | 41 +++++- src/lake/Lake/Build/Fetch.lean | 2 +- src/lake/Lake/Build/Imports.lean | 10 +- src/lake/Lake/Build/Library.lean | 37 ++--- src/lake/Lake/Build/Module.lean | 137 ++++++++---------- src/lake/Lake/Build/Target/Basic.lean | 2 +- src/lake/Lake/Config/Dynlib.lean | 6 + src/lake/Lake/Load/Resolve.lean | 2 +- src/lake/Lake/Util/Cycle.lean | 4 + src/lake/tests/badImport/test.sh | 36 +---- src/lake/tests/buildArgs/test.sh | 32 +--- src/lake/tests/common.sh | 65 +++++++++ src/lake/tests/precompileArgs/clean.sh | 1 - src/lake/tests/precompileArgs/test.sh | 29 ---- .../Foo.lean | 1 + .../Foo/Bar.lean | 0 src/lake/tests/precompileLink/Foo/Baz.lean | 3 + src/lake/tests/precompileLink/FooDep.lean | 3 + src/lake/tests/precompileLink/FooDepDep.lean | 1 + src/lake/tests/precompileLink/clean.sh | 1 + .../lakefile.lean | 4 + src/lake/tests/precompileLink/orderTest.lean | 7 + src/lake/tests/precompileLink/test.sh | 25 ++++ src/shell/CMakeLists.txt | 3 +- 24 files changed, 246 insertions(+), 206 deletions(-) create mode 100644 src/lake/tests/common.sh delete mode 100755 src/lake/tests/precompileArgs/clean.sh delete mode 100755 src/lake/tests/precompileArgs/test.sh rename src/lake/tests/{precompileArgs => precompileLink}/Foo.lean (50%) rename src/lake/tests/{precompileArgs => precompileLink}/Foo/Bar.lean (100%) create mode 100644 src/lake/tests/precompileLink/Foo/Baz.lean create mode 100644 src/lake/tests/precompileLink/FooDep.lean create mode 100644 src/lake/tests/precompileLink/FooDepDep.lean create mode 100755 src/lake/tests/precompileLink/clean.sh rename src/lake/tests/{precompileArgs => precompileLink}/lakefile.lean (84%) create mode 100644 src/lake/tests/precompileLink/orderTest.lean create mode 100755 src/lake/tests/precompileLink/test.sh diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index 66087354b2..34f0bd840b 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -209,14 +209,14 @@ def fetchFileTrace (file : FilePath) (text := false) : JobM BuildTrace := do /-- Builds `file` using `build` unless it already exists and the current job's -trace matches the trace stored in the `.trace` file. If built, save the new -trace and cache `file`'s hash in a `.hash` file. Otherwise, try to fetch the +trace matches the trace stored in the `.trace` file. If built, saves the new +trace and caches `file`'s hash in a `.hash` file. Otherwise, tries to fetch the hash from the `.hash` file using `fetchFileTrace`. Build logs (if any) are saved to the trace file and replayed from there if the build is skipped. For example, given `file := "foo.c"`, compares `getTrace` with that in -`foo.c.trace` with the hash cached in `foo.c.hash` and the log cached in -`foo.c.trace`. +`foo.c.trace`. If built, the hash is cached in `foo.c.hash` and the new +trace is saved to `foo.c.trace` (including the build log). If `text := true`, `file` is hashed as a text file rather than a binary file. -/ @@ -395,6 +395,29 @@ private def mkLinkObjArgs args := args.push s!"-l{lib.name}" return args +/-- +Topologically sorts the library dependency tree by name. +Libraries come *before* their dependencies. +-/ +private partial def mkLinkOrder (libs : Array Dynlib) : JobM (Array Dynlib) := do + let r := libs.foldlM (m := Except (Cycle String)) (init := ({}, #[])) fun (v, o) lib => + go lib [] v o + match r with + | .ok (_, order) => pure order + | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}" +where + go lib (ps : List String) (v : RBMap String Unit compare) (o : Array Dynlib) := do + let o := o.push lib + if v.contains lib.name then + return (v, o) + if ps.contains lib.name then + throw (lib.name :: ps) + let ps := lib.name :: ps + let v := v.insert lib.name () + let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib => + go lib ps v o + return (v, o) + /-- Build a shared library by linking the results of `linkJobs` using the Lean toolchain's C compiler. @@ -404,7 +427,7 @@ def buildSharedLib (linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib)) (weakArgs traceArgs : Array String := #[]) (linker := "c++") (extraDepTrace : JobM _ := pure BuildTrace.nil) - (plugin := false) + (plugin := false) (linkDeps := Platform.isWindows) : SpawnM (Job Dynlib) := (Job.collectArray linkObjs).bindM fun objs => do (Job.collectArray linkLibs).mapM (sync := true) fun libs => do @@ -412,9 +435,10 @@ def buildSharedLib addPlatformTrace -- shared libraries are platform-dependent artifacts addTrace (← extraDepTrace) buildFileUnlessUpToDate' libFile do + let libs ← if linkDeps then mkLinkOrder libs else pure #[] let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs compileSharedLib libFile args linker - return {name := libName, path := libFile, plugin} + return {name := libName, path := libFile, deps := libs, plugin} /-- Build a shared library by linking the results of `linkJobs` @@ -424,6 +448,7 @@ def buildLeanSharedLib (libName : String) (libFile : FilePath) (linkObjs : Array (Job FilePath)) (linkLibs : Array (Job Dynlib)) (weakArgs traceArgs : Array String := #[]) (plugin := false) + (linkDeps := Platform.isWindows) : SpawnM (Job Dynlib) := (Job.collectArray linkObjs).bindM fun objs => do (Job.collectArray linkLibs).mapM (sync := true) fun libs => do @@ -432,10 +457,11 @@ def buildLeanSharedLib addPlatformTrace -- shared libraries are platform-dependent artifacts buildFileUnlessUpToDate' libFile do let lean ← getLeanInstall + let libs ← if linkDeps then mkLinkOrder libs else pure #[] let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags compileSharedLib libFile args lean.cc - return {name := libName, path := libFile, plugin} + return {name := libName, path := libFile, deps := libs, plugin} /-- Build an executable by linking the results of `linkJobs` @@ -453,6 +479,7 @@ def buildLeanExe addPlatformTrace -- executables are platform-dependent artifacts buildFileUnlessUpToDate' exeFile do let lean ← getLeanInstall + let libs ← mkLinkOrder libs let args := mkLinkObjArgs objs libs ++ weakArgs ++ traceArgs ++ lean.ccLinkFlags sharedLean compileExe exeFile args lean.cc diff --git a/src/lake/Lake/Build/Fetch.lean b/src/lake/Lake/Build/Fetch.lean index fd1f89231e..3e80314c86 100644 --- a/src/lake/Lake/Build/Fetch.lean +++ b/src/lake/Lake/Build/Fetch.lean @@ -36,7 +36,7 @@ abbrev RecBuildT (m : Type → Type) := /-- Log build cycle and error. -/ @[specialize] def buildCycleError [MonadError m] (cycle : Cycle BuildKey) : m α := - error s!"build cycle detected:\n{"\n".intercalate <| cycle.map (s!" {·}")}" + error s!"build cycle detected:\n{formatCycle cycle}" instance [Monad m] [MonadError m] : MonadCycleOf BuildKey (RecBuildT m) where throwCycle := buildCycleError diff --git a/src/lake/Lake/Build/Imports.lean b/src/lake/Lake/Build/Imports.lean index feb1b3ae92..9df1c63ada 100644 --- a/src/lake/Lake/Build/Imports.lean +++ b/src/lake/Lake/Build/Imports.lean @@ -37,8 +37,8 @@ def buildImportsAndDeps let dynlibsJob ← root.dynlibs.fetchIn root let pluginsJob ← root.plugins.fetchIn root modJob.bindM fun _ => - impLibsJob.bindM fun impLibs => - dynlibsJob.bindM fun dynlibs => - pluginsJob.bindM fun plugins => - externLibsJob.mapM fun externLibs => do - return computeModuleDeps impLibs externLibs dynlibs plugins + impLibsJob.bindM (sync := true) fun impLibs => + dynlibsJob.bindM (sync := true) fun dynlibs => + pluginsJob.bindM (sync := true) fun plugins => + externLibsJob.mapM (sync := true) fun externLibs => do + computeModuleDeps impLibs externLibs dynlibs plugins diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean index b6c5cee547..9dab0a45e0 100644 --- a/src/lake/Lake/Build/Library.lean +++ b/src/lake/Lake/Build/Library.lean @@ -96,27 +96,22 @@ protected def LeanLib.recBuildShared (self : LeanLib) : FetchM (Job Dynlib) := d let objJobs ← self.moreLinkObjs.foldlM (init := objJobs) (·.push <$> ·.fetchIn self.pkg) let libJobs ← id do - -- Fetch dependnecy dynlibs - -- for platforms that must link to them (e.g., Windows) - if Platform.isWindows then - let imps ← mods.foldlM (init := OrdModuleSet.empty) fun imps mod => do - return imps.appendArray (← (← mod.transImports.fetch).await) - let s := (NameSet.empty.insert self.name, #[]) - let (_, jobs) ← imps.foldlM (init := s) fun (libs, jobs) imp => do - if libs.contains imp.lib.name then - return (libs, jobs) - else - let job ← imp.lib.shared.fetch - let moreJobs ← imp.lib.moreLinkLibs.mapM (·.fetchIn self.pkg) - let jobs := jobs.push job ++ moreJobs - return (libs.insert imp.lib.name, jobs) - let jobs ← self.moreLinkLibs.foldlM - (·.push <$> ·.fetchIn self.pkg) jobs - let jobs ← self.pkg.externLibs.foldlM - (·.push <$> ·.dynlib.fetch) jobs - return jobs - else - return #[] + -- Fetch dependency dynlibs + -- for situations that need them (see `Dynlib.deps`) + let imps ← mods.foldlM (init := OrdModuleSet.empty) fun imps mod => do + return imps.appendArray (← (← mod.transImports.fetch).await) + let s := (NameSet.empty.insert self.name, #[]) + let (_, jobs) ← imps.foldlM (init := s) fun (libs, jobs) imp => do + if libs.contains imp.lib.name then + return (libs, jobs) + else + let jobs ← jobs.push <$> imp.lib.shared.fetch + return (libs.insert imp.lib.name, jobs) + let jobs ← self.moreLinkLibs.foldlM + (·.push <$> ·.fetchIn self.pkg) jobs + let jobs ← self.pkg.externLibs.foldlM + (·.push <$> ·.dynlib.fetch) jobs + return jobs buildLeanSharedLib self.libName self.sharedLibFile objJobs libJobs self.weakLinkArgs self.linkArgs (plugin := self.roots.size == 1) diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index d51d0b76a9..6b9dde3072 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -106,54 +106,70 @@ def fetchExternLibs (pkgs : Array Package) : FetchM (Job (Array Dynlib)) := Job.collectArray <$> pkgs.flatMapM (·.externLibs.mapM (·.dynlib.fetch)) private def Module.fetchImportLibsCore - (self : Module) (imps : Array Module) - (init : NameSet × Array (Job Dynlib)): FetchM (NameSet × Array (Job Dynlib)) -:= imps.foldlM (init := init) fun (libs, jobs) imp => do - if libs.contains imp.lib.name then - return (libs, jobs) - else if self.lib.name = imp.lib.name then - let job ← imp.dynlib.fetch - return (libs, jobs.push job) - else - - let jobs ← imp.lib.moreLinkLibs.foldlM (init := jobs) - (·.push <$> ·.fetchIn imp.pkg) - -- Lean wants the external library symbols before module symbols. - let jobs ← jobs.push <$> imp.lib.shared.fetch - return (libs.insert imp.lib.name, jobs) - + (self : Module) (imps : Array Module) (compileSelf : Bool) + (init : NameSet × Array (Job Dynlib)) +: FetchM (NameSet × Array (Job Dynlib)) := + imps.foldlM (init := init) fun (libs, jobs) imp => do + if libs.contains imp.lib.name then + return (libs, jobs) + else if compileSelf && self.lib.name = imp.lib.name then + let job ← imp.dynlib.fetch + return (libs, jobs.push job) + else if compileSelf || imp.shouldPrecompile then + let jobs ← jobs.push <$> imp.lib.shared.fetch + return (libs.insert imp.lib.name, jobs) + else + return (libs, jobs) /-- Computes the transitive dynamic libraries of a module's imports. Modules from the same library are loaded individually, while modules from other libraries are loaded as part of the whole library. -/ @[inline] private def Module.fetchImportLibs - (self : Module) (imps : Array Module) : FetchM (Job (Array Dynlib)) -:= do - let s ← self.fetchImportLibsCore imps ({}, #[]) - return Job.collectArray s.2 + (self : Module) (imps : Array Module) (compileSelf : Bool) +: FetchM (Array (Job Dynlib)) := + (·.2) <$> self.fetchImportLibsCore imps compileSelf ({}, #[]) /-- Fetch the dynlibs of a list of imports. **For internal use.** -/ @[inline] def fetchImportLibs (mods : Array Module) : FetchM (Job (Array Dynlib)) := do let (_, jobs) ← mods.foldlM (init := ({}, #[])) fun s mod => do - let precompileImports ← - if mod.shouldPrecompile - then mod.transImports.fetch - else mod.precompileImports.fetch - let precompileImports ← precompileImports.await - mod.fetchImportLibsCore precompileImports s + let imports ← (← mod.imports.fetch).await + mod.fetchImportLibsCore imports mod.shouldPrecompile s let jobs ← mods.foldlM (init := jobs) fun jobs mod => do - if mod.shouldPrecompile - then jobs.push <$> mod.dynlib.fetch + if mod.shouldPrecompile then + jobs.push <$> mod.dynlib.fetch else return jobs return Job.collectArray jobs +/-- +Topologically sorts the library dependency tree by name. +Libraries come *after* their dependencies. +-/ +private partial def mkLoadOrder (libs : Array Dynlib) : FetchM (Array Dynlib) := do + let r := libs.foldlM (m := Except (Cycle String)) (init := ({}, #[])) fun (v, o) lib => + go lib [] v o + match r with + | .ok (_, order) => pure order + | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}" +where + go lib (ps : List String) (v : RBMap String Unit compare) (o : Array Dynlib) := do + if v.contains lib.name then + return (v, o) + if ps.contains lib.name then + throw (lib.name :: ps) + let ps := lib.name :: ps + let v := v.insert lib.name () + let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib => + go lib ps v o + let o := o.push lib + return (v, o) + def computeModuleDeps (impLibs : Array Dynlib) (externLibs : Array Dynlib) (dynlibs : Array Dynlib) (plugins : Array Dynlib) -: ModuleDeps := Id.run do +: FetchM ModuleDeps := do /- Requirements: * Lean wants the external library symbols before module symbols. @@ -162,8 +178,9 @@ def computeModuleDeps Everything else loads fine with just the augmented library path. * Linux needs the augmented path to resolve nested dependencies in dynlibs. -/ - let mut plugins := plugins + let impLibs ← mkLoadOrder impLibs let mut dynlibs := externLibs ++ dynlibs + let mut plugins := plugins for impLib in impLibs do if impLib.plugin then plugins := plugins.push impLib @@ -190,20 +207,17 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do if imp.name = mod.name then logError s!"{mod.leanFile}: module imports itself" imp.olean.fetch - let precompileImports ← if mod.shouldPrecompile then - mod.transImports.fetch else mod.precompileImports.fetch - let precompileImports ← precompileImports.await - let importLibsJob ← mod.fetchImportLibs precompileImports - let pkgs := precompileImports.foldl (·.insert ·.pkg) OrdPackageSet.empty - let pkgs := if mod.shouldPrecompile then pkgs.insert mod.pkg else pkgs - let externLibsJob ← fetchExternLibs pkgs.toArray + let impLibsJob ← Job.collectArray <$> + mod.fetchImportLibs directImports mod.shouldPrecompile + let externLibsJob ← Job.collectArray <$> + mod.pkg.externLibs.mapM (·.dynlib.fetch) let dynlibsJob ← mod.dynlibs.fetchIn mod.pkg let pluginsJob ← mod.plugins.fetchIn mod.pkg extraDepJob.bindM fun _ => do importJob.bindM (sync := true) fun _ => do let depTrace ← takeTrace - importLibsJob.bindM (sync := true) fun impLibs => do + impLibsJob.bindM (sync := true) fun impLibs => do externLibsJob.bindM (sync := true) fun externLibs => do dynlibsJob.bindM (sync := true) fun dynlibs => do pluginsJob.mapM (sync := true) fun plugins => do @@ -211,7 +225,7 @@ def Module.recBuildDeps (mod : Module) : FetchM (Job ModuleDeps) := ensureJob do | none => addTrace depTrace | some false => addTrace depTrace; addPlatformTrace | some true => setTrace depTrace - return computeModuleDeps impLibs externLibs dynlibs plugins + computeModuleDeps impLibs externLibs dynlibs plugins /-- The `ModuleFacetConfig` for the builtin `depsFacet`. -/ def Module.depsFacetConfig : ModuleFacetConfig depsFacet := @@ -366,44 +380,21 @@ def Module.oFacetConfig : ModuleFacetConfig oFacet := Recursively build the shared library of a module (e.g., for `--load-dynlib` or `--plugin`). -/ --- TODO: Return `Job OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`? def Module.recBuildDynlib (mod : Module) : FetchM (Job Dynlib) := withRegisterJob s!"{mod.name}:dynlib" do - -- Fetch object files - let modLinkJobs ← mod.nativeFacets true |>.mapM (·.fetch mod) - let modLinksJob := Job.collectArray modLinkJobs - - -- Build dynlib - let buildDynlib (moreLibs : Array Dynlib) := - modLinksJob.mapM fun modLinks => do - addLeanTrace - addPlatformTrace -- shared libraries are platform-dependent artifacts - addPureTrace mod.linkArgs - buildFileUnlessUpToDate' mod.dynlibFile do - let lean ← getLeanInstall - let args := - modLinks.map toString ++ - moreLibs.map (·.path.toString) ++ - mod.weakLinkArgs ++ mod.linkArgs ++ lean.ccLinkSharedFlags - compileSharedLib mod.dynlibFile args lean.cc - return ⟨mod.dynlibFile, mod.dynlibName, true⟩ - + let objJobs ← (mod.nativeFacets true).mapM (·.fetch mod) -- Fetch dependencies' dynlibs - -- for platforms that must link to them (e.g., Windows) - if Platform.isWindows then - let imps ← (← mod.transImports.fetch).await - let impLibs ← mod.fetchImportLibs imps - let dynlibsJob ← (mod.dynlibs ++ mod.plugins).fetchIn mod.pkg - let pkgs := imps.foldl (·.insert ·.pkg) OrdPackageSet.empty - |>.insert mod.pkg |>.toArray - let externLibsJob ← fetchExternLibs pkgs - impLibs.bindM fun impLibs => - dynlibsJob.bindM (sync := true) fun dynlibs => - externLibsJob.bindM (sync := true) fun externLibs => - buildDynlib (impLibs ++ externLibs ++ dynlibs) - else - buildDynlib #[] + let libJobs ← id do + let imps ← (← mod.imports.fetch).await + let libJobs ← mod.fetchImportLibs imps true + let libJobs ← mod.lib.moreLinkLibs.foldlM + (·.push <$> ·.fetchIn mod.pkg) libJobs + let libJobs ← mod.pkg.externLibs.foldlM + (·.push <$> ·.dynlib.fetch) libJobs + return libJobs + buildLeanSharedLib mod.dynlibName mod.dynlibFile objJobs libJobs + mod.weakLinkArgs mod.linkArgs (plugin := true) /-- The `ModuleFacetConfig` for the builtin `dynlibFacet`. -/ def Module.dynlibFacetConfig : ModuleFacetConfig dynlibFacet := diff --git a/src/lake/Lake/Build/Target/Basic.lean b/src/lake/Lake/Build/Target/Basic.lean index bc5346f5ca..d7f51b92d2 100644 --- a/src/lake/Lake/Build/Target/Basic.lean +++ b/src/lake/Lake/Build/Target/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ prelude -import Lake.Build.Data +import Lake.Build.Key /-! # Lake Targets diff --git a/src/lake/Lake/Config/Dynlib.lean b/src/lake/Lake/Config/Dynlib.lean index 46b10ac83f..3c38479fc0 100644 --- a/src/lake/Lake/Config/Dynlib.lean +++ b/src/lake/Lake/Config/Dynlib.lean @@ -5,6 +5,7 @@ Authors: Mac Malone -/ prelude import Lake.Config.OutFormat +import Lake.Build.Target.Basic open System Lean @@ -18,6 +19,11 @@ structure Dynlib where name : String /-- Whether this library can be loaded as a plugin. -/ plugin := false + /-- + Transitive dependencies of this library for situations that need them + (e.g., linking on Windows, loading via `lean`). + -/ + deps : Array Dynlib := #[] deriving Inhabited, Repr /-- Optional library directory (for `-L`). -/ diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean index d636c112dc..ebc4e70075 100644 --- a/src/lake/Lake/Load/Resolve.lean +++ b/src/lake/Lake/Load/Resolve.lean @@ -81,7 +81,7 @@ abbrev DepStackT m := CallStackT Name m /-- Log dependency cycle and error. -/ @[specialize] def depCycleError [MonadError m] (cycle : Cycle Name) : m α := - error s!"dependency cycle detected:\n{"\n".intercalate <| cycle.map (s!" {·}")}" + error s!"dependency cycle detected:\n{formatCycle cycle}" instance [Monad m] [MonadError m] : MonadCycleOf Name (DepStackT m) where throwCycle := depCycleError diff --git a/src/lake/Lake/Util/Cycle.lean b/src/lake/Lake/Util/Cycle.lean index 9f30824418..1d457e8793 100644 --- a/src/lake/Lake/Util/Cycle.lean +++ b/src/lake/Lake/Util/Cycle.lean @@ -6,6 +6,7 @@ Authors: Mac Malone prelude import Init.Control.Except import Init.Data.List.Basic +import Init.Data.ToString namespace Lake @@ -15,6 +16,9 @@ abbrev CallStack κ := List κ /-- A `CallStack` ending in a cycle. -/ abbrev Cycle κ := CallStack κ +def formatCycle [ToString κ] (cycle : Cycle κ) : String := + "\n".intercalate <| cycle.map (s!" {·}") + /-- A monad equipped with a call stack. -/ class MonadCallStackOf (κ : semiOutParam (Type u)) (m : Type u → Type v) where getCallStack : m (CallStack κ) diff --git a/src/lake/tests/badImport/test.sh b/src/lake/tests/badImport/test.sh index a33a42310e..228608800a 100755 --- a/src/lake/tests/badImport/test.sh +++ b/src/lake/tests/badImport/test.sh @@ -1,9 +1,5 @@ #!/usr/bin/env bash -set -euo pipefail - -exit 0 # TODO: flaky test disabled - -LAKE=${LAKE:-../../.lake/build/bin/lake} +source ../common.sh ./clean.sh @@ -14,36 +10,6 @@ LAKE=${LAKE:-../../.lake/build/bin/lake} # https://github.com/leanprover/lean4/issues/3351 # https://github.com/leanprover/lean4/issues/3809 -test_run() { - echo "[Command]" - echo "$> lake" "$@" - if $LAKE "$@" >produced.out 2>&1; then - rc=$? - else - rc=$? - fi - echo "Lake exited with code $rc" - echo "[Output]" - cat produced.out - return $rc -} - -test_err() { - expected=$1; shift - if test_run "$@"; then rc=$?; else rc=$?; fi - echo "[Match \"$expected\"]" - if grep --color -F "$expected" produced.out; then - if [ $rc != 1 ]; then - echo "[Outcome]" - echo "Lake unexpectedly succeeded." - return 1 - fi - else - echo "No match found." - return 1 - fi -} - # Test a module with a bad import does not kill the whole build test_err "Building Etc" build Lib.U Etc # Test importing a missing module from outside the workspace diff --git a/src/lake/tests/buildArgs/test.sh b/src/lake/tests/buildArgs/test.sh index e2c6b349ad..7bb497bc0f 100755 --- a/src/lake/tests/buildArgs/test.sh +++ b/src/lake/tests/buildArgs/test.sh @@ -1,41 +1,11 @@ #!/usr/bin/env bash -set -euo pipefail - -exit 0 # TODO: flaky test disabled - -LAKE=${LAKE:-../../.lake/build/bin/lake} +source ../common.sh ./clean.sh # Test that changing `moreLean/Leanc/LinkArgs` triggers a rebuild # Test that changing `weakLean/Leanc/LinkArgs` does not -test_run() { - echo "[Command]" - echo "$> lake" "$@" - if $LAKE "$@" >produced.out 2>&1; then - rc=$? - else - rc=$? - fi - echo "Lake exited with code $rc" - echo "[Output]" - cat produced.out - return $rc -} - -test_out() { - expected=$1; shift - if test_run "$@"; then rc=$?; else rc=$?; fi - echo "[Match \"$expected\"]" - if grep --color -F "$expected" produced.out; then - return $rc - else - echo "No match found." - return 1 - fi -} - # Test `leanArgs` test_run build +Hello -R # see https://github.com/leanprover/lake/issues/50 diff --git a/src/lake/tests/common.sh b/src/lake/tests/common.sh new file mode 100644 index 0000000000..974c3eef0a --- /dev/null +++ b/src/lake/tests/common.sh @@ -0,0 +1,65 @@ +set -euo pipefail + +LAKE=${LAKE:-lake} + +if [ "${OS:-}" = Windows_NT ]; then +LIB_PREFIX= +SHARED_LIB_EXT=dll +elif [ "`uname`" = Darwin ]; then +LIB_PREFIX=lib +SHARED_LIB_EXT=dylib +else +LIB_PREFIX=lib +SHARED_LIB_EXT=so +fi + +test_run() { + echo "[COMMAND]" + echo "$> lake" "$@" + if $LAKE "$@" >produced.out 2>&1; then + rc=$? + else + rc=$? + fi + echo "Lake exited with code $rc" + echo "[OUTPUT]" + cat produced.out + return $rc +} + +match_out() { + expected=$1; shift + echo "[MATCH \"$expected\"]" + if grep --color -F -- "$expected" produced.out; then + return 0 + else + echo "No match found." + return 1 + fi +} + +test_out() { + expected=$1; shift + if test_run "$@"; then rc=$?; else rc=$?; fi + match_out "$expected" + return $rc +} + +test_err() { + expected=$1; shift + if test_run "$@"; then rc=$?; else rc=$?; fi + if match_out "$expected"; then + if [ $rc != 1 ]; then + echo "[OUTCOME]" + echo "Lake unexpectedly succeeded." + return 1 + fi + fi +} + +test_maybe_err() { + expected=$1; shift + test_run "$@" || true + match_out "$expected" +} + diff --git a/src/lake/tests/precompileArgs/clean.sh b/src/lake/tests/precompileArgs/clean.sh deleted file mode 100755 index b6e54c681e..0000000000 --- a/src/lake/tests/precompileArgs/clean.sh +++ /dev/null @@ -1 +0,0 @@ -rm -rf .lake lake-manifest.json diff --git a/src/lake/tests/precompileArgs/test.sh b/src/lake/tests/precompileArgs/test.sh deleted file mode 100755 index ae7280d220..0000000000 --- a/src/lake/tests/precompileArgs/test.sh +++ /dev/null @@ -1,29 +0,0 @@ -#!/usr/bin/env bash -set -exo pipefail - -LAKE=${LAKE:-../../.lake/build/bin/lake} - -if [ "$OS" = Windows_NT ]; then -LIB_PREFIX= -SHARED_LIB_EXT=dll -elif [ "`uname`" = Darwin ]; then -LIB_PREFIX=lib -SHARED_LIB_EXT=dylib -else -LIB_PREFIX=lib -SHARED_LIB_EXT=so -fi - -./clean.sh - -# Test that `moreLinkArgs` are included when linking precompiled modules -($LAKE build -KlinkArgs=-lBaz 2>&1 || true) | grep --color -- "-lBaz" - -# Test that dynlibs are part of the module trace unless `platformIndependent` is set -$LAKE build -R -echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT -($LAKE build 2>&1 --rehash && exit 1 || true) | grep --color "Building Foo" -rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT -$LAKE build -R -KplatformIndependent=true -echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT -$LAKE build --rehash --no-build diff --git a/src/lake/tests/precompileArgs/Foo.lean b/src/lake/tests/precompileLink/Foo.lean similarity index 50% rename from src/lake/tests/precompileArgs/Foo.lean rename to src/lake/tests/precompileLink/Foo.lean index e3cdd6def7..2885c88931 100644 --- a/src/lake/tests/precompileArgs/Foo.lean +++ b/src/lake/tests/precompileLink/Foo.lean @@ -1 +1,2 @@ import Foo.Bar +import Foo.Baz diff --git a/src/lake/tests/precompileArgs/Foo/Bar.lean b/src/lake/tests/precompileLink/Foo/Bar.lean similarity index 100% rename from src/lake/tests/precompileArgs/Foo/Bar.lean rename to src/lake/tests/precompileLink/Foo/Bar.lean diff --git a/src/lake/tests/precompileLink/Foo/Baz.lean b/src/lake/tests/precompileLink/Foo/Baz.lean new file mode 100644 index 0000000000..022ecda8c5 --- /dev/null +++ b/src/lake/tests/precompileLink/Foo/Baz.lean @@ -0,0 +1,3 @@ +import FooDep + +initialize greetingRef : IO.Ref String ← IO.mkRef greeting diff --git a/src/lake/tests/precompileLink/FooDep.lean b/src/lake/tests/precompileLink/FooDep.lean new file mode 100644 index 0000000000..2df7897fbd --- /dev/null +++ b/src/lake/tests/precompileLink/FooDep.lean @@ -0,0 +1,3 @@ +import FooDepDep + +def greeting := hello diff --git a/src/lake/tests/precompileLink/FooDepDep.lean b/src/lake/tests/precompileLink/FooDepDep.lean new file mode 100644 index 0000000000..7026689f8d --- /dev/null +++ b/src/lake/tests/precompileLink/FooDepDep.lean @@ -0,0 +1 @@ +def hello := "Hello" diff --git a/src/lake/tests/precompileLink/clean.sh b/src/lake/tests/precompileLink/clean.sh new file mode 100755 index 0000000000..333b50aba2 --- /dev/null +++ b/src/lake/tests/precompileLink/clean.sh @@ -0,0 +1 @@ +rm -rf .lake lake-manifest.json produced.out diff --git a/src/lake/tests/precompileArgs/lakefile.lean b/src/lake/tests/precompileLink/lakefile.lean similarity index 84% rename from src/lake/tests/precompileArgs/lakefile.lean rename to src/lake/tests/precompileLink/lakefile.lean index 4a63e8eb87..ef9d4a929b 100644 --- a/src/lake/tests/precompileArgs/lakefile.lean +++ b/src/lake/tests/precompileLink/lakefile.lean @@ -8,3 +8,7 @@ lean_lib Foo where precompileModules := true platformIndependent := if get_config? platformIndependent |>.isSome then true else none moreLinkArgs := if let some cfg := get_config? linkArgs then cfg.splitOn " " |>.toArray else #[] + +lean_lib FooDep +lean_lib FooDepDep +lean_exe orderTest diff --git a/src/lake/tests/precompileLink/orderTest.lean b/src/lake/tests/precompileLink/orderTest.lean new file mode 100644 index 0000000000..74f5dcbd41 --- /dev/null +++ b/src/lake/tests/precompileLink/orderTest.lean @@ -0,0 +1,7 @@ +-- import a module of lib `Foo` which does not import `FooDep` +import Foo.Bar +-- then, import a module which does +import Foo.Baz + +def main : IO Unit := do + IO.println (← greetingRef.get) diff --git a/src/lake/tests/precompileLink/test.sh b/src/lake/tests/precompileLink/test.sh new file mode 100755 index 0000000000..84df75a03d --- /dev/null +++ b/src/lake/tests/precompileLink/test.sh @@ -0,0 +1,25 @@ +#!/usr/bin/env bash +source ../common.sh + +./clean.sh + +# Test that the link & load order of precompiled libraries is correct +# https://github.com/leanprover/lean4/issues/7790 +test_run -v exe orderTest + +# Test that `moreLinkArgs` are included when linking precompiled modules +./clean.sh +test_maybe_err "-lBogus" build -KlinkArgs=-lBogus +./clean.sh + +# Test that dynlibs are part of the module trace unless `platformIndependent` is set +test_run build -R +echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT +test_err "Building Foo" build --rehash +rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT +test_run build -R -KplatformIndependent=true +echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT +test_run build --rehash --no-build + +# cleanup +rm -f produced.out diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index e07631be3e..40b770516b 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -185,11 +185,12 @@ ENDFOREACH(T) # bootstrap: too slow # toolchain: requires elan to download toolchain # online: downloads remote repositories +# badImport/buildArgs: flaky for unknown reasons file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/tests/test.sh" "${LEAN_SOURCE_DIR}/lake/examples/test.sh") FOREACH(T ${LEANLAKETESTS}) - if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*") + if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online|buildArgs|badImport).*") GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY) GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME) add_test(NAME "leanlaketest_${DIR_NAME}"