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.

Sign up for GitHub

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

Jump to bottom

feat: check that every file imports Mathlib.Init #18281

Open
wants to merge 10 commits into
base: master
Choose a base branch
from
Open

feat: check that every file imports Mathlib.Init #18281

wants to merge 10 commits into from
+59 −5

Commits on Oct 27, 2024

  1. Add the scaffolding.

    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    786ce14 View commit details
    Browse the repository at this point in the history

  2. Implement the check

    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    d64abe4 View commit details
    Browse the repository at this point in the history

  3. Clean up.

    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    4fc5134 View commit details
    Browse the repository at this point in the history

  4. chore: import Mathlib.Init in all files 

    This manually adds 'import Mathlib.Init' to all files which are currently missing this.
A future PR will add an automatic check for this.
    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    270dd97 View commit details
    Browse the repository at this point in the history

  5. Fix

    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    1725670 View commit details
    Browse the repository at this point in the history

  6. chore: fix linter warnings 

    Stream'.corec' was pre-existing; add it to the exceptions list
    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    66eac27 View commit details
    Browse the repository at this point in the history

  7. Tweaks

    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    59a26ad View commit details
    Browse the repository at this point in the history

  8. Tweak comment in Mathlib.Init.

    @grunweg
    grunweg committed Oct 27, 2024
    Configuration menu
    Copy the full SHA
    885562f View commit details
    Browse the repository at this point in the history

Commits on Oct 28, 2024

  1. Merge branch 'master' into MR-mathlib-init-check

    @grunweg
    grunweg committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    9083d5e View commit details
    Browse the repository at this point in the history

  2. Last tweaks.

    @grunweg
    grunweg committed Oct 28, 2024
    Configuration menu
    Copy the full SHA
    bebfe32 View commit details
    Browse the repository at this point in the history