From 6badf7f055bd9c86b810019bce82ff4ae18814c1 Mon Sep 17 00:00:00 2001 From: Koukyosyumei Date: Thu, 22 Oct 2026 22:00:34 -0400 Subject: [PATCH 1/3] bump h5i-app to 0.1.3 --- Cargo.lock | 26 ++++++++++----------- Cargo.toml | 18 +++++++------- README.md | 2 +- crates/h5i-app-cli/Cargo.toml | 2 +- crates/h5i-app-core/Cargo.toml | 2 +- crates/h5i-app-gpu/Cargo.lock | 2 +- crates/h5i-app-gpu/Cargo.toml | 2 +- crates/h5i-app-gpu/backend-oxide/Cargo.lock | 6 ++--- crates/h5i-app-gpu/backend-oxide/Cargo.toml | 2 +- crates/h5i-app-http/Cargo.toml | 2 +- crates/h5i-app-json/Cargo.toml | 2 +- crates/h5i-app-mem/Cargo.toml | 2 +- crates/h5i-app-pg/Cargo.toml | 2 +- crates/h5i-app-pgsql/Cargo.toml | 2 +- crates/h5i-app-schema/Cargo.toml | 2 +- crates/h5i-app-sql/Cargo.toml | 2 +- crates/h5i-app-std/Cargo.toml | 2 +- crates/h5i-app-token/Cargo.toml | 2 +- crates/h5i-app-xtask/Cargo.toml | 2 +- crates/h5i-app/Cargo.toml | 2 +- examples/app/Cargo.lock | 18 +++++++------- 21 files changed, 51 insertions(+), 51 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fc1e31855..fa895343c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1139,7 +1139,7 @@ dependencies = [ [[package]] name = "h5i-app" -version = "0.1.2" +version = "0.1.3" dependencies = [ "h5i-app-core", "h5i-app-http", @@ -1153,7 +1153,7 @@ dependencies = [ [[package]] name = "h5i-app-cli" -version = "0.1.2" +version = "0.1.3" dependencies = [ "anyhow", "clap", @@ -1169,11 +1169,11 @@ dependencies = [ [[package]] name = "h5i-app-core" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-http" -version = "0.1.2" +version = "0.1.3" dependencies = [ "axum 0.8.9", "h5i-app-core", @@ -1187,7 +1187,7 @@ dependencies = [ [[package]] name = "h5i-app-json" -version = "0.1.2" +version = "0.1.3" dependencies = [ "proptest", "serde_json", @@ -1195,7 +1195,7 @@ dependencies = [ [[package]] name = "h5i-app-mem" -version = "0.1.2" +version = "0.1.3" dependencies = [ "h5i-app-core", "h5i-app-pg", @@ -1204,7 +1204,7 @@ dependencies = [ [[package]] name = "h5i-app-pg" -version = "0.1.2" +version = "0.1.3" dependencies = [ "bytes", "deadpool-postgres", @@ -1219,7 +1219,7 @@ dependencies = [ [[package]] name = "h5i-app-pgsql" -version = "0.1.2" +version = "0.1.3" dependencies = [ "h5i-app-sql", ] @@ -1237,23 +1237,23 @@ dependencies = [ [[package]] name = "h5i-app-schema" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-sql" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-std" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-token" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-xtask" -version = "0.1.2" +version = "0.1.3" dependencies = [ "anyhow", "clap", diff --git a/Cargo.toml b/Cargo.toml index 55e9b8203..60484f021 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -24,15 +24,15 @@ sha2 = "0.10" # crates publish against each other. External dependencies are declared in # each crate, not here: a user's build of h5i-app must not inherit the h5i # CLI's feature choices (serde_json's `preserve_order`, for one). -h5i-app-core = { path = "crates/h5i-app-core", version = "0.1.2" } -h5i-app-http = { path = "crates/h5i-app-http", version = "0.1.2" } -h5i-app-json = { path = "crates/h5i-app-json", version = "0.1.2" } -h5i-app-pg = { path = "crates/h5i-app-pg", version = "0.1.2" } -h5i-app-pgsql = { path = "crates/h5i-app-pgsql", version = "0.1.2" } -h5i-app-schema = { path = "crates/h5i-app-schema", version = "0.1.2" } -h5i-app-sql = { path = "crates/h5i-app-sql", version = "0.1.2" } -h5i-app-std = { path = "crates/h5i-app-std", version = "0.1.2" } -h5i-app-token = { path = "crates/h5i-app-token", version = "0.1.2" } +h5i-app-core = { path = "crates/h5i-app-core", version = "0.1.3" } +h5i-app-http = { path = "crates/h5i-app-http", version = "0.1.3" } +h5i-app-json = { path = "crates/h5i-app-json", version = "0.1.3" } +h5i-app-pg = { path = "crates/h5i-app-pg", version = "0.1.3" } +h5i-app-pgsql = { path = "crates/h5i-app-pgsql", version = "0.1.3" } +h5i-app-schema = { path = "crates/h5i-app-schema", version = "0.1.3" } +h5i-app-sql = { path = "crates/h5i-app-sql", version = "0.1.3" } +h5i-app-std = { path = "crates/h5i-app-std", version = "0.1.3" } +h5i-app-token = { path = "crates/h5i-app-token", version = "0.1.3" } # The repo's primary product is the `h5i` binary, so it lives at the root # (`cargo install --path .` / `cargo run` do the obvious thing). The library it diff --git a/README.md b/README.md index 1b13eb966..a74e0c379 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ npx skills add h5i-dev/h5i ```toml [dependencies] -h5i-app = { version = "0.1.2", features = ["http", "postgres"] } +h5i-app = { version = "0.1.3", features = ["http", "postgres"] } ```

diff --git a/crates/h5i-app-cli/Cargo.toml b/crates/h5i-app-cli/Cargo.toml index 2aa65e9c7..708f2de1f 100644 --- a/crates/h5i-app-cli/Cargo.toml +++ b/crates/h5i-app-cli/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-cli" description = "`h5i app`: extract an h5i-app kernel to Lean, gate its proofs, and test the spec with mutants" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" publish = false # The whole development loop of an h5i-app application, behind one command diff --git a/crates/h5i-app-core/Cargo.toml b/crates/h5i-app-core/Cargo.toml index 80daba4bd..284a0bf94 100644 --- a/crates/h5i-app-core/Cargo.toml +++ b/crates/h5i-app-core/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-core" description = "Core contract between a verified h5i-app kernel and its untrusted shell" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-gpu/Cargo.lock b/crates/h5i-app-gpu/Cargo.lock index 9bee9abde..e1b8aba03 100644 --- a/crates/h5i-app-gpu/Cargo.lock +++ b/crates/h5i-app-gpu/Cargo.lock @@ -176,7 +176,7 @@ checksum = "e4eba85ea1d0a966a983acd07deee566e67395d2d96b6fb39e62b5a833f1eb0b" [[package]] name = "h5i-app-gpu" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-gpu-backend-nvvm" diff --git a/crates/h5i-app-gpu/Cargo.toml b/crates/h5i-app-gpu/Cargo.toml index 689863b91..cecf1a9c3 100644 --- a/crates/h5i-app-gpu/Cargo.toml +++ b/crates/h5i-app-gpu/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "h5i-app-gpu" -version = "0.1.2" +version = "0.1.3" edition = "2024" license = "Apache-2.0" description = "Optional batch execution adapters and differential checks for application kernels" diff --git a/crates/h5i-app-gpu/backend-oxide/Cargo.lock b/crates/h5i-app-gpu/backend-oxide/Cargo.lock index 7086a9421..0039d653f 100644 --- a/crates/h5i-app-gpu/backend-oxide/Cargo.lock +++ b/crates/h5i-app-gpu/backend-oxide/Cargo.lock @@ -31,7 +31,7 @@ dependencies = [ [[package]] name = "h5i-app-gpu-backend-oxide" -version = "0.1.2" +version = "0.1.3" dependencies = [ "calculator-kernel", "cuda-device", @@ -40,11 +40,11 @@ dependencies = [ [[package]] name = "h5i-app-schema" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-sql" -version = "0.1.2" +version = "0.1.3" [[package]] name = "parallel-kernel" diff --git a/crates/h5i-app-gpu/backend-oxide/Cargo.toml b/crates/h5i-app-gpu/backend-oxide/Cargo.toml index 6a315fb27..11e7166a2 100644 --- a/crates/h5i-app-gpu/backend-oxide/Cargo.toml +++ b/crates/h5i-app-gpu/backend-oxide/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "h5i-app-gpu-backend-oxide" -version = "0.1.2" +version = "0.1.3" edition = "2024" license = "Apache-2.0" publish = false diff --git a/crates/h5i-app-http/Cargo.toml b/crates/h5i-app-http/Cargo.toml index fb86b6ef3..c5e439210 100644 --- a/crates/h5i-app-http/Cargo.toml +++ b/crates/h5i-app-http/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-http" description = "HTTP shell for h5i-app kernels: authentication and input decoding (trusted), dispatch to the engine" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-json/Cargo.toml b/crates/h5i-app-json/Cargo.toml index b74ceecd9..426b1583e 100644 --- a/crates/h5i-app-json/Cargo.toml +++ b/crates/h5i-app-json/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-json" description = "JSON writer for h5i-app replies, extracted to Lean and proven" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-mem/Cargo.toml b/crates/h5i-app-mem/Cargo.toml index 14d9820a2..d27516616 100644 --- a/crates/h5i-app-mem/Cargo.toml +++ b/crates/h5i-app-mem/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "h5i-app-mem" -version = "0.1.2" +version = "0.1.3" edition = "2024" license = "Apache-2.0" description = "Single-owner RAM read cache with PostgreSQL write-through execution" diff --git a/crates/h5i-app-pg/Cargo.toml b/crates/h5i-app-pg/Cargo.toml index 9d50c7af7..3697aaa8e 100644 --- a/crates/h5i-app-pg/Cargo.toml +++ b/crates/h5i-app-pg/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-pg" description = "PostgreSQL engine for h5i-app: tenant-scoped snapshots, SERIALIZABLE execution with retry, idempotency" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-pgsql/Cargo.toml b/crates/h5i-app-pgsql/Cargo.toml index f791d607e..ff6cc41f7 100644 --- a/crates/h5i-app-pgsql/Cargo.toml +++ b/crates/h5i-app-pgsql/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-pgsql" description = "PostgreSQL text for h5i-app's planned statements; extracted to Lean and proven to mean what the planner's statements mean" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-schema/Cargo.toml b/crates/h5i-app-schema/Cargo.toml index 468d992fa..4057487e2 100644 --- a/crates/h5i-app-schema/Cargo.toml +++ b/crates/h5i-app-schema/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-schema" description = "Declare kernel row types once; get the structs and their table mappings" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-sql/Cargo.toml b/crates/h5i-app-sql/Cargo.toml index b8ba55f8b..6fa865aaf 100644 --- a/crates/h5i-app-sql/Cargo.toml +++ b/crates/h5i-app-sql/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-sql" description = "Pure planner from h5i-app write sets to keyed SQL statements; extracted to Lean and proven" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-std/Cargo.toml b/crates/h5i-app-std/Cargo.toml index 7165d5321..81d4d6b76 100644 --- a/crates/h5i-app-std/Cargo.toml +++ b/crates/h5i-app-std/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-std" description = "Byte strings, sets and maps for h5i-app kernels, extracted to Lean and proven" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-token/Cargo.toml b/crates/h5i-app-token/Cargo.toml index 9a6da3a09..077bf2693 100644 --- a/crates/h5i-app-token/Cargo.toml +++ b/crates/h5i-app-token/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-token" description = "Bearer token encoding and parsing for h5i-app, extracted to Lean and proven" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" repository = "https://github.com/h5i-dev/h5i" homepage = "https://github.com/h5i-dev/h5i" readme = "../h5i-app/README.md" diff --git a/crates/h5i-app-xtask/Cargo.toml b/crates/h5i-app-xtask/Cargo.toml index f49db4dfe..c9e35db99 100644 --- a/crates/h5i-app-xtask/Cargo.toml +++ b/crates/h5i-app-xtask/Cargo.toml @@ -3,7 +3,7 @@ name = "h5i-app-xtask" description = "Repository checks: `cargo app-verify`, and `cargo app` for `h5i app` without the browser build" edition = "2024" license = "Apache-2.0" -version = "0.1.2" +version = "0.1.3" publish = false [dependencies] diff --git a/crates/h5i-app/Cargo.toml b/crates/h5i-app/Cargo.toml index 501aaed08..ae4a4ff67 100644 --- a/crates/h5i-app/Cargo.toml +++ b/crates/h5i-app/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "h5i-app" -version = "0.1.2" +version = "0.1.3" edition = "2024" license = "Apache-2.0" repository = "https://github.com/h5i-dev/h5i" diff --git a/examples/app/Cargo.lock b/examples/app/Cargo.lock index af0167ab4..7fb92de05 100644 --- a/examples/app/Cargo.lock +++ b/examples/app/Cargo.lock @@ -465,11 +465,11 @@ checksum = "e4eba85ea1d0a966a983acd07deee566e67395d2d96b6fb39e62b5a833f1eb0b" [[package]] name = "h5i-app-core" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-http" -version = "0.1.2" +version = "0.1.3" dependencies = [ "axum", "h5i-app-core", @@ -483,11 +483,11 @@ dependencies = [ [[package]] name = "h5i-app-json" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-mem" -version = "0.1.2" +version = "0.1.3" dependencies = [ "h5i-app-core", "h5i-app-pg", @@ -496,7 +496,7 @@ dependencies = [ [[package]] name = "h5i-app-pg" -version = "0.1.2" +version = "0.1.3" dependencies = [ "bytes", "deadpool-postgres", @@ -511,22 +511,22 @@ dependencies = [ [[package]] name = "h5i-app-pgsql" -version = "0.1.2" +version = "0.1.3" dependencies = [ "h5i-app-sql", ] [[package]] name = "h5i-app-schema" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-sql" -version = "0.1.2" +version = "0.1.3" [[package]] name = "h5i-app-token" -version = "0.1.2" +version = "0.1.3" [[package]] name = "hax-lib" From 80a0a8e22162b44784caf248683ed7ad890d3700 Mon Sep 17 00:00:00 2001 From: Koukyosyumei Date: Thu, 22 Oct 2026 22:05:23 -0400 Subject: [PATCH 2/3] include h5i-app-gpu in the workspace --- Cargo.lock | 4 ++++ Cargo.toml | 9 +++++++-- crates/h5i-app-gpu/Cargo.toml | 4 ---- crates/h5i-app-gpu/{ => backend-nvvm}/Cargo.lock | 0 docs/app/GPU.md | 2 +- 5 files changed, 12 insertions(+), 7 deletions(-) rename crates/h5i-app-gpu/{ => backend-nvvm}/Cargo.lock (100%) diff --git a/Cargo.lock b/Cargo.lock index fa895343c..02c892ec8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1171,6 +1171,10 @@ dependencies = [ name = "h5i-app-core" version = "0.1.3" +[[package]] +name = "h5i-app-gpu" +version = "0.1.3" + [[package]] name = "h5i-app-http" version = "0.1.3" diff --git a/Cargo.toml b/Cargo.toml index 60484f021..56358b93c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,8 +1,13 @@ [workspace] members = ["crates/*"] # The h5i-app examples are their own workspace, depending on the h5i-app -# crates by path as an application would. -exclude = ["examples/app", "crates/h5i-app-gpu"] +# crates by path as an application would. The GPU backends need CUDA and git +# dependencies, so they build separately too. +exclude = [ + "examples/app", + "crates/h5i-app-gpu/backend-nvvm", + "crates/h5i-app-gpu/backend-oxide", +] resolver = "3" # Shared dependency versions for every workspace crate — a single source of diff --git a/crates/h5i-app-gpu/Cargo.toml b/crates/h5i-app-gpu/Cargo.toml index cecf1a9c3..ab318b257 100644 --- a/crates/h5i-app-gpu/Cargo.toml +++ b/crates/h5i-app-gpu/Cargo.toml @@ -4,7 +4,3 @@ version = "0.1.3" edition = "2024" license = "Apache-2.0" description = "Optional batch execution adapters and differential checks for application kernels" -[workspace] -members = ["backend-nvvm"] -default-members = ["."] -exclude = ["backend-oxide"] diff --git a/crates/h5i-app-gpu/Cargo.lock b/crates/h5i-app-gpu/backend-nvvm/Cargo.lock similarity index 100% rename from crates/h5i-app-gpu/Cargo.lock rename to crates/h5i-app-gpu/backend-nvvm/Cargo.lock diff --git a/docs/app/GPU.md b/docs/app/GPU.md index 30339054c..7f6971a66 100644 --- a/docs/app/GPU.md +++ b/docs/app/GPU.md @@ -135,7 +135,7 @@ device compilation probe without the failing host runtime. ## Earlier calculator / Result failures -`crates/h5i-app-gpu` is a separate workspace/toolchain invocation, excluded from +`crates/h5i-app-gpu/backend-oxide` is a separate workspace/toolchain invocation, excluded from normal extraction and builds. Its default CPU test calls the existing calculator kernel's `compute`, including checked arithmetic errors. The `calculator-probe` feature adds a thin `#[kernel]` batch wrapper with separate From 4a1d61fa540ed9ca4e3605c53baede565d9820cc Mon Sep 17 00:00:00 2001 From: Koukyosyumei Date: Thu, 22 Oct 2026 22:06:36 -0400 Subject: [PATCH 3/3] revert backend-oxide to 0.1.0 --- crates/h5i-app-gpu/backend-oxide/Cargo.lock | 2 +- crates/h5i-app-gpu/backend-oxide/Cargo.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/h5i-app-gpu/backend-oxide/Cargo.lock b/crates/h5i-app-gpu/backend-oxide/Cargo.lock index 0039d653f..44ff35d56 100644 --- a/crates/h5i-app-gpu/backend-oxide/Cargo.lock +++ b/crates/h5i-app-gpu/backend-oxide/Cargo.lock @@ -31,7 +31,7 @@ dependencies = [ [[package]] name = "h5i-app-gpu-backend-oxide" -version = "0.1.3" +version = "0.1.0" dependencies = [ "calculator-kernel", "cuda-device", diff --git a/crates/h5i-app-gpu/backend-oxide/Cargo.toml b/crates/h5i-app-gpu/backend-oxide/Cargo.toml index 11e7166a2..af02cbe3b 100644 --- a/crates/h5i-app-gpu/backend-oxide/Cargo.toml +++ b/crates/h5i-app-gpu/backend-oxide/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "h5i-app-gpu-backend-oxide" -version = "0.1.3" +version = "0.1.0" edition = "2024" license = "Apache-2.0" publish = false