[hermes] Check llms-full.txt in CI (#3194)

Makes progress on #3152

gherrit-pr-id: Gqdqcqcelrxsnq77ga5y3cnwtq46kh7mc

Author: joshlf

.github/workflows/hermes.yml

@@ -48,6 +48,10 @@ jobs:
           cache-from: type=gha
           cache-to: type=gha,mode=max
 
+      # Ensure `llms-full.txt` file is up-to-date.
+      - name: Check doc generation
+        run: docker run --rm -v $GITHUB_WORKSPACE/hermes:/workspace hermes-ci:local cargo run -p doc_gen -- --check
+
       # Run unit tests separately, as they're much less likely to have bugs
       # during local development, and this makes the GitHub Actions output
       # easier to skim (in particular, it's clear at a glance whether a failure

hermes/Cargo.lock

@@ -1,4 +1,5 @@
 [workspace]
+members = [".", "tools/doc_gen"]
 
 [package]
 name = "cargo-hermes"

hermes/Cargo.toml

@@ -37,6 +37,8 @@ COPY build.rs build.rs
 COPY src src
 # Since Cargo.toml explicitly declares [[test]] "integration", this file must exist for Cargo to parse it.
 COPY tests/integration.rs tests/integration.rs
+# Copy tools because they are part of the workspace members
+COPY tools tools
 
 # Download and verify the required versions of Charon and Aeneas.
 RUN cargo run --bin cargo-hermes setup && \

hermes/Dockerfile

@@ -267,7 +267,7 @@ Hermes specifications are written directly in your Rust source code using specia
 
 ## 1. Annotation Chains
 
-To attach a specification to a function, struct, or trait, write a `///` doc-comment block immediately preceding the definition. 
+To attach a specification to a function, struct, or trait, write a `///` doc-comment block immediately preceding the definition.
 
 The block must begin with the `hermes` language string.
 ```rust
@@ -298,15 +298,15 @@ In addition to attaching specs directly to items, you can define a standalone bl
 
 Hermes uses a strict, indentation-sensitive parser (similar to Python or YAML). **Whitespace is semantically significant.**
 
-The rule is simple: **Any line that is indented further than the leading clause belongs to that clause.** 
+The rule is simple: **Any line that is indented further than the leading clause belongs to that clause.**
 If you break an expression across multiple lines, every continuation line *must* be indented deeper than the line that started it.
 
 **Valid:**
 ```rust
 /// ```hermes
 /// requires:
 ///   let x = 5
-///   let y = 
+///   let y =
 ///     x + 2
 /// ```
 ```
@@ -316,7 +316,7 @@ If you break an expression across multiple lines, every continuation line *must*
 /// ```hermes
 /// requires:
 ///   let x = 5
-///   let y = 
+///   let y =
 ///   x + 2    <-- ERROR: Not indented deeper than `let y =`
 /// ```
 ```
@@ -339,7 +339,7 @@ However, Hermes explicitly disables standard implicits in favor of **Strict Impl
 
 **Why is this required?**
 Standard implicits (`{}`) instruct Lean to eagerly guess and synthesize the typeclass immediately when the function is evaluated. For complex spatial traits (like `HasStaticLayout`), this eager synthesis often panics the solver before the proof even begins.
-Strict implicits (`{{ }}`) politely instruct Lean to *delay* synthesis until the exact moment the trait is actively applied to a concrete value. 
+Strict implicits (`{{ }}`) politely instruct Lean to *delay* synthesis until the exact moment the trait is actively applied to a concrete value.
 
 If you are refactoring a Hermes spec, do not replace `{{_sz: Sized Self}}` with `{_sz: Sized Self}`. You will likely break downstream proofs invisibly.
 
@@ -358,9 +358,9 @@ If you simply write an expression, you are defining an anonymous bound.
 ///   x > 0
 /// ```
 ```
-This requires that `x > 0`. Internally, Hermes names this bound `h_unnamed`.
+This requires that `x > 0`. Internally, Hermes names this bound `h_anon`.
 
-**The Singleton Limit:** Because Hermes collapses anonymous bounds into `h_unnamed`, **you may only have one anonymous bound per clause.** If you have multiple requirements, you must name them.
+**The Singleton Limit:** Because Hermes collapses anonymous bounds into `h_anon`, **you may only have one anonymous bound per clause.** If you have multiple requirements, you must name them.
 
 ### Named Bounds
 If multiple `requires` or `ensures` bounds are required, they must be named:
@@ -373,7 +373,7 @@ If multiple `requires` or `ensures` bounds are required, they must be named:
 ```
 
 Naming your bounds is critical for two reasons:
-1. It bypasses the `h_unnamed` singleton limit.
+1. It bypasses the `h_anon` singleton limit.
 2. It allows you to explicitly reference the proven hypothesis (like `h_x_positive`) in downstream proofs or custom lemmas. Any name you provide here becomes an active variable in the local Lean context during verification.
 
 ## 5. Axioms and FFI
@@ -396,7 +396,10 @@ In addition to function-level pre- and post-conditions, Hermes allows you to def
 
 ### `isValid`
 
-`isValid` defines a structural invariant for a type. 
+> [!WARNING]
+> `isValid` annotations are currently unsound. To use them, you must provide the `--unsound-allow-is-valid` flag to Hermes.
+
+`isValid` defines a structural invariant for a type.
 
 ```rust
 /// ```hermes
@@ -421,7 +424,7 @@ Under the hood, this implements the `Hermes.IsValid` typeclass for that struct.
 pub unsafe trait Unaligned: Sized {}
 ```
 
-Implementers of the `unsafe trait` must provide a proof of `isSafe`. 
+Implementers of the `unsafe trait` must provide a proof of `isSafe`.
 
 **Crucially**, generic functions bounding on the trait (e.g., `fn foo<T: Unaligned>()`) **do not** automatically receive this mathematical assumption in their preconditions, because the trait bound alone does not prove the invariant holds in a generic context. You must explicitly request the `isSafe` property in your `requires` block (see Module 6 for how to consume and apply trait bounds).
 
@@ -483,7 +486,7 @@ Bounds are namespaced to either pre-conditions or post-conditions. An anonymous
 
 ````rust
 /// ```hermes
-/// isSafe : 
+/// isSafe :
 ///   ∀ (self : Self), True
 /// ```
 ````
@@ -510,13 +513,13 @@ pub unsafe fn safe_div(a: u32, b: u32) -> u32 { unsafe { a / b } }
 
 Hermes automatically defines or injects the following structural names.
 
-**`h_unnamed`**: The singleton name assigned to an anonymous `requires` or `ensures` block. These are namespaced to either pre-conditions or post-conditions, so they don't conflict.
+**`h_anon`**: The singleton name assigned to an anonymous `requires` or `ensures` block. These are namespaced to either pre-conditions or post-conditions, so they don't conflict.
 
 ````rust
 /// ```hermes
-/// requires: x > 0        -- Named `h_unnamed`
-/// ensures: ret = x + 1   -- Named `h_unnamed`
-/// proof:                 -- Proves `h_unnamed`
+/// requires: x > 0        -- Named `h_anon`
+/// ensures: ret = x + 1   -- Named `h_anon`
+/// proof:                 -- Proves `h_anon`
 ///   ...
 /// ```
 ````
@@ -558,7 +561,7 @@ fn foo() -> MyType {}
 /// proof (h_progress):    -- Prove execution doesn't fail (e.g. divide by zero) or loop forever
 ///   ...
 /// ```
-fn safe_div(x: u32, y: u32) -> u32 {} 
+fn safe_div(x: u32, y: u32) -> u32 {}
 ````
 
 **`h_returns`**: The hypothesis binding the successful evaluation of the function to the implicitly-available values `ret`, `arg'`, etc.
@@ -742,24 +745,24 @@ Writing a Lean proof is not like other forms of software engineering. A Lean pro
 The following is a workflow for solving [problem]. It is recursive – you will use this workflow to solve sub-problems as well.
 
 1. Make sure you understand your goal, context, and constraints for [problem] *completely* and *precisely*.
-  a. Spend as much time as you need *thinking* in order to come to this understanding.
-  b. If there is any ambiguity whatsoever, ask for clarification.
-  c. Repeat the process of clarification-asking and thinking until you have a *complete* and *precise* understanding of your goal, context, and constraints.
-  d. Record this in as much details as you can in comments the file you are editing.
+    1. Spend as much time as you need *thinking* in order to come to this understanding.
+    2. If there is any ambiguity whatsoever, ask for clarification.
+    3. Repeat the process of clarification-asking and thinking until you have a *complete* and *precise* understanding of your goal, context, and constraints.
+    4. Record this in as much details as you can in comments the file you are editing.
 2. Once you understand the goal, context, and constraints for [problem], brainstorm a *complete* solution. Your solution must be *complete*, as the act of thinking through details may make you realize that you need to adjust your high-level plan.
-  a. Spend as much time as it takes to think through your solution *completely* until you are confident that *every detail* is correct.
-  b. Record this in as much details as you can in comments the file you are editing.
+    1. Spend as much time as it takes to think through your solution *completely* until you are confident that *every detail* is correct.
+    2. Record this in as much details as you can in comments the file you are editing.
 3. You are now ready to start writing code.
-  a. Start with the specification (`requires` and `ensures` clauses).
-  b. Get these working with the `verify` subcommand and the `--allow-sorry` flag, omitting any proofs.
-  c. Iterate until everything verifies, implying that your specification is internally consistent. This does not necessarily mean that it's the *right* specification, only that Hermes understands it.
-  d. Run the `expand` subcommand to see what Lean is generated, and make sure it looks like what you expect. This will help you when you start writing proofs.
+    1. Start with the specification (`requires` and `ensures` clauses).
+    2. Get these working with the `verify` subcommand and the `--allow-sorry` flag, omitting any proofs.
+    3. Iterate until everything verifies, implying that your specification is internally consistent. This does not necessarily mean that it's the *right* specification, only that Hermes understands it.
+    4. Run the `expand` subcommand to see what Lean is generated, and make sure it looks like what you expect. This will help you when you start writing proofs.
 4. Move on to the proof.
-  a. First, break the proof down into lemmas. Spend as much time as you need thinking through the lemmas and how they fit together to prove the main proof.
-  b. Write the *definitions* of each lemma, but do *not* prove them – leave their proofs as `sorry` for now.
+    1. First, break the proof down into lemmas. Spend as much time as you need thinking through the lemmas and how they fit together to prove the main proof.
+    2. Write the *definitions* of each lemma, but do *not* prove them – leave their proofs as `sorry` for now.
 5. Write the top-level proof, using the lemmas you defined in the previous step.
-  a. Iterate until this proof verifies, using the `--allow-sorry` flag.
-  b. If you get stuck *at all*, consider whether you need to re-visit a previous step or "pop up" one level of abstraction to reconsider your broader plan.
+    1. Iterate until this proof verifies, using the `--allow-sorry` flag.
+    2. If you get stuck *at all*, consider whether you need to re-visit a previous step or "pop up" one level of abstraction to reconsider your broader plan.
 6. Once the top-level proof verifies, you can start proving the lemmas one by one. For each lemma, you will use *this entire workflow*, but applied to [sub-problem] instead of the top-level [problem].
 
 Overall, your workflow will look like a recursive application of this entire workflow. Always be prepared to "pop up" one level of abstraction to reconsider your broader plan.

hermes/llms-full.txt

@@ -0,0 +1,9 @@
+[package]
+name = "doc_gen"
+version = "0.1.0"
+edition = "2024"
+publish = false
+
+[dependencies]
+tree-sitter = "0.25"
+tree-sitter-lean4 = "0.2"

hermes/tools/doc_gen/Cargo.toml

@@ -1,10 +1,3 @@
-#!/usr/bin/env -S cargo +nightly -Zscript
----
-[dependencies]
-tree-sitter = "0.25"
-tree-sitter-lean4 = "0.2"
----
-
 use std::{env, fs, path::Path, process};
 
 fn extract_signature(kind: &str, text: &str) -> String {
@@ -122,7 +115,7 @@ fn main() {
         let existing = fs::read_to_string(target_file).unwrap_or_default();
         if existing != full_txt {
             eprintln!(
-                "Error: {} is out of date. Please run `tools/doc_gen.rs` to update it.",
+                "Error: {} is out of date. Please run `cargo run -p doc_gen` to update it.",
                 target_file
             );
             process::exit(1);

hermes/tools/doc_gen.rs hermes/tools/doc_gen/src/main.rshermes/tools/doc_gen.rs renamed to hermes/tools/doc_gen/src/main.rs

@@ -1 +1 @@
-{"files":{".cargo_vcs_info.json":"cf43644f4417a371f3b570fae27b3a6949dc254c597474a10b7ee23839965437","AUTHORS":"d5fca2653c88ad02d197faead77e22b80c70636b5bec6e02f2805f389a21b86d","CHANGELOG.md":"33e288ac35f2f0045f692c87624de90f10166e3bd0b3b311eeb7d28560a67aa1","CONTRIBUTING.md":"a7e0f3d282301aa5f4b546ed7fc5376159569987a002f24bf57082d49746fde6","Cargo.lock":"8846412681720cb85ae6a79ac3eae84ca145c7cb4a809e0bd52a3cbaed31ee31","Cargo.toml":"fe2d3062136b9c1bdacc09aaf8ad2766a4182de39732498de8bbb21c62f4384a","Cargo.toml.orig":"fc005fab26a48ff9c66f508c538a84b05cb5b5aea0968acf97daf9092687599a","LICENSE":"3bc70e239e91272782006c638fc0452a714d384224f11f0923036b7be07cf9b5","PERFORMANCE.md":"9de4fa787572943e7e350a2688002d571e986190e4869d08587048974bc2fcc6","README.md":"5321b581e5d6bea76875bc3ef93a482184fea9616b45f73781f5ec16542bdf9c","benches/bench.rs":"ec5005c0ec5b5155ae334f9204dffac98b583c377773dbe81e460ecf7404c1d0","codecov.yml":"d6ebfcadb4d940a0f86ab1a99928b673195c7d84cecee17a5eefeaf396c8477b","examples/toy.rs":"33c5f572f2afa1e0d359845708bd984bc95e272b4dcac0eb3ce55668b2a9d03b","src/analyze.rs":"0ea9e0b9661cef8c804a750459d6caf196b298dae1267d52661f1894f88c47d6","src/compile.rs":"54afdafd8004bc3cd27074e949fb1ccf0c81af0992f9c140141bea8f182ed42c","src/error.rs":"931e720cd907f7f62d41c10b69174f286c2944bb4230df8c3c1428aa75056260","src/expand.rs":"6eff8afef144363d8ebbb90922448783cf2ebfc71ef716948bd9da54793663af","src/lib.rs":"5fceb05786b2e860ec2141c8e6bfbb85014c97b4f48cc634d0842b81b0dd6477","src/parse.rs":"8991c0f8b311f404cd63bc8f2beb898055f14c2fd899ccfb86055b396a596229","src/replacer.rs":"5bf1c99d598c27248fd6591dab000e649eedc8f51179f904e00b94ac27919dc3","src/vm.rs":"8442aec0c60680576130f0ebbd6da494bba14d1141e7035f66c68f3849933731","tests/captures.rs":"0b561bbec208af0cdea12c8b10e3c72eab80ef2dbf1a9c1007fdffc7401b4434","tests/common/mod.rs":"b8ab2a7a3a25adad8317c8eb1f4566df6a81978c3a7ab49847ec2f838d77c888","tests/finding.rs":"76e60d370ae71585a304018fe0398e5206fe431fe21bbde6347cc2572afff0e5","tests/matching.rs":"3f8d1e0f6567375866b14610eda6e2dc1e96ed26ba1a451fe0c4bb2bf6f774fb","tests/oniguruma.rs":"78a54ef464d08fa7192959eb50c3de03df7dae0f9d41831b06ecfa170dfcfd65","tests/oniguruma/.gitattributes":"b8d35d419a619abf4283b4f1e8a3daeaca142c87df6634b4cd706b726d29a88d","tests/oniguruma/README.md":"eae6ac089cd32010ffacb4b2f0f8cbac03ad2623e115386af53bfc93e04d1903","tests/oniguruma/test_utf8.c":"1e4813ac64703cfdbcdca359b82856c5c6778abf977e577992f6b34ab26b92de","tests/oniguruma/test_utf8_ignore.c":"88760e1779017c58dfca5b03f382df7b067dceefcb4b52d81aef36f096b918a0","tests/regex_options.rs":"1744e707e8d76f19b999728c6b7de6e0e531342d1cd708af61ffbe74cef84a3f","tests/replace.rs":"689fef80c2cd243a510be212cb8e6a04a30a0b0fa6f1dd6be63b17a9abb158d8","tests/splitting.rs":"55a60e7953e92cf542fff8016c24607d3da4fdf9cbf68712348cc430b2bc0f3f"},"package":"6e24cb5a94bcae1e5408b0effca5cd7172ea3c5755049c5f3af4cd283a165298"}
+{"files":{".cargo_vcs_info.json":"cf43644f4417a371f3b570fae27b3a6949dc254c597474a10b7ee23839965437","AUTHORS":"d5fca2653c88ad02d197faead77e22b80c70636b5bec6e02f2805f389a21b86d","CHANGELOG.md":"33e288ac35f2f0045f692c87624de90f10166e3bd0b3b311eeb7d28560a67aa1","CONTRIBUTING.md":"a7e0f3d282301aa5f4b546ed7fc5376159569987a002f24bf57082d49746fde6","Cargo.lock":"8846412681720cb85ae6a79ac3eae84ca145c7cb4a809e0bd52a3cbaed31ee31","Cargo.toml":"fe2d3062136b9c1bdacc09aaf8ad2766a4182de39732498de8bbb21c62f4384a","Cargo.toml.orig":"fc005fab26a48ff9c66f508c538a84b05cb5b5aea0968acf97daf9092687599a","LICENSE":"3bc70e239e91272782006c638fc0452a714d384224f11f0923036b7be07cf9b5","PERFORMANCE.md":"9de4fa787572943e7e350a2688002d571e986190e4869d08587048974bc2fcc6","README.md":"5321b581e5d6bea76875bc3ef93a482184fea9616b45f73781f5ec16542bdf9c","benches/bench.rs":"ec5005c0ec5b5155ae334f9204dffac98b583c377773dbe81e460ecf7404c1d0","codecov.yml":"d6ebfcadb4d940a0f86ab1a99928b673195c7d84cecee17a5eefeaf396c8477b","examples/toy.rs":"33c5f572f2afa1e0d359845708bd984bc95e272b4dcac0eb3ce55668b2a9d03b","src/analyze.rs":"0ea9e0b9661cef8c804a750459d6caf196b298dae1267d52661f1894f88c47d6","src/compile.rs":"54afdafd8004bc3cd27074e949fb1ccf0c81af0992f9c140141bea8f182ed42c","src/error.rs":"931e720cd907f7f62d41c10b69174f286c2944bb4230df8c3c1428aa75056260","src/expand.rs":"6eff8afef144363d8ebbb90922448783cf2ebfc71ef716948bd9da54793663af","src/lib.rs":"5fceb05786b2e860ec2141c8e6bfbb85014c97b4f48cc634d0842b81b0dd6477","src/parse.rs":"8991c0f8b311f404cd63bc8f2beb898055f14c2fd899ccfb86055b396a596229","src/replacer.rs":"5bf1c99d598c27248fd6591dab000e649eedc8f51179f904e00b94ac27919dc3","src/vm.rs":"8442aec0c60680576130f0ebbd6da494bba14d1141e7035f66c68f3849933731","tests/captures.rs":"0b561bbec208af0cdea12c8b10e3c72eab80ef2dbf1a9c1007fdffc7401b4434","tests/common/mod.rs":"b8ab2a7a3a25adad8317c8eb1f4566df6a81978c3a7ab49847ec2f838d77c888","tests/finding.rs":"76e60d370ae71585a304018fe0398e5206fe431fe21bbde6347cc2572afff0e5","tests/matching.rs":"3f8d1e0f6567375866b14610eda6e2dc1e96ed26ba1a451fe0c4bb2bf6f774fb","tests/oniguruma.rs":"78a54ef464d08fa7192959eb50c3de03df7dae0f9d41831b06ecfa170dfcfd65","tests/oniguruma/README.md":"eae6ac089cd32010ffacb4b2f0f8cbac03ad2623e115386af53bfc93e04d1903","tests/oniguruma/test_utf8.c":"1e4813ac64703cfdbcdca359b82856c5c6778abf977e577992f6b34ab26b92de","tests/oniguruma/test_utf8_ignore.c":"88760e1779017c58dfca5b03f382df7b067dceefcb4b52d81aef36f096b918a0","tests/regex_options.rs":"1744e707e8d76f19b999728c6b7de6e0e531342d1cd708af61ffbe74cef84a3f","tests/replace.rs":"689fef80c2cd243a510be212cb8e6a04a30a0b0fa6f1dd6be63b17a9abb158d8","tests/splitting.rs":"55a60e7953e92cf542fff8016c24607d3da4fdf9cbf68712348cc430b2bc0f3f"},"package":"6e24cb5a94bcae1e5408b0effca5cd7172ea3c5755049c5f3af4cd283a165298"}