From bd8465c47fbc3668f6505d93aa1848fd99823630 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 4 Sep 2026 03:55:00 +0000 Subject: [PATCH 1/2] docs: retire issue-intake fallback copy --- README.md | 12 +----------- SECURITY.md | 4 ++-- 2 files changed, 3 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index b1074fd3..e0d6da2e 100644 --- a/README.md +++ b/README.md @@ -295,20 +295,10 @@ For current instructions to **submit a solution**, start at the stable page: > **[lean-lang.org/eval/submit/](https://lean-lang.org/eval/submit/)** -That page is the primary authenticated submission path from -`2026-09-02T06:57:10Z`. The application itself is at +That page is the supported authenticated submission path. The application itself is at `https://lean-eval-submission-server.lean-eval.workers.dev/`; this change of origin is expected. -[Submission issue -intake](https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml) -remains available as a fallback through at least `2026-09-30T06:57:10Z`, four -weeks after the overlap began. Conditional on stable operation, adequate -adoption, no unresolved severity-high incident, and a reconciled final corpus, -that is the planned retirement time. This notice was issued at -`2026-09-02T23:06:35Z`, more than two weeks in advance. Retirement will be -postponed if any gate is not satisfied. - Scheduled release is recommended for authenticated intake, while submitters may keep accepted source private instead. Once selected, scheduled release cannot be changed back to private. Accepted source is published under the diff --git a/SECURITY.md b/SECURITY.md index c1cc2a00..e4014a1a 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -6,7 +6,7 @@ untrusted submitter Lean code. This document explains the sandbox invariants, the comparator trust model, and the pinned-dependency policy that the whole evaluation pipeline rests on. -The **submission pipeline** itself — issue intake, fetching submission +The **submission pipeline** itself — authenticated intake, fetching submission source, the evaluation workflow, recording results, and the overall adversarial-submission threat model — lives in the submissions repository and is documented there: @@ -33,7 +33,7 @@ The adversary is a submitter who controls a `Submission.lean` (and files under `Submission/`). The goal we resist here: **untrusted submitter Lean escaping comparator's sandbox, or comparator accepting a Solution that does not actually prove the Challenge.** The pipeline-level framing of -the same adversary (issue intake, token handling, confidentiality) is in +the same adversary (server intake, token handling, confidentiality) is in the submissions repo's `SECURITY.md`. The submitter does not control `Challenge.lean`, `Solution.lean`, From d60087c6ac4e03d7386fcc9e15f47b3ff195d44d Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 4 Sep 2026 04:03:23 +0000 Subject: [PATCH 2/2] test: keep issue redirects server-only --- .github/ISSUE_TEMPLATE/config.yml | 5 +--- .github/ISSUE_TEMPLATE/problem-report.yml | 8 ++---- .github/ISSUE_TEMPLATE/submit.yml | 11 +++----- tests/python/test_issue_templates.py | 33 +++++++++++++++++++++++ 4 files changed, 39 insertions(+), 18 deletions(-) create mode 100644 tests/python/test_issue_templates.py diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml index 737ada1a..dd7269ee 100644 --- a/.github/ISSUE_TEMPLATE/config.yml +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -2,10 +2,7 @@ blank_issues_enabled: true contact_links: - name: Submit a benchmark solution url: https://lean-lang.org/eval/submit/ - about: Primary authenticated submission path from 2026-09-02T06:57:10Z. - - name: Submission issue fallback - url: https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml - about: Available through at least 2026-09-30T06:57:10Z and possibly longer. + about: Supported authenticated submission path. - 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/problem-report.yml b/.github/ISSUE_TEMPLATE/problem-report.yml index 397a689d..a3ed3fa6 100644 --- a/.github/ISSUE_TEMPLATE/problem-report.yml +++ b/.github/ISSUE_TEMPLATE/problem-report.yml @@ -13,12 +13,8 @@ body: is unprovable as stated, imports are missing, or the intended interpretation is ambiguous. - For submission instructions, use the primary authenticated path at - https://lean-lang.org/eval/submit/. The launch overlap starts at - 2026-09-02T06:57:10Z. Issue intake remains available as a fallback through - at least 2026-09-30T06:57:10Z, no earlier than four weeks after the - overlap begins, and may stay open longer. Any closure will be announced - at least two weeks in advance. + For submission instructions, use the supported authenticated path at + https://lean-lang.org/eval/submit/. Scheduled release is recommended for authenticated intake, while you may keep accepted source private instead. Once selected, scheduled diff --git a/.github/ISSUE_TEMPLATE/submit.yml b/.github/ISSUE_TEMPLATE/submit.yml index 17b2a79a..7c36136b 100644 --- a/.github/ISSUE_TEMPLATE/submit.yml +++ b/.github/ISSUE_TEMPLATE/submit.yml @@ -12,12 +12,7 @@ body: **https://lean-lang.org/eval/submit/** - That page is the primary authenticated submission path from - 2026-09-02T06:57:10Z. Issue intake remains available as a fallback through - at least 2026-09-30T06:57:10Z, no earlier than four weeks after the - overlap begins, and may stay open longer: - - **https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.yml** + That page is the supported authenticated submission path. Scheduled release is recommended for authenticated intake, while you may keep accepted source private instead. Once selected, scheduled @@ -28,12 +23,12 @@ body: Nothing filed here will be evaluated or recorded on the leaderboard. - You can close this draft and follow one of the links above; there is + You can close this draft and follow the stable page above; there is nothing more to do in this repository. - type: checkboxes id: ack attributes: label: Acknowledgement options: - - label: I understand this repository does not accept submissions and I should follow the stable LeanEval submission page or its documented issue-intake fallback instead. + - label: I understand this repository does not accept submissions and I should follow the stable LeanEval submission page instead. required: true diff --git a/tests/python/test_issue_templates.py b/tests/python/test_issue_templates.py new file mode 100644 index 00000000..41f9a030 --- /dev/null +++ b/tests/python/test_issue_templates.py @@ -0,0 +1,33 @@ +from __future__ import annotations + +import pathlib +import unittest + + +ROOT = pathlib.Path(__file__).resolve().parents[2] +TEMPLATES = ( + ROOT / ".github/ISSUE_TEMPLATE/config.yml", + ROOT / ".github/ISSUE_TEMPLATE/submit.yml", + ROOT / ".github/ISSUE_TEMPLATE/problem-report.yml", +) + + +class IssueTemplateTests(unittest.TestCase): + def test_submission_redirects_are_server_only(self) -> None: + for template in TEMPLATES: + with self.subTest(template=template.name): + text = template.read_text(encoding="utf-8") + self.assertIn("https://lean-lang.org/eval/submit/", text) + for retired_copy in ( + "lean-eval-submissions/issues/new", + "issue intake", + "issue-intake", + "2026-09-02T06:57:10Z", + "2026-09-30T06:57:10Z", + "fallback through", + ): + self.assertNotIn(retired_copy, text.lower()) + + +if __name__ == "__main__": + unittest.main()