diff --git a/anneal/src/aeneas.rs b/anneal/src/aeneas.rs
index 834d31f3a9..5a33937f97 100644
--- a/anneal/src/aeneas.rs
+++ b/anneal/src/aeneas.rs
@@ -273,10 +273,7 @@ pub fn run_aeneas(
     // we use it. Otherwise, we default to the managed toolchain directory.
     let toolchain = crate::setup::Toolchain::resolve()?;
     let path = toolchain.root.display();
-    let aeneas_dep = format!(
-        r#"require aeneas from git "file://{path}/backends/lean" @ "main" -- {}"#,
-        env!("ANNEAL_AENEAS_REV")
-    );
+    let aeneas_dep = format!(r#"require aeneas from "{path}/backends/lean""#);
 
     let roots_str = lake_roots.iter().map(|r| format!("`{}", r)).collect::<Vec<_>>().join(", ");
 
@@ -378,222 +375,6 @@ pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]
     write_if_changed(&lean_generated_root.join("Generated.lean"), &generated_imports)
         .context("Failed to write Generated.lean")?;
 
-    // To avoid a slow full rebuild of dependencies in the newly generated
-    // workspace, we manually materialize the dependencies and fix up Lake's
-    // build trace files.
-    //
-    // Lake records absolute paths in its trace files. By default, when we
-    // generate a workspace and run `lake build`, Lake clones the dependencies
-    // into the workspace's `.lake/packages` directory. Since the paths in the
-    // clone do not match the paths in the toolchain where dependencies were
-    // pre-built, Lake considers the traces invalid and rebuilds everything.
-    //
-    // We bypass this by:
-    // - Manually writing the manifest with local file URLs.
-    // - Copying the pre-built dependency directories directly from the
-    //   toolchain to avoid cloning.
-    // - Post-processing the trace files to replace toolchain paths with
-    //   workspace paths.
-
-    // We read the `lake-manifest.json` generated during toolchain setup,
-    // modify it to include Aeneas as a dependency, and write it directly to
-    // the workspace. This prevents Lake from running dependency resolution
-    // and post-update hooks that would attempt to download external assets.
-    println!("Writing modified manifest to generated workspace...");
-    let lean_root = roots.lean_root();
-    let toolchain = crate::setup::Toolchain::resolve()?;
-    let toolchain_manifest_path =
-        toolchain.root.join("backends").join("lean").join("lake-manifest.json");
-    let user_manifest_path = lean_root.join("lake-manifest.json");
-
-    if toolchain_manifest_path.exists() {
-        let content = fs::read_to_string(&toolchain_manifest_path)
-            .context("Failed to read toolchain manifest")?;
-        let mut manifest: serde_json::Value =
-            serde_json::from_str(&content).context("Failed to parse toolchain manifest")?;
-
-        // Change name to anneal_verification
-        manifest["name"] = serde_json::Value::String("anneal_verification".to_string());
-
-        // Read actual HEAD commit of Aeneas in toolchain
-        let toolchain_aeneas_dir = toolchain.root.join("backends").join("lean");
-        let output = Command::new("git")
-            .args(["rev-parse", "HEAD"])
-            .current_dir(&toolchain_aeneas_dir)
-            .output()
-            .context("Failed to run `git rev-parse HEAD` in toolchain Aeneas")?;
-
-        if !output.status.success() {
-            bail!("`git rev-parse HEAD` failed in toolchain Aeneas");
-        }
-        let aeneas_rev = String::from_utf8(output.stdout)
-            .context("Failed to parse git output")?
-            .trim()
-            .to_string();
-
-        // Inject aeneas dependency
-        let aeneas_dep = serde_json::json!({
-            "configFile": "lakefile.lean",
-            "inherited": false,
-            "inputRev": "main",
-            "manifestFile": "lake-manifest.json",
-            "name": "aeneas",
-            "rev": aeneas_rev,
-            "scope": "",
-            "subDir": null,
-            "type": "git",
-            "url": format!("file://{}", toolchain_aeneas_dir.to_str().unwrap())
-        });
-
-        if let Some(packages) = manifest["packages"].as_array_mut() {
-            packages.insert(0, aeneas_dep);
-        } else {
-            bail!("Manifest packages is not an array");
-        }
-
-        let new_content = serde_json::to_string_pretty(&manifest)
-            .context("Failed to serialize modified manifest")?;
-        fs::write(&user_manifest_path, new_content).context("Failed to write user manifest")?;
-    } else {
-        bail!("Toolchain manifest missing at {}", toolchain_manifest_path.display());
-    }
-
-    // We manually copy the Aeneas package and all resolved dependencies from
-    // the toolchain into the workspace's `.lake/packages` directory. This
-    // populates the clones with the pre-built `.lake/build` artifacts.
-    // We also update the Git remote URL in each clone to match the local
-    // file URLs in the manifest, preventing Lake from deleting them due to
-    // a URL mismatch.
-    println!("Materializing packages by copying from toolchain...");
-    let user_project_packages = lean_root.join(".lake").join("packages");
-
-    // Ensure .lake/packages exists
-    fs::create_dir_all(&user_project_packages)
-        .context("Failed to create .lake/packages directory")?;
-
-    // Copy Aeneas
-    let toolchain_aeneas_dir = toolchain.root.join("backends").join("lean");
-    let user_aeneas_dir = user_project_packages.join("aeneas");
-
-    if toolchain_aeneas_dir.exists() {
-        if user_aeneas_dir.exists() {
-            fs::remove_dir_all(&user_aeneas_dir)
-                .context("Failed to remove existing Aeneas directory in workspace")?;
-        }
-        let status = Command::new("cp")
-            .args(["-r", toolchain_aeneas_dir.to_str().unwrap(), user_aeneas_dir.to_str().unwrap()])
-            .status()
-            .context("Failed to copy Aeneas directory")?;
-        if !status.success() {
-            bail!("Failed to copy Aeneas directory from toolchain to workspace");
-        }
-
-        // Add Git remote 'origin' to match manifest
-        let status = Command::new("git")
-            .args([
-                "remote",
-                "add",
-                "origin",
-                &format!("file://{}", toolchain_aeneas_dir.to_str().unwrap()),
-            ])
-            .current_dir(&user_aeneas_dir)
-            .status()
-            .context("Failed to run `git remote add` in Aeneas clone")?;
-        if !status.success() {
-            bail!("`git remote add` failed in Aeneas clone");
-        }
-    }
-
-    // Copy dependencies
-    let toolchain_packages_dir = toolchain.root.join("packages");
-    if toolchain_packages_dir.exists() {
-        for entry in fs::read_dir(&toolchain_packages_dir)
-            .context("Failed to read toolchain packages directory")?
-        {
-            let entry = entry.context("Failed to read directory entry")?;
-            let path = entry.path();
-            if path.is_dir() {
-                let pkg_name = path.file_name().unwrap().to_str().unwrap();
-                let user_pkg_dir = user_project_packages.join(pkg_name);
-
-                if user_pkg_dir.exists() {
-                    fs::remove_dir_all(&user_pkg_dir)
-                        .context("Failed to remove existing package directory in workspace")?;
-                }
-                let status = Command::new("cp")
-                    .args(["-r", path.to_str().unwrap(), user_pkg_dir.to_str().unwrap()])
-                    .status()
-                    .context("Failed to copy package directory")?;
-                if !status.success() {
-                    bail!("Failed to copy package directory for {}", pkg_name);
-                }
-
-                // Update Git remote URL to match manifest
-                let status = Command::new("git")
-                    .args([
-                        "remote",
-                        "set-url",
-                        "origin",
-                        &format!("file://{}", path.to_str().unwrap()),
-                    ])
-                    .current_dir(&user_pkg_dir)
-                    .status()
-                    .context("Failed to run `git remote set-url` in package clone")?;
-                if !status.success() {
-                    bail!("`git remote set-url` failed in package clone for {}", pkg_name);
-                }
-            }
-        }
-    }
-
-    // Finally, we fix the non-portable absolute paths embedded in Lake's
-    // `.trace` files. We replace all occurrences of paths pointing to the
-    // toolchain with the corresponding paths in the workspace's clone
-    // directory. This convinces Lake that the pre-built artifacts are valid
-    // for the current workspace location.
-    println!("Post-processing traces in the clone...");
-    let toolchain_aeneas = toolchain.root.join("backends").join("lean");
-    let toolchain_aeneas_str = toolchain_aeneas.to_str().unwrap();
-    let user_project_aeneas = user_project_packages.join("aeneas");
-    let user_project_aeneas_str = user_project_aeneas.to_str().unwrap();
-    let toolchain_packages_str = toolchain_packages_dir.to_str().unwrap();
-    let user_project_packages_str = user_project_packages.to_str().unwrap();
-
-    let process_build_dir = |dir: &Path| -> Result<()> {
-        if dir.exists() {
-            let walker = WalkDir::new(dir).into_iter();
-            for entry in walker {
-                let entry = entry.context("Failed to walk build directory")?;
-                let path = entry.path();
-                if path.is_file() && path.extension().map_or(false, |ext| ext == "trace") {
-                    let content = fs::read_to_string(path).context("Failed to read trace file")?;
-                    let mut new_content =
-                        content.replace(toolchain_aeneas_str, user_project_aeneas_str);
-                    new_content =
-                        new_content.replace(toolchain_packages_str, user_project_packages_str);
-
-                    if new_content != content {
-                        fs::write(path, new_content).context("Failed to write trace file")?;
-                    }
-                }
-            }
-        }
-        Ok(())
-    };
-
-    // Process all packages in .lake/packages
-    if user_project_packages.exists() {
-        for entry in
-            fs::read_dir(&user_project_packages).context("Failed to read user project packages")?
-        {
-            let entry = entry.context("Failed to read directory entry")?;
-            let path = entry.path();
-            if path.is_dir() {
-                process_build_dir(&path.join(".lake").join("build"))?;
-            }
-        }
-    }
-
     Ok(())
 }
 
diff --git a/anneal/src/setup.rs b/anneal/src/setup.rs
index bdfed7baa1..05cb3b73ad 100644
--- a/anneal/src/setup.rs
+++ b/anneal/src/setup.rs
@@ -374,6 +374,37 @@ fn make_writable(path: &Path) -> Result<()> {
     Ok(())
 }
 
+/// Recursively removes write permissions from all files and directories.
+fn make_read_only_recursive(path: &Path) -> Result<()> {
+    if path.exists() {
+        for entry in WalkDir::new(path) {
+            let entry = entry.context("Failed to walk directory for read-only setup")?;
+            let p = entry.path();
+            let mut perms = fs::metadata(p)?.permissions();
+            perms.set_readonly(true);
+            fs::set_permissions(p, perms)
+                .with_context(|| format!("Failed to set read-only permissions on {:?}", p))?;
+        }
+    }
+    Ok(())
+}
+
+/// Recursively restores write permissions for the owner.
+fn make_writable_recursive(path: &Path) -> Result<()> {
+    if path.exists() {
+        for entry in WalkDir::new(path) {
+            let entry = entry.context("Failed to walk directory for writable setup")?;
+            let p = entry.path();
+            let mut perms = fs::metadata(p)?.permissions();
+            #[allow(clippy::permissions_set_readonly_false)]
+            perms.set_readonly(false);
+            fs::set_permissions(p, perms)
+                .with_context(|| format!("Failed to set writable permissions on {:?}", p))?;
+        }
+    }
+    Ok(())
+}
+
 /// Decodes a hexadecimal string into its byte representation.
 const fn decode_hex(s: &str) -> Option<[u8; 32]> {
     let bytes = s.as_bytes();
@@ -855,263 +886,68 @@ pub fn run_setup() -> Result<()> {
     }
 
     // We now perform the core rewriting of dependency configurations to point
-    // to the filesystem-local paths we just created.
-    //
-    // We first read the manifest to know the exact resolved commit hashes,
-    // ensuring we preserve the versions resolved by Lake in step 2.
+    // to the filesystem-local paths we just created using relative path dependencies.
     let manifest_path = lean_dir.join("lake-manifest.json");
-    let revs = read_manifest_revs(&manifest_path)?;
-
-    // Helper to get rev or fallback
-    let get_rev = |name: &str| -> &str { revs.get(name).map(|s| s.as_str()).unwrap_or("main") };
 
-    // We hardcode the target strings for replacement because parsing arbitrary
-    // Lean configuration files in Rust is fragile. Since this toolchain pins
-    // specific versions of dependencies, these target strings are stable for
-    // this version of Anneal.
-    //
-    // Rewrite URLs in Aeneas lakefile.lean
+    // Rewrite URLs in Aeneas lakefile.lean to use path dependency
     let aeneas_lakefile = lean_dir.join("lakefile.lean");
-    let mathlib_rev = get_rev("mathlib");
     let target = "require mathlib from git\n  \"https://github.com/leanprover-community/mathlib4.git\" @ \"v4.28.0-rc1\"";
-    let replacement = format!(
-        "require mathlib from git\n  \"file://{}/packages/mathlib\" @ \"{}\"",
-        tmp_root.display(),
-        mathlib_rev
-    );
-    strict_replace_file_content(&aeneas_lakefile, target, &replacement)?;
+    let replacement = "require mathlib from \"../../packages/mathlib\"";
+    strict_replace_file_content(&aeneas_lakefile, target, replacement)?;
 
-    // Rewrite URLs in Mathlib lakefile.lean
+    // Rewrite URLs in Mathlib lakefile.lean to use relative path dependencies
     let mathlib_lakefile = packages_dir.join("mathlib").join("lakefile.lean");
-    let batteries_rev = get_rev("batteries");
-    let qq_rev = get_rev("Qq");
-    let aesop_rev = get_rev("aesop");
-    let proofwidgets_rev = get_rev("proofwidgets");
-    let import_graph_rev = get_rev("importGraph");
-    let lean_search_client_rev = get_rev("LeanSearchClient");
-    let plausible_rev = get_rev("plausible");
-
     let mathlib_replacements = [
         (
             "require \"leanprover-community\" / \"batteries\" @ git \"main\"",
-            format!(
-                "require batteries from git \"file://{}/packages/batteries\" @ \"{}\"",
-                tmp_root.display(),
-                batteries_rev
-            ),
-        ),
-        (
-            "require \"leanprover-community\" / \"Qq\" @ git \"master\"",
-            format!(
-                "require Qq from git \"file://{}/packages/Qq\" @ \"{}\"",
-                tmp_root.display(),
-                qq_rev
-            ),
+            "require batteries from \"../batteries\"",
         ),
+        ("require \"leanprover-community\" / \"Qq\" @ git \"master\"", "require Qq from \"../Qq\""),
         (
             "require \"leanprover-community\" / \"aesop\" @ git \"master\"",
-            format!(
-                "require aesop from git \"file://{}/packages/aesop\" @ \"{}\"",
-                tmp_root.display(),
-                aesop_rev
-            ),
+            "require aesop from \"../aesop\"",
         ),
         (
             "require \"leanprover-community\" / \"proofwidgets\" @ git \"v0.0.86\"",
-            format!(
-                "require proofwidgets from git \"file://{}/packages/proofwidgets\" @ \"{}\"",
-                tmp_root.display(),
-                proofwidgets_rev
-            ),
+            "require proofwidgets from \"../proofwidgets\"",
         ),
         (
             "require \"leanprover-community\" / \"importGraph\" @ git \"main\"",
-            format!(
-                "require importGraph from git \"file://{}/packages/importGraph\" @ \"{}\"",
-                tmp_root.display(),
-                import_graph_rev
-            ),
+            "require importGraph from \"../importGraph\"",
         ),
         (
             "require \"leanprover-community\" / \"LeanSearchClient\" @ git \"main\"",
-            format!(
-                "require LeanSearchClient from git \"file://{}/packages/LeanSearchClient\" @ \"{}\"",
-                tmp_root.display(),
-                lean_search_client_rev
-            ),
+            "require LeanSearchClient from \"../LeanSearchClient\"",
         ),
         (
             "require \"leanprover-community\" / \"plausible\" @ git \"main\"",
-            format!(
-                "require plausible from git \"file://{}/packages/plausible\" @ \"{}\"",
-                tmp_root.display(),
-                plausible_rev
-            ),
+            "require plausible from \"../plausible\"",
         ),
     ];
 
     for (target, replacement) in &mathlib_replacements {
-        strict_replace_file_content(&mathlib_lakefile, target, &replacement)?;
+        strict_replace_file_content(&mathlib_lakefile, target, replacement)?;
     }
 
-    // Rewrite URLs in Aesop lakefile.toml
+    // Rewrite URLs in Aesop lakefile.toml to use relative path dependency
     let aesop_lakefile = packages_dir.join("aesop").join("lakefile.toml");
     let target = "[[require]]\nname = \"batteries\"\ngit = \"https://github.com/leanprover-community/batteries\"\nrev = \"v4.28.0-rc1\"";
-    let replacement = format!(
-        "[[require]]\nname = \"batteries\"\ngit = \"file://{}/packages/batteries\"\nrev = \"v4.28.0-rc1\"",
-        tmp_root.display()
-    );
-    strict_replace_file_content(&aesop_lakefile, target, &replacement)?;
+    let replacement = "[[require]]\nname = \"batteries\"\npath = \"../batteries\"";
+    strict_replace_file_content(&aesop_lakefile, target, replacement)?;
 
-    // Rewrite URLs in ImportGraph lakefile.toml
+    // Rewrite URLs in ImportGraph lakefile.toml to use relative path dependency
     let import_graph_lakefile = packages_dir.join("importGraph").join("lakefile.toml");
     let target = "[[require]]\nname = \"Cli\"\nscope = \"leanprover\"\nrev = \"v4.28.0-rc1\"";
-    let replacement = format!(
-        "[[require]]\nname = \"Cli\"\ngit = \"file://{}/packages/Cli\"\nrev = \"v4.28.0-rc1\"",
-        tmp_root.display()
-    );
-    strict_replace_file_content(&import_graph_lakefile, target, &replacement)?;
-
-    // We must also update the manifest file itself. If we only update the
-    // `lakefile`s, Lake will see that the manifest is out of date and attempt
-    // to re-resolve or re-clone from GitHub.
-    //
-    // Rewrite URLs in lake-manifest.json
-    update_manifest_urls(&manifest_path, tmp_root)?;
-
-    prebuild_lean_library(&lean_dir, &toolchain.cache_dir())?;
+    let replacement = "[[require]]\nname = \"Cli\"\npath = \"../Cli\"";
+    strict_replace_file_content(&import_graph_lakefile, target, replacement)?;
 
-    // Phase 2: Rewrite URLs to point to the final toolchain root.
-    //
-    // During the build in Phase 1, we used paths pointing to the temporary
-    // directory so that Lake could resolve and build dependencies correctly.
-    // Now that the build is complete, we must rewrite these paths to point
-    // to the final installation directory (`toolchain.root`) before we
-    // perform the atomic swap. This ensures that when the toolchain is
-    // used by user projects, all internal references are valid.
-    println!("Rewriting URLs to final toolchain root...");
-
-    let target_aeneas = format!(
-        "require mathlib from git\n  \"file://{}/packages/mathlib\" @ \"{}\"",
-        tmp_root.display(),
-        mathlib_rev
-    );
-    let replacement_aeneas = format!(
-        "require mathlib from git\n  \"file://{}/packages/mathlib\" @ \"{}\"",
-        toolchain.root.display(),
-        mathlib_rev
-    );
-    strict_replace_file_content(&aeneas_lakefile, &target_aeneas, &replacement_aeneas)?;
-
-    for (orig_target, phase1_rep) in &mathlib_replacements {
-        let phase2_rep = phase1_rep
-            .replace(&tmp_root.display().to_string(), &toolchain.root.display().to_string());
-        strict_replace_file_content(&mathlib_lakefile, &phase1_rep, &phase2_rep)?;
+    // Delete the manifest file. Since all dependencies are resolved via paths,
+    // Lake does not need a manifest file to lock revisions.
+    if manifest_path.exists() {
+        fs::remove_file(&manifest_path).context("Failed to delete manifest")?;
     }
 
-    let target_aesop = format!(
-        "[[require]]\nname = \"batteries\"\ngit = \"file://{}/packages/batteries\"\nrev = \"v4.28.0-rc1\"",
-        tmp_root.display()
-    );
-    let replacement_aesop = format!(
-        "[[require]]\nname = \"batteries\"\ngit = \"file://{}/packages/batteries\"\nrev = \"v4.28.0-rc1\"",
-        toolchain.root.display()
-    );
-    strict_replace_file_content(&aesop_lakefile, &target_aesop, &replacement_aesop)?;
-
-    let target_import_graph = format!(
-        "[[require]]\nname = \"Cli\"\ngit = \"file://{}/packages/Cli\"\nrev = \"v4.28.0-rc1\"",
-        tmp_root.display()
-    );
-    let replacement_import_graph = format!(
-        "[[require]]\nname = \"Cli\"\ngit = \"file://{}/packages/Cli\"\nrev = \"v4.28.0-rc1\"",
-        toolchain.root.display()
-    );
-    strict_replace_file_content(
-        &import_graph_lakefile,
-        &target_import_graph,
-        &replacement_import_graph,
-    )?;
-
-    // Also update manifest for Phase 2
-    update_manifest_urls(&manifest_path, &toolchain.root)?;
-
-    // Commit changes in local repositories so that Git clone operations
-    // performed by Lake in user projects will see the rewritten URLs.
-    println!("Committing changes in local repositories...");
-
-    // Commit in Aeneas
-    let status = Command::new("git")
-        .args(["add", "."])
-        .current_dir(&lean_dir)
-        .status()
-        .context("Failed to run `git add` in Aeneas")?;
-    if !status.success() {
-        bail!("`git add` failed in Aeneas");
-    }
-
-    let status = Command::new("git")
-        .args(["commit", "-m", "Anneal: rewrite dependencies to local paths", "-q"])
-        .env("GIT_AUTHOR_NAME", "Anneal")
-        .env("GIT_AUTHOR_EMAIL", "anneal@example.com")
-        .env("GIT_COMMITTER_NAME", "Anneal")
-        .env("GIT_COMMITTER_EMAIL", "anneal@example.com")
-        .current_dir(&lean_dir)
-        .status()
-        .context("Failed to run `git commit` in Aeneas")?;
-    if !status.success() {
-        bail!("`git commit` failed in Aeneas");
-    }
-
-    // Commit in dependencies
-    if packages_dir.exists() {
-        for entry in fs::read_dir(&packages_dir).context("Failed to read packages directory")? {
-            let entry = entry.context("Failed to read directory entry")?;
-            let path = entry.path();
-            if path.is_dir() {
-                if path.join(".git").exists() {
-                    let output = Command::new("git")
-                        .args(["status", "--porcelain"])
-                        .current_dir(&path)
-                        .output()
-                        .context("Failed to run `git status` in dependency")?;
-
-                    if !output.stdout.is_empty() {
-                        println!(
-                            "Committing changes in dependency: {:?}",
-                            path.file_name().unwrap()
-                        );
-                        let status = Command::new("git")
-                            .args(["add", "."])
-                            .current_dir(&path)
-                            .status()
-                            .context("Failed to run `git add` in dependency")?;
-                        if !status.success() {
-                            bail!("`git add` failed in dependency {:?}", path);
-                        }
-
-                        let status = Command::new("git")
-                            .args([
-                                "commit",
-                                "-m",
-                                "Anneal: rewrite dependencies to local paths",
-                                "-q",
-                            ])
-                            .env("GIT_AUTHOR_NAME", "Anneal")
-                            .env("GIT_AUTHOR_EMAIL", "anneal@example.com")
-                            .env("GIT_COMMITTER_NAME", "Anneal")
-                            .env("GIT_COMMITTER_EMAIL", "anneal@example.com")
-                            .current_dir(&path)
-                            .status()
-                            .context("Failed to run `git commit` in dependency")?;
-                        if !status.success() {
-                            bail!("`git commit` failed in dependency {:?}", path);
-                        }
-                    }
-                }
-            }
-        }
-    }
+    prebuild_lean_library(&lean_dir, &toolchain.cache_dir())?;
 
     // Lake records absolute paths in its `.trace` files (e.g., in the
     // compiler command lines). Since we built the project in a temporary
@@ -1166,11 +1002,19 @@ pub fn run_setup() -> Result<()> {
     // allow the rename to succeed on Unix systems.
     let tmp_path = temp_dir.into_path();
     if toolchain.root.exists() {
+        make_writable_recursive(&toolchain.root)?;
         fs::remove_dir_all(&toolchain.root).context("Failed to remove old toolchain directory")?;
     }
     fs::rename(&tmp_path, &toolchain.root)
         .context("Failed to rename temporary toolchain directory to target")?;
 
+    // Create an empty .lock file so that future verify runs (which are read-only)
+    // can open it in read-only mode to acquire shared locks.
+    let lock_path = toolchain.root.join(".lock");
+    fs::File::create(&lock_path).context("Failed to create lock file in setup")?;
+
+    make_read_only_recursive(&toolchain.root)?;
+
     Ok(())
 }