3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 21:19:29 +00:00

latest improvers

This commit is contained in:
Don Syme 2025-09-17 13:49:00 +01:00
parent 2364ea42ba
commit aabdb407d1
6 changed files with 180 additions and 162 deletions

57
.github/workflows/ask.lock.yml generated vendored
View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run: # To update this file, edit the corresponding .md file and run:
# gh aw compile # gh aw compile
# #
# Effective stop-time: 2025-09-19 12:19:14 # Effective stop-time: 2025-09-19 12:48:19
name: "Question Answering Researcher" name: "Question Answering Researcher"
on: on:
@ -1066,7 +1066,7 @@ jobs:
WORKFLOW_NAME="Question Answering Researcher" WORKFLOW_NAME="Question Answering Researcher"
# Check stop-time limit # Check stop-time limit
STOP_TIME="2025-09-19 12:19:14" STOP_TIME="2025-09-19 12:48:19"
echo "Checking stop-time limit: $STOP_TIME" echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds # Convert stop time to epoch seconds
@ -1396,24 +1396,21 @@ jobs:
* @returns {string} The string with unknown domains redacted * @returns {string} The string with unknown domains redacted
*/ */
function sanitizeUrlDomains(s) { function sanitizeUrlDomains(s) {
return s.replace( return s.replace(/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, match => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, // Extract just the URL part after https://
(match) => { const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract just the URL part after https:// // Extract the hostname part (before first slash, colon, or other delimiter)
const urlAfterProtocol = match.slice(8); // Remove 'https://' const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Extract the hostname part (before first slash, colon, or other delimiter) // Check if this domain or any parent domain is in the allowlist
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase(); const isAllowed = allowedDomains.some(allowedDomain => {
// Check if this domain or any parent domain is in the allowlist const normalizedAllowed = allowedDomain.toLowerCase();
const isAllowed = allowedDomains.some(allowedDomain => { return (
const normalizedAllowed = allowedDomain.toLowerCase(); hostname === normalizedAllowed ||
return ( hostname.endsWith("." + normalizedAllowed)
hostname === normalizedAllowed || );
hostname.endsWith("." + normalizedAllowed) });
); return isAllowed ? match : "(redacted)";
}); });
return isAllowed ? match : "(redacted)";
}
);
} }
/** /**
* Remove unknown protocols except https * Remove unknown protocols except https
@ -2113,16 +2110,22 @@ jobs:
} }
core.setOutput("output", JSON.stringify(validatedOutput)); core.setOutput("output", JSON.stringify(validatedOutput));
core.setOutput("raw_output", outputContent); core.setOutput("raw_output", outputContent);
// Write processed output to step summary using core.summary
try {
await core.summary
.addRaw("## Processed Output\n\n")
.addRaw("```json\n")
.addRaw(JSON.stringify(validatedOutput))
.addRaw("\n```\n")
.write();
core.info("Successfully wrote processed output to step summary");
} catch (error) {
const errorMsg = error instanceof Error ? error.message : String(error);
core.warning(`Failed to write to step summary: ${errorMsg}`);
}
} }
// Call the main function // Call the main function
await main(); await main();
- name: Print sanitized agent output
run: |
echo "## Processed Output" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo '``````json' >> $GITHUB_STEP_SUMMARY
echo '${{ steps.collect_output.outputs.output }}' >> $GITHUB_STEP_SUMMARY
echo '``````' >> $GITHUB_STEP_SUMMARY
- name: Upload sanitized agent output - name: Upload sanitized agent output
if: always() && env.GITHUB_AW_AGENT_OUTPUT if: always() && env.GITHUB_AW_AGENT_OUTPUT
uses: actions/upload-artifact@v4 uses: actions/upload-artifact@v4

57
.github/workflows/ci-doctor.lock.yml generated vendored
View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run: # To update this file, edit the corresponding .md file and run:
# gh aw compile # gh aw compile
# #
# Effective stop-time: 2025-09-19 12:19:14 # Effective stop-time: 2025-09-19 12:48:19
name: "CI Failure Doctor" name: "CI Failure Doctor"
"on": "on":
@ -547,7 +547,7 @@ jobs:
WORKFLOW_NAME="CI Failure Doctor" WORKFLOW_NAME="CI Failure Doctor"
# Check stop-time limit # Check stop-time limit
STOP_TIME="2025-09-19 12:19:14" STOP_TIME="2025-09-19 12:48:19"
echo "Checking stop-time limit: $STOP_TIME" echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds # Convert stop time to epoch seconds
@ -1010,24 +1010,21 @@ jobs:
* @returns {string} The string with unknown domains redacted * @returns {string} The string with unknown domains redacted
*/ */
function sanitizeUrlDomains(s) { function sanitizeUrlDomains(s) {
return s.replace( return s.replace(/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, match => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, // Extract just the URL part after https://
(match) => { const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract just the URL part after https:// // Extract the hostname part (before first slash, colon, or other delimiter)
const urlAfterProtocol = match.slice(8); // Remove 'https://' const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Extract the hostname part (before first slash, colon, or other delimiter) // Check if this domain or any parent domain is in the allowlist
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase(); const isAllowed = allowedDomains.some(allowedDomain => {
// Check if this domain or any parent domain is in the allowlist const normalizedAllowed = allowedDomain.toLowerCase();
const isAllowed = allowedDomains.some(allowedDomain => { return (
const normalizedAllowed = allowedDomain.toLowerCase(); hostname === normalizedAllowed ||
return ( hostname.endsWith("." + normalizedAllowed)
hostname === normalizedAllowed || );
hostname.endsWith("." + normalizedAllowed) });
); return isAllowed ? match : "(redacted)";
}); });
return isAllowed ? match : "(redacted)";
}
);
} }
/** /**
* Remove unknown protocols except https * Remove unknown protocols except https
@ -1727,16 +1724,22 @@ jobs:
} }
core.setOutput("output", JSON.stringify(validatedOutput)); core.setOutput("output", JSON.stringify(validatedOutput));
core.setOutput("raw_output", outputContent); core.setOutput("raw_output", outputContent);
// Write processed output to step summary using core.summary
try {
await core.summary
.addRaw("## Processed Output\n\n")
.addRaw("```json\n")
.addRaw(JSON.stringify(validatedOutput))
.addRaw("\n```\n")
.write();
core.info("Successfully wrote processed output to step summary");
} catch (error) {
const errorMsg = error instanceof Error ? error.message : String(error);
core.warning(`Failed to write to step summary: ${errorMsg}`);
}
} }
// Call the main function // Call the main function
await main(); await main();
- name: Print sanitized agent output
run: |
echo "## Processed Output" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo '``````json' >> $GITHUB_STEP_SUMMARY
echo '${{ steps.collect_output.outputs.output }}' >> $GITHUB_STEP_SUMMARY
echo '``````' >> $GITHUB_STEP_SUMMARY
- name: Upload sanitized agent output - name: Upload sanitized agent output
if: always() && env.GITHUB_AW_AGENT_OUTPUT if: always() && env.GITHUB_AW_AGENT_OUTPUT
uses: actions/upload-artifact@v4 uses: actions/upload-artifact@v4

View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run: # To update this file, edit the corresponding .md file and run:
# gh aw compile # gh aw compile
# #
# Effective stop-time: 2025-09-19 12:19:14 # Effective stop-time: 2025-09-19 12:48:20
name: "Daily Backlog Burner" name: "Daily Backlog Burner"
"on": "on":
@ -527,7 +527,7 @@ jobs:
WORKFLOW_NAME="Daily Backlog Burner" WORKFLOW_NAME="Daily Backlog Burner"
# Check stop-time limit # Check stop-time limit
STOP_TIME="2025-09-19 12:19:14" STOP_TIME="2025-09-19 12:48:20"
echo "Checking stop-time limit: $STOP_TIME" echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds # Convert stop time to epoch seconds
@ -923,24 +923,21 @@ jobs:
* @returns {string} The string with unknown domains redacted * @returns {string} The string with unknown domains redacted
*/ */
function sanitizeUrlDomains(s) { function sanitizeUrlDomains(s) {
return s.replace( return s.replace(/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, match => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, // Extract just the URL part after https://
(match) => { const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract just the URL part after https:// // Extract the hostname part (before first slash, colon, or other delimiter)
const urlAfterProtocol = match.slice(8); // Remove 'https://' const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Extract the hostname part (before first slash, colon, or other delimiter) // Check if this domain or any parent domain is in the allowlist
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase(); const isAllowed = allowedDomains.some(allowedDomain => {
// Check if this domain or any parent domain is in the allowlist const normalizedAllowed = allowedDomain.toLowerCase();
const isAllowed = allowedDomains.some(allowedDomain => { return (
const normalizedAllowed = allowedDomain.toLowerCase(); hostname === normalizedAllowed ||
return ( hostname.endsWith("." + normalizedAllowed)
hostname === normalizedAllowed || );
hostname.endsWith("." + normalizedAllowed) });
); return isAllowed ? match : "(redacted)";
}); });
return isAllowed ? match : "(redacted)";
}
);
} }
/** /**
* Remove unknown protocols except https * Remove unknown protocols except https
@ -1640,16 +1637,22 @@ jobs:
} }
core.setOutput("output", JSON.stringify(validatedOutput)); core.setOutput("output", JSON.stringify(validatedOutput));
core.setOutput("raw_output", outputContent); core.setOutput("raw_output", outputContent);
// Write processed output to step summary using core.summary
try {
await core.summary
.addRaw("## Processed Output\n\n")
.addRaw("```json\n")
.addRaw(JSON.stringify(validatedOutput))
.addRaw("\n```\n")
.write();
core.info("Successfully wrote processed output to step summary");
} catch (error) {
const errorMsg = error instanceof Error ? error.message : String(error);
core.warning(`Failed to write to step summary: ${errorMsg}`);
}
} }
// Call the main function // Call the main function
await main(); await main();
- name: Print sanitized agent output
run: |
echo "## Processed Output" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo '``````json' >> $GITHUB_STEP_SUMMARY
echo '${{ steps.collect_output.outputs.output }}' >> $GITHUB_STEP_SUMMARY
echo '``````' >> $GITHUB_STEP_SUMMARY
- name: Upload sanitized agent output - name: Upload sanitized agent output
if: always() && env.GITHUB_AW_AGENT_OUTPUT if: always() && env.GITHUB_AW_AGENT_OUTPUT
uses: actions/upload-artifact@v4 uses: actions/upload-artifact@v4

View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run: # To update this file, edit the corresponding .md file and run:
# gh aw compile # gh aw compile
# #
# Effective stop-time: 2025-09-19 12:19:14 # Effective stop-time: 2025-09-19 12:48:20
name: "Daily Perf Improver" name: "Daily Perf Improver"
"on": "on":
@ -541,7 +541,7 @@ jobs:
WORKFLOW_NAME="Daily Perf Improver" WORKFLOW_NAME="Daily Perf Improver"
# Check stop-time limit # Check stop-time limit
STOP_TIME="2025-09-19 12:19:14" STOP_TIME="2025-09-19 12:48:20"
echo "Checking stop-time limit: $STOP_TIME" echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds # Convert stop time to epoch seconds
@ -998,24 +998,21 @@ jobs:
* @returns {string} The string with unknown domains redacted * @returns {string} The string with unknown domains redacted
*/ */
function sanitizeUrlDomains(s) { function sanitizeUrlDomains(s) {
return s.replace( return s.replace(/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, match => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, // Extract just the URL part after https://
(match) => { const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract just the URL part after https:// // Extract the hostname part (before first slash, colon, or other delimiter)
const urlAfterProtocol = match.slice(8); // Remove 'https://' const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Extract the hostname part (before first slash, colon, or other delimiter) // Check if this domain or any parent domain is in the allowlist
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase(); const isAllowed = allowedDomains.some(allowedDomain => {
// Check if this domain or any parent domain is in the allowlist const normalizedAllowed = allowedDomain.toLowerCase();
const isAllowed = allowedDomains.some(allowedDomain => { return (
const normalizedAllowed = allowedDomain.toLowerCase(); hostname === normalizedAllowed ||
return ( hostname.endsWith("." + normalizedAllowed)
hostname === normalizedAllowed || );
hostname.endsWith("." + normalizedAllowed) });
); return isAllowed ? match : "(redacted)";
}); });
return isAllowed ? match : "(redacted)";
}
);
} }
/** /**
* Remove unknown protocols except https * Remove unknown protocols except https
@ -1715,16 +1712,22 @@ jobs:
} }
core.setOutput("output", JSON.stringify(validatedOutput)); core.setOutput("output", JSON.stringify(validatedOutput));
core.setOutput("raw_output", outputContent); core.setOutput("raw_output", outputContent);
// Write processed output to step summary using core.summary
try {
await core.summary
.addRaw("## Processed Output\n\n")
.addRaw("```json\n")
.addRaw(JSON.stringify(validatedOutput))
.addRaw("\n```\n")
.write();
core.info("Successfully wrote processed output to step summary");
} catch (error) {
const errorMsg = error instanceof Error ? error.message : String(error);
core.warning(`Failed to write to step summary: ${errorMsg}`);
}
} }
// Call the main function // Call the main function
await main(); await main();
- name: Print sanitized agent output
run: |
echo "## Processed Output" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo '``````json' >> $GITHUB_STEP_SUMMARY
echo '${{ steps.collect_output.outputs.output }}' >> $GITHUB_STEP_SUMMARY
echo '``````' >> $GITHUB_STEP_SUMMARY
- name: Upload sanitized agent output - name: Upload sanitized agent output
if: always() && env.GITHUB_AW_AGENT_OUTPUT if: always() && env.GITHUB_AW_AGENT_OUTPUT
uses: actions/upload-artifact@v4 uses: actions/upload-artifact@v4

View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run: # To update this file, edit the corresponding .md file and run:
# gh aw compile # gh aw compile
# #
# Effective stop-time: 2025-09-19 12:19:15 # Effective stop-time: 2025-09-19 12:48:20
name: "Daily Test Coverage Improver" name: "Daily Test Coverage Improver"
"on": "on":
@ -541,7 +541,7 @@ jobs:
WORKFLOW_NAME="Daily Test Coverage Improver" WORKFLOW_NAME="Daily Test Coverage Improver"
# Check stop-time limit # Check stop-time limit
STOP_TIME="2025-09-19 12:19:15" STOP_TIME="2025-09-19 12:48:20"
echo "Checking stop-time limit: $STOP_TIME" echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds # Convert stop time to epoch seconds
@ -973,24 +973,21 @@ jobs:
* @returns {string} The string with unknown domains redacted * @returns {string} The string with unknown domains redacted
*/ */
function sanitizeUrlDomains(s) { function sanitizeUrlDomains(s) {
return s.replace( return s.replace(/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, match => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, // Extract just the URL part after https://
(match) => { const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract just the URL part after https:// // Extract the hostname part (before first slash, colon, or other delimiter)
const urlAfterProtocol = match.slice(8); // Remove 'https://' const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Extract the hostname part (before first slash, colon, or other delimiter) // Check if this domain or any parent domain is in the allowlist
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase(); const isAllowed = allowedDomains.some(allowedDomain => {
// Check if this domain or any parent domain is in the allowlist const normalizedAllowed = allowedDomain.toLowerCase();
const isAllowed = allowedDomains.some(allowedDomain => { return (
const normalizedAllowed = allowedDomain.toLowerCase(); hostname === normalizedAllowed ||
return ( hostname.endsWith("." + normalizedAllowed)
hostname === normalizedAllowed || );
hostname.endsWith("." + normalizedAllowed) });
); return isAllowed ? match : "(redacted)";
}); });
return isAllowed ? match : "(redacted)";
}
);
} }
/** /**
* Remove unknown protocols except https * Remove unknown protocols except https
@ -1690,16 +1687,22 @@ jobs:
} }
core.setOutput("output", JSON.stringify(validatedOutput)); core.setOutput("output", JSON.stringify(validatedOutput));
core.setOutput("raw_output", outputContent); core.setOutput("raw_output", outputContent);
// Write processed output to step summary using core.summary
try {
await core.summary
.addRaw("## Processed Output\n\n")
.addRaw("```json\n")
.addRaw(JSON.stringify(validatedOutput))
.addRaw("\n```\n")
.write();
core.info("Successfully wrote processed output to step summary");
} catch (error) {
const errorMsg = error instanceof Error ? error.message : String(error);
core.warning(`Failed to write to step summary: ${errorMsg}`);
}
} }
// Call the main function // Call the main function
await main(); await main();
- name: Print sanitized agent output
run: |
echo "## Processed Output" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo '``````json' >> $GITHUB_STEP_SUMMARY
echo '${{ steps.collect_output.outputs.output }}' >> $GITHUB_STEP_SUMMARY
echo '``````' >> $GITHUB_STEP_SUMMARY
- name: Upload sanitized agent output - name: Upload sanitized agent output
if: always() && env.GITHUB_AW_AGENT_OUTPUT if: always() && env.GITHUB_AW_AGENT_OUTPUT
uses: actions/upload-artifact@v4 uses: actions/upload-artifact@v4

57
.github/workflows/pr-fix.lock.yml generated vendored
View file

@ -2,7 +2,7 @@
# To update this file, edit the corresponding .md file and run: # To update this file, edit the corresponding .md file and run:
# gh aw compile # gh aw compile
# #
# Effective stop-time: 2025-09-19 12:19:15 # Effective stop-time: 2025-09-19 12:48:20
name: "PR Fix" name: "PR Fix"
on: on:
@ -1071,7 +1071,7 @@ jobs:
WORKFLOW_NAME="PR Fix" WORKFLOW_NAME="PR Fix"
# Check stop-time limit # Check stop-time limit
STOP_TIME="2025-09-19 12:19:15" STOP_TIME="2025-09-19 12:48:20"
echo "Checking stop-time limit: $STOP_TIME" echo "Checking stop-time limit: $STOP_TIME"
# Convert stop time to epoch seconds # Convert stop time to epoch seconds
@ -1427,24 +1427,21 @@ jobs:
* @returns {string} The string with unknown domains redacted * @returns {string} The string with unknown domains redacted
*/ */
function sanitizeUrlDomains(s) { function sanitizeUrlDomains(s) {
return s.replace( return s.replace(/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, match => {
/\bhttps:\/\/[^\s\])}'"<>&\x00-\x1f,;]+/gi, // Extract just the URL part after https://
(match) => { const urlAfterProtocol = match.slice(8); // Remove 'https://'
// Extract just the URL part after https:// // Extract the hostname part (before first slash, colon, or other delimiter)
const urlAfterProtocol = match.slice(8); // Remove 'https://' const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase();
// Extract the hostname part (before first slash, colon, or other delimiter) // Check if this domain or any parent domain is in the allowlist
const hostname = urlAfterProtocol.split(/[\/:\?#]/)[0].toLowerCase(); const isAllowed = allowedDomains.some(allowedDomain => {
// Check if this domain or any parent domain is in the allowlist const normalizedAllowed = allowedDomain.toLowerCase();
const isAllowed = allowedDomains.some(allowedDomain => { return (
const normalizedAllowed = allowedDomain.toLowerCase(); hostname === normalizedAllowed ||
return ( hostname.endsWith("." + normalizedAllowed)
hostname === normalizedAllowed || );
hostname.endsWith("." + normalizedAllowed) });
); return isAllowed ? match : "(redacted)";
}); });
return isAllowed ? match : "(redacted)";
}
);
} }
/** /**
* Remove unknown protocols except https * Remove unknown protocols except https
@ -2144,16 +2141,22 @@ jobs:
} }
core.setOutput("output", JSON.stringify(validatedOutput)); core.setOutput("output", JSON.stringify(validatedOutput));
core.setOutput("raw_output", outputContent); core.setOutput("raw_output", outputContent);
// Write processed output to step summary using core.summary
try {
await core.summary
.addRaw("## Processed Output\n\n")
.addRaw("```json\n")
.addRaw(JSON.stringify(validatedOutput))
.addRaw("\n```\n")
.write();
core.info("Successfully wrote processed output to step summary");
} catch (error) {
const errorMsg = error instanceof Error ? error.message : String(error);
core.warning(`Failed to write to step summary: ${errorMsg}`);
}
} }
// Call the main function // Call the main function
await main(); await main();
- name: Print sanitized agent output
run: |
echo "## Processed Output" >> $GITHUB_STEP_SUMMARY
echo "" >> $GITHUB_STEP_SUMMARY
echo '``````json' >> $GITHUB_STEP_SUMMARY
echo '${{ steps.collect_output.outputs.output }}' >> $GITHUB_STEP_SUMMARY
echo '``````' >> $GITHUB_STEP_SUMMARY
- name: Upload sanitized agent output - name: Upload sanitized agent output
if: always() && env.GITHUB_AW_AGENT_OUTPUT if: always() && env.GITHUB_AW_AGENT_OUTPUT
uses: actions/upload-artifact@v4 uses: actions/upload-artifact@v4