From 0ed98421e26861f8622ecab3400f1360647c462c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 21 May 2026 23:38:02 +0000 Subject: [PATCH 1/2] chore: add redirect issue template pointing submitters at lean-eval-submissions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #278 removed the submission template from this repo but stale `?template=submit.yml` links (in old Zulip threads, READMEs, browser history) still resolve here and land users on a blank issue chooser. Two recent submissions (#281, #282) were misfiled and never evaluated. Add back a stub `submit.yml` whose only purpose is to display a "moved — go file at leanprover/lean-eval-submissions" banner with a required acknowledgement checkbox. Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/ISSUE_TEMPLATE/submit.yml | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 .github/ISSUE_TEMPLATE/submit.yml diff --git a/.github/ISSUE_TEMPLATE/submit.yml b/.github/ISSUE_TEMPLATE/submit.yml new file mode 100644 index 0000000..67a781d --- /dev/null +++ b/.github/ISSUE_TEMPLATE/submit.yml @@ -0,0 +1,26 @@ +name: Submit benchmark solution (moved) +description: Benchmark submissions now live in leanprover/lean-eval-submissions; this template just points you there. +title: "[wrong repo] please file at leanprover/lean-eval-submissions" +body: + - type: markdown + attributes: + value: | + ## Benchmark submissions have moved + + The hosted submission pipeline (issue intake, fetch, evaluate, leaderboard + recording) is no longer in this repository. It now lives in: + + **https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml** + + Please open your submission there. Nothing filed here will be evaluated or + recorded on the leaderboard. + + You can close this draft and follow the link above; there is nothing more + to do in this repository. + - type: checkboxes + id: ack + attributes: + label: Acknowledgement + options: + - label: I understand this repository no longer accepts submissions and I should file at leanprover/lean-eval-submissions instead. + required: true From ae04f9ca902df86307b4a8f04e6b4ff95ab8b84d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 21 May 2026 23:42:26 +0000 Subject: [PATCH 2/2] chore: surface the move in the chooser UI Rename the stub template's `name` from "Submit benchmark solution (moved)" to "Moved: submit at lean-eval-submissions" so a user scanning the chooser cannot mistake it for the live submit path, and add a `contact_links` entry that points directly at the lean-eval-submissions submit form, placed first so it is the most prominent option in the chooser. Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/ISSUE_TEMPLATE/config.yml | 3 +++ .github/ISSUE_TEMPLATE/submit.yml | 4 ++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml index 50b18dc..e0ba78b 100644 --- a/.github/ISSUE_TEMPLATE/config.yml +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -1,5 +1,8 @@ blank_issues_enabled: true contact_links: + - name: Submit a benchmark solution + url: https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml + about: Benchmark submissions are filed in leanprover/lean-eval-submissions, not here. - name: Discussion on Zulip url: https://leanprover.zulipchat.com/#narrow/channel/583341-Model-comparisons-for-Lean/topic/LeanEval/with/594108910 about: General questions and discussion about lean-eval happen in the #Model-comparisons-for-Lean > LeanEval topic on the Lean Zulip. diff --git a/.github/ISSUE_TEMPLATE/submit.yml b/.github/ISSUE_TEMPLATE/submit.yml index 67a781d..b08c704 100644 --- a/.github/ISSUE_TEMPLATE/submit.yml +++ b/.github/ISSUE_TEMPLATE/submit.yml @@ -1,5 +1,5 @@ -name: Submit benchmark solution (moved) -description: Benchmark submissions now live in leanprover/lean-eval-submissions; this template just points you there. +name: "Moved: submit at lean-eval-submissions" +description: Benchmark submissions live in leanprover/lean-eval-submissions. This template only exists to catch stale links and redirect you there. title: "[wrong repo] please file at leanprover/lean-eval-submissions" body: - type: markdown