fix: errata and artifact cache

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

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

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}