Form-created submissions never reach the leaderboard (`intake` skipped ⇒ `record` skipped)

@kim-em — apologies for filing here; blank issues are disabled in lean-eval-submissions, so there is no obvious place for a report about its workflow.

Symptom

Submissions created through the issue form never reach the leaderboard. evaluate passes, archive passes, record is skipped, and notify then closes the issue as not planned with

Recording the submission to the leaderboard did not complete (record job: skipped)

which reads as a rejection even though the proof passed.

Concrete case: lean-eval-submissions#956, run 31083300191. evaluate ran for 1h33m and its artifact contains

{ "passed": ["pi_succ_sphere_n_mulEquiv_zmod_two"] }

but nothing was written to results/kitaken1.json.

Cause

intake (added in lean-eval-submissions#953) is gated on

github.event.action == 'opened' &&
startsWith(github.event.issue.title, '[submission]') &&
!contains(github.event.issue.labels.*.name, 'submission')

while .github/ISSUE_TEMPLATE/submit.yml carries labels: [submission]. A form-created issue therefore already has the label at opened, so intake is skipped. evaluate and archive carry always() and still run; record does not, so the skip propagates through the dependency chain.

Label provenance makes the split visible:

So the documented path — the "Submit benchmark solution" form — is currently the broken one, and only API-created issues work.

Suggested fix

record:
  needs: [evaluate, archive]
  if: >-
    always() &&
    needs.evaluate.result == 'success' &&
    needs.archive.result == 'success'

and/or dropping labels: [submission] from submit.yml so intake can apply it, or relaxing the intake guard.

It might also be worth softening the notify message: closing as not planned with a red ✗ is hard to distinguish from a genuine verification failure.

No action needed on my own submission — #957 is going through the working path. Filing this so other submitters do not lose results the same way. Happy to move it to Zulip if you prefer.

Start with the GitHub Actions workflow containing the intake, evaluate, archive, record, and notify jobs, then compare its conditions with .github/ISSUE_TEMPLATE/submit.yml. Reproduce the form-created path using the linked run or issue and verify that a passing submission reaches record and writes the expected results entry without being reported as not planned.