[anneal] Prime Lake traces in one server traversal

anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml

@@ -1,4 +1,4 @@
 description = """
-Purpose: Verifies that the installed Nix-built archive can be used read-only by a fresh generated Lake workspace.
-Behavior: Builds and diagnoses a tiny workspace with a complete relative Lake manifest pointing at the installed Aeneas archive.
+Purpose: Verifies that the installed Nix-built archive can be used read-only by a fresh generated Lake workspace and the Lean language server.
+Behavior: Builds, diagnoses, and runs IDE setup-file on a tiny workspace with a complete relative Lake manifest pointing at the installed Aeneas archive.
 """

anneal/tests/integration.rs

@@ -338,6 +338,10 @@ lean_lib Generated where
     )?;
     write_relative_archive_manifest(&workspace, &aeneas_lean)?;
 
+    // This is the workspace-loading path used by the Lean language server and
+    // IDE InfoView on first open. `setup-file` checks dependency traces in hash
+    // mode and is not allowed to repair the read-only archive.
+    run_lake_archive_setup_file(test_name, &workspace, toolchain_root, &lean_root)?;
     // This mirrors v1's generated workspace contract with the Nix-built
     // archive: dependency paths are locked relative to the workspace, package
     // caches are read-only, and `--old` must reuse the prebuilt Lake outputs.
@@ -351,7 +355,14 @@ lean_lib Generated where
         test_name,
         &workspace,
         &lean_root,
-        &["--keep-toolchain", "env", "lean", "--json", "generated/Generated.lean"],
+        &[
+            "--keep-toolchain",
+            "env",
+            "lean",
+            "--setup=lean-server-setup.json",
+            "--json",
+            "generated/Generated.lean",
+        ],
     )?;
 
     Ok(())
@@ -464,6 +475,111 @@ fn run_lake_archive_command(
     lean_root: &Path,
     args: &[&str],
 ) -> Result<(), Box<dyn std::error::Error>> {
+    let cmd = lake_archive_command(workspace, lean_root, args)?;
+    run_command_with_profile(test_name, Some("archive_lake_cache_reuse"), cmd)?.assert.success();
+    Ok(())
+}
+
+fn run_lake_archive_setup_file(
+    test_name: &str,
+    workspace: &Path,
+    toolchain_root: &Path,
+    lean_root: &Path,
+) -> Result<(), Box<dyn std::error::Error>> {
+    let cmd = lake_archive_command(
+        workspace,
+        lean_root,
+        &[
+            "--keep-toolchain",
+            "setup-file",
+            "generated/Generated.lean",
+            "-",
+            "--no-build",
+            "--no-cache",
+            "--quiet",
+        ],
+    )?;
+    let header = json!({
+        "imports": [{
+            "module": "Aeneas",
+            "importAll": false,
+            "isExported": true,
+            "isMeta": false,
+        }],
+        "isModule": false,
+    });
+    let input = format!("{header}\n");
+    let run = run_command_with_input_profile(
+        test_name,
+        Some("archive_lake_cache_reuse"),
+        cmd,
+        Some(input.as_bytes()),
+    )?;
+    let assert = run.assert.success();
+    let setup: Value = serde_json::from_slice(&assert.get_output().stdout)?;
+    let import_arts = setup
+        .get("importArts")
+        .and_then(Value::as_object)
+        .ok_or_else(|| invalid_data("Lake setup-file output has no importArts object"))?;
+    if !import_arts.contains_key("Aeneas") {
+        return Err(invalid_data("Lake setup-file output has no Aeneas import artifact").into());
+    }
+    for (module, artifacts) in import_arts {
+        let artifacts = artifacts.as_array().ok_or_else(|| {
+            invalid_data(format!("Lake setup-file artifacts for {module} are not an array"))
+        })?;
+        for artifact in artifacts {
+            let artifact = artifact.as_str().ok_or_else(|| {
+                invalid_data(format!("Lake setup-file artifact for {module} is not a path"))
+            })?;
+            validate_setup_artifact(toolchain_root, artifact)?;
+        }
+    }
+    for field in ["dynlibs", "plugins"] {
+        let artifacts = setup
+            .get(field)
+            .and_then(Value::as_array)
+            .ok_or_else(|| invalid_data(format!("Lake setup-file output has no {field} array")))?;
+        for artifact in artifacts {
+            let artifact = artifact.as_str().ok_or_else(|| {
+                invalid_data(format!("Lake setup-file {field} entry is not a path"))
+            })?;
+            validate_setup_artifact(toolchain_root, artifact)?;
+        }
+    }
+    fs::write(workspace.join("lean-server-setup.json"), &assert.get_output().stdout)?;
+    Ok(())
+}
+
+fn validate_setup_artifact(
+    toolchain_root: &Path,
+    artifact: &str,
+) -> Result<(), Box<dyn std::error::Error>> {
+    let artifact = Path::new(artifact);
+    if !artifact.is_file() {
+        return Err(invalid_data(format!(
+            "Lake setup-file returned a missing artifact: {}",
+            artifact.display()
+        ))
+        .into());
+    }
+    let artifact = fs::canonicalize(artifact)?;
+    let toolchain_root = fs::canonicalize(toolchain_root)?;
+    if !artifact.starts_with(&toolchain_root) {
+        return Err(invalid_data(format!(
+            "Lake setup-file returned an artifact outside the installed toolchain: {}",
+            artifact.display()
+        ))
+        .into());
+    }
+    Ok(())
+}
+
+fn lake_archive_command(
+    workspace: &Path,
+    lean_root: &Path,
+    args: &[&str],
+) -> Result<process::Command, Box<dyn std::error::Error>> {
     let lean_bin = lean_root.join("bin");
     let mut cmd = process::Command::new(lean_bin.join("lake"));
     cmd.args(args)
@@ -479,8 +595,7 @@ fn run_lake_archive_command(
         prepend_env_paths(lib_var, &[lean_root.join("lib"), lean_root.join("lib/lean")])?,
     );
 
-    run_command_with_profile(test_name, Some("archive_lake_cache_reuse"), cmd)?.assert.success();
-    Ok(())
+    Ok(cmd)
 }
 
 fn prepend_env_paths(
@@ -555,20 +670,34 @@ fn acquire_toolchain_run_slot() -> ToolchainRunPermit {
 }
 
 fn run_command_with_profile(
+    test: &str,
+    phase: Option<&str>,
+    cmd: process::Command,
+) -> io::Result<CommandRun> {
+    run_command_with_input_profile(test, phase, cmd, None)
+}
+
+fn run_command_with_input_profile(
     test: &str,
     phase: Option<&str>,
     mut cmd: process::Command,
+    input: Option<&[u8]>,
 ) -> io::Result<CommandRun> {
     let argv: Vec<_> = std::iter::once(cmd.get_program().to_string_lossy().to_string())
         .chain(cmd.get_args().map(|arg| arg.to_string_lossy().to_string()))
         .collect();
     let cwd = cmd.get_current_dir().map(|dir| dir.display().to_string());
     let started = Instant::now();
 
-    cmd.stdin(Stdio::null()).stdout(Stdio::piped()).stderr(Stdio::piped());
-    let child = cmd.spawn()?;
+    cmd.stdin(if input.is_some() { Stdio::piped() } else { Stdio::null() })
+        .stdout(Stdio::piped())
+        .stderr(Stdio::piped());
+    let mut child = cmd.spawn()?;
     let child_pid = child.id();
     let sampler = ProcessSampler::start(test, phase, child_pid);
+    if let Some(input) = input {
+        child.stdin.take().expect("piped command stdin is missing").write_all(input)?;
+    }
     let output = child.wait_with_output()?;
     let metrics = sampler.map(ProcessSampler::finish);
 

anneal/v2/flake.nix

@@ -302,6 +302,12 @@
           dontPatchELF = true;
           dontStrip = true;
 
+          preFixup = pkgs.lib.optionalString pkgs.stdenv.isDarwin ''
+            # This fixed-output fetch must preserve cached native artifacts
+            # exactly; Darwin's generic fixup hook would rewrite them.
+            fixDarwinDylibNamesIn() { :; }
+          '';
+
           outputHashMode = "recursive";
           outputHashAlgo = "sha256";
           outputHash = mathlibCacheDownloadSha256;
@@ -387,10 +393,16 @@
         };
 
         # Builds the Aeneas Lean backend against vendored, relative Lake paths.
-        packages.aeneas-compiled = pkgs.stdenv.mkDerivation {
+        packages.aeneas-compiled = pkgs.stdenv.mkDerivation ({
           pname = "aeneas-compiled";
           version = "0.1.0";
 
+          # Lake records content hashes for its native artifacts. Preserve
+          # those bytes after the final trace refresh; runtime binaries are
+          # normalized later when the omnibus archive is staged.
+          dontPatchELF = true;
+          dontStrip = true;
+
           src = pkgs.runCommand "empty-src" {} "mkdir $out";
 
           leanToolchain = self.packages.${system}.lean-toolchain;
@@ -446,31 +458,24 @@
             "test -f ../../packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean"
             (runLeanCommand "lake --old build")
             "test -f ../../packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Merge.olean"
-            # FIXME: Remove this v1-only package config primer once generated
+            # FIXME: Remove this v1-only workspace primer once generated
             # workspaces migrate to v2.
             # Anneal v1 generated workspaces require this package directly
-            # from the installed archive. Prime the package config that Lake
-            # needs in that dependency context before the archive is frozen.
+            # from the installed archive. Prime both the named package config
+            # and hash-mode build traces that `lake setup-file` needs in that
+            # dependency context before the archive is frozen.
             "mkdir -p $TMPDIR/aeneas-config-primer/generated"
             "cp lean-toolchain $TMPDIR/aeneas-config-primer/lean-toolchain"
             "cat > $TMPDIR/aeneas-config-primer/generated/Generated.lean <<'EOF'"
             "import Aeneas"
             "EOF"
-            "cat > $TMPDIR/aeneas-config-primer/lakefile.lean <<'EOF'"
-            "import Lake"
-            "open Lake DSL"
-            ""
-            "require aeneas from \"@AENEAS_ROOT@\""
-            ""
-            "package anneal_verification"
-            ""
-            "@[default_target]"
-            "lean_lib «Generated» where"
-            "  srcDir := \"generated\""
-            "  roots := #[`Generated]"
-            "EOF"
+            "cp ${./prime-lakefile.lean} $TMPDIR/aeneas-config-primer/lakefile.lean"
+            "chmod +w $TMPDIR/aeneas-config-primer/lakefile.lean"
             "substituteInPlace $TMPDIR/aeneas-config-primer/lakefile.lean --replace-fail @AENEAS_ROOT@ \"$PWD\""
-            "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --old build Generated"})"
+            # `refreshLakeTraces` runs the same setup graph as Lean's language
+            # server once in old mode, computes real artifact hashes, and only
+            # publishes all exact hash-mode module traces after it succeeds.
+            "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake run Anneal.refreshLakeTraces generated/Generated.lean"})"
             "test -f .lake/config/aeneas/lakefile.olean"
             "python3 ${./rewrite-lake-vendor.py} --root . --packages-dir ../../packages --rewrite-traces --trace-prefix \"$leanToolchain=lean\""
             "TRACE_ABS_RE='(^|[\"[:space:]=:])/(nix/store|build|private/tmp/nix-build|ANNEAL_PLACEHOLDER_ROOT)'"
@@ -481,14 +486,29 @@
             "fi"
             # Prune unused Lean modules and bulky upstream metadata.
             "python3 ${./prune-lake-cache.py} --project-root . --packages-root ../../packages"
+            # This is an assertion, not another refresh round: the ordinary
+            # hash-mode command used by Lean InfoView must accept the finished
+            # package tree without writing any repair metadata.
+            "chmod -R a-w . ../../packages"
+            "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake setup-file generated/Generated.lean --no-build --no-cache --quiet >/dev/null"})"
+            "if find . ../../packages -type f -name \"*.trace.nobuild\" -print -quit | grep -q .; then"
+            "  echo \"ERROR: Lake setup-file left no-build repair traces behind\" >&2"
+            "  exit 1"
+            "fi"
             "cd ../.."
             "mkdir -p $out/backends $out/packages"
             "cp -r backends/lean $out/backends/"
             "cp -r packages/* $out/packages/"
             "mkdir -p $out/bin"
             "cp \$(find $aeneasUnpacked -maxdepth 1 -type f -executable) $out/bin/"
           ];
-        };
+        } // pkgs.lib.optionalAttrs pkgs.stdenv.isDarwin {
+          preFixup = ''
+            # nixpkgs' Darwin fixup hook otherwise rewrites every cached
+            # `.dylib`/`.so` after Lake records its content hash.
+            fixDarwinDylibNamesIn() { :; }
+          '';
+        });
 
         # Stages the relocatable toolchain bundle before compression.
         packages.omnibus-tar = pkgs.stdenv.mkDerivation {
@@ -523,7 +543,11 @@
           ] ++ pkgs.lib.optionals pkgs.stdenv.isLinux [
             # Remove Nix dynamic-linker and RPATH references from ELF binaries.
             "echo \"Cleaning up Nix store references...\""
-            "find $TMPDIR/dist_staging -type f -executable | while read -r file; do"
+            # Cached Lake artifacts were hashed by `aeneas-compiled`; mutating
+            # them here would make the read-only archive fail hash-mode IDE
+            # setup. They are already relocatable, so normalize only runtime
+            # and toolchain executables.
+            "find $TMPDIR/dist_staging -type f -executable ! -path \"$TMPDIR/dist_staging/aeneas/*/.lake/*\" | while read -r file; do"
             "  if file \"\$file\" | grep -q \"ELF 64-bit\"; then"
             "    echo \"Patching and stripping \$file...\""
             "    if patchelf --print-interpreter \"\$file\" >/dev/null 2>&1; then"