Merge pull request #8574 from Z3Prover/copilot/fix-a3-python-file-processing

Fix a3-python workflow sparse-checkout to include Python source files

.github/workflows/README-a3-python-fix.md

@@ -0,0 +1,60 @@
+# A3 Python Workflow Fix
+
+## Problem
+The a3-python workflow was not finding Python files in the repository because it was using sparse-checkout and only checking out `.github` and `.agents` directories. The Python source files in `src/api/python/z3/` were not being checked out.
+
+## Solution
+Added a custom `steps:` configuration in the workflow frontmatter to run `git sparse-checkout add src` before the agent executes. This ensures the Python source files are available for analysis.
+
+## Changes Made
+
+### 1. Frontmatter Update (lines 24-28)
+```yaml
+steps:
+  - name: Checkout Python source files
+    run: |
+      git sparse-checkout add src
+      echo "Python source files checked out from src directory"
+```
+
+This step runs before the AI agent starts, expanding the sparse-checkout to include the `src/` directory.
+
+### 2. Updated Analysis Instructions
+- Updated Phase 2.1 to explicitly verify `src/api/python/z3/` files are available
+- Changed the a3 command from `a3 analyze` to `a3 scan` with proper flags
+- Added specific documentation about which Python files should be analyzed:
+  - `z3.py` - Main Z3 Python API (350KB+)
+  - `z3printer.py` - Pretty printing functionality
+  - `z3num.py`, `z3poly.py`, `z3rcf.py` - Numeric and polynomial modules
+  - `z3types.py`, `z3util.py` - Type definitions and utilities
+
+### 3. Updated Exit Conditions
+Added mention of sparse checkout issues in the exit conditions to help with future debugging.
+
+## How to Recompile
+
+After modifying `a3-python.md`, you must recompile the workflow to generate the updated `.lock.yml` file:
+
+```bash
+# Compile the specific workflow
+gh aw compile a3-python
+
+# Or compile all workflows
+gh aw compile
+```
+
+This will update `a3-python.lock.yml` with the new sparse-checkout step.
+
+## Testing
+
+To test the workflow locally or in a PR:
+1. Trigger the workflow manually via workflow_dispatch
+2. Check the logs to verify:
+   - The "Checkout Python source files" step runs successfully
+   - Python files in `src/api/python/z3/` are found
+   - The a3 scan command analyzes those files
+
+## Related Files
+- `a3-python.md` - The workflow definition (source of truth)
+- `a3-python.lock.yml` - The compiled GitHub Actions workflow (auto-generated)
+- `src/api/python/z3/*.py` - The Python files that should be analyzed

.github/workflows/a3-python.md

@@ -21,6 +21,11 @@ name: A3 Python Code Analysis
 strict: true
 timeout-minutes: 45
 tracker-id: a3-python-analysis
+steps:
+  - name: Checkout Python source files
+    run: |
+      git sparse-checkout add src
+      echo "Python source files checked out from src directory"
 ---
 
 # A3 Python Code Analysis Agent
@@ -59,28 +64,36 @@ a3 --help || python -m a3 --help
 
 ### 2.1 Identify Python Files
 
-Find all Python files in the src directory:
+The Z3 repository contains Python source files primarily in `src/api/python/z3/`. Verify these files are available:
 
 ```bash
-find ${{ github.workspace }}/src -name "*.py" -type f | head -20
+# Check that src directory was checked out
+ls -la ${{ github.workspace }}/src/api/python/z3/
+
+# List Python files
+find ${{ github.workspace }}/src -name "*.py" -type f | head -30
 ```
 
 ### 2.2 Run a3-python Analysis
 
-Run the a3 analyze command on the src directory and save output to a file:
+Run the a3 scan command on the repository to analyze all Python files, particularly those in `src/api/python/z3/`:
 
 ```bash
 cd ${{ github.workspace }}
 
-# Try different command variations based on what's available
+# Ensure PATH includes a3 command
+export PATH="$PATH:/home/runner/.local/bin"
+
+# Run a3 scan on the repository with focus on src directory
 if command -v a3 &> /dev/null; then
-    a3 analyze ./src --generate-docs --dependency-graph > a3-python-output.txt 2>&1 || \
-    a3 analyze ./src > a3-python-output.txt 2>&1 || \
-    a3 debug ./src --execute-tests --validate-imports > a3-python-output.txt 2>&1 || \
-    echo "a3 analyze command failed with all variations" > a3-python-output.txt
+    # Run with multiple options for comprehensive analysis
+    a3 scan . --verbose --dse-verify --deduplicate --consolidate-variants > a3-python-output.txt 2>&1 || \
+    a3 scan src --verbose --functions --dse-verify > a3-python-output.txt 2>&1 || \
+    a3 scan src/api/python --verbose > a3-python-output.txt 2>&1 || \
+    echo "a3 scan command failed with all variations" > a3-python-output.txt
 elif python -m a3 --help &> /dev/null; then
-    python -m a3 analyze ./src > a3-python-output.txt 2>&1 || \
-    echo "python -m a3 analyze command failed" > a3-python-output.txt
+    python -m a3 scan src > a3-python-output.txt 2>&1 || \
+    echo "python -m a3 scan command failed" > a3-python-output.txt
 else
     echo "ERROR: a3-python tool not available" > a3-python-output.txt
 fi
@@ -90,7 +103,11 @@ ls -lh a3-python-output.txt
 cat a3-python-output.txt
 ```
 
-**Important**: Capture the complete output including any errors, warnings, and findings.
+**Important**: The a3-python tool should analyze the Python files in `src/api/python/z3/` which include:
+- `z3.py` - Main Z3 Python API (350KB+)
+- `z3printer.py` - Pretty printing functionality
+- `z3num.py`, `z3poly.py`, `z3rcf.py` - Numeric and polynomial modules
+- `z3types.py`, `z3util.py` - Type definitions and utilities
 
 ## Phase 3: Post-Process and Analyze Results
 
@@ -268,6 +285,7 @@ Create the issue using the safe-outputs configuration:
 
 Exit gracefully without creating an issue if:
 - Analysis tool failed to run or install
+- Python source files in `src/api/python/z3` were not checked out (sparse checkout issue)
 - No Python files found in src directory
 - Output file is empty or invalid
 - Zero or one true positive identified