chore: add further comments in #7291 (#7317)

Just recording an explanation from the review of #7291 into the source code.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Cache/IO.lean

@@ -245,7 +245,8 @@ Each build file also has a `Bool` indicating whether that file is required for c
 def mkBuildPaths (path : FilePath) : IO $ List (FilePath × Bool) := do
   let packageDir ← getPackageDir path
   return [
-    (packageDir / LIBDIR / path.withExtension "trace", true), -- this one has to be first
+    -- Note that `packCache` below requires that the `.trace` file is first in this list.
+    (packageDir / LIBDIR / path.withExtension "trace", true),
     (packageDir / LIBDIR / path.withExtension "olean", true),
     (packageDir / LIBDIR / path.withExtension "olean.hash", true),
     (packageDir / LIBDIR / path.withExtension "ilean", true),
@@ -274,6 +275,8 @@ def packCache (hashMap : HashMap) (overwrite : Bool) (comment : Option String :=
     if ← allExist buildPaths then
       if overwrite || !(← zipPath.pathExists) then
         tasks := tasks.push <| ← IO.asTask do
+          -- Note here we require that the `.trace` file is first
+          -- in the list generated by `mkBuildPaths`.
           let trace :: args := (← buildPaths.filterM (·.1.pathExists)) |>.map (·.1.toString)
             | unreachable!
           runCmd (← getLeanTar) $ #[zipPath.toString, trace] ++