[anneal][v2] Add and integrate nix-built exocrate by mdittmer · Pull Request #3383 · google/zerocopy

mdittmer · 2026-05-19T20:18:04Z

Add nix derivations for exocrate
Add setup sub-command to locate-or-install exocrate
Add integration test for "developer mode" setup that presumes local
exocrate archive
Add github workflows to:
- Warm nix cache
- Locally link exocrate archive from nix, then run all tests

Latest Update: v19 — Compare vs v18

📚 Full Patch History

Links show the diff between the row version and the column version.

Version	v18	v17	v16	v15	v14	v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v19	v18	v17	v16	v15	v14	v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v18		v17	v16	v15	v14	v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v17			v16	v15	v14	v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v16				v15	v14	v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v15					v14	v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v14						v13	v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v13							v12	v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v12								v11	v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v11									v10	v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v10										v9	v8	v7	v6	v5	v4	v3	v2	v1	Base
v9											v8	v7	v6	v5	v4	v3	v2	v1	Base
v8												v7	v6	v5	v4	v3	v2	v1	Base
v7													v6	v5	v4	v3	v2	v1	Base
v6														v5	v4	v3	v2	v1	Base
v5															v4	v3	v2	v1	Base
v4																v3	v2	v1	Base
v3																	v2	v1	Base
v2																		v1	Base
v1																			Base

⬇️ Download this PR

Branch

git fetch origin refs/heads/Gwhroikc5idscowxamayknlke2uiddzv3 && git checkout -b pr-Gwhroikc5idscowxamayknlke2uiddzv3 FETCH_HEAD

Checkout

git fetch origin refs/heads/Gwhroikc5idscowxamayknlke2uiddzv3 && git checkout FETCH_HEAD

Cherry Pick

git fetch origin refs/heads/Gwhroikc5idscowxamayknlke2uiddzv3 && git cherry-pick FETCH_HEAD

Pull

git pull origin refs/heads/Gwhroikc5idscowxamayknlke2uiddzv3

Stacked PRs enabled by GHerrit.

codecov-commenter · 2026-05-19T20:20:42Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 91.85%. Comparing base (5fc5d5b) to head (1da6e9a).
⚠️ Report is 2 commits behind head on main.

Additional details and impacted files

@@            Coverage Diff             @@
##             main    #3383      +/-   ##
==========================================
+ Coverage   91.84%   91.85%   +0.01%     
==========================================
  Files          20       20              
  Lines        6080     6093      +13     
==========================================
+ Hits         5584     5597      +13     
  Misses        496      496

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

joshlf · 2026-05-20T00:05:10Z


+use clap::Parser as _;
+
+/// Anneal: A Literate Verification Toolchain


Suggested change

/// Anneal: A Literate Verification Toolchain

/// Anneal

I suspect we're going to move away from the "literate verification" phrase, which I've found confuses ~everybody

You edited the wrong src/main.rs 😛

joshlf · 2026-05-20T00:12:44Z

TODO(joshlf): Review this file

mdittmer · 2026-05-20T00:54:04Z

@joshlf I don't know enough about action permissions to know whether these are unneeded. If they are needed, I'm not sure the most sensible prose to explain why in this context.

joshlf · 2026-05-25T18:59:00Z

+        uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1
+
+      - name: Run Magic Nix Cache
+        uses: DeterminateSystems/magic-nix-cache-action@main # zizmor: ignore[unpinned-uses]


Can we pin this?

joshlf · 2026-05-25T18:59:03Z

+        uses: DeterminateSystems/determinate-nix-action@441b9e401ac050c38a07d8313748c5c2d17e8aff # v3.6.1
+
+      - name: Run Magic Nix Cache
+        uses: DeterminateSystems/magic-nix-cache-action@main # zizmor: ignore[unpinned-uses]


Can we pin this?

joshlf · 2026-05-25T19:00:52Z

+      # to maintain the principle of least privilege.
+      - name: Enable unprivileged user namespaces (Ubuntu 24.04)


Suggested change

# to maintain the principle of least privilege.

- name: Enable unprivileged user namespaces (Ubuntu 24.04)

# to maintain the principle of least privilege.

#

# FIXME(#3412): Deduplicate this with what's repeated below?

- name: Enable unprivileged user namespaces (Ubuntu 24.04)

joshlf · 2026-05-25T19:02:17Z


+use clap::Parser as _;
+
+/// Anneal: A Literate Verification Toolchain


You edited the wrong src/main.rs 😛

- Add nix derivations for exocrate - Add `setup` sub-command to locate-or-install exocrate - Add integration test for "developer mode" `setup` that presumes local exocrate archive - Add github workflows to: - Warm nix cache - Locally link exocrate archive from nix, then run all tests gherrit-pr-id: Gwhroikc5idscowxamayknlke2uiddzv3

joshlf · 2026-06-03T18:03:41Z

+              "  local top_dir=$(ls tmp_extract | head -n 1)"
+              # Resolve the component directory path nested inside top_dir
+              # (e.g. 'tmp_extract/rustc-nightly-x86_64-unknown-linux-gnu/rustc')
+              # This perfectly replicates setup.rs double-directory skipping.


It feels like this is just a reference to how a particular .rs file is currently implemented. Can you just explain the behavior directly instead of making reference to a file the reader may not have read, and whose behavior may change out from under us?

joshlf · 2026-06-03T18:06:23Z

+          dontUnpack = true;
+
+          buildPhase = builtins.concatStringsSep "\n" [
+            # 1. Unpack the downloaded archive directly into output directory


Let's not number these? It's one more thing we have to keep up to date, and doesn't really add any value.

joshlf · 2026-06-03T18:07:17Z

+          ];
+
+          installPhase = builtins.concatStringsSep "\n" [
+            # 1. Copy the downloaded .ltar cache files from ~/.cache/mathlib/


Same here re: numbered lists

joshlf · 2026-06-03T18:07:42Z

+          ];
+
+          buildPhase = builtins.concatStringsSep "\n" [
+            # 1. Copy the clean, git-scrubbed package directories to the output path.


Same here re: numbered lists

joshlf · 2026-06-03T18:08:26Z

+            "echo \"Using leantar binary at: \$LEANTAR_BIN\""
+            # 3. Unpack all downloaded .ltar archives recursively using leantar.
+            #
+            # Why: Lake precompiled dependency object files reside in .ltar archives.


Remove the Why: prefix here and elsewhere. It's obvious that this is an explanation from context.

joshlf · 2026-06-03T18:12:03Z

+            # and lakefiles to use local path dependencies. This allows Lake to resolve
+            # all checkouts offline from local directories directly, bypassing all Git
+            # checks and preventing it from triggering dynamic clones.
+            "python3 << 'EOF'"


Why this style here but a single multi-line string for the previous python script?

This was referenced May 19, 2026

[anneal][v2] Initial commit of exocrate #3376

Merged

[anneal][v2] Independently vendor and patch toml_const #3381

Merged

[anneal][v2][exocrate] Crate-level documentation #3382

Merged

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch from 41bb90e to ca9434e Compare May 19, 2026 23:44

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch 2 times, most recently from 34394dc to b45304b Compare May 20, 2026 00:00

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch from ca9434e to d22541f Compare May 20, 2026 00:00

joshlf requested changes May 20, 2026

View reviewed changes

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from b45304b to d060c92 Compare May 20, 2026 00:17

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch from d22541f to cb85c73 Compare May 20, 2026 00:17

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from d060c92 to 929a91b Compare May 20, 2026 00:50

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from 929a91b to bf31762 Compare May 20, 2026 13:36

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch from cb85c73 to f2d675b Compare May 20, 2026 13:36

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch 2 times, most recently from 82c32c9 to 5f697f9 Compare May 20, 2026 15:25

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch from f2d675b to ebd4245 Compare May 20, 2026 17:10

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch 3 times, most recently from 3412078 to 5909564 Compare May 20, 2026 21:08

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from 5909564 to fe81493 Compare May 25, 2026 18:30

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch from ebd4245 to f549d17 Compare May 25, 2026 18:30

joshlf requested changes May 25, 2026

View reviewed changes

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from fe81493 to f300c70 Compare May 25, 2026 19:12

mdittmer mentioned this pull request May 25, 2026

SQUASH ME into toml_cost dep #3413

Closed

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from f300c70 to f3e3b5e Compare May 25, 2026 19:34

mdittmer force-pushed the Gmum75fawi66ursah6w4azlcro7hvrkf4 branch 2 times, most recently from 4f657b1 to 9606fec Compare May 25, 2026 22:48

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from f3e3b5e to f838f8e Compare May 25, 2026 22:48

Base automatically changed from Gmum75fawi66ursah6w4azlcro7hvrkf4 to main May 26, 2026 12:42

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from f838f8e to 9f29506 Compare May 27, 2026 18:13

mdittmer mentioned this pull request May 27, 2026

[anneal][v2] Vendor charon_lib #3418

Open

mdittmer force-pushed the Gwhroikc5idscowxamayknlke2uiddzv3 branch from 9f29506 to 1da6e9a Compare June 3, 2026 12:59

joshlf requested changes Jun 3, 2026

View reviewed changes


		use clap::Parser as _;

		/// Anneal: A Literate Verification Toolchain

		# to maintain the principle of least privilege.
		- name: Enable unprivileged user namespaces (Ubuntu 24.04)

Conversation

mdittmer commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov-commenter commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mdittmer commented May 20, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mdittmer commented May 19, 2026 •

edited

Loading

codecov-commenter commented May 19, 2026 •

edited

Loading