Skip to content

README.md

Latest commit

 

History

History
369 lines (287 loc) · 18 KB

README.md

File metadata and controls

369 lines (287 loc) · 18 KB
Raw

z3-guide-app — the GitHub App that publishes the generated docs

OSPO, used throughout this file, is Microsoft's Open Source Programs Office — the team that, with 1ES, runs the microsoftopensource GitHub enterprise and the official Microsoft organizations. They own the microsoft org, so they are the only ones who can accept an App transfer into it, install an App on its repositories, and approve later permission changes. Their queue is microsoft/github-operations.

Why an App is needed

.github/workflows/update-parameter-docs.yml regenerates three pages from every new Z3 release and opens a pull request with the result:

Page Generated by
website/docs-programming/04 - Parameters.md scripts/generate-parameter-docs.py (from the released z3 binary)
website/docs-smtlib/03 - strategies/06 - summary.md doc/mk_tactic_doc.py in the Z3 release sources
website/docs-smtlib/03 - strategies/07 - simplifiers-summary.md doc/mk_tactic_doc.py in the Z3 release sources

The workflow cannot open that pull request with the built-in GITHUB_TOKEN: organization policy blocks Actions from creating pull requests. The two alternatives are a contributor-owned PAT or a GitHub App:

  • A fine-grained PAT now expires after ~7 days and has no renewal API, so the secret lapses and the workflow breaks silently.
  • A classic repo PAT is wildly over-privileged — write access to every repo the owning account can push to — and is tied to one person.
  • A GitHub App mints short-lived, per-run installation tokens scoped to exactly the repos it is installed on, owned by the org rather than by a person, with nothing to rotate on a schedule.

This mirrors z3prover-ci-bot, the App already doing the same job for Z3Prover/z3 and Z3Prover/bench (see docs/github-app/README.md in Z3Prover/bench).

Exact least-privilege permission set (derived from the workflow)

Permission Access Why
Metadata Read-only mandatory
Contents Read & write push the automation/update-z3-parameters branch
Pull requests Read & write open / update the parameter-update pull request

No Issues permission (the workflow has no issue fallback), no account or organization permissions, no webhook.

Visibility must be public ("Any account"). This is counter-intuitive for a single-repo automation identity, but OSPO's config-as-code review bot validates the App through GET /apps/{slug} (src/review-pr.ts), and that endpoint returns 404 for a private App — even to its own owner. A private App is rejected with "The app slug could not be validated as a public GitHub App." The already-approved z3prover-ci-bot is public for the same reason. Public only means other accounts may install it; every installation still requires that account's admin to approve, and the App carries no secrets.

Installed on one repository: microsoft/z3guide.

The workflow narrows the minted token even further with permission-contents: write / permission-pull-requests: write and repositories: z3guide, so a run can never use more than it declares.

Files in this folder

File Purpose
manifest.json the App manifest — name, permissions, no webhook
create-app.html open in a browser to create the App from the manifest in one click; keep in sync with manifest.json
z3-guide-app.install.yml the config-as-code install file to PR into microsoft/github-operations at apps/microsoft/z3-guide-app.yml
ospo-transfer-request.md ready-to-submit answers for the OSPO transfer ticket (step 2 below)

Step-by-step setup

1. Create the App on your personal account

Done — z3-guide-app, App ID 4662589, owned by @levnach. Kept here as the record of how it was created and what it must look like if it is ever recreated. Still outstanding from this step: Generate a private key.

Microsoft OSPO asks you to create the App on a personal account first and then request the transfer to the org.

Sign in to github.com in the browser you use for this. If you are signed out, GitHub discards the manifest and the App form reports Invalid GitHub App configuration — "url" wasn't supplied. That message means signed out, not bad manifest: posting the manifest in manifest.json without a session reproduces it exactly. Open https://github.com/settings/apps/new — if it shows the Register new GitHub App form you are signed in; if it shows a sign-in page, sign in first.

Option A — manual form (recommended; no manifest quirks)

Go to https://github.com/settings/apps/new and fill in:

  • GitHub App name: z3-guide-app (if taken, append -2)
  • Homepage URL: https://github.com/microsoft/z3guide — this is the field the manifest calls url
  • Identifying and authorizing users: leave Redirect URI blank and leave Request user authorization (OAuth) during installation unchecked; the App never acts on behalf of a user
  • Post installation → Setup URL: blank
  • Webhook: untick Active (leave Webhook URL blank)
  • Repository permissions:
    • Contents → Read and write
    • Pull requests → Read and write
    • (Metadata → Read-only is added automatically)
  • Subscribe to events: none
  • Where can this GitHub App be installed? → Any account (see the visibility note above; OSPO's review bot cannot see a private App)
  • Click Create GitHub App

Option B — one-click manifest

Open create-app.html in the browser while signed in, click the button, review the pre-filled confirmation, and click Create GitHub App.

App names are globally unique. If z3-guide-app had been taken, the name in both manifest.json and create-app.html would need to change, and z3-guide-app.install.yml would need renaming to match — OSPO's automation derives the App slug from that file name.

Then click Generate a private key (saves a .pem) and copy the Client ID (Iv23li…) and the numeric App ID.

Verify the registration before going further

The permission checkboxes are easy to miss on the create form, and an App with no permissions fails only much later, at the first real run. Check what GitHub actually recorded — this needs nothing but openssl and the .pem:

cat > /tmp/appjwt.sh <<'SH'
set -euo pipefail
PEM="$1"; APP_ID="$2"
b64url() { openssl base64 -A | tr '+/' '-_' | tr -d '='; }
now=$(date +%s)
header=$(printf '{"alg":"RS256","typ":"JWT"}' | b64url)
payload=$(printf '{"iat":%d,"exp":%d,"iss":"%s"}' $((now-60)) $((now+540)) "$APP_ID" | b64url)
signing_input="${header}.${payload}"
sig=$(printf '%s' "$signing_input" | openssl dgst -sha256 -sign "$PEM" -binary | b64url)
printf '%s.%s' "$signing_input" "$sig"
SH

JWT=$(bash /tmp/appjwt.sh /path/to/z3-guide-app.*.private-key.pem 4662589)
curl -s -H "Authorization: Bearer $JWT" https://api.github.com/app \
  | python3 -c "import json,sys; d=json.load(sys.stdin); print(d['slug'], d['client_id'], d['permissions'])"

A correct registration prints:

z3-guide-app Iv23li6lyE3PHafpr9qb {'contents': 'write', 'metadata': 'read', 'pull_requests': 'write'}

{} means no permissions were saved — fix them at https://github.com/settings/apps/z3-guide-app/permissions and press Save changes. A successful call also proves the private key matches the App.

Check the webhook too. The create form happily accepts the Homepage URL as the Webhook URL and leaves the hook active, which produces a perpetual stream of failed deliveries and contradicts the no-webhook posture OSPO reviews:

curl -s -H "Authorization: Bearer $JWT" https://api.github.com/app/hook/config

This must return 404 (Not found). If it returns a url, untick Active in the Webhook section of https://github.com/settings/apps/z3-guide-app, clear the URL, and save. Do this before the transfer in step 2 — once the App belongs to the org you may not be able to edit its settings until an org owner grants App-Manager rights.

GET /app/hook/config reports only the stored configuration; it has no active field. GET /app/hook/deliveries is the complementary check — it returns 404 once the webhook is disabled, and lists deliveries while it is live. Treat the pair as the test: both 404 means no webhook.

2. Ask OSPO to move the App to the org

Done — filed as microsoft/github-operations#1726 and accepted; the App is now owned by the microsoft org.

Open a Transfer and configure a first-party GitHub App issue on microsoft/github-operations. ospo-transfer-request.md holds the exact answers to paste into that form; the short version is:

  • GitHub app name: z3-guide-app
  • Transfer to: microsoft (the org that owns z3guide). OSPO routes Apps created purely to work around reduced PAT lifetimes to microsoftengineering instead — if they ask for that, first flip the App to Any account under Advanced in the App settings, otherwise it cannot be installed on microsoft/z3guide from a different owning org.
  • App type: first-party app used for internal scenarios, engineering, development
  • Side effects: it opens a pull request on the repos it is installed on, so it should be installed on selected repositories only — never org-wide
  • Initial App Managers: the maintainers who will hold the private key

After the ticket is filed, initiate the transfer from App settings → Advanced → Transfer ownership.

3. Request the installation via config-as-code

Merged as microsoft/github-operations#1727; their review bot reported Valid: 1 | Warnings: 0 | Invalid: 0. The installation itself is applied asynchronously by OSPO — see the status block at the end of this file for how to poll for it.

z3-guide-app.install.yml already carries the real Client ID and App ID. Open a pull request on microsoft/github-operations adding it as apps/microsoft/z3-guide-app.yml. OSPO's automation installs the App on the listed repositories.

4. Store the App credentials on this repository

Do this after step 3. Setting the variable and secret before the App is actually installed satisfies the preflight guard, so the workflow stops skipping and starts failing at the token step instead — the exact failure mode the guard exists to prevent.

gh variable set Z3GUIDE_APP_CLIENT_ID  --repo microsoft/z3guide --body "Iv23li6lyE3PHafpr9qb"
gh secret   set Z3GUIDE_APP_PRIVATE_KEY --repo microsoft/z3guide < z3-guide-app.*.private-key.pem

Until both exist the workflow's preflight job emits a warning and skips the run instead of failing, so an unconfigured repository does not produce a red build every night.

5. Verify

Run the workflow manually with force enabled:

gh workflow run "Update Z3 parameter documentation" --repo microsoft/z3guide -f force=true

The resulting pull request must be authored by app/z3-guide-app.

Maintenance

Who can manage it

  • Org owners (via Microsoft OSPO / microsoft/github-operations) are the only role that can change the installed repositories, transfer, or delete the App, and the role that must approve permission changes.
  • App Managers can edit App settings (keys, name, requested permissions) once an org owner grants the team App-Manager rights. Until then, route setting changes through an OSPO ticket.

Rotate the private key

Keys never expire; rotate roughly yearly, or immediately if the .pem leaks:

  1. App settings → Private keys → Generate a new key (downloads a .pem).
  2. gh secret set Z3GUIDE_APP_PRIVATE_KEY --repo microsoft/z3guide < newkey.pem
  3. Re-run the workflow with force=true and confirm it is green.
  4. Delete the old key in App settings.

Treat the .pem like a root credential: never commit it, never paste it into logs. It is the only long-lived secret behind the docs automation.

Add or remove a target repository

  1. Edit apps/microsoft/z3-guide-app.yml in microsoft/github-operations (source copy: z3-guide-app.install.yml here) and open a pull request.
  2. After it merges, update the repositories: list of the create-github-app-token step in every workflow that needs the new repo.

Change permissions

Edit the App's permissions in settings (or via OSPO), update the expected_permissions value in the install config, and keep the permission-* inputs on the create-github-app-token step in sync. GitHub then requires an org owner to approve the new permissions before they take effect.

Troubleshooting

Symptom Cause
Workflow skipped with a "not configured" warning vars.Z3GUIDE_APP_CLIENT_ID or secrets.Z3GUIDE_APP_PRIVATE_KEY is missing (step 4)
The 'client-id' … input must be set to a non-empty string the same missing variable/secret, on an older workflow without the preflight guard
Invalid GitHub App configuration — "url" wasn't supplied when creating the App you are signed out of github.com in that browser; GitHub drops the manifest on anonymous requests (step 1)
401 / Repository not found private key mismatch (rotate and re-set the secret), or the repository is not part of the installation (step 3)
Resource not accessible by integration the App registration has no permissions; GET /app returns {} — set Contents and Pull requests to write and save (step 1)
Failed ping deliveries under Advanced → Recent Deliveries a webhook is active, usually with the Homepage URL pasted in as the Webhook URL; untick Active and clear the URL (step 1)
OSPO PR bot: "The app slug could not be validated as a public GitHub App" the App is private; GET /apps/z3-guide-app returns 404. Use Make public under Advanced (step 1)
GitHub Actions is not permitted to create or approve pull requests the PR step is using GITHUB_TOKEN instead of the App token

To tell a genuinely malformed manifest apart from a signed-out browser, inspect what the form would send instead of trusting the error text: open create-app.html and run this in the browser console.

JSON.parse(new FormData(document.getElementById('f')).get('manifest'))

If it returns an object with a url field, the manifest is fine and the error is the missing session.

Source of truth

This file. Update the permission table, the installed-repository list and the setup steps whenever the App ID, installed repos, permissions, or secrets change.

Current status

Live. Created on 2026-08-20 as z3-guide-app, now owned by the microsoft org and installed on microsoft/z3guide.

  • App ID: 4662589
  • Client ID: Iv23li6lyE3PHafpr9qb
  • Private key: generated; held outside the repository
  • Permissions: contents=write, metadata=read, pull_requests=write
  • Webhook: none — GET /app/hook/config and GET /app/hook/deliveries both return 404
  • Visibility: public ("Any account") — required so OSPO's review bot can resolve the App via GET /apps/z3-guide-app
  • Transfer ticket: microsoft/github-operations#1726 — accepted; GET /app reports owner: microsoft (Organization)
  • Install request: microsoft/github-operations#1727 — merged; review bot reported Valid: 1 | Warnings: 0 | Invalid: 0
  • Installation: id 155278905, repository_selection: selected, covering exactly one repository, microsoft/z3guide
  • Credentials: Z3GUIDE_APP_CLIENT_ID (variable) and Z3GUIDE_APP_PRIVATE_KEY (secret) are set on microsoft/z3guide

Verified end to end by minting an installation access token and listing the repositories it grants — total_count: 1, microsoft/z3guide — which is the same path actions/create-github-app-token takes in the workflow.

Live and verified end to end. #258 is merged, so the nightly run is active. A workflow_dispatch run on 2026-08-20 (32411177729) passed both jobs and opened #259 as app/z3-guide-app, which is the whole chain working: App token minted, branch pushed, pull request authored by the App.

The currency check named exactly the two stale pages and left the current one alone, as intended:

Regenerating because 'website/docs-smtlib/03 - strategies/06 - summary.md' does not reference z3-5.1.0.
Regenerating because 'website/docs-smtlib/03 - strategies/07 - simplifiers-summary.md' does not reference z3-5.1.0.

Outstanding:

  1. Merge #259. It adds the Generated from marker to 06 and 07 and picks up an upstream wording fix. Once it lands, all three pages carry the marker and the check reports "All generated pages already reference z3-5.1.0; nothing to do." — so the job stops regenerating daily and only acts on a genuinely new Z3 release.

Merging the config-as-code request does not install the App by itself. The in-repo installer workflow (.github/workflows/enterprise-apps.yaml_ignore) is archived — "FUNCTIONALITY MOVED ELSEWHERE" — so OSPO applies installs asynchronously and there is no public workflow run to watch. Poll GET /repos/microsoft/z3guide/installation (404 not yet, 200 installed) rather than installations_count from GET /app.