fix: lake: correct exe perms on restore (#14240)

This PR ensures executables are executable when restored from the Lake
cache even if they were not originally executable in the cache (e.g.,
because they were downloaded through `lake cache get`).

This is does not correct permissions for executables obtained from the
cache without restoring them. However, building executables in the
standard way (e.g., via `lean_exe` / `buildLeanExe`) should always
restore them.

Author: tydeu

src/lake/Lake/Build/Common.lean

@@ -657,6 +657,11 @@ public def restoreArtifact (file : FilePath) (art : Artifact) (exe := false) : L
       -- writing to such paths as this can corrupt the cache if the file was hard linked instead
       let r := {read := true, write := false, execution := exe}
       IO.setAccessRights file ⟨r, r, r⟩
+    else if exe then
+      -- Ensure restored executables are executable
+      -- They may not have been if acquired through `lake cache get`
+      let r := {read := true, write := false, execution := exe}
+      IO.setAccessRights file ⟨r, r, r⟩
     logVerbose s!"restored artifact from cache to: {file}"
     writeFileHash file art.hash
   return art.useLocalFile file

tests/lake/tests/cache/test.sh

@@ -329,6 +329,13 @@ test_restored +Module:olean.server Module.olean.server
 test_restored +Module:olean.private Module.olean.private
 test_restored +Module:ir Module.ir
 
+# Verify that a hard linked restored executable is given the right
+# permissions to run even if the cached artifact lacked them (e.g.,
+# because it came from `lake cache get`)
+test_cmd chmod 444 $CACHE_DIR/artifacts/*
+test_cmd rm -rf .lake/build/bin
+test_run exe test
+
 # Verify that invalid outputs do not break Lake
 if command -v jq > /dev/null; then # skip if no jq found
   libPath=$($LAKE query Test:static)