diff --git a/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml b/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml index bd44e3c3bc..5714e4edec 100644 --- a/anneal/tests/fixtures/archive_lake_cache_reuse/anneal.toml +++ b/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. """ diff --git a/anneal/tests/integration.rs b/anneal/tests/integration.rs index 8fc6f6b9b4..ce5215b663 100644 --- a/anneal/tests/integration.rs +++ b/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> { + 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> { + 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> { + 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> { 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,9 +670,18 @@ fn acquire_toolchain_run_slot() -> ToolchainRunPermit { } fn run_command_with_profile( + test: &str, + phase: Option<&str>, + cmd: process::Command, +) -> io::Result { + 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 { 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())) @@ -565,10 +689,15 @@ fn run_command_with_profile( 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); diff --git a/anneal/v2/flake.nix b/anneal/v2/flake.nix index 433fcf5c64..5a219f4bc5 100644 --- a/anneal/v2/flake.nix +++ b/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,6 +486,15 @@ "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/" @@ -488,7 +502,13 @@ "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" diff --git a/anneal/v2/prime-lakefile.lean b/anneal/v2/prime-lakefile.lean new file mode 100644 index 0000000000..94f7d08586 --- /dev/null +++ b/anneal/v2/prime-lakefile.lean @@ -0,0 +1,112 @@ +/- +Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. +-/ + +import Lake + +open Lake DSL + +namespace Anneal + +open System + +private structure TraceUpdate where + path : FilePath + metadata : BuildMetadata + +private def TraceUpdate.tempPath (self : TraceUpdate) : FilePath := + FilePath.mk <| self.path.toString ++ ".anneal-tmp" + +private def getBuildStore : JobM BuildStore := + JobM.ofFn fun _ _ _ store _ state => do + return .ok (← store.get) state + +private def verifyArtifactHash (artifact : Artifact) : JobM PUnit := do + let actualHash ← computeFileHash artifact.path + unless actualHash == artifact.hash do + IO.eprintln s!"Lake returned a stale hash for {artifact.path}: expected {artifact.hash}, got {actualHash}" + error s!"Lake returned a stale hash for {artifact.path}" + +private def verifyArtifactHashes (artifacts : ModuleOutputArtifacts) : JobM PUnit := do + verifyArtifactHash artifacts.olean + artifacts.oleanServer?.forM verifyArtifactHash + artifacts.oleanPrivate?.forM verifyArtifactHash + verifyArtifactHash artifacts.ilean + artifacts.ir?.forM verifyArtifactHash + verifyArtifactHash artifacts.c + artifacts.bc?.forM verifyArtifactHash + artifacts.ltar?.forM verifyArtifactHash + +set_option linter.deprecated false in +private def collectTraceUpdates (ws : Workspace) (store : BuildStore) : JobM (Array TraceUpdate) := do + let mut updates := #[] + for ⟨key, familyJob⟩ in store do + match key with + | .packageModuleFacet packageName moduleName facet => + if h : facet = Module.leanArtsFacet then + have ofData := by unfold BuildData; simp [h] + let job : Job ModuleOutputArtifacts := cast ofData familyJob + let some artifacts ← job.wait? | continue + let some pkg := ws.findPackageByKey? packageName | continue + let some mod := pkg.findModule? moduleName | continue + -- Artifact hashes are checked before publishing the replacement trace. + verifyArtifactHashes artifacts + let savedTrace ← readTraceFile mod.traceFile + let log := match savedTrace with + | .ok metadata => metadata.log + | .missing | .invalid => {} + let metadata := BuildMetadata.ofBuild job.getTrace artifacts.descrs log + let needsUpdate := match savedTrace with + | .ok saved => saved.toJson != metadata.toJson + | .missing | .invalid => true + if needsUpdate then + updates := updates.push {path := mod.traceFile, metadata} + | _ => pure () + return updates + +private def writeTraceUpdates (updates : Array TraceUpdate) : IO Unit := do + -- Serialize every replacement before publishing any of them, so a staging + -- error cannot leave a half-refreshed trace set. + for update in updates do + update.metadata.writeFile update.tempPath + for update in updates do + IO.FS.rename update.tempPath update.path + +/-- +Set up one Lean file using Lake's old-mode fallback, then promote the exact +current dependency traces for every module visited by the successful build. + +Writes are deliberately deferred until the root build has completed. Updating +a child trace earlier would advance its mtime and could make an old-mode parent +appear older than its inputs before Lake reaches it. +-/ +script refreshLakeTraces (args) do + let ws ← getWorkspace + let fileName ← match args with + | [fileName] => pure fileName + | _ => throw <| IO.userError "expected exactly one Lean file" + let some path ← resolvePath? fileName + | throw <| IO.userError s!"file not found: {fileName}" + let updates ← ws.runBuild (cfg := {oldMode := true, trustHash := false}) do + (← setupServerModule fileName path none).mapM fun _ => do + collectTraceUpdates ws (← getBuildStore) + writeTraceUpdates updates + IO.println s!"refreshed {updates.size} Lake module traces in one build" + return 0 + +end Anneal + +require aeneas from "@AENEAS_ROOT@" + +package anneal_verification + +@[default_target] +lean_lib «Generated» where + srcDir := "generated" + roots := #[`Generated]