') + ')', 'gi'); if (regex.test(text)) { found = true; var frag = document.createDocumentFragment(); var parts = text.split(regex); parts.forEach(function(part, i) { if (i % 2 === 0) { frag.appendChild(document.createTextNode(part)); } else { var span = document.createElement('span'); span.className = 'userscript-highlight'; span.textContent = part; frag.appendChild(span); } }); node.parentNode.replaceChild(frag, node); } }); } else if (node.nodeType === 1 && node.childNodes) { // element var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT']; if (!skipTags.includes(node.tagName)) { Array.from(node.childNodes).forEach(highlight); } } } highlight(document.body); // Re-highlight on dynamic content var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1 || node.nodeType === 3) highlight(node); }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ', 'i'); if (__m === '*' || __re.test(location.href)) { // Strip utm_, fbclid, gclid, etc. from all links on page (function() { var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content', 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid', 'ref', 'ref_src', 'source', 'medium', 'campaign']; function cleanUrl(url) { try { var u = new URL(url, window.location.origin); var changed = false; trackingParams.forEach(function(p) { if (u.searchParams.has(p)) { u.searchParams.delete(p); changed = true; } }); return changed ? u.toString() : url; } catch (e) { return url; } } function cleanLinks() { document.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } cleanLinks(); var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1) { if (node.tagName === 'A') cleanLinks(); node.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); } })(); (function(){ try { var __m = "youtube.com"; var __re = new RegExp('^' + "youtube\\.com" + ', 'i'); if (__m === '*' || __re.test(location.href)) { // Auto-enable theater mode on YouTube (function() { function tryTheater() { var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]'); if (btn && !btn.classList.contains('activated')) { btn.click(); } } // Try immediately tryTheater(); // Try after navigation (SPA) var lastUrl = location.href; setInterval(function() { if (location.href !== lastUrl) { lastUrl = location.href; setTimeout(tryTheater, 500); } }, 1000); // Also try on player load var observer = new MutationObserver(tryTheater); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ', 'i'); if (__m === '*' || __re.test(location.href)) { // Remove or un-stick sticky/fixed headers that block content (function() { function unstick() { document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) { if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') { el.style.position = 'static'; el.style.top = 'auto'; el.style.zIndex = 'auto'; } }); } unstick(); var observer = new MutationObserver(unstick); observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] }); })(); } } catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); } })(); })(); add a3-rust workflow to generate verification output from Halley Young's Rust checker by NikolajBjorner · Pull Request #647 · microsoft/litebox · GitHub
Skip to content

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

Open
Nikolaj Bjorner (NikolajBjorner) wants to merge 1 commit into
microsoft:mainfrom
NikolajBjorner:main
Open

add a3-rust workflow to generate verification output from Halley Young's Rust checker#647
Nikolaj Bjorner (NikolajBjorner) wants to merge 1 commit into
microsoft:mainfrom
NikolajBjorner:main

Conversation

@NikolajBjorner

Copy link
Copy Markdown

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>

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks Nikolaj! As I'd mentioned in our separate discussions, this is really cool, and indeed from the test results you had shown, the issues shown were ones we would like to fix up.

Reading the workflow, I have some changes I'd like to make before merging it, so as to keep things more maintainable long-term, but given current constraints, I won't be able to bump this to the top of the list for a little while, I hope you understand.

Keeping this PR open but marking it as a "request changes" as a reminder to myself that I'd like to make changes before merging. No explicit changes requested from you right now, thanks!

Sign up for freeto 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.

2 participants

@NikolajBjorner@jaybosamiya-ms