chore: redirect stale submit template links to lean-eval-submissions#290
Merged
Conversation
…ubmissions 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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR adds a stub
.github/ISSUE_TEMPLATE/submit.ymlto this repositorythat points submitters at
leanprover/lean-eval-submissions. PR #278moved the hosted submission pipeline out, but stale
/issues/new?template=submit.ymllinks in old Zulip threads, READMEs,docs, and browser autocomplete continue to resolve here and now land
users on a blank issue chooser. Two recent submissions
(#281, #282) were misfiled in this repo and never evaluated.
The new template carries no inputs other than a required acknowledgement
checkbox; its body is a single markdown block pointing at
https://github.com/leanprover/lean-eval-submissions/issues/new?template=submit.ymland explaining that nothing filed here will be evaluated or recorded on
the leaderboard. Any issue that does get filed through it is auto-titled
[wrong repo] please file at leanprover/lean-eval-submissionsso it istrivial to triage.
🤖 Prepared with Claude Code