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

[KitaKen1]

@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:

issue	submission label applied by	intake	record
#955	github-actions[bot] (by intake)	success	success
#956	issue author (form, at creation)	skipped	skipped
#957 (same submission, re-filed via the API with no labels)	github-actions[bot]	success	running

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.