Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update toolchain #51

Merged
merged 3 commits into from
Sep 12, 2024
Merged

Update toolchain #51

merged 3 commits into from
Sep 12, 2024

Conversation

eyihluyc
Copy link
Member

@eyihluyc eyihluyc commented Sep 12, 2024

Update from lean4:v4.11.0 to lean4:v4.12.0-rc1.


PR-Codex overview

This PR introduces changes related to unused variables in the Lean codebase.

Detailed summary

  • Updated UnusedVariables linter options in various files
  • Reordered arguments in Mem and IsAttached inductive definitions
  • Modified substitute and incLocatorsFrom functions
  • Updated revisions in lake-manifest.json files

The following files were skipped due to too many changes: Minimal/Calculus.lean

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

@0crat
Copy link

0crat commented Sep 12, 2024

@eyihluyc As per our policy, naming Git branches like "update-toolchain" isn't recommended and incurs a -12 point penalty. For better practices, name your branch after the ticket number you're addressing, such as "50". This ensures clarity and consistency. Your current balance stands at +4. Let's aim for improvement in future branch naming.

@eyihluyc eyihluyc requested a review from Anatolay September 12, 2024 08:04
@eyihluyc eyihluyc merged commit 8d5729a into master Sep 12, 2024
2 checks passed
@eyihluyc eyihluyc deleted the update-toolchain branch September 12, 2024 18:24
@0crat
Copy link

0crat commented Sep 12, 2024

@Anatolay Hey there! 👋 Thanks for your review! You've earned +4 points, which is the minimum according to our policy. We had to deduct some points because there was only 1 comment (we aim for at least 6), but we made sure you got something for your effort. Remember, more comments can boost your points up to +8! Your current balance is -16. Keep up the good work and let's aim for more detailed reviews next time! 💪

@0crat
Copy link

0crat commented Sep 12, 2024

@eyihluyc Great work on your contribution! 🌟 You've earned +4 points: +4 base, -8 for excess code (442 >= 200), -4 for minimal comments, +12 bonus. Your balance is now -8. Remember, quality matters - keep the contributions coming, focusing on concise code and thorough documentation!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants