Skip to content

Commit 054f7e0

Browse files
dsymedsyme
committed
update workflows
1 parent 298f992 commit 054f7e0

6 files changed

Lines changed: 130 additions & 114 deletions

File tree

‎.github/aw/actions-lock.json‎

Lines changed: 13 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,16 +40,26 @@
4040
"version": "v7.0.0",
4141
"sha": "bbbca2ddaa5d8feaa63e36b76fdaad77386f024f"
4242
},
43-
"github/gh-aw-actions/setup@v0.76.1": {
43+
"github/gh-aw-actions/setup@v0.78.2": {
4444
"repo": "github/gh-aw-actions/setup",
45-
"version": "v0.76.1",
46-
"sha": "46d564922b082d0db93244972e8005ea6904ee5f"
45+
"version": "v0.78.2",
46+
"sha": "268bf92726cb8153337c07166f382ee46e4fd897"
4747
},
4848
"github/gh-aw/actions/setup-cli@v0.76.1": {
4949
"repo": "github/gh-aw/actions/setup-cli",
5050
"version": "v0.76.1",
5151
"sha": "58d1bedbb7200f59c2d224151339e38fd8687d05"
5252
},
53+
"github/gh-aw/actions/setup-cli@v0.78.1": {
54+
"repo": "github/gh-aw/actions/setup-cli",
55+
"version": "v0.78.1",
56+
"sha": "bb82d257a1aac50e66a82284a98646ac93bfe802"
57+
},
58+
"github/gh-aw/actions/setup-cli@v0.78.2": {
59+
"repo": "github/gh-aw/actions/setup-cli",
60+
"version": "v0.78.2",
61+
"sha": "a7d4043a8224182262356a32931099b76fd332eb"
62+
},
5363
"github/gh-aw/actions/setup@v0.66.1": {
5464
"repo": "github/gh-aw/actions/setup",
5565
"version": "v0.66.1",

‎workflows/ai-moderator.md‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,10 +15,6 @@ on:
1515
skip-roles: [admin, maintainer, write, triage]
1616
skip-bots: [github-actions, copilot, dependabot]
1717

18-
rate-limit:
19-
max: 5
20-
window: 60
21-
2218
# # This workflow runs often, so you can use a small model to keep costs down.
2319
# engine:
2420
# model: small

‎workflows/lean-squad.md‎

Lines changed: 78 additions & 72 deletions
Original file line numberDiff line numberDiff line change
@@ -94,64 +94,64 @@ steps:
9494
env:
9595
GH_TOKEN: ${{ github.token }}
9696
run: |
97-
mkdir -p /tmp/gh-aw
97+
mkdir -p /tmp/gh-aw/agent
9898
9999
# Count Lean files, excluding the .lake build cache
100-
find . -name "*.lean" 2>/dev/null | grep -cv "\.lake/" > /tmp/gh-aw/lean_count.txt || echo 0 > /tmp/gh-aw/lean_count.txt
100+
find . -name "*.lean" 2>/dev/null | grep -cv "\.lake/" > /tmp/gh-aw/agent/lean_count.txt || echo 0 > /tmp/gh-aw/agent/lean_count.txt
101101
102102
# Count Rust source files (for Aeneas eligibility)
103-
find . -name "*.rs" -not -path "./target/*" 2>/dev/null | wc -l > /tmp/gh-aw/rust_count.txt || echo 0 > /tmp/gh-aw/rust_count.txt
103+
find . -name "*.rs" -not -path "./target/*" 2>/dev/null | wc -l > /tmp/gh-aw/agent/rust_count.txt || echo 0 > /tmp/gh-aw/agent/rust_count.txt
104104
105105
# Detect CI workflows for FV
106-
[ -f ".github/workflows/lean-ci.yml" ] && echo 1 > /tmp/gh-aw/has_lean_ci.txt || echo 0 > /tmp/gh-aw/has_lean_ci.txt
107-
[ -f ".github/workflows/aeneas-generate.yml" ] && echo 1 > /tmp/gh-aw/has_aeneas_ci.txt || echo 0 > /tmp/gh-aw/has_aeneas_ci.txt
106+
[ -f ".github/workflows/lean-ci.yml" ] && echo 1 > /tmp/gh-aw/agent/has_lean_ci.txt || echo 0 > /tmp/gh-aw/agent/has_lean_ci.txt
107+
[ -f ".github/workflows/aeneas-generate.yml" ] && echo 1 > /tmp/gh-aw/agent/has_aeneas_ci.txt || echo 0 > /tmp/gh-aw/agent/has_aeneas_ci.txt
108108
109109
# Count runnable correspondence-test artifacts for Task 8
110110
find . \( -path "./formal-verification/tests/*" -o -path "./formal-verification/correspondence-tests/*" \) -type f 2>/dev/null \
111-
| wc -l > /tmp/gh-aw/correspondence_test_count.txt || echo 0 > /tmp/gh-aw/correspondence_test_count.txt
111+
| wc -l > /tmp/gh-aw/agent/correspondence_test_count.txt || echo 0 > /tmp/gh-aw/agent/correspondence_test_count.txt
112112
113113
# Detect CORRESPONDENCE.md, CRITIQUE.md, REPORT.md, and paper/paper.tex
114-
[ -f "formal-verification/CORRESPONDENCE.md" ] && echo 1 > /tmp/gh-aw/has_correspondence.txt || echo 0 > /tmp/gh-aw/has_correspondence.txt
115-
[ -f "formal-verification/CRITIQUE.md" ] && echo 1 > /tmp/gh-aw/has_critique.txt || echo 0 > /tmp/gh-aw/has_critique.txt
116-
[ -f "formal-verification/REPORT.md" ] && echo 1 > /tmp/gh-aw/has_report.txt || echo 0 > /tmp/gh-aw/has_report.txt
117-
[ -f "formal-verification/paper/paper.tex" ] && echo 1 > /tmp/gh-aw/has_paper.txt || echo 0 > /tmp/gh-aw/has_paper.txt
114+
[ -f "formal-verification/CORRESPONDENCE.md" ] && echo 1 > /tmp/gh-aw/agent/has_correspondence.txt || echo 0 > /tmp/gh-aw/agent/has_correspondence.txt
115+
[ -f "formal-verification/CRITIQUE.md" ] && echo 1 > /tmp/gh-aw/agent/has_critique.txt || echo 0 > /tmp/gh-aw/agent/has_critique.txt
116+
[ -f "formal-verification/REPORT.md" ] && echo 1 > /tmp/gh-aw/agent/has_report.txt || echo 0 > /tmp/gh-aw/agent/has_report.txt
117+
[ -f "formal-verification/paper/paper.tex" ] && echo 1 > /tmp/gh-aw/agent/has_paper.txt || echo 0 > /tmp/gh-aw/agent/has_paper.txt
118118
119119
# Detect formal-verification directory
120-
[ -d "formal-verification" ] && echo 1 > /tmp/gh-aw/fv_dir.txt || echo 0 > /tmp/gh-aw/fv_dir.txt
120+
[ -d "formal-verification" ] && echo 1 > /tmp/gh-aw/agent/fv_dir.txt || echo 0 > /tmp/gh-aw/agent/fv_dir.txt
121121
122122
# Count markdown docs inside formal-verification/
123123
find . \( -path "*/formal-verification/*.md" -o -path "*/formal-verification/specs/*.md" \) 2>/dev/null \
124-
| wc -l > /tmp/gh-aw/fv_docs.txt || echo 0 > /tmp/gh-aw/fv_docs.txt
124+
| wc -l > /tmp/gh-aw/agent/fv_docs.txt || echo 0 > /tmp/gh-aw/agent/fv_docs.txt
125125
126126
# Fetch open FV Squad issues
127127
gh issue list --state open --label lean-squad --json number 2>/dev/null \
128-
> /tmp/gh-aw/fv_issues.json || echo "[]" > /tmp/gh-aw/fv_issues.json
128+
> /tmp/gh-aw/agent/fv_issues.json || echo "[]" > /tmp/gh-aw/agent/fv_issues.json
129129
130130
# Fetch open FV Squad PRs
131131
gh pr list --state open --limit 50 --json number,title 2>/dev/null \
132132
| python3 -c "
133133
import json, sys
134134
d = json.load(sys.stdin)
135135
print(json.dumps([x for x in d if x['title'].startswith('[lean-squad]')]))" \
136-
> /tmp/gh-aw/fv_prs.json || echo "[]" > /tmp/gh-aw/fv_prs.json
136+
> /tmp/gh-aw/agent/fv_prs.json || echo "[]" > /tmp/gh-aw/agent/fv_prs.json
137137
138138
python3 - << 'EOF'
139139
import json, os, random, re
140140
from pathlib import Path
141141
142-
lean_count = int(open('/tmp/gh-aw/lean_count.txt').read().strip() or 0)
143-
rust_count = int(open('/tmp/gh-aw/rust_count.txt').read().strip() or 0)
144-
has_lean_ci = int(open('/tmp/gh-aw/has_lean_ci.txt').read().strip() or 0)
145-
has_aeneas_ci = int(open('/tmp/gh-aw/has_aeneas_ci.txt').read().strip() or 0)
146-
correspondence_test_count = int(open('/tmp/gh-aw/correspondence_test_count.txt').read().strip() or 0)
147-
has_correspondence = int(open('/tmp/gh-aw/has_correspondence.txt').read().strip() or 0)
148-
has_critique = int(open('/tmp/gh-aw/has_critique.txt').read().strip() or 0)
149-
has_report = int(open('/tmp/gh-aw/has_report.txt').read().strip() or 0)
150-
has_paper = int(open('/tmp/gh-aw/has_paper.txt').read().strip() or 0)
151-
fv_dir = int(open('/tmp/gh-aw/fv_dir.txt').read().strip() or 0)
152-
fv_docs = int(open('/tmp/gh-aw/fv_docs.txt').read().strip() or 0)
153-
fv_issues = json.load(open('/tmp/gh-aw/fv_issues.json'))
154-
fv_prs = json.load(open('/tmp/gh-aw/fv_prs.json'))
142+
lean_count = int(open('/tmp/gh-aw/agent/lean_count.txt').read().strip() or 0)
143+
rust_count = int(open('/tmp/gh-aw/agent/rust_count.txt').read().strip() or 0)
144+
has_lean_ci = int(open('/tmp/gh-aw/agent/has_lean_ci.txt').read().strip() or 0)
145+
has_aeneas_ci = int(open('/tmp/gh-aw/agent/has_aeneas_ci.txt').read().strip() or 0)
146+
correspondence_test_count = int(open('/tmp/gh-aw/agent/correspondence_test_count.txt').read().strip() or 0)
147+
has_correspondence = int(open('/tmp/gh-aw/agent/has_correspondence.txt').read().strip() or 0)
148+
has_critique = int(open('/tmp/gh-aw/agent/has_critique.txt').read().strip() or 0)
149+
has_report = int(open('/tmp/gh-aw/agent/has_report.txt').read().strip() or 0)
150+
has_paper = int(open('/tmp/gh-aw/agent/has_paper.txt').read().strip() or 0)
151+
fv_dir = int(open('/tmp/gh-aw/agent/fv_dir.txt').read().strip() or 0)
152+
fv_docs = int(open('/tmp/gh-aw/agent/fv_docs.txt').read().strip() or 0)
153+
fv_issues = json.load(open('/tmp/gh-aw/agent/fv_issues.json'))
154+
fv_prs = json.load(open('/tmp/gh-aw/agent/fv_prs.json'))
155155
156156
n_issues = len(fv_issues)
157157
n_prs = len(fv_prs)
@@ -421,7 +421,7 @@ steps:
421421
'weights': {str(k): round(v, 2) for k, v in weights.items()},
422422
'selected_tasks': chosen,
423423
}
424-
with open('/tmp/gh-aw/task_selection.json', 'w') as f:
424+
with open('/tmp/gh-aw/agent/task_selection.json', 'w') as f:
425425
json.dump(result, f, indent=2)
426426
EOF
427427
@@ -465,7 +465,7 @@ Read memory at the **start** of every run. Update and save it at the **end** of
465465

466466
## Workflow
467467

468-
At the start of your run, read `/tmp/gh-aw/task_selection.json`. It contains:
468+
At the start of your run, read `/tmp/gh-aw/agent/task_selection.json`. It contains:
469469

470470
- `phase_flags`: coarse heuristics derived from repository state about which phases are underway
471471
- `selected_tasks`: two tasks chosen by a phase-weighted random draw
@@ -534,11 +534,13 @@ fi
534534
# --- Record lean availability ---
535535
if command -v lean &>/dev/null; then
536536
lean --version
537-
echo "LEAN_AVAILABLE=true" > /tmp/lean_status.txt
538-
lean --version >> /tmp/lean_status.txt
537+
mkdir -p /tmp/gh-aw/agent
538+
echo "LEAN_AVAILABLE=true" > /tmp/gh-aw/agent/lean_status.txt
539+
lean --version >> /tmp/gh-aw/agent/lean_status.txt
539540
else
540541
echo "=== Lean Squad: lean not available — proofs will be UNVERIFIED ==="
541-
echo "LEAN_AVAILABLE=false" > /tmp/lean_status.txt
542+
mkdir -p /tmp/gh-aw/agent
543+
echo "LEAN_AVAILABLE=false" > /tmp/gh-aw/agent/lean_status.txt
542544
fi
543545
```
544546

@@ -559,22 +561,22 @@ After writing or modifying `.lean` files, **always** attempt `lake build` and ca
559561
cd formal-verification/lean
560562
if lean --version &>/dev/null 2>&1; then
561563
echo "=== Lean Squad: running lake build ==="
562-
if lake build 2>&1 | tee /tmp/lake_build.log; then
563-
echo "=== Lean Squad: lake build PASSED — $(grep -c 'sorry' /tmp/lake_build.log || echo 0) sorry(s) remain ==="
564-
echo "LAKE_BUILD=passed" >> /tmp/lean_status.txt
564+
if lake build 2>&1 | tee /tmp/gh-aw/agent/lake_build.log; then
565+
echo "=== Lean Squad: lake build PASSED — $(grep -c 'sorry' /tmp/gh-aw/agent/lake_build.log || echo 0) sorry(s) remain ==="
566+
echo "LAKE_BUILD=passed" >> /tmp/gh-aw/agent/lean_status.txt
565567
else
566568
echo "=== Lean Squad: lake build FAILED ==="
567-
echo "LAKE_BUILD=failed" >> /tmp/lean_status.txt
568-
tail -40 /tmp/lake_build.log
569+
echo "LAKE_BUILD=failed" >> /tmp/gh-aw/agent/lean_status.txt
570+
tail -40 /tmp/gh-aw/agent/lake_build.log
569571
fi
570572
else
571573
echo "=== Lean Squad: skipping lake build — lean not installed ==="
572-
echo "LAKE_BUILD=skipped" >> /tmp/lean_status.txt
574+
echo "LAKE_BUILD=skipped" >> /tmp/gh-aw/agent/lean_status.txt
573575
fi
574576
```
575577

576578
**Every PR that includes `.lean` files MUST include a verification status block** (copy
577-
the relevant lines from `/tmp/lean_status.txt`). Use one of these templates:
579+
the relevant lines from `/tmp/gh-aw/agent/lean_status.txt`). Use one of these templates:
578580

579581
```
580582
> ⚠️ Lean toolchain not available: elan installation failed (network/firewall — see run logs).
@@ -698,7 +700,7 @@ formal-verification/
698700
- Include `#check` and `example` expressions to confirm the spec is at least well-typed
699701
3. Focus on the most valuable properties: correctness of key operations, representation invariants, round-trip properties, monotonicity, idempotence — whatever is most likely to catch bugs or build confidence.
700702
4. **MANDATORY**: Run `lake build` (or `lean --stdin`) to verify the file is syntactically correct even with `sorry`. Fix ALL Lean 4 syntax and type errors before proceeding. Do not create a PR if `lake build` fails due to errors in your new file.
701-
5. Create a PR. The PR MUST include the verification status block from `/tmp/lean_status.txt`.
703+
5. Create a PR. The PR MUST include the verification status block from `/tmp/gh-aw/agent/lean_status.txt`.
702704
6. Update memory: advance target to phase 3, note the Lean file path, list the stated propositions.
703705

704706
---
@@ -716,7 +718,7 @@ formal-verification/
716718
- Use `sorry` only for genuinely hard sub-problems — minimise it
717719
3. Update the proposition statements to reference the Lean implementation (replace abstract stubs with the actual Lean function names).
718720
4. **MANDATORY**: Run `lake build` to verify the file is correct. Fix ALL errors — do not create a PR while `lake build` fails. If you cannot fix the errors, leave the file in its last passing state and document the remaining issues in the PR description.
719-
5. Create a PR. The PR MUST include the verification status block from `/tmp/lean_status.txt`.
721+
5. Create a PR. The PR MUST include the verification status block from `/tmp/gh-aw/agent/lean_status.txt`.
720722
6. Update memory: advance target to phase 4, describe the model and its abstractions.
721723

722724
---
@@ -846,38 +848,39 @@ if ! command -v opam &>/dev/null; then
846848
fi
847849
848850
# --- Clone and build Charon ---
851+
mkdir -p /tmp/gh-aw/agent
849852
CHARON_PIN=$(cat aeneas/charon-pin 2>/dev/null || echo main)
850-
git clone https://github.com/AeneasVerif/charon /tmp/charon
851-
cd /tmp/charon && git checkout "$CHARON_PIN"
853+
git clone https://github.com/AeneasVerif/charon /tmp/gh-aw/agent/charon
854+
cd /tmp/gh-aw/agent/charon && git checkout "$CHARON_PIN"
852855
853856
# Install charon-ml (OCaml library)
854-
opam install /tmp/charon -y
857+
opam install /tmp/gh-aw/agent/charon -y
855858
856859
# Build the Charon Rust binary
857-
cd /tmp/charon/charon
860+
cd /tmp/gh-aw/agent/charon/charon
858861
cargo build --release
859-
mkdir -p /tmp/charon/bin
860-
cp target/release/charon /tmp/charon/bin/
861-
cp target/release/charon-driver /tmp/charon/bin/
862+
mkdir -p /tmp/gh-aw/agent/charon/bin
863+
cp target/release/charon /tmp/gh-aw/agent/charon/bin/
864+
cp target/release/charon-driver /tmp/gh-aw/agent/charon/bin/
862865
863866
# --- Clone and build Aeneas ---
864-
git clone https://github.com/AeneasVerif/aeneas /tmp/aeneas
865-
ln -s /tmp/charon /tmp/aeneas/charon
867+
git clone https://github.com/AeneasVerif/aeneas /tmp/gh-aw/agent/aeneas
868+
ln -s /tmp/gh-aw/agent/charon /tmp/gh-aw/agent/aeneas/charon
866869
867870
opam install -y \
868871
ppx_deriving visitors easy_logging zarith yojson core_unix \
869872
ocamlgraph menhir ocamlformat unionFind progress domainslib
870873
871-
opam exec -- bash -c "cd /tmp/aeneas/src && dune build"
872-
mkdir -p /tmp/aeneas/bin
873-
cp /tmp/aeneas/src/_build/default/main.exe /tmp/aeneas/bin/aeneas
874+
opam exec -- bash -c "cd /tmp/gh-aw/agent/aeneas/src && dune build"
875+
mkdir -p /tmp/gh-aw/agent/aeneas/bin
876+
cp /tmp/gh-aw/agent/aeneas/src/_build/default/main.exe /tmp/gh-aw/agent/aeneas/bin/aeneas
874877
875878
# --- Verify ---
876-
if [ -x /tmp/aeneas/bin/aeneas ] && [ -x /tmp/charon/bin/charon ]; then
877-
echo "AENEAS_AVAILABLE=true" > /tmp/aeneas_status.txt
879+
if [ -x /tmp/gh-aw/agent/aeneas/bin/aeneas ] && [ -x /tmp/gh-aw/agent/charon/bin/charon ]; then
880+
echo "AENEAS_AVAILABLE=true" > /tmp/gh-aw/agent/aeneas_status.txt
878881
echo "=== Lean Squad: Charon + Aeneas toolchain ready ==="
879882
else
880-
echo "AENEAS_AVAILABLE=false" > /tmp/aeneas_status.txt
883+
echo "AENEAS_AVAILABLE=false" > /tmp/gh-aw/agent/aeneas_status.txt
881884
echo "=== Lean Squad: Aeneas toolchain build FAILED ==="
882885
fi
883886
```
@@ -894,18 +897,18 @@ Work on **one small target at a time** (a single module, file, or function). Do
894897

895898
```bash
896899
# Determine the Charon-required Rust toolchain
897-
CHARON_TOOLCHAIN=$(grep 'channel' /tmp/charon/charon/rust-toolchain | cut -d '"' -f 2)
900+
CHARON_TOOLCHAIN=$(grep 'channel' /tmp/gh-aw/agent/charon/charon/rust-toolchain | cut -d '"' -f 2)
898901

899902
# Run Charon — adjust cargo features as needed for the crate
900-
PATH="/tmp/charon/bin:$PATH" RUSTUP_TOOLCHAIN="$CHARON_TOOLCHAIN" \
903+
PATH="/tmp/gh-aw/agent/charon/bin:$PATH" RUSTUP_TOOLCHAIN="$CHARON_TOOLCHAIN" \
901904
charon cargo --preset=aeneas \
902905
-- --no-default-features --features <relevant-features>
903906
```
904907

905908
1. Run Aeneas to generate Lean from the LLBC:
906909

907910
```bash
908-
/tmp/aeneas/bin/aeneas -backend lean -split-files <crate>.llbc \
911+
/tmp/gh-aw/agent/aeneas/bin/aeneas -backend lean -split-files <crate>.llbc \
909912
-dest formal-verification/lean/FVSquad/Aeneas/Generated
910913
```
911914

@@ -1047,10 +1050,11 @@ jobs:
10471050
10481051
- name: Build and verify all proofs
10491052
run: |
1053+
mkdir -p /tmp/gh-aw/agent
10501054
echo "=== lake build starting ==="
1051-
lake build 2>&1 | tee /tmp/lake_build.log
1055+
lake build 2>&1 | tee /tmp/gh-aw/agent/lake_build.log
10521056
BUILD_EXIT=${PIPESTATUS[0]}
1053-
SORRY_COUNT=$(grep -c 'sorry' /tmp/lake_build.log || true)
1057+
SORRY_COUNT=$(grep -c 'sorry' /tmp/gh-aw/agent/lake_build.log || true)
10541058
echo ""
10551059
echo "=== lake build exit code: $BUILD_EXIT ==="
10561060
echo "=== 'sorry' occurrences in build output: $SORRY_COUNT ==="
@@ -1061,7 +1065,7 @@ jobs:
10611065
uses: actions/upload-artifact@v4
10621066
with:
10631067
name: lake-build-log
1064-
path: /tmp/lake_build.log
1068+
path: /tmp/gh-aw/agent/lake_build.log
10651069
CIEOF
10661070
echo "=== Lean Squad: created .github/workflows/lean-ci.yml ==="
10671071
else
@@ -1339,10 +1343,12 @@ if ! command -v pdflatex &>/dev/null; then
13391343
fi
13401344

13411345
if command -v pdflatex &>/dev/null; then
1342-
echo "LATEX_AVAILABLE=true" > /tmp/latex_status.txt
1343-
pdflatex --version | head -1 >> /tmp/latex_status.txt
1346+
mkdir -p /tmp/gh-aw/agent
1347+
echo "LATEX_AVAILABLE=true" > /tmp/gh-aw/agent/latex_status.txt
1348+
pdflatex --version | head -1 >> /tmp/gh-aw/agent/latex_status.txt
13441349
else
1345-
echo "LATEX_AVAILABLE=false" > /tmp/latex_status.txt
1350+
mkdir -p /tmp/gh-aw/agent
1351+
echo "LATEX_AVAILABLE=false" > /tmp/gh-aw/agent/latex_status.txt
13461352
echo "=== Lean Squad: LaTeX not available — paper will not be compiled ==="
13471353
fi
13481354
```
@@ -1530,13 +1536,13 @@ Theorem & File & Property & Status & Tactics \\
15301536
cd formal-verification/paper
15311537
if command -v latexmk &>/dev/null; then
15321538
echo "=== Lean Squad: compiling paper ==="
1533-
if latexmk -pdf -interaction=nonstopmode paper.tex 2>&1 | tee /tmp/latex_build.log; then
1539+
if latexmk -pdf -interaction=nonstopmode paper.tex 2>&1 | tee /tmp/gh-aw/agent/latex_build.log; then
15341540
echo "=== Lean Squad: paper compiled successfully ==="
1535-
echo "PAPER_BUILD=passed" >> /tmp/latex_status.txt
1541+
echo "PAPER_BUILD=passed" >> /tmp/gh-aw/agent/latex_status.txt
15361542
else
15371543
echo "=== Lean Squad: paper compilation FAILED ==="
1538-
echo "PAPER_BUILD=failed" >> /tmp/latex_status.txt
1539-
tail -40 /tmp/latex_build.log
1544+
echo "PAPER_BUILD=failed" >> /tmp/gh-aw/agent/latex_status.txt
1545+
tail -40 /tmp/gh-aw/agent/latex_build.log
15401546
fi
15411547
elif command -v pdflatex &>/dev/null; then
15421548
echo "=== Lean Squad: compiling paper (pdflatex) ==="
@@ -1545,13 +1551,13 @@ elif command -v pdflatex &>/dev/null; then
15451551
&& pdflatex -interaction=nonstopmode paper.tex \
15461552
&& pdflatex -interaction=nonstopmode paper.tex
15471553
if [ -f paper.pdf ]; then
1548-
echo "PAPER_BUILD=passed" >> /tmp/latex_status.txt
1554+
echo "PAPER_BUILD=passed" >> /tmp/gh-aw/agent/latex_status.txt
15491555
else
1550-
echo "PAPER_BUILD=failed" >> /tmp/latex_status.txt
1556+
echo "PAPER_BUILD=failed" >> /tmp/gh-aw/agent/latex_status.txt
15511557
fi
15521558
else
15531559
echo "=== Lean Squad: LaTeX not available — skipping compilation ==="
1554-
echo "PAPER_BUILD=skipped" >> /tmp/latex_status.txt
1560+
echo "PAPER_BUILD=skipped" >> /tmp/gh-aw/agent/latex_status.txt
15551561
fi
15561562
```
15571563

0 commit comments

Comments
 (0)