Skip to content

add a3-rust workflow to generate verification output from Halley Young's Rust checker#647

Open
NikolajBjorner wants to merge 1 commit intomicrosoft:mainfrom
NikolajBjorner:main
Open

add a3-rust workflow to generate verification output from Halley Young's Rust checker#647
NikolajBjorner wants to merge 1 commit intomicrosoft:mainfrom
NikolajBjorner:main

Conversation

@NikolajBjorner
Copy link

This is going to be my first attempt to integrate what I call the a3-rust checker with a github project.
There are two parts to it:

  1. a3-rust.yml - a standard github action workflow that calls an extended static checker for rust to identify common programming mistakes.
  2. setting up agentic workflows in the repository and installing an agentic workflow.
    • per gh.io/gh-aw (https://github.github.io/gh-aw/setup/quick-start/)

      • open a fresh code space in github.
      • gh extension install github/gh-aw
      • and I tend to then "gh aw init" and "git push" though the setup instructions are fluctuating a bit.
      • agentic workflows are soon going to be broadly advertised. So you are still cutting edge.
      • then, also from the litebox repository do: "aw add https://github.com/Z3Prover/z3/blob/master/a3/a3-rust.md" It should install the agentic workflow I prepared to post-process the output of a3-rust.yml.

      The two workflows are set up to be run manually. You can change this, but first run a3-rust.yml, then when it finishes (take 1hr currently), then run the agentic workflow.

It should create an issue, hopefully with a reasonable report if it claims it finds bugs. I haven't been able to test this last mile step because I can't post issues from my sandbox (or at least I don't easily see how to do this).

Could I persuade you to give it a spin?

@microsoft/halleyyoung_microsoft
@ Peli

…g's Rust checker

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.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