diff --git a/README.md b/README.md index a4c19f2..a41d1bf 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ written in Bend, with a VS Code extension. ## Install -bolt needs Bend 2.0.32 or later; it is built and checked on Bend 2.0.34, the +bolt needs Bend 2.0.32 or later; it is built and checked on Bend 2.0.35, the version `flake.lock` pins. Any install of it will do: the one `curl -fsSL https://bend-lang.com/install.sh | sh` installs, one from nix, or one built from source. You do not need ez or nix. Building bolt needs clang diff --git a/SPEC.md b/SPEC.md index a9ddcda..183d3fc 100644 --- a/SPEC.md +++ b/SPEC.md @@ -156,7 +156,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted | BOLT-TRUST-3 | The directory listing effect (`src/walk/dir.c`, `dir.js`) returns a directory's entries, marking directories with `/`, the OS tells the truth when the directory probe (`src/walk/disk.bend` `is_dir`) asks whether a path is a folder, and the file read effect returns a file's text. | The walk and the reads are foreign code; the planner takes their answers as given. | | BOLT-TRUST-4 | The LSP transport (`src/lsp/transport/fd.c`, `fd.js`) delivers stdin bytes in order and writes stdout bytes whole. | Foreign code over descriptors 0 and 1. | | BOLT-TRUST-5 | `bend --check-only` never runs `main`, and prints its report in the shape `src/lsp/report.bend` parses, naming a def in `Location:` the way `src/lsp/checker/names.bend` builds its names. | bend is a separate program, and the report format has already drifted once (`report_import`). | -| BOLT-TRUST-6 | The proof gate runner runs bend on every PROOF.bend and accepts only an exact `ALL PROOFS CHECK` first line. | It is the flake's `proofs` check, a shell loop over every PROOF.bend on the flake's bend (2.0.34), until ez's `mkProofs` runs on that bend. CI builds from a clean tree. | +| BOLT-TRUST-6 | The proof gate runner runs bend on every PROOF.bend and accepts only an exact `ALL PROOFS CHECK` first line. | It is the flake's `proofs` check, a shell loop over every PROOF.bend on the flake's bend (2.0.35), until ez's `mkProofs` runs on that bend. CI builds from a clean tree. | | BOLT-TRUST-7 | Every commit on `main` passed `ci.yml`. | The repository ruleset "main: require ci" requires the `check / check` job on `main` (since 2026-09-22). release-please PRs, which get no CI run, merge through an admin pull-request bypass. | | BOLT-TRUST-8 | shake v0.2.0 (`0x085b03c84ca37125e38dddede7b91e55`) parses argv as its proved rows say: SHAKE-TOK-1, SHAKE-TOK-3, SHAKE-TOK-4, SHAKE-PARSE-2, SHAKE-PARSE-3, SHAKE-PARSE-4, SHAKE-PARSE-8, SHAKE-GET-1, SHAKE-GET-2 and SHAKE-ERR-1; ezjson v1.1.0 (`0x81c67699424929b5c44cd8577e18117f`) parses and prints JSON correctly. | Pinned dependencies, by ez.toml hash, each proving its own rows in its own gate at the pinned tag. bolt reads shake through `main.bend` only and never unfolds its parser: the BOLT-CLI laws that name an argv take the answer those rows guarantee as premises, each citing its row, and prove what bolt does with it. | | BOLT-TRUST-9 | Each interpreter answers the World's questions and executes plans faithfully. | It makes no decisions and is kept small enough to review line by line. The listing and read effects it calls are BOLT-TRUST-3. | diff --git a/flake.lock b/flake.lock index cc682bf..a6c804d 100644 --- a/flake.lock +++ b/flake.lock @@ -7,17 +7,17 @@ ] }, "locked": { - "lastModified": 1790643370, - "narHash": "sha256-VYGPIHkNeccEaBHGer1B7+GNiWKQBiN/iiS7PozBXx0=", + "lastModified": 1791027223, + "narHash": "sha256-VsMHe5HUg9EC+l8PlfOu2IHTVmP5Vu04GPDYwSkm6q8=", "owner": "bendlang", "repo": "bend", - "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", + "rev": "5a0b523f7759335164f1dead0e0815234a5fd9dc", "type": "github" }, "original": { "owner": "bendlang", "repo": "bend", - "rev": "777ee0b55c485afdd7e68bd917b3d23a88d77371", + "rev": "5a0b523f7759335164f1dead0e0815234a5fd9dc", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 29cfd46..c31b7d9 100644 --- a/flake.nix +++ b/flake.nix @@ -2,17 +2,17 @@ description = "bolt: a linter, checker and language server for Bend 2"; inputs.nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; - # bendlang/bend's flake at the commit that packages 2.0.34 (the v2.0.34 tag - # still packages 2.0.33): bolt builds on it, lints itself with the bolt it + # bendlang/bend's flake at the commit that packages 2.0.35 (the v2.0.35 tag + # still packages 2.0.34): bolt builds on it, lints itself with the bolt it # builds, and checks.proofs runs every PROOF.bend on it inputs.bend = { - url = "github:bendlang/bend/777ee0b55c485afdd7e68bd917b3d23a88d77371"; + url = "github:bendlang/bend/5a0b523f7759335164f1dead0e0815234a5fd9dc"; inputs.nixpkgs.follows = "nixpkgs"; }; inputs.ez = { url = "github:Emerging-Patterns/ez"; inputs.nixpkgs.follows = "nixpkgs"; - # ez's flake.lock names the same 2.0.34 commit as inputs.bend + # ez follows this flake's bend (2.0.35); ez's own lock still names 2.0.34 inputs.bend.follows = "bend"; };