feat(lattices): prove Lyubashevsky–Seiler short-element invertibility… #1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Refresh KB Generated Files | |
| on: | |
| push: | |
| branches: ["main"] | |
| paths: | |
| - "ArkLib/**/*.lean" | |
| - "blueprint/src/references.bib" | |
| - "docs/kb/papers/**" | |
| - "docs/kb/sources/**" | |
| - "scripts/kb/**" | |
| - ".github/workflows/kb-generated.yml" | |
| workflow_dispatch: | |
| permissions: | |
| contents: write | |
| pull-requests: write | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| refresh: | |
| if: github.actor != 'github-actions[bot]' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| with: | |
| fetch-depth: 0 | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| - uses: actions/setup-python@v6 | |
| with: | |
| python-version: "3.12" | |
| - name: Regenerate KB files | |
| run: python3 ./scripts/kb/regenerate.py | |
| - name: Check generated files | |
| run: python3 ./scripts/kb/check_generated.py | |
| - name: Lint generated KB state | |
| run: python3 ./scripts/kb/lint.py --strict-cited-pages --use-generated-indexes | |
| - name: Open generated update PR | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| BRANCH_NAME: automation/kb-generated-${{ github.sha }} | |
| run: | | |
| if git diff --quiet -- docs/kb/_generated docs/kb/papers docs/kb/sources; then | |
| echo "No KB generated updates to propose." | |
| exit 0 | |
| fi | |
| git config user.name "github-actions[bot]" | |
| git config user.email "41898282+github-actions[bot]@users.noreply.github.com" | |
| git switch -c "$BRANCH_NAME" | |
| git add -A docs/kb/_generated docs/kb/papers docs/kb/sources | |
| git commit -m "chore(kb): refresh generated files" | |
| invalid_paths="$(git diff --name-only HEAD^ HEAD | grep -Ev '^(docs/kb/_generated/|docs/kb/papers/|docs/kb/sources/)' || true)" | |
| if [ -n "$invalid_paths" ]; then | |
| echo "Refusing to auto-merge unexpected generated-files PR paths:" | |
| echo "$invalid_paths" | |
| exit 1 | |
| fi | |
| git push --force-with-lease origin "HEAD:$BRANCH_NAME" | |
| body="$RUNNER_TEMP/kb-generated-pr.md" | |
| { | |
| echo "Regenerates ArkLib knowledge-base derived files after a merge to \`main\`." | |
| echo | |
| echo "Generated by \`.github/workflows/kb-generated.yml\` for source commit \`${GITHUB_SHA}\`." | |
| echo | |
| echo "This PR may update:" | |
| echo | |
| echo "- \`docs/kb/_generated/**\`" | |
| echo "- stub-only cited paper pages under \`docs/kb/papers/\`" | |
| echo "- stub-only source metadata under \`docs/kb/sources/\`" | |
| } > "$body" | |
| existing_pr="$(gh pr list \ | |
| --base main \ | |
| --head "$BRANCH_NAME" \ | |
| --state open \ | |
| --json number \ | |
| --jq '.[0].number // empty')" | |
| if [ -n "$existing_pr" ]; then | |
| gh pr edit "$existing_pr" \ | |
| --title "chore(kb): refresh generated files" \ | |
| --body-file "$body" | |
| pr_url="$(gh pr view "$existing_pr" --json url --jq .url)" | |
| else | |
| pr_url="$(gh pr create \ | |
| --base main \ | |
| --head "$BRANCH_NAME" \ | |
| --title "chore(kb): refresh generated files" \ | |
| --body-file "$body")" | |
| fi | |
| gh pr merge "$pr_url" --auto --squash --delete-branch |