diff --git a/lakefile.lean b/lakefile.lean index e9f229f9b..ec95979b7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -468,18 +468,17 @@ script run (args) do return 1 pure chosen -- Build every module in the selected libraries; their compiled `.olean` headers are authoritative - -- on which modules carry tests. + -- as to which modules include tests. let (modInfos, libMods) ← runBuild do - let mut oleanJobs := #[] - let mut infos : Array (Lean.Name × System.FilePath) := #[] + let mut oleanJobs : Array (Job (Lean.Name × System.FilePath)) := #[] let mut libMods : Array (Lake.LeanLib × Array Lean.Name) := #[] for lib in libs do let mods ← (← lib.modules.fetch).await libMods := libMods.push (lib, mods.map (·.name)) for m in mods do - oleanJobs := oleanJobs.push (← m.olean.fetch) - infos := infos.push (m.name, m.oleanFile) - pure <| (Job.collectArray oleanJobs).map (sync := true) fun _ => (infos, libMods) + -- The job's path locates the `.olean`, which is in Lake's artifact cache when that is enabled + oleanJobs := oleanJobs.push <| (← m.olean.fetch).map (sync := true) (m.name, ·) + pure <| (Job.collectArray oleanJobs).map (sync := true) fun infos => (infos, libMods) -- A test module is one whose `.olean` records a test. Module-system test modules go in the bridge -- module (`import all`); non-module ones can only be imported by the non-module main. let mut moduleMods : Array Lean.Name := #[] @@ -489,11 +488,11 @@ script run (args) do if info.hasTests then if info.isModule then moduleMods := moduleMods.push moduleName else nonModuleMods := nonModuleMods.push moduleName - -- A module that sits under a library's roots without being reachable from them is never built, so - -- any tests it defines are silently left out. A library is checked when it was named on the - -- command line, since naming it declares that its tests are expected, or when its built modules - -- carry tests. That is a configuration slip rather than a test failure, so it is a warning that - -- the runner reports alongside the results, and the run goes ahead. + -- A module that is unreachable from its library root without being transitively imported by said + -- roots is never built, so any tests it defines are silently left out. A library is checked when + -- it was named on the command line, since naming it declares that its tests are expected, or when + -- its built modules include tests. That is a configuration slip rather than a test failure, so it + -- is a warning that the runner reports alongside the results, and the run goes ahead. let testMods := moduleMods ++ nonModuleMods let mut unreachable : Array (Lake.LeanLib × Array Lean.Name) := #[] for (lib, mods) in libMods do @@ -529,8 +528,11 @@ script run (args) do if let some parent := file.parent then IO.FS.createDirAll parent let changed ← if ← file.pathExists then pure ((← IO.FS.readFile file) != src) else pure true if changed then IO.FS.writeFile file src - -- Build and run the root package's runner. - let exePath ← runBuild (ws.root.facet `errataRunner).fetch + -- Build and run the root package's runner. The generated modules are not part of one of the + -- workspaces's library targets, so Lake does not resolve them as imports. Instead, Lean finds + -- them in the build directory, where artifacts from Lake's cache are restored. + let exePath ← { ws with lakeEnv.restoreAllArtifacts? := some true }.runBuild + (ws.root.facet `errataRunner).fetch -- Each of the driver's warnings follows `--driver-warning`, which must match -- `Errata.driverWarningFlag`; the runner reports them alongside its own. let warningArgs := driverWarnings.flatMap (#["--driver-warning", ·]) @@ -631,24 +633,30 @@ module_facet literate mod : System.FilePath := do let exeJob ← «verso-literate».fetch let modJob ← mod.olean.fetch + let setupJob ← mod.setup.fetch let buildDir := ws.root.buildDir let litFile := mod.filePath (buildDir / "literate") "json" + -- The setup locates the module's imports, which are in Lake's artifact cache when that is enabled + let setupFile := mod.filePath (buildDir / "literate-setup") "json" let optArgs := leanOptionArgs mod exeJob.bindM fun exeFile => - modJob.mapM fun _oleanPath => do - addLeanTrace - addTrace (← computeTrace exeFile) - addPureTrace (toString optArgs) "leanOptions" - buildFileUnlessUpToDate' (text := true) litFile <| - proc { - cmd := exeFile.toString - args := #[mod.name.toString, litFile.toString] ++ optArgs - env := ← getAugmentedEnv - } - pure litFile + modJob.bindM fun _oleanPath => + setupJob.mapM fun setup => do + addLeanTrace + addTrace (← computeTrace exeFile) + addPureTrace (toString optArgs) "leanOptions" + buildFileUnlessUpToDate' (text := true) litFile do + IO.FS.createDirAll (setupFile.parent.getD buildDir) + IO.FS.writeFile setupFile (Lean.toJson setup).compress + proc { + cmd := exeFile.toString + args := #[mod.name.toString, litFile.toString, "--setup", setupFile.toString] ++ optArgs + env := ← getAugmentedEnv + } + pure litFile library_facet literate lib : Array System.FilePath := do let mods ← (← lib.modules.fetch).await diff --git a/src/verso-literate/VersoLiterateMain.lean b/src/verso-literate/VersoLiterateMain.lean index d5d3b7dcb..e8703040a 100644 --- a/src/verso-literate/VersoLiterateMain.lean +++ b/src/verso-literate/VersoLiterateMain.lean @@ -42,6 +42,9 @@ OPTS may be: --suppress-namespaces FILE Suppress the showing of the whitespace-delimited list of namespaces in FILE + + --setup FILE + Load imported modules from the artifacts listed in FILE, a Lake module setup " /-- @@ -623,8 +626,7 @@ private def collectItemImages (items : Array ModuleItem') : Array String := end ImageCollection - -unsafe def go (suppressedNamespaces : Array Name) (extraImports : Array Name) (mod : String) (leanOptions : Options) (out : IO.FS.Stream) : IO UInt32 := do +unsafe def go (suppressedNamespaces : Array Name) (extraImports : Array Name) (mod : String) (leanOptions : Options) (importArts : NameMap ImportArtifacts) (out : IO.FS.Stream) : IO UInt32 := do try initSearchPath (← findSysroot) let modName := mod.toName @@ -642,7 +644,7 @@ unsafe def go (suppressedNamespaces : Array Name) (extraImports : Array Name) (m let (headerStx, parserState, msgs) ← Parser.parseHeader ictx let imports := headerToImports headerStx enableInitializersExecution - let env ← Compat.importModules (extraImports.map ({module := ·}) ++ imports) {} + let env ← importModules (extraImports.map ({module := ·}) ++ imports) {} (loadExts := true) (arts := importArts) -- Rewrite `weak.` options based on the definitions discovered during imports let leanOptions ← Lean.Language.Lean.reparseOptions leanOptions let pctx : Frontend.Context := {inputCtx := ictx} @@ -699,6 +701,7 @@ structure Config where outFile : Option String := none extraImports : Array Name := #[] leanOptions : Options := {} + importArts : NameMap ImportArtifacts := {} /-- Parses a `-Dname=value` flag into a Lean option, registering it in `opts`. A registered option's @@ -756,6 +759,12 @@ where go { cfg with suppressedNamespaces := cfg.suppressedNamespaces ++ nss' } more else throw <| .userError "No namespace file given after --suppress-namespaces" + | "--setup" :: more => do + if let file :: more := more then + let setup ← ModuleSetup.load file + go { cfg with importArts := setup.importArts } more + else + throw <| .userError "No setup file given after --setup" | "--import" :: more => do if let mod :: more := more then go { cfg with extraImports := cfg.extraImports.push mod.toName } more @@ -779,16 +788,16 @@ where unsafe def main (args : List String) : IO UInt32 := do try - let {suppressedNamespaces, mod, outFile, extraImports, leanOptions} ← Config.fromArgs args + let {suppressedNamespaces, mod, outFile, extraImports, leanOptions, importArts} ← Config.fromArgs args if mod.isEmpty then throw <| .userError s!"No import module provided" match outFile with | none => - go suppressedNamespaces extraImports mod leanOptions (← IO.getStdout) + go suppressedNamespaces extraImports mod leanOptions importArts (← IO.getStdout) | some outFile => if let some p := (outFile : System.FilePath).parent then IO.FS.createDirAll p IO.FS.withFile outFile .write fun h => - go suppressedNamespaces extraImports mod leanOptions (.ofHandle h) + go suppressedNamespaces extraImports mod leanOptions importArts (.ofHandle h) catch e => IO.eprintln e IO.println helpText diff --git a/test-projects/literate-config/lake-manifest.json b/test-projects/literate-config/lake-manifest.json index ebbb42b0e..d9005af1e 100644 --- a/test-projects/literate-config/lake-manifest.json +++ b/test-projects/literate-config/lake-manifest.json @@ -1,78 +1,64 @@ -{ - "version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "2842b9871b04862f944c032e34052cb9448ccb71", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "68a463c484e24708627b8761e8730e76b295d1e2", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "e50948299c4dc4a4c21b1c34b6a6a4fddc19f912", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - } - ], - "name": "«literate-config-test»", - "lakeDir": ".lake", - "fixedToolchain": false -} +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "copy": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "«literate-config-test»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/test-projects/literate-multi-root/lake-manifest.json b/test-projects/literate-multi-root/lake-manifest.json index 76cee1b56..a22ce08ba 100644 --- a/test-projects/literate-multi-root/lake-manifest.json +++ b/test-projects/literate-multi-root/lake-manifest.json @@ -1,78 +1,64 @@ -{ - "version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "type": "path", - "scope": "", - "name": "verso", - "manifestFile": "lake-manifest.json", - "inherited": false, - "dir": "../..", - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "", - "rev": "2842b9871b04862f944c032e34052cb9448ccb71", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover/illuminate", - "type": "git", - "subDir": null, - "scope": "", - "rev": "68a463c484e24708627b8761e8730e76b295d1e2", - "name": "illuminate", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "", - "rev": "e50948299c4dc4a4c21b1c34b6a6a4fddc19f912", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover/subverso", - "type": "git", - "subDir": null, - "scope": "", - "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c", - "name": "subverso", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean" - } - ], - "name": "«literate-multi-root-test»", - "lakeDir": ".lake", - "fixedToolchain": false -} +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": + [{"type": "path", + "scope": "", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../..", + "copy": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "843844fa601dd56767b1eb22b7ada5b64d5e567a", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/illuminate", + "type": "git", + "subDir": null, + "scope": "", + "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f", + "name": "illuminate", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "fb13df72ecefd8ddbf9291021d7f33a8673eb57b", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso", + "type": "git", + "subDir": null, + "scope": "", + "rev": "acbaca235b6f905c2ae90c1be2aa62da7014178c", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}], + "name": "«literate-multi-root-test»", + "lakeDir": ".lake", + "fixedToolchain": false}