[WIP] Cleanup #2977

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open

joshlf wants to merge 1 commit into Gb4a4c349671f37aad9e084998afdb7c57d92be43 from G0b9216c6738c722e3424be5ee5e085157b5813f9

+164,849 −223

tools/Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

tools/hermes/Cargo.toml

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -5,9 +5,11 @@ edition = "2024"
  
    [dependencies]

    anyhow = "1.0.100"

    cargo_metadata = "0.18"

    clap = { version = "4.5.56", features = ["derive"] }

    env_logger = "0.11"

    log = "0.4"

    quote = "1.0.43"

    regex = "1.12.2"

    walkdir = "2.5.0"

    cargo_metadata = "0.18"

    syn = { version = "2.0.114", features = ["full", "visit", "visit-mut", "extra-traits"] }

    quote = "1.0.43"

    walkdir = "2.5.0"

tools/hermes/src/desugar.rs

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -34,7 +34,7 @@ pub fn desugar_spec(
  
                // Check if this file looks like signature args.

                // It might be `(x y : Usize)` or `add_mod (x y : Usize)`.

                // We also support instance arguments like `[Layout T]`.

                if let Some(start_idx) = line.find(|c| c == '(' || c == '[') {

                if let Some(start_idx) = line.find(['(', '[']) {

                    // Assume everything from start_idx onwards is args.

                    // And ignore what's before it (likely function name).

                    signature_args = Some(line[start_idx..].to_string());

    @@ -86,17 +86,17 @@ pub fn desugar_spec(
  
    fn parse_binders(ensures_content: &str) -> Result<(Vec<String>, String)> {

        // |ret, x_final| logic

        if let Some(start) = ensures_content.find('|') {

            if let Some(end) = ensures_content[start + 1..].find('|') {

                let binders_str = &ensures_content[start + 1..start + 1 + end];

                let logic = &ensures_content[start + 1 + end + 1..];

                let binders = binders_str

                    .split(',')

                    .map(|s| s.trim().to_string())

                    .filter(|s| !s.is_empty())

                    .collect();

                return Ok((binders, logic.trim().to_string()));

            }

        if let Some(start) = ensures_content.find('|')

            && let Some(end) = ensures_content[start + 1..].find('|')

        {

            let binders_str = &ensures_content[start + 1..start + 1 + end];

            let logic = &ensures_content[start + 1 + end + 1..];

            let binders = binders_str

                .split(',')

                .map(|s| s.trim().to_string())

                .filter(|s| !s.is_empty())

                .collect();

            return Ok((binders, logic.trim().to_string()));

        }

        bail!("Malformed ensures clause: missing |...| binders");

    }

    @@ -116,7 +116,7 @@ fn generate_body(
  
            out.push_str("exists");

            for b in binders {

                if b != "_" {

                    out.push_str(" ");

                    out.push(' ');

                    out.push_str(b);

                } else {

                    // If it's "_", we usually need a name for the exists,

tools/hermes/src/docs.rs

-Original file line number
+Diff line change
@@ -0,0 +1,74 @@
+    // Copyright 2026 The Fuchsia Authors
+    //
+    // Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+    // <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+    // license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+    // This file may not be copied, modified, or distributed except according to
+    // those terms.
+    use syn::{Attribute, Expr, ExprLit, Lit, Meta};
+    /// Extracts the string content of a `#[doc = "..."]` or `/// ...` attribute.
+    /// Returns `None` if the attribute is not a doc comment.
+    pub fn parse_doc_attr(attr: &Attribute) -> Option<String> {
+        if !attr.path().is_ident("doc") {
+            return None;
+        }
+        match &attr.meta {
+            Meta::NameValue(nv) => match &nv.value {
+                Expr::Lit(ExprLit { lit: Lit::Str(s), .. }) => Some(s.value()),
+                _ => None,
+            },
+            _ => None,
+        }
+    }
+    /// Helper to check if a line is a Hermes directive.
+    /// Returns the trimmed content if it matches the prefix, otherwise None.
+    /// This handles the `///@` syntax.
+    /// Parses a specific Hermes tag from a line.
+    /// Returns `Some(content)` if the line starts with `///@ <tag>` or `///@<tag>`.
+    /// Content is trimmed.
+    /// Example: `parse_hermes_tag("@ lean spec", "lean spec")` -> `Some(...)`
+    pub fn parse_hermes_tag<'a>(line: &'a str, tag: &str) -> Option<&'a str> {
+        let trimmed = line.trim();
+        if !trimmed.starts_with('@') {
+            return None;
+        }
+        // Check for "@ <tag>" or "@<tag>"
+        // We expect usage like "@ lean spec"
+        let prefix_space = format!("@ {}", tag);
+        if let Some(rest) = trimmed.strip_prefix(&prefix_space) {
+            return Some(rest.trim());
+        }
+        let prefix_nospace = format!("@{}", tag);
+        if let Some(rest) = trimmed.strip_prefix(&prefix_nospace) {
+            return Some(rest.trim());
+        }
+        None
+    }
+    /// Checks if a line is a Hermes directive (starts with `@`).
+    pub fn is_hermes_directive(line: &str) -> bool {
+        line.trim().starts_with('@')
+    }
+    /// Iterates over all doc attributes, parsing them, splitting into lines,
+    /// and yielding only those that are Hermes directives (start with `@`).
+    /// Returns trimmed lines.
+    pub fn iter_hermes_lines(attrs: &[Attribute]) -> impl Iterator<Item = String> + '_ {
+        attrs.iter().flat_map(|attr| {
+            if let Some(doc) = parse_doc_attr(attr) {
+                // We must collect to separate lifetime from `doc`
+                doc.lines()
+                    .map(|line| line.trim().to_string())
+                    .filter(|line| is_hermes_directive(line))
+                    .collect::<Vec<_>>()
+            } else {
+                Vec::new()
+            }
+        })
+    }

tools/hermes/src/include/__hermes_std.rs

-Original file line number
+Diff line change
@@ -1,3 +1,13 @@
+    // Copyright 2026 The Fuchsia Authors
+    //
+    // Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+    // <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+    // license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+    // This file may not be copied, modified, or distributed except according to
+    // those terms.
+    #![allow(dead_code, unused_imports)]
     pub use ::std::*;
     // Re-export the prelude so 'use std::prelude::rust_2021::*' works.
@@ Expand Down @@

tools/hermes/src/lib.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -14,6 +14,7 @@ @@
     //! - Stitching generated Lean code with user-provided proofs.
     pub mod desugar;
+    pub mod docs;
     pub mod orchestration;
     pub mod parser;
     pub mod pipeline;
@@ Expand Down @@

tools/hermes/src/main.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -50,6 +50,7 @@ pub enum Commands { @@
     }
     fn main() -> Result<()> {
+        env_logger::init();
         let CargoCli::Hermes(args) = CargoCli::parse();
         let Commands::Verify { crate_name, dest, aeneas_path, manifest_path, allow_sorry } =
             args.command;
@@ Expand Down @@

tools/hermes/src/orchestration.rs

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -20,18 +20,23 @@ pub fn run_charon(crate_root: &Path, dest_file: &Path, manifest_path: Option<&Pa
  
        let crate_root = crate_root.to_str().unwrap();

        let dest_file = dest_file.to_str().unwrap();

        println!("Running charon in {:?}", crate_root);

        log::debug!("Running charon in {:?}", crate_root);

        let mut cmd = Command::new("charon");

        cmd.env_remove("CARGO_TARGET_DIR"); // Avoid deadlock with outer cargo

        // Avoid deadlock with outer cargo

        cmd.env_remove("CARGO_TARGET_DIR");

        // Triggered when we convert `unsafe { ... }` into `{ ... }`.

        cmd.env("RUSTFLAGS", "-Aunused_braces");

        cmd.current_dir(crate_root);

        cmd.arg("cargo");

        // Charon args first

        args(&mut cmd, &["--dest-file", dest_file, "--preset", "aeneas"]);

        args(&mut cmd, &["--dest-file", dest_file, "--preset", "aeneas", "--error-on-warnings"]);

        if let Some(path) = manifest_path {

            cmd.arg("--");

            if path.extension().map_or(false, |e| e == "rs") {

            if path.extension().is_some_and(|e| e == "rs") {

                cmd.arg("-Zscript");

            }

            cmd.arg("--manifest-path");

    @@ -45,6 +50,8 @@ pub fn run_charon(crate_root: &Path, dest_file: &Path, manifest_path: Option<&Pa
  
        Ok(())

    }

    const ALL_AENEAS_BACKENDS: &str = "BorrowCheck,Builtin,Contexts,Deps,Errors,Extract,FunsAnalysis,Interp,InterpAbs,InterpBorrows,InterpExpansion,InterpExpressions,InterpJoin,InterpLoops,InterpLoopsFixedPoint,InterpMatchCtxs,InterpPaths,InterpProjectors,InterpReduceCollapse,InterpStatements,Invariants,MainLogger,PrePasses,PureMicroPasses,PureMicroPasses.simplify_aggregates_unchanged_fields,PureTypeCheck,PureUtils,RegionsHierarchy,ReorderDecls,SCC,SymbolicToPure,SymbolicToPureAbs,SymbolicToPureExpressions,SymbolicToPureTypes,SymbolicToPureValues,Translate,TypesAnalysis";

    /// Runs the Aeneas tool to translate LLBC files into Lean code.

    ///

    /// # Arguments

    @@ -55,7 +62,23 @@ pub fn run_aeneas(llbc_path: &Path, dest: &Path) -> Result<()> {
  
        let dest = dest.to_str().unwrap();

        let mut cmd = Command::new("aeneas");

        args(&mut cmd, &["-backend", "lean", llbc_path, "-dest", dest]);

        args(

            &mut cmd,

            &[

                "-backend",

                "lean",

                // TODO: Uncomment these once we've suppressed all warnings or

                // built a mechanism to conditionally disable passing this flag.

                //

                // "-log-error",

                // ALL_AENEAS_BACKENDS,

                "-warnings-as-errors",

                "-no-progress-bar",

                llbc_path,

                "-dest",

                dest,

            ],

        );

        let status = cmd.status().context("Failed to execute aeneas. Ensure it is in your PATH.")?;

        if !status.success() {

    @@ -72,6 +95,7 @@ pub fn run_lake_build(dir: &Path) -> Result<()> {
  
        let status = Command::new("lake")

            .current_dir(dir)

            .arg("build")

            .arg("--quiet")

            .status()

            .context("Failed to execute lake. Ensure Lean 4 is installed.")?;

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] Cleanup #2977

Diff view

Diff view

Uh oh!

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!

[WIP] Cleanup #2977

Are you sure you want to change the base?

[WIP] Cleanup #2977

Uh oh!

Diff view

Diff view

Uh oh!

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!