Truncate issue body to GitHub's 65536 character limit#208
Conversation
Agent-Logs-Url: https://github.com/leanprover-community/lean-update/sessions/963ea0c2-2f7c-4e4d-abb8-04d8cd8c850b Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
| # Truncate body if it exceeds GitHub's 65536 character limit | ||
| MAX_BODY_LEN=65536 | ||
| TRUNCATION_NOTICE=" | ||
| ...(省略しています / truncated)" |
Agent-Logs-Url: https://github.com/leanprover-community/lean-update/sessions/1a2bffc6-a139-4a4d-8681-7867c001d1a1 Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
|
結論:このままでも主目的はだいたい満たすが、markdown が壊れるので修正推奨です。 主な変更は BODY 作成後に 65536 文字を超えたら末尾を切って ...(truncated) を付けるものです。差分は scripts/create-issue.sh に9行追加だけです。  問題点:
提案コメント: This fixes the immediate API error, but I think we should truncate PREFIX="$DESCRIPTION
Files changed in update:$BULLET_LIST
## Build Output
\`\`\`
"
SUFFIX="
\`\`\`
"
TRUNCATION_NOTICE="
...(truncated)"
MAX_BODY_LEN=65536
AVAILABLE=$((MAX_BODY_LEN - ${#PREFIX} - ${#SUFFIX}))
if [ ${#BUILD_OUTPUT} -gt $AVAILABLE ]; then
TRUNCATE_AT=$((AVAILABLE - ${#TRUNCATION_NOTICE}))
BUILD_OUTPUT="${BUILD_OUTPUT:0:$TRUNCATE_AT}$TRUNCATION_NOTICE"
fi
BODY="$PREFIX$BUILD_OUTPUT$SUFFIX"
This preserves the Markdown structure even when the build output is very large.
判定:**Request changes 寄り**。機能の方向性は正しいですが、ログが長いと Markdown が壊れるので、merge 前に直した方がよいです。 |
Agent-Logs-Url: https://github.com/leanprover-community/lean-update/sessions/81e492a3-0c90-4a6a-9dc8-8dd8ff6e9780 Co-authored-by: Seasawher <47292598+Seasawher@users.noreply.github.com>
Fixed in e0cd185. The truncation now happens on |
GitHub rejects issue creation when the body exceeds 65536 characters. Large
lake buildoutputs increate-issue.shcan easily trigger this.Change
Rather than truncating the assembled
BODYas a whole (which could cut inside the fenced code block and leave the closing```missing), the implementation reserves space for the static prefix and suffix first, then truncates onlyBUILD_OUTPUTif it exceeds the remaining budget:This ensures the closing code fence is always present and the issue body is valid Markdown even when the build log is very large.
${#...}counts characters (not bytes), matching GitHub's character-based limit.