diff --git a/anneal/src/aeneas.rs b/anneal/src/aeneas.rs index 6fab4b23e6..4ca04e40cf 100644 --- a/anneal/src/aeneas.rs +++ b/anneal/src/aeneas.rs @@ -15,15 +15,13 @@ use std::{ fmt::Write, fs, io::{BufRead, BufReader}, - path::{Path, PathBuf}, + path::PathBuf, process::Stdio, sync::{Arc, Mutex}, - time::SystemTime, }; use anyhow::{Context, Result, bail}; use indicatif::{ProgressBar, ProgressStyle}; -use walkdir::WalkDir; use crate::{generate, resolve::LockedRoots, scanner::AnnealArtifact, setup::Tool}; @@ -271,8 +269,10 @@ pub fn run_aeneas( // 4. Write Lakefile // - // Aeneas and its Lean dependencies are unpacked from the managed archive. - let path = materialize_aeneas_dependency(&tmp_lean_root, &lean_root, &toolchain)?; + // Aeneas and its Lean dependencies are used directly from the managed + // archive. The archive build primes dependency caches, and setup makes + // Lake's small `.lake/config` lock area writable. + let path = toolchain.aeneas_lean_dir(); let aeneas_dep = format!( r#"-- Aeneas rev: {} require aeneas from "{}""#, @@ -312,16 +312,15 @@ lean_lib «User» where // temporary directory with the real one. let lean_root = roots.lean_root(); if lean_root.exists() { - // Preserve the `.lake` directory and manifest to prevent re-downloading - // dependencies (like Mathlib) on subsequent runs. + // Preserve the `.lake` directory for generated-workspace build/config + // caches, but let Lake regenerate the manifest from the current + // Lakefile. The Aeneas dependency is an absolute path into the + // installed toolchain, so a manifest from another setup location would + // point at stale archive paths. let old_lake = lean_root.join(".lake"); - let old_manifest = lean_root.join("lake-manifest.json"); if old_lake.exists() { fs::rename(&old_lake, tmp_lean_root.join(".lake"))?; } - if old_manifest.exists() { - fs::rename(&old_manifest, tmp_lean_root.join("lake-manifest.json"))?; - } // Remove the existing directory before renaming the temporary directory. // Note: `fs::rename` on Unix typically requires the target directory to be @@ -338,171 +337,6 @@ lean_lib «User» where Ok(()) } -fn materialize_aeneas_dependency( - tmp_lean_root: &Path, - lean_root: &Path, - toolchain: &crate::setup::Toolchain, -) -> Result { - let vendor_root = tmp_lean_root.join("vendor").join("aeneas"); - let lean_dst = vendor_root.join("backends").join("lean"); - let packages_dst = vendor_root.join("packages"); - - println!("Materializing packages by copying from toolchain..."); - copy_toolchain_tree_writable(&toolchain.aeneas_lean_dir(), &lean_dst) - .context("Failed to copy Aeneas Lean package from toolchain")?; - copy_toolchain_tree_writable(&toolchain.aeneas_root().join("packages"), &packages_dst) - .context("Failed to copy Aeneas Lean dependencies from toolchain")?; - - Ok(lean_root.join("vendor").join("aeneas").join("backends").join("lean")) -} - -fn copy_toolchain_tree_writable(src: &Path, dst: &Path) -> Result<()> { - if dst.exists() { - fs::remove_dir_all(dst) - .with_context(|| format!("Failed to remove stale directory {}", dst.display()))?; - } - - let mut entries = WalkDir::new(src).into_iter(); - while let Some(entry) = entries.next() { - let entry = entry.with_context(|| format!("Failed to walk {}", src.display()))?; - let path = entry.path(); - let rel = path.strip_prefix(src).with_context(|| { - format!("Failed to relativize {} against {}", path.display(), src.display()) - })?; - let target = dst.join(rel); - - if is_lake_build_dir(rel) { - // The Nix-built archive already contains Lake build caches for the - // immutable Aeneas dependency tree. Link those caches back to the - // read-only toolchain instead of copying several GiB of `.olean` - // files into every generated Lean workspace. The surrounding - // package/config/source files are still copied below so Lake can - // update small mutable metadata such as `.lake/config`. - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).with_context(|| { - format!("Failed to create parent directory {}", parent.display()) - })?; - } - create_symlink(path, &target).with_context(|| { - format!( - "Failed to link prebuilt Lake cache {} to {}", - path.display(), - target.display() - ) - })?; - entries.skip_current_dir(); - } else if entry.file_type().is_dir() { - fs::create_dir_all(&target) - .with_context(|| format!("Failed to create directory {}", target.display()))?; - } else if entry.file_type().is_symlink() { - let link = fs::read_link(path) - .with_context(|| format!("Failed to read symlink {}", path.display()))?; - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).with_context(|| { - format!("Failed to create parent directory {}", parent.display()) - })?; - } - create_symlink(&link, &target) - .with_context(|| format!("Failed to copy symlink {}", target.display()))?; - } else if entry.file_type().is_file() { - if let Some(parent) = target.parent() { - fs::create_dir_all(parent).with_context(|| { - format!("Failed to create parent directory {}", parent.display()) - })?; - } - fs::copy(path, &target).with_context(|| { - format!("Failed to copy {} to {}", path.display(), target.display()) - })?; - make_writable(&target)?; - } - } - - for entry in WalkDir::new(dst).contents_first(true) { - let entry = entry.with_context(|| format!("Failed to walk {}", dst.display()))?; - if !entry.file_type().is_symlink() { - make_writable(entry.path())?; - } - } - - normalize_lake_input_mtimes(dst)?; - - Ok(()) -} - -fn is_lake_build_dir(rel: &Path) -> bool { - rel.file_name().is_some_and(|name| name == "build") - && rel.parent().and_then(Path::file_name).is_some_and(|name| name == ".lake") -} - -#[cfg(unix)] -fn create_symlink(src: &Path, dst: &Path) -> std::io::Result<()> { - std::os::unix::fs::symlink(src, dst) -} - -#[cfg(windows)] -fn create_symlink(src: &Path, dst: &Path) -> std::io::Result<()> { - if src.is_dir() { - std::os::windows::fs::symlink_dir(src, dst) - } else { - std::os::windows::fs::symlink_file(src, dst) - } -} - -fn make_writable(path: &Path) -> Result<()> { - let metadata = - fs::symlink_metadata(path).with_context(|| format!("Failed to stat {}", path.display()))?; - if metadata.file_type().is_symlink() { - return Ok(()); - } - let mut perms = metadata.permissions(); - if perms.readonly() { - #[allow(clippy::permissions_set_readonly_false)] - perms.set_readonly(false); - fs::set_permissions(path, perms) - .with_context(|| format!("Failed to make {} writable", path.display()))?; - } - Ok(()) -} - -fn normalize_lake_input_mtimes(root: &Path) -> Result<()> { - // The installed toolchain archive is intentionally read-only, and - // `copy_toolchain_tree_writable` symlinks `.lake/build` directories back to - // that archive so each verification workspace does not copy several GiB of - // prebuilt `.olean` files. That optimization only works if Lake accepts the - // linked cache artifacts as newer than the copied source/config files. A - // normal file copy gives the copied inputs fresh mtimes, so Lake `--old` - // can decide that archive outputs are stale and then fail while trying to - // remove read-only files through the `.lake/build` symlinks. Mirror the - // archive builder's convention: copied Lake inputs are older than the - // archive cache artifacts, while generated project files keep their normal - // mtimes and remain mutable. - for entry in WalkDir::new(root) { - let entry = entry.with_context(|| format!("Failed to walk {}", root.display()))?; - if !entry.file_type().is_file() || !is_lake_input_file(entry.path()) { - continue; - } - - let file = fs::File::options().write(true).open(entry.path()).with_context(|| { - format!("Failed to open {} to normalize mtime", entry.path().display()) - })?; - file.set_times(fs::FileTimes::new().set_modified(SystemTime::UNIX_EPOCH)) - .with_context(|| format!("Failed to normalize mtime for {}", entry.path().display()))?; - } - - Ok(()) -} - -fn is_lake_input_file(path: &Path) -> bool { - if path.extension().and_then(|ext| ext.to_str()) == Some("lean") { - return true; - } - - matches!( - path.file_name().and_then(|name| name.to_str()), - Some("lakefile.toml" | "lake-manifest.json" | "lean-toolchain") - ) -} - /// Generates Anneal `Specs.lean` and writes `Generated.lean`, but does not run the `lake build`. pub fn generate_lean_workspace(roots: &LockedRoots, artifacts: &[AnnealArtifact]) -> Result<()> { let lean_generated_root = roots.lean_generated_root(); @@ -760,11 +594,10 @@ fn configure_lake_command( // FIXME: Replace this with a cleaner toolchain/archive contract. // // The Nix-built archive contains prebuilt Lake outputs for the vendored - // Aeneas package, and `materialize_aeneas_dependency` links each generated - // verification workspace's `vendor/aeneas/backends/lean/.lake/build` back - // to that read-only archive cache. That is only sound if Lake evaluates the - // vendored Aeneas package with the same build configuration that was used - // when the archive was produced. + // Aeneas package, and generated verification workspaces require that + // package directly from the installed archive. That is only sound if Lake + // evaluates Aeneas with the same build configuration that was used when the + // archive was produced. // // Aeneas' Lakefile currently makes one of those build settings depend on // the ambient `CI` environment variable: @@ -775,9 +608,8 @@ fn configure_lake_command( // sets `CI=true` for normal workflow steps. If we let that variable reach // this child process, Lake observes a different Aeneas package config than // the one recorded in the archive traces. It then invalidates the prebuilt - // cache and attempts to rebuild/remove files below the symlinked - // `.lake/build`, which fails because those archive files are intentionally - // read-only. + // cache and attempts to rebuild/remove files below the installed archive's + // read-only `.lake/build`. // // Scrubbing `CI` here keeps local runs, example CI jobs, and the integration // test harness aligned with the archive build environment. A cleaner future diff --git a/anneal/src/setup.rs b/anneal/src/setup.rs index ba84910a82..e449f604d3 100644 --- a/anneal/src/setup.rs +++ b/anneal/src/setup.rs @@ -1,8 +1,14 @@ //! Subcommand for installing Anneal dependencies. -use std::{path::PathBuf, process::Command}; +use std::{ + fs, + path::{Path, PathBuf}, + process::Command, + time::SystemTime, +}; -use anyhow::Context as _; +use anyhow::{Context as _, Result}; +use walkdir::WalkDir; pub struct SetupArgs { pub local_archive: Option, @@ -56,7 +62,9 @@ impl Toolchain { let root = CONFIG .resolve_installation_dir(location()) .context("Toolchain not installed. Please run 'cargo anneal setup' first.")?; - Ok(Self { root }) + let toolchain = Self { root }; + toolchain.prepare_lake_packages()?; + Ok(toolchain) } pub fn bin_dir(&self) -> PathBuf { @@ -106,6 +114,12 @@ impl Toolchain { Command::new(tool.path(self)) } } + + fn prepare_lake_packages(&self) -> Result<()> { + let aeneas_root = self.aeneas_root(); + make_lake_config_dirs_writable(&aeneas_root)?; + normalize_lake_input_mtimes(&aeneas_root) + } } pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> { @@ -120,10 +134,115 @@ pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> { let installation_dir = CONFIG .resolve_installation_dir_or_install(location(), source) .context("failed to resolve-or-install dependencies")?; + Toolchain { root: installation_dir.clone() } + .prepare_lake_packages() + .context("failed to prepare Lake package directories")?; log::info!("anneal toolchain is installed at {:?}", installation_dir); Ok(()) } +fn make_lake_config_dirs_writable(root: &Path) -> Result<()> { + if !root.exists() { + return Ok(()); + } + + let mut entries = WalkDir::new(root).into_iter(); + while let Some(entry) = entries.next() { + let entry = entry.with_context(|| format!("Failed to walk {}", root.display()))?; + let path = entry.path(); + + if entry.file_type().is_dir() && is_lake_dir(path) { + ensure_lake_config_dir_writable(path)?; + entries.skip_current_dir(); + } + } + + Ok(()) +} + +fn ensure_lake_config_dir_writable(lake_dir: &Path) -> Result<()> { + let config_dir = lake_dir.join("config"); + if !config_dir.exists() { + let original_permissions = fs::symlink_metadata(lake_dir) + .with_context(|| format!("Failed to stat {}", lake_dir.display()))? + .permissions(); + make_writable(lake_dir)?; + fs::create_dir_all(&config_dir) + .with_context(|| format!("Failed to create {}", config_dir.display()))?; + fs::set_permissions(lake_dir, original_permissions) + .with_context(|| format!("Failed to restore permissions on {}", lake_dir.display()))?; + } + make_tree_writable(&config_dir) +} + +fn make_tree_writable(root: &Path) -> Result<()> { + for entry in WalkDir::new(root) { + let entry = entry.with_context(|| format!("Failed to walk {}", root.display()))?; + make_writable(entry.path())?; + } + Ok(()) +} + +fn make_writable(path: &Path) -> Result<()> { + let metadata = + fs::symlink_metadata(path).with_context(|| format!("Failed to stat {}", path.display()))?; + if metadata.file_type().is_symlink() { + return Ok(()); + } + let mut perms = metadata.permissions(); + if perms.readonly() { + #[allow(clippy::permissions_set_readonly_false)] + perms.set_readonly(false); + fs::set_permissions(path, perms) + .with_context(|| format!("Failed to make {} writable", path.display()))?; + } + Ok(()) +} + +fn is_lake_dir(path: &Path) -> bool { + path.file_name().is_some_and(|name| name == ".lake") +} + +fn normalize_lake_input_mtimes(root: &Path) -> Result<()> { + let mut entries = WalkDir::new(root).into_iter(); + while let Some(entry) = entries.next() { + let entry = entry.with_context(|| format!("Failed to walk {}", root.display()))?; + let path = entry.path(); + + if entry.file_type().is_dir() && is_lake_build_dir(path) { + entries.skip_current_dir(); + continue; + } + + if !entry.file_type().is_file() || !is_lake_input_file(path) { + continue; + } + + let file = fs::File::open(path) + .with_context(|| format!("Failed to open {} to normalize mtime", path.display()))?; + file.set_times(fs::FileTimes::new().set_modified(SystemTime::UNIX_EPOCH)) + .with_context(|| format!("Failed to normalize mtime for {}", path.display()))?; + } + + Ok(()) +} + +fn is_lake_build_dir(path: &Path) -> bool { + path.file_name().is_some_and(|name| name == "build") + && path.parent().and_then(Path::file_name).is_some_and(|name| name == ".lake") +} + +fn is_lake_input_file(path: &Path) -> bool { + if path.extension().and_then(|ext| ext.to_str()) == Some("lean") { + return true; + } + + matches!( + path.file_name().and_then(|name| name.to_str()), + Some("lakefile.lean" | "lakefile.toml" | "lake-manifest.json" | "lean-toolchain") + ) +} + fn location() -> exocrate::Location { if let Some(dir) = std::env::var_os("ANNEAL_TOOLCHAIN_DIR") { exocrate::Location::Custom(PathBuf::from(dir)) @@ -210,4 +329,57 @@ mod tests { PathBuf::from("/tmp/toolchain/aeneas/bin/aeneas") ); } + + #[test] + fn lake_config_fixup_leaves_build_cache_readonly() { + let temp = tempfile::tempdir().unwrap(); + let aeneas_root = temp.path().join("aeneas"); + let source_file = aeneas_root.join("backends/lean/Aeneas.lean"); + let config_file = aeneas_root.join("backends/lean/.lake/config/aeneas/lakefile.olean"); + let build_file = aeneas_root.join("backends/lean/.lake/build/lib/lean/Aeneas.olean"); + let package_lake_dir = aeneas_root.join("packages/MiniDep/.lake"); + + std::fs::create_dir_all(source_file.parent().unwrap()).unwrap(); + std::fs::create_dir_all(config_file.parent().unwrap()).unwrap(); + std::fs::create_dir_all(build_file.parent().unwrap()).unwrap(); + std::fs::create_dir_all(package_lake_dir.join("build")).unwrap(); + std::fs::write(&source_file, "import Aeneas").unwrap(); + std::fs::write(&config_file, "config").unwrap(); + std::fs::write(&build_file, "build").unwrap(); + + make_tree_readonly(&aeneas_root); + Toolchain { root: temp.path().to_path_buf() }.prepare_lake_packages().unwrap(); + + let package_config_dir = package_lake_dir.join("config"); + assert!(package_config_dir.is_dir()); + assert!(!std::fs::metadata(&package_config_dir).unwrap().permissions().readonly()); + assert!( + !std::fs::metadata(config_file.parent().unwrap()).unwrap().permissions().readonly() + ); + assert!(!std::fs::metadata(&config_file).unwrap().permissions().readonly()); + assert!(std::fs::metadata(&build_file).unwrap().permissions().readonly()); + assert_eq!(modified_secs(&source_file), 0); + assert_ne!(modified_secs(&build_file), 0); + + make_tree_writable(&aeneas_root).unwrap(); + } + + fn modified_secs(path: &Path) -> u64 { + std::fs::metadata(path) + .unwrap() + .modified() + .unwrap() + .duration_since(SystemTime::UNIX_EPOCH) + .unwrap() + .as_secs() + } + + fn make_tree_readonly(root: &Path) { + for entry in WalkDir::new(root).contents_first(true) { + let entry = entry.unwrap(); + let mut perms = std::fs::metadata(entry.path()).unwrap().permissions(); + perms.set_readonly(true); + std::fs::set_permissions(entry.path(), perms).unwrap(); + } + } } diff --git a/anneal/v2/flake.nix b/anneal/v2/flake.nix index 7d260ce371..29b47f709a 100644 --- a/anneal/v2/flake.nix +++ b/anneal/v2/flake.nix @@ -445,6 +445,30 @@ "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" + # 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. + "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" + "substituteInPlace $TMPDIR/aeneas-config-primer/lakefile.lean --replace-fail @AENEAS_ROOT@ \"$PWD\"" + "(cd $TMPDIR/aeneas-config-primer && ${runLeanCommand "lake --old build Generated"})" + "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)'" "if find . ../../packages -type f -name \"*.trace\" -exec grep -EIl \"\$TRACE_ABS_RE\" {} + | tee /tmp/non-relocatable-traces | grep -q .; then" @@ -578,6 +602,7 @@ aeneas/bin/aeneas \ aeneas/bin/charon \ aeneas/bin/charon-driver \ + aeneas/backends/lean/.lake/config/aeneas/lakefile.olean \ aeneas/backends/lean/lakefile.lean \ aeneas/packages/mathlib/lake-manifest.json \ aeneas/packages/mathlib/.lake/config/mathlib/lakefile.olean \ diff --git a/anneal/v2/rewrite-lake-vendor.py b/anneal/v2/rewrite-lake-vendor.py index 053d407440..e61fc99283 100755 --- a/anneal/v2/rewrite-lake-vendor.py +++ b/anneal/v2/rewrite-lake-vendor.py @@ -155,6 +155,14 @@ def rewrite_trace_prefixes( ) for name in packages ] + root_package_patterns = [ + # Aeneas release archives can already contain traces produced in an + # upstream staging directory such as + # `/var/lib/.../dist_staging/backends/lean/...`. Those paths are not + # known to Nix, so strip any absolute package-root prefix ending in the + # Aeneas Lean backend layout. + re.compile(r"(?, 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. + +"""Unit tests for rewrite-lake-vendor.py.""" + +from __future__ import annotations + +import importlib.util +import tempfile +import unittest +from pathlib import Path + + +SCRIPT = Path(__file__).resolve().parents[1] / "rewrite-lake-vendor.py" +SPEC = importlib.util.spec_from_file_location("rewrite_lake_vendor", SCRIPT) +assert SPEC is not None and SPEC.loader is not None +rewrite_lake_vendor = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(rewrite_lake_vendor) + + +def write(path: Path, contents: str = "") -> None: + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(contents, encoding="utf-8") + + +class RewriteLakeVendorTests(unittest.TestCase): + def test_rewrites_upstream_aeneas_backend_trace_prefix(self) -> None: + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) / "aeneas" / "backends" / "lean" + packages_dir = Path(tmp) / "aeneas" / "packages" + packages_dir.mkdir(parents=True) + + trace = root / ".lake" / "build" / "lib" / "lean" / "AeneasMeta" / "Utils.trace" + upstream_root = "/var/lib/github-runner-work/aeneas/aeneas/dist_staging/backends/lean" + write( + trace, + f"""{{ + "log": [{{"message": "lean {upstream_root}/AeneasMeta/Utils.lean"}}], + "inputs": [["{upstream_root}/AeneasMeta/Utils.lean", "cfad31626f87a3ad"]] +}} +""", + ) + + count = rewrite_lake_vendor.rewrite_trace_prefixes( + root=root, + packages_dir=packages_dir, + packages={}, + extra_prefixes=[], + ) + + self.assertEqual(count, 1) + rewritten = trace.read_text(encoding="utf-8") + self.assertNotIn("/var/lib", rewritten) + self.assertNotIn("backends/lean", rewritten) + self.assertIn("AeneasMeta/Utils.lean", rewritten) + + +if __name__ == "__main__": + unittest.main() diff --git a/june_5-7_joshlf_changes_summary.md b/june_5-7_joshlf_changes_summary.md new file mode 100644 index 0000000000..1ae993fe65 --- /dev/null +++ b/june_5-7_joshlf_changes_summary.md @@ -0,0 +1,177 @@ +# June 5-7 @joshlf Anneal Changes + +This summary covers the Anneal-related work that landed or was pushed during +June 5-7, 2026. There were two distinct streams of activity: + +1. `@joshlf` merged mainline PRs that move Anneal v1 setup and CI onto the + Nix-built toolchain archive path. +2. `@joshlf` force-pushed amended commits onto `@mdittmer`'s open Anneal v2 PR + stack. Those commits still list Mark as author, but Joshua as committer. + +## Source Links + +Mainline source at `origin/main` commit `83dbc577c`: + +- Anneal v1 setup: +- Anneal v1 Aeneas/Lake materialization and symlink handling: +- Anneal v1 `lake --old` invocation: +- Anneal v1 exocrate metadata: +- Anneal v1 build-time metadata export: +- Shared exocrate installer: +- Anneal v2 Nix archive build: +- Anneal v2 Lake vendor rewriting: +- Anneal v2 cache pruning: +- Anneal CI workflow: +- Anneal release workflow: + +Relevant PRs: + +- - `[anneal] Move setup and CI onto Nix archive` +- - `[anneal][release] Add exocrate archive metadata helpers` +- - `[anneal][release] Publish Nix-built toolchain archives` +- - `[anneal] Keep vendored Lake inputs older than archive caches` +- - `[anneal][v2] Stabilize Nix omnibus archive builds` +- - `[anneal][release] Upload toolchain archives before publishing release` +- - `Release Anneal 0.1.0-alpha.24` + +Open `@mdittmer` v2 stack amended by `@joshlf`: + +- - `[anneal][v2] Add Cargo dependencies` +- - `[anneal][v2] Add utility functions: environment helpers and DirLock` +- - `[anneal][v2] Add exocrate toolchain setup and Toolchain resolver` +- - `[anneal][v2] Add Cargo workspace resolution and target resolution logic` +- - `[anneal][v2] Add scanner module to map workspace packages to AnnealArtifacts` +- - `[anneal][v2] Add DiagnosticMapper to map compiler errors back to Rust source code` +- - `[anneal][v2] Add charon execution engine, expand command CLI, and integration tests` +- - `[anneal][v2] Implement out-of-tree dependency chasing for expand command` +- - `[anneal][v2] Add pinned charon_lib dependency` +- - `[anneal][v2][exocrate] Add install fixup hook` + +## What Landed On Main + +### v1 setup now consumes the Nix-built archive + +PR #3438 replaced the older v1 setup path with an exocrate-backed installer. +The v1 `setup` command now resolves a versioned toolchain directory under +`.anneal/toolchain` using metadata generated from `Cargo.toml`, `Cargo.lock`, +and the host platform. The archive layout is shared with the v2 Nix build: +`aeneas`, `lean`, `rust`, and the Lake cache live under the installed +toolchain root. + +This makes v1 setup behave more like v2: CI first builds or downloads the same +Nix-produced archive, then v1 installs it with: + +```text +cargo run --features __install_exocrate -- setup --local-archive ... +``` + +The important shift is that v1 no longer has a bespoke setup path that fetches +and arranges Aeneas, Lean, Rust, and Lake artifacts separately. It consumes the +same archive shape produced by the v2 flake. + +### v2 owns the archive construction + +PR #3444 stabilized the v2 Nix archive build. The flake now does the heavy +assembly work: + +- downloads platform-specific Aeneas, Rust, Lean, and `leantar` inputs; +- downloads and unpacks the Mathlib cache; +- rewrites Lake dependencies to path dependencies; +- seeds package `.lake/build` directories with cache artifacts; +- rewrites trace files so absolute Nix and checkout paths do not leak into the + final bundle; +- prunes unused Mathlib artifacts; +- runs layout and relocatability checks; and +- emits a portable `anneal-exocrate.tar.zst` archive. + +In effect, v2 is now the build-system owner for the toolchain bundle consumed +by both v2 and v1. + +### Release automation now publishes those archives + +PRs #3440, #3441, #3445, and #3446 added and exercised release support for the +Nix-built archives: + +- #3440 added archive metadata helpers. +- #3441 taught the release workflow to build and publish toolchain archives. +- #3445 changed ordering so the toolchain archives are uploaded before the + crate release metadata is finalized. +- #3446 released `anneal` `0.1.0-alpha.24`, with `Cargo.toml` pointing to the + published platform archives and expected SHA-256 values. + +### CI now fans out from one archive build + +The Anneal GitHub workflow now builds the Nix archive in a dedicated job and +uses it for v1 setup/tests and examples. The workflow also restores/saves Nix +caches and performs archive size/layout checks. This is a real simplification +for CI topology: the expensive archive build is centralized instead of being +implicitly reconstructed by every consumer job. + +## What Was Pushed Onto Mark's v2 PR Stack + +On June 7, `@joshlf` force-pushed amended commits onto Mark's open v2 PR stack. +The latest commits are still authored by Mark but were committed by Joshua. +The notable changes are: + +- #3398 was changed from checked-in vendored Cargo dependencies to normal Cargo + dependencies/lockfile updates. The giant `anneal/v2/vendor` approach was + removed from that PR. +- #3418 likewise changed from vendoring `charon_lib` to adding a pinned + dependency. +- #3399 through #3403 were mostly rebased with little or no patch-level change. +- #3404 gained feature-gating around exocrate-heavy tests and minor cleanup in + the Charon/integration-test area. +- #3405 kept the out-of-tree dependency chasing work, but simplified one + integration fixture by generating a small synthetic `log` path dependency + instead of copying/truncating a real vendored crate. The current commit notes + that some generated test plumbing still deserves review. +- #3436 moved the install fixup hook out of v2-specific setup code and into the + shared top-level `exocrate` crate, because the installer is now shared by v1 + and v2 archive consumers. + +The direction of these changes is consistent: avoid checking huge generated +vendor trees into the v2 Rust crate, keep archive construction in Nix, and move +installation behavior into the common exocrate layer. + +## v1's Extra Complications + +The new v1 setup path consumes the v2-style archive, but v1 still cannot simply +point Lake at the installed read-only archive in place. v1 generates a fresh +Lean workspace for each target Rust crate, and that generated workspace needs +path dependencies to Aeneas and its vendored Lake packages. + +The current bridge is manual tree materialization: + +- v1 copies Aeneas Lean sources and package metadata from the installed + toolchain into the generated workspace; +- it preserves ordinary symlinks while copying; +- when it reaches a Lake build directory, it creates a symlink from the + generated workspace back to the installed toolchain's `.lake/build` cache + rather than copying several GiB of `.olean` and trace data; +- it makes copied files writable; and +- it normalizes Lake input mtimes to the Unix epoch and runs `lake --old`. + +The mtime normalization plus `lake --old` keep Lake from deciding that the +copied inputs are newer than the prebuilt artifacts. The symlinked +`.lake/build` directories avoid the cost and disk usage of copying the Nix-built +cache into every generated v1 workspace. + +That is the main complexity retained or reintroduced for v1: the archive is +built in a Nix/v2 style, but v1 still materializes a per-invocation workspace +and manually symlinks build-cache directories back to the shared installed +archive. + +## Relationship To The Symlink Question + +The v2 flake already demonstrates a cleaner model at archive-build time: create +path dependencies, seed their `.lake/build` directories with valid artifacts, +rewrite traces to portable paths, prune what is not needed, and freeze inputs so +Lake does not rebuild. The v1 implementation uses the result of that process, +but then reconstructs enough of the dependency tree inside each generated +workspace that it needs manual symlinks to avoid copying the expensive cache. + +The open question for the June 8 investigation is whether v1 can instead +generate a workspace that directly uses a symlink-free, portable, prebuilt +package layout. The goal would be to preserve the performance benefits of +shared cache artifacts while removing per-run symlink management from the Rust +setup/build path. diff --git a/june_8_anneal_build_and_setup_investigation.md b/june_8_anneal_build_and_setup_investigation.md new file mode 100644 index 0000000000..77f0ca3b7c --- /dev/null +++ b/june_8_anneal_build_and_setup_investigation.md @@ -0,0 +1,208 @@ +# June 8 Anneal Build And Setup Investigation + +## Summary + +The v1 symlink complexity is avoidable. A small reproducible Lake experiment in +`micro-lake-experiments/` verifies a symlink-free strategy that matches the v2 +archive design: + +- keep the installed archive as the single copy of Aeneas and its Lake path + dependencies; +- have generated v1 workspaces require Aeneas directly from the installed + archive; +- keep archive `.lake/build` artifacts read-only and shared; +- make only tiny archive `.lake/config` directories writable so Lake can take + package config locks; and +- remove per-workspace copying and `.lake/build` symlinking. + +The experiment also verified the important negative case: a completely +read-only direct archive fails because Lake tries to create a lock file under +the dependency package's `.lake/config` directory. + +## Existing v1 Behavior + +Current v1 consumes the v2-style archive, but then reconstructs much of the +archive layout inside each generated Lean workspace: + +1. Copy `aeneas/backends/lean` from the installed toolchain into + `lean/vendor/aeneas/backends/lean`. +2. Copy `aeneas/packages` into `lean/vendor/aeneas/packages`. +3. Preserve ordinary symlinks. +4. Replace copied package `.lake/build` directories with symlinks back to the + installed archive's `.lake/build` directories. +5. Make copied files writable. +6. Normalize copied Lake input mtimes to the Unix epoch. +7. Run `lake --old build Generated Anneal`. + +The symlinks avoid copying several GiB of prebuilt `.olean` artifacts into each +generated workspace. The mtime normalization exists because copied source/config +files would otherwise be newer than the read-only archive build cache, causing +Lake to invalidate or delete artifacts through those symlinks. + +## How This Maps To v2 + +The v2 `flake.nix` already prepares most of the desired archive state: + +- dependencies are vendored as path packages under `aeneas/packages`; +- package `.lake/build` directories are seeded with prebuilt cache artifacts; +- Lake requirements and manifests are rewritten to path dependencies; +- trace paths are rewritten to avoid non-portable absolute Nix/build paths; +- source/config mtimes are normalized before `lake --old build`; +- unused artifacts are pruned; and +- the final archive is made read-only. + +The gap is not `.lake/build`. The gap is Lake's package configuration area. +When a generated workspace requires `aeneas/backends/lean` directly as a path +dependency, Lake creates or locks files under: + +```text +aeneas/backends/lean/.lake/config/aeneas/ +``` + +A fully read-only archive therefore fails before it can replay the already +valid `.lake/build` artifacts. + +## New Experiment + +I added: + +```text +../micro-lake-experiments/experiments/test-symlink-free-toolchain-path.sh +../micro-lake-experiments/artifacts/symlink_free_toolchain_path_analysis.md +``` + +The script builds a small Anneal-shaped archive fixture: + +```text +archive/ + aeneas/ + backends/lean/ # package "aeneas" + packages/MiniDep/ # transitive path dependency +``` + +It then: + +1. prebuilds the archive packages; +2. rewrites traces to package-relative paths; +3. primes Lake package config while the archive is writable; +4. makes the archive fully read-only; +5. verifies the fully read-only negative control fails on + `.lake/config/aeneas/lakefile.olean.lock`; +6. makes only `.lake/config` writable; +7. builds two generated workspaces at different paths that require Aeneas + directly from the archive; and +8. verifies there are no symlinks and no generated-workspace vendor copies. + +The successful builds replayed prebuilt archive artifacts: + +```text +Replayed MiniDep.Basic +Replayed Aeneas +Built Generated +``` + +Post-run checks: + +- writable files under archive `.lake/build`: `0` +- symlinks under the test fixture: `0` +- writable paths under archive `.lake/config`: `8` +- generated workspace vendor directory: absent + +## Implemented v1 Fix + +The implementation follows the experiment, with two extra fixes discovered by +running a real v1 example against the Nix-built archive: + +1. The v2 archive build primes Aeneas package config for dependency use before + final archive packaging. +2. The v2 trace rewriter strips upstream Aeneas release trace prefixes ending + in `backends/lean/`. Without this, Aeneas traces retained paths such as + `/var/lib/.../dist_staging/backends/lean/AeneasMeta/Utils.lean`, and v1 + invalidated the archive cache. +3. Setup/install restores write permission to archive `.lake/config` + directories and creates missing config dirs for older installed archives. +4. Setup/install normalizes Lean/Lake source/config input mtimes to the Unix + epoch while leaving `.lake/build` artifacts read-only. +5. v1 `aeneas.rs` writes `require aeneas from + "/aeneas/backends/lean"` directly. +6. v1 no longer copies `aeneas/backends/lean` or `aeneas/packages` into the + generated workspace. +7. v1 no longer creates `.lake/build` symlinks. +8. v1 no longer preserves `lake-manifest.json` across workspace regeneration, + because the direct Aeneas dependency path includes the active setup + location. Preserving the manifest can point Lake at a stale toolchain root. + +This should reduce v1 complexity and improve setup/build behavior: + +- no per-run tree copy of Aeneas and packages; +- no symlink creation or symlink portability concerns; +- no per-run mtime mutation of copied package inputs; +- no large cache copy; +- package artifacts are still replayed from the shared installed archive; and +- only generated project files are built in each v1 workspace. + +## Real Archive Verification + +The full Nix archive path was verified after implementation: + +```text +nix build ./anneal/v2#omnibus-archive-layout-check --print-build-logs +``` + +This built the local archive, replayed Aeneas in the config-primer workspace, +rewrote traces, pruned Mathlib, compressed the archive, and passed the updated +layout check requiring: + +```text +aeneas/backends/lean/.lake/config/aeneas/lakefile.olean +``` + +Setup was then tested against the built archive: + +```text +ANNEAL_TOOLCHAIN_DIR=/tmp/anneal-toolchain-test... \ +cargo run --manifest-path anneal/Cargo.toml -- \ + setup --local-archive /nix/store/...-anneal-toolchain-omnibus-0.1.0 +``` + +Observed setup properties: + +- setup time: about 48 seconds for the 1.35 GiB archive; +- writable files under installed archive `.lake/build`: `0`; +- installed archive source input mtime: Unix epoch; +- installed archive build artifact mtime: preserved archive timestamp; +- `aeneas/backends/lean/.lake/config/aeneas` writable: yes. + +The `checked_add` example then verified successfully: + +```text +ANNEAL_TOOLCHAIN_DIR=/tmp/anneal-toolchain-test... \ +cargo run --manifest-path anneal/Cargo.toml -- \ + verify --manifest-path anneal/Cargo.toml --example checked_add --allow-sorry +``` + +First successful run after the fixes took about 13 seconds. A second run took +about 6.6 seconds. The generated workspace had: + +- no `vendor/` directory; +- no symlinks; and +- a generated `lakefile.lean` requiring Aeneas directly from the installed + archive path. + +Additional checks run: + +```text +python3 -m unittest discover -s anneal/v2/tests -p 'test_*.py' +cargo test --manifest-path anneal/Cargo.toml setup::tests -- --nocapture +cargo test --manifest-path anneal/Cargo.toml --bin cargo-anneal +bash anneal/v2/check-flake-eval.sh +``` + +## Remaining Verification + +The implementation is now tested against both tiny packages and the full local +Nix archive. Remaining useful checks are broader rather than blocking: + +- concurrent v1 runs, since the installed archive will have a small shared + writable `.lake/config` surface; and +- full GitHub workflow validation across all runner platforms. diff --git a/june_8_improve-anneal-for-playground/findings.md b/june_8_improve-anneal-for-playground/findings.md new file mode 100644 index 0000000000..3bfd8b3a65 --- /dev/null +++ b/june_8_improve-anneal-for-playground/findings.md @@ -0,0 +1,132 @@ +# rust-anneal-playground investigation + +## Project wiring + +`platonicsock/rust-anneal-playground` is a fork of the Rust Playground. The +Anneal integration is intentionally thin: + +- The frontend sends the execution-tool value `anneal-verify`. +- The Axum server parses that into `ExecutionTool::AnnealVerify`. +- The orchestrator maps it to `cargo anneal verify`. +- `compiler/base/Dockerfile` currently installs `cargo-anneal` version + `0.1.0-alpha.23` and runs `cargo anneal setup` while building the compiler + image. + +The relevant source locations in the playground checkout are: + +- `ui/frontend/actions.ts`: `performCargoAnnealOnly` +- `ui/src/server_axum.rs`: `parse_execution_tool` +- `compiler/base/orchestrator/src/coordinator.rs`: `ExecutionTool::AnnealVerify` +- `compiler/base/Dockerfile`: `cargo install --locked cargo-anneal --version 0.1.0-alpha.23` + +HTTP requests build a fresh coordinator and shut it down at the end of the +request. WebSocket sessions keep a coordinator alive for the session/idle +window, so repeated requests in one live session can reuse the same compiler +container. + +## Reproduction + +I reproduced the workflow with a single-file playground crate containing the +`checked_add` Anneal example. I compared two manifests: + +- `minimal`: a tiny `Cargo.toml` with only the `playground` package. +- `playground`: a copy of `compiler/base/Cargo.toml`, which is the real + playground top-crates manifest. + +The reproducer is `reproduce_playground_workflows.sh`. It creates both crates, +runs `cargo metadata`, `cargo-anneal generate`, and `cargo-anneal verify`, and +captures stdout/stderr/timings under `results/`. + +Manual probe timings from this machine: + +| Case | Elapsed | Key trace time | +| --- | ---: | --- | +| minimal `cargo metadata --no-deps` | 0.01s | n/a | +| playground `cargo metadata --no-deps` | 0.02s | n/a | +| minimal `generate` | 0.70s | Charon 0.13s, Aeneas 0.39s | +| minimal first `verify` | 11.99s | Charon 0.09s, Aeneas 0.39s, Lake 8.11s | +| minimal second `verify` | 6.27s | Charon 0.09s, Aeneas 0.39s, Lake 2.38s | +| playground first `generate` | 37.99s | Charon 32.99s, Aeneas 0.39s | +| playground second `generate` | 1.50s | Charon 0.49s, Aeneas 0.39s | +| playground warm `verify` | 12.56s | Charon 0.49s, Aeneas 0.39s, Lake 7.88s | +| direct Lake build with no rewrite | 0.81s | no Anneal regeneration | +| `lake env true` | 0.40s | Lake environment startup only | +| direct `lean --json` diagnostics | 3.13s | with cached `LEAN_PATH` | + +The first playground-manifest run created a `target/anneal/cargo_target` tree of +about 2.8 GiB with hundreds of compiled dependency artifacts. The second run was +fast because that private Anneal target tree was warm. + +## Bottlenecks + +The playground-specific slowdown is not Aeneas. Aeneas stayed near 0.4s in all +small-code experiments. + +The large first-run cost is Charon invoking Cargo against the real playground +manifest. Even though Charon receives `--start-from crate::checked_add`, Cargo +still has to prepare the package dependency graph described by +`compiler/base/Cargo.toml`. Anneal v1 deliberately sets `CARGO_TARGET_DIR` to +`target/anneal/cargo_target`, so this work does not use the normal +`/playground/target` directory built by the playground Dockerfile. + +Using the normal target directory is not an obvious Anneal fix. The Anneal +toolchain's Rust is `rustc 1.98.0-nightly (2026-05-30)` in this local archive, +while the playground compiler image builds ordinary Rust artifacts using its +selected stable/beta/nightly channel. Cargo fingerprints are toolchain-sensitive, +so the existing prebuilt `/playground/target` artifacts are not guaranteed to be +reusable by Charon. Mixing Anneal's Rust artifacts into the ordinary playground +target directory would also make the normal Rust Playground paths noisier. + +The Lean-side floor for this example is roughly 4-5 seconds when dependencies +are warm: + +- `lake build` with no regenerated sources is under 1s. +- `lake env lean --json` diagnostics are around 3s. +- `lake env` startup itself is only about 0.4s, so replacing `lake env lean` + with direct `lean --json` plus cached `LEAN_PATH` is not a major win. + +Current Anneal regeneration swaps in a fresh Lean source tree each run, so Lake +does more work than the no-rewrite case even when generated files are identical. +Preserving mtimes for unchanged generated Lean files would likely save around +1-2s on repeated identical runs. That is a modest win and adds implementation +complexity; it is not the main playground bottleneck. + +## Recommended playground-side changes + +The cleanest high-impact fix is in the playground image/build strategy: + +- During the compiler image build, after `cargo anneal setup`, run an Anneal + command against the real `compiler/base/Cargo.toml` with a tiny annotated + `src/main.rs`. `cargo anneal generate` is enough to warm Charon/Cargo without + paying the Lake proof build. +- Keep the resulting `target/anneal/cargo_target` in the image. This moves the + 30s-plus first Charon/Cargo cost from user request latency to image build + time. +- Use WebSocket execution for interactive sessions where possible, because a + live session can reuse the same coordinator/container and its warmed + `target/anneal` tree. + +The Dockerfile already runs `cargo build`, `cargo build --release`, and +`cargo clippy` to prewarm the ordinary Rust Playground cache. Anneal needs an +analogous prewarm for its private `target/anneal/cargo_target`. + +## Anneal v1 changes + +I did not find a concrete, clean, complexity-reducing Anneal v1 code change to +commit for this task. + +The already-pushed symlink-free setup branch helps the playground indirectly by +removing per-run vendor copies/symlinks and making archive setup simpler, but it +does not change the main playground bottleneck: the first Charon/Cargo run over +the full top-crates manifest in a cold Anneal target directory. + +Potential Anneal improvements exist, but they are not obvious fixes to push from +this investigation: + +- Preserving mtimes for unchanged generated Lean files could shave repeated + verify runs by roughly 1-2s. +- Caching `LEAN_PATH` and invoking `lean --json` directly instead of + `lake env lean --json` saves at most a few tenths of a second in this probe. +- A standalone/non-Cargo extraction mode could be very fast for snippets with no + external crates, but preserving correctness for arbitrary playground code that + may use top-crates dependencies would require a new design. diff --git a/june_8_improve-anneal-for-playground/reproduce_playground_workflows.sh b/june_8_improve-anneal-for-playground/reproduce_playground_workflows.sh new file mode 100755 index 0000000000..6473a28f40 --- /dev/null +++ b/june_8_improve-anneal-for-playground/reproduce_playground_workflows.sh @@ -0,0 +1,229 @@ +#!/usr/bin/env bash +set -euo pipefail + +SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" +ZEROCOPY_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)" +WORKSPACE_ROOT="$(cd "$ZEROCOPY_ROOT/.." && pwd)" +if [[ -z "${PLAYGROUND_ROOT:-}" ]]; then + PLAYGROUND_ROOT="" + for candidate in \ + "$WORKSPACE_ROOT/rust-anneal-playground" \ + "$ZEROCOPY_ROOT/../rust-anneal-playground" \ + "$PWD/../rust-anneal-playground" \ + /usr/local/google/Projects/workspaces-open/*/rust-anneal-playground + do + if [[ -d "$candidate" ]]; then + PLAYGROUND_ROOT="$candidate" + break + fi + done +fi +ANNEAL_BIN="${ANNEAL_BIN:-$ZEROCOPY_ROOT/anneal/target/debug/cargo-anneal}" +RESULT_DIR="${RESULT_DIR:-$SCRIPT_DIR/results/$(date -u +%Y%m%dT%H%M%SZ)}" +VERIFY_TIMEOUT="${VERIFY_TIMEOUT:-180}" +RUN_FULL_PLAYGROUND="${RUN_FULL_PLAYGROUND:-1}" + +if [[ ! -d "$PLAYGROUND_ROOT" ]]; then + echo "PLAYGROUND_ROOT does not exist: $PLAYGROUND_ROOT" >&2 + echo "Clone https://github.com/platonicsock/rust-anneal-playground next to zerocopy, or set PLAYGROUND_ROOT." >&2 + exit 1 +fi + +if [[ ! -x "$ANNEAL_BIN" ]]; then + cargo build --manifest-path "$ZEROCOPY_ROOT/anneal/Cargo.toml" --bin cargo-anneal +fi + +if [[ -z "${ANNEAL_TOOLCHAIN_DIR:-}" ]]; then + if [[ -d "$ZEROCOPY_ROOT/anneal/target/anneal-toolchain" ]]; then + export ANNEAL_TOOLCHAIN_DIR="$ZEROCOPY_ROOT/anneal/target/anneal-toolchain" + else + echo "ANNEAL_TOOLCHAIN_DIR is not set and no local anneal/target/anneal-toolchain was found." >&2 + echo "Run cargo anneal setup first, or set ANNEAL_TOOLCHAIN_DIR to an installed toolchain parent." >&2 + exit 1 + fi +fi + +mkdir -p "$RESULT_DIR" +WORK_DIR="$RESULT_DIR/work" +mkdir -p "$WORK_DIR" +TIMINGS="$RESULT_DIR/timings.tsv" +printf 'case\tstatus\telapsed_hms\telapsed_seconds\n' > "$TIMINGS" + +write_checked_add() { + local dst="$1" + mkdir -p "$(dirname "$dst")" + cat > "$dst" <<'RS' +/// Performs checked addition. +/// +/// ```lean, anneal, spec +/// ensures: match ret with +/// | .none => (x : Int) + (y : Int) > I32.max \/ (x : Int) + (y : Int) < I32.min +/// | .some v => (v : Int) = (x : Int) + (y : Int) +/// proof (h_anon): +/// unfold checked_add at h_returns +/// have h := Aeneas.Std.I32.checked_add_bv_spec x y +/// simp_all [Aeneas.Std.I32.checked_add] +/// cases ret <;> simp_all <;> scalar_tac +/// proof (h_progress): +/// unfold checked_add +/// simp_all +/// ``` +pub fn checked_add(x: i32, y: i32) -> Option { + x.checked_add(y) +} + +fn main() {} +RS +} + +make_minimal_project() { + local project="$1" + mkdir -p "$project/src" + cat > "$project/Cargo.toml" <<'TOML' +[package] +name = "playground" +version = "0.0.1" +edition = "2021" +TOML + write_checked_add "$project/src/main.rs" +} + +make_playground_project() { + local project="$1" + mkdir -p "$project/src" + python3 - "$PLAYGROUND_ROOT/compiler/base/Cargo.toml" "$project/Cargo.toml" <<'PY' +import pathlib +import sys + +src = pathlib.Path(sys.argv[1]) +dst = pathlib.Path(sys.argv[2]) +text = src.read_text() +package_header = text.split("[profile.dev]", 1)[0] +if "edition =" not in package_header: + text = text.replace( + 'authors = ["The Rust Playground"]\n', + 'authors = ["The Rust Playground"]\nedition = "2021"\n', + 1, + ) +dst.write_text(text) +PY + write_checked_add "$project/src/main.rs" +} + +run_timed() { + local name="$1" + shift + local stdout="$RESULT_DIR/$name.stdout" + local stderr="$RESULT_DIR/$name.stderr" + local timefile="$RESULT_DIR/$name.time" + printf '%q ' "$@" > "$RESULT_DIR/$name.command" + printf '\n' >> "$RESULT_DIR/$name.command" + + set +e + /usr/bin/time -f 'elapsed_hms=%E +elapsed_seconds=%e' -o "$timefile" timeout "$VERIFY_TIMEOUT" "$@" >"$stdout" 2>"$stderr" + local status=$? + set -e + + local elapsed_hms elapsed_seconds + elapsed_hms="$(sed -n 's/^elapsed_hms=//p' "$timefile" | tail -1)" + elapsed_seconds="$(sed -n 's/^elapsed_seconds=//p' "$timefile" | tail -1)" + printf '%s\t%s\t%s\t%s\n' "$name" "$status" "$elapsed_hms" "$elapsed_seconds" >> "$TIMINGS" +} + +extract_trace_times() { + local file="$1" + if [[ -f "$file" ]]; then + grep -E "Charon for|Aeneas for|'lake build' took" "$file" || true + fi +} + +minimal="$WORK_DIR/minimal" +playground="$WORK_DIR/playground" +make_minimal_project "$minimal" +make_playground_project "$playground" + +run_timed metadata_minimal cargo metadata --format-version 1 --manifest-path "$minimal/Cargo.toml" --no-deps +run_timed minimal_generate env ANNEAL_TOOLCHAIN_DIR="$ANNEAL_TOOLCHAIN_DIR" RUST_LOG=trace "$ANNEAL_BIN" generate --manifest-path "$minimal/Cargo.toml" +run_timed minimal_verify_1 env ANNEAL_TOOLCHAIN_DIR="$ANNEAL_TOOLCHAIN_DIR" RUST_LOG=trace "$ANNEAL_BIN" verify --manifest-path "$minimal/Cargo.toml" +run_timed minimal_verify_2 env ANNEAL_TOOLCHAIN_DIR="$ANNEAL_TOOLCHAIN_DIR" RUST_LOG=trace "$ANNEAL_BIN" verify --manifest-path "$minimal/Cargo.toml" + +if [[ "$RUN_FULL_PLAYGROUND" = "1" ]]; then + run_timed metadata_playground cargo metadata --format-version 1 --manifest-path "$playground/Cargo.toml" --no-deps + run_timed playground_generate_1 env ANNEAL_TOOLCHAIN_DIR="$ANNEAL_TOOLCHAIN_DIR" RUST_LOG=trace "$ANNEAL_BIN" generate --manifest-path "$playground/Cargo.toml" + run_timed playground_generate_2 env ANNEAL_TOOLCHAIN_DIR="$ANNEAL_TOOLCHAIN_DIR" RUST_LOG=trace "$ANNEAL_BIN" generate --manifest-path "$playground/Cargo.toml" + run_timed playground_verify_warm env ANNEAL_TOOLCHAIN_DIR="$ANNEAL_TOOLCHAIN_DIR" RUST_LOG=trace "$ANNEAL_BIN" verify --manifest-path "$playground/Cargo.toml" + + lean_root="$(find "$playground/target/anneal" -mindepth 2 -maxdepth 2 -type d -name lean | head -1 || true)" + toolchain_root="$(find "$ANNEAL_TOOLCHAIN_DIR/.anneal/toolchain" -mindepth 1 -maxdepth 1 -type d | head -1 || true)" + if [[ -n "$lean_root" && -n "$toolchain_root" ]]; then + lake_env=( + env -u CI + "LEAN_SYSROOT=$toolchain_root/lean" + "MATHLIB_NO_CACHE_ON_UPDATE=1" + "LAKE_CACHE_DIR=$toolchain_root/lake-cache" + "PATH=$toolchain_root/lean/bin:$PATH" + "LD_LIBRARY_PATH=$toolchain_root/lean/lib:$toolchain_root/lean/lib/lean:${LD_LIBRARY_PATH:-}" + ) + run_timed playground_manual_lake_no_rewrite \ + bash -c 'cd "$1" && shift && "$@" --keep-toolchain --old build Generated Anneal' \ + bash "$lean_root" "${lake_env[@]}" "$toolchain_root/lean/bin/lake" + run_timed playground_lake_env_true \ + bash -c 'cd "$1" && shift && "$@" --keep-toolchain env true' \ + bash "$lean_root" "${lake_env[@]}" "$toolchain_root/lean/bin/lake" + + specs="$(find "$lean_root/generated" -name 'Playground*.lean' | head -1 || true)" + if [[ -n "$specs" ]]; then + "${lake_env[@]}" "$toolchain_root/lean/bin/lake" --keep-toolchain env printenv LEAN_PATH > "$RESULT_DIR/playground.LEAN_PATH" + lean_path="$(cat "$RESULT_DIR/playground.LEAN_PATH")" + run_timed playground_direct_lean_diagnostics \ + env -u CI "LEAN_SYSROOT=$toolchain_root/lean" "LEAN_PATH=$lean_path" \ + "MATHLIB_NO_CACHE_ON_UPDATE=1" "LAKE_CACHE_DIR=$toolchain_root/lake-cache" \ + "PATH=$toolchain_root/lean/bin:$PATH" \ + "LD_LIBRARY_PATH=$toolchain_root/lean/lib:$toolchain_root/lean/lib/lean:${LD_LIBRARY_PATH:-}" \ + "$toolchain_root/lean/bin/lean" --json "$specs" + fi + fi +fi + +{ + echo "# Playground Workflow Results" + echo + echo "- Result directory: $RESULT_DIR" + echo "- Playground root: $PLAYGROUND_ROOT" + echo "- Anneal binary: $ANNEAL_BIN" + echo "- Anneal toolchain parent: $ANNEAL_TOOLCHAIN_DIR" + echo "- Timeout per command: ${VERIFY_TIMEOUT}s" + echo + echo "## Timings" + echo + echo '```tsv' + cat "$TIMINGS" + echo '```' + echo + echo "## Trace Times" + echo + for f in "$RESULT_DIR"/*.stderr; do + base="$(basename "$f")" + if extract_trace_times "$f" >/tmp/anneal-trace-times.$$; then + if [[ -s /tmp/anneal-trace-times.$$ ]]; then + echo "### $base" + echo + echo '```text' + cat /tmp/anneal-trace-times.$$ + echo '```' + echo + fi + fi + rm -f /tmp/anneal-trace-times.$$ + done + if [[ -d "$playground/target" ]]; then + echo "## Playground Target Size" + echo + echo '```text' + du -sh "$playground/target" "$playground/target/anneal/cargo_target" 2>/dev/null || true + echo '```' + fi +} > "$RESULT_DIR/summary.md" + +echo "$RESULT_DIR"