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 new file mode 100644 index 0000000..b08c704 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/submit.yml @@ -0,0 +1,26 @@ +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 + 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