chore: minor review-related touchups

Author: tydeu

src/LeanIR.lean

@@ -91,8 +91,6 @@ public def main (args : List String) : IO UInt32 := do
     -- level exported because otherwise we would try to load the current module's `.ir`
     finalizeImport (leakEnv := true) (loadExts := false) (level := .exported) (loadIRSig := true) s imports opts
   let env := env.setMainModule modName
-  -- As the environment imports the module to compile, it does not inherit its package.
-  -- Take it from the setup.
   let env := env.setModulePackage setup.package?
 
   let initExt {α β σ} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) : IO Environment := do

src/lake/Lake/Build/Common.lean

@@ -387,6 +387,19 @@ public def cacheFileHash (file : FilePath) (text := false) : IO Unit := do
   let hash ← computeFileHash file text
   writeFileHash file hash
 
+/--
+If `file` exists, computes its hash and saves it to a `.hash` file.
+
+If `text := true`, `file` is hashed as a text file rather than a binary file.
+-/
+public def cacheFileHashIfExists (file : FilePath) (text := false) : IO Unit := do
+  try
+    let hash ← computeFileHash file text
+    writeFileHash file hash
+  catch
+    | .noFileOrDirectory .. => pure ()
+    | e => throw e
+
 /-- Remove the cached hash of a file (its `.hash` file) if it exists. -/
 public def clearFileHash (file : FilePath) : IO Unit := do
   removeFileIfExists <| file.toString ++ ".hash"

src/lake/Lake/Build/Module.lean

@@ -768,22 +768,20 @@ public def Module.clearOutputHashes (mod : Module) : IO PUnit := do
 
 /-- Cache the file hashes of the module build outputs in `.hash` files. -/
 public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
-  if (← mod.ltarFile.pathExists) then
-    cacheFileHash mod.ltarFile
-  cacheFileHash mod.oleanFile
-  if (← mod.oleanServerFile.pathExists) then
-    cacheFileHash mod.oleanServerFile
-  if (← mod.oleanPrivateFile.pathExists)  then
-    cacheFileHash mod.oleanPrivateFile
-  cacheFileHash mod.ileanFile
-  if (← mod.irSigFile.pathExists) then
-    cacheFileHash mod.irSigFile
-  if (← mod.irFile.pathExists)  then
-    cacheFileHash mod.irFile
-  if (← mod.cFile.pathExists) then
-    cacheFileHash mod.cFile
-  if Lean.Internal.hasLLVMBackend () then
-    cacheFileHash mod.bcFile
+  -- Hashes on not conditional on module metadata (e.g., `isModule`).
+  -- Lake will determine which files to use (and which to delete) as part of the build proccess.
+  try
+    cacheFileHashIfExists mod.ltarFile
+    cacheFileHashIfExists mod.oleanFile
+    cacheFileHashIfExists mod.oleanServerFile
+    cacheFileHashIfExists mod.oleanPrivateFile
+    cacheFileHashIfExists mod.ileanFile
+    cacheFileHashIfExists mod.irSigFile
+    cacheFileHashIfExists mod.irFile
+    cacheFileHashIfExists mod.cFile
+    cacheFileHashIfExists mod.bcFile
+  catch e =>
+    error s!"failed to save output hashes: {e}"
 
 def ModuleOutputDescrs.resolve
   (descrs : ModuleOutputDescrs) (service? : Option CacheServiceName) (scope? : Option CacheServiceScope)