Skip to content

Add deal framework for formal verification with release no-ops#167

Open
KeithCu wants to merge 2 commits intomasterfrom
jules-formal-verification-deal-setup-2851407568774976233
Open

Add deal framework for formal verification with release no-ops#167
KeithCu wants to merge 2 commits intomasterfrom
jules-formal-verification-deal-setup-2851407568774976233

Conversation

@KeithCu
Copy link
Copy Markdown
Owner

@KeithCu KeithCu commented Mar 21, 2026

This commit introduces the infrastructure needed to begin formal verification using the deal library. It includes the necessary dependencies in pyproject.toml and provides a compatibility wrapper (plugin/framework/deal_compat.py) that safely aliases decorators in debug builds while stubbing them out in release builds so end-users don't incur performance overhead or need to install deal.


PR created automatically by Jules for task 2851407568774976233 started by @KeithCu

Added `deal` and `crosshair-tool` to pyproject.toml dev dependencies.
Created `plugin/framework/deal_compat.py` to conditionally load `deal`
decorators during development while substituting them with robust,
zero-overhead no-op functions in release builds (detected by the absence
of the `plugin/tests/` directory).

Updated AGENTS.md to document the correct usage of this compatibility
layer.

Co-authored-by: KeithCu <662157+KeithCu@users.noreply.github.com>
@google-labs-jules
Copy link
Copy Markdown

👋 Jules, reporting for duty! I'm here to lend a hand with this pull request.

When you start a review, I'll add a 👀 emoji to each comment to let you know I've read it. I'll focus on feedback directed at me and will do my best to stay out of conversations between you and other bots or reviewers to keep the noise down.

I'll push a commit with your requested changes shortly after. Please note there might be a delay between these steps, but rest assured I'm on the job!

For more direct control, you can switch me to Reactive Mode. When this mode is on, I will only act on comments where you specifically mention me with @jules. You can find this option in the Pull Request section of your global Jules UI settings. You can always switch back!

New to Jules? Learn more at jules.google/docs.


For security, I will only act on instructions from the user who triggered this task.

Added `deal` and `crosshair-tool` to pyproject.toml dev dependencies.
Vendored the `deal` library into `plugin/contrib/deal/` to ensure
compatibility with the LibreOffice embedded Python runtime without
requiring external installation by users.

Created `plugin/framework/deal_compat.py` to conditionally load `deal`
decorators (trying the vendored version first) during development while
substituting them with robust, zero-overhead no-op functions in release
builds (detected by the absence of the `plugin/tests/` directory).

Updated AGENTS.md to document the correct usage of this compatibility
layer.

Co-authored-by: KeithCu <662157+KeithCu@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant