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

chore: adaptations to nightly-2024-03-11 #11314

Merged
merged 60 commits into from
Mar 13, 2024
Merged

chore: adaptations to nightly-2024-03-11 #11314

merged 60 commits into from
Mar 13, 2024

Commits on Mar 12, 2024

  1. chore: adaptations for nightly-2024-03-11

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    134f441 View commit details
    Browse the repository at this point in the history

  2. fix from Johan

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    79f1ba4 View commit details
    Browse the repository at this point in the history

  3. update

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    def155c View commit details
    Browse the repository at this point in the history

  4. fix

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    0dec6a8 View commit details
    Browse the repository at this point in the history

  5. cleanup

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    091af2a View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Data/List/Basic.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @semorrison @github-actions
    semorrison and github-actions[bot] committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    4552881 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'bump/nightly-2024-03-11' of github.com:leanprover-commu… 

    …nity/mathlib4 into bump/nightly-2024-03-11
    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    78c3666 View commit details
    Browse the repository at this point in the history

  8. long lines

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    2378451 View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/Data/Nat/Digits.lean

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    411f6c5 View commit details
    Browse the repository at this point in the history

  10. expand comments

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    88ab48e View commit details
    Browse the repository at this point in the history

  11. Merge branch 'bump/nightly-2024-03-11' of github.com:leanprover-commu… 

    …nity/mathlib4 into bump/nightly-2024-03-11
    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    28b487b View commit details
    Browse the repository at this point in the history

  12. double align

    @riccardobrasca
    riccardobrasca committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    c33cdb8 View commit details
    Browse the repository at this point in the history

  13. fix this

    @riccardobrasca
    riccardobrasca committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    7befb8f View commit details
    Browse the repository at this point in the history

  14. fix sorry

    @eric-wieser
    eric-wieser committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    527f2a9 View commit details
    Browse the repository at this point in the history

  15. Algebra.Homology.Augment, use honest fun instead of by cases

    @kmill @Ruben-VandeVelde
    kmill authored and Ruben-VandeVelde committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    0a03277 View commit details
    Browse the repository at this point in the history

  16. says

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    6a48fa2 View commit details
    Browse the repository at this point in the history

  17. remove

    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    ac2f221 View commit details
    Browse the repository at this point in the history

  18. fix says

    @mattrobball @Ruben-VandeVelde
    mattrobball authored and Ruben-VandeVelde committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    8857be7 View commit details
    Browse the repository at this point in the history

  19. merge bump/v4.8.0

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    94343c4 View commit details
    Browse the repository at this point in the history

  20. merge Mario's patch to Ordinal/Notation

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    5b6c8c9 View commit details
    Browse the repository at this point in the history

  21. clean up

    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    92861e0 View commit details
    Browse the repository at this point in the history

  22. fix

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    81a752f View commit details
    Browse the repository at this point in the history

  23. fixes

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    9e80fbb View commit details
    Browse the repository at this point in the history

  24. fixes

    @Ruben-VandeVelde
    Ruben-VandeVelde committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    bac29b8 View commit details
    Browse the repository at this point in the history

  25. fix Nat/Cast/Defs

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    eea60d7 View commit details
    Browse the repository at this point in the history

  26. Merge branch 'bump/nightly-2024-03-11' of github.com:leanprover-commu… 

    …nity/mathlib4 into bump/nightly-2024-03-11
    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    73794f9 View commit details
    Browse the repository at this point in the history

  27. remove stray prime?

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    0b6eccd View commit details
    Browse the repository at this point in the history

  28. simplify proof

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    bb47464 View commit details
    Browse the repository at this point in the history

  29. long line

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    2a73d3e View commit details
    Browse the repository at this point in the history

  30. change FIXME in TensorProduct/Graded/Internal to an adaptation note

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    3c968e4 View commit details
    Browse the repository at this point in the history

  31. Merge branch 'mrb/remove_coe_eq' into bump/nightly-2024-03-11

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    0263a8e View commit details
    Browse the repository at this point in the history

  32. fix test

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    0b59c6a View commit details
    Browse the repository at this point in the history

  33. fix tests

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    85cd382 View commit details
    Browse the repository at this point in the history

  34. lint

    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    7410d4a View commit details
    Browse the repository at this point in the history

  35. lint

    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    b604582 View commit details
    Browse the repository at this point in the history

  36. Merge remote-tracking branch 'refs/remotes/origin/bump/nightly-2024-0… 

    …3-11' into bump/nightly-2024-03-11
    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    fb03a88 View commit details
    Browse the repository at this point in the history

  37. adaptation note about compile_inductive% Nat

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    8f916d7 View commit details
    Browse the repository at this point in the history

  38. Merge branch 'bump/nightly-2024-03-11' of github.com:leanprover-commu… 

    …nity/mathlib4 into bump/nightly-2024-03-11
    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    3442403 View commit details
    Browse the repository at this point in the history

  39. cleanup CompileInductive

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    ba125ba View commit details
    Browse the repository at this point in the history

  40. lint

    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    c79b04c View commit details
    Browse the repository at this point in the history

  41. restore test

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    89a5021 View commit details
    Browse the repository at this point in the history

  42. Merge remote-tracking branch 'refs/remotes/origin/bump/nightly-2024-0… 

    …3-11' into bump/nightly-2024-03-11
    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    4b82ffc View commit details
    Browse the repository at this point in the history

  43. Apply suggestions from code review

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    b5fee61 View commit details
    Browse the repository at this point in the history

  44. cleanup

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    d56a2f2 View commit details
    Browse the repository at this point in the history

  45. Merge branch 'bump/nightly-2024-03-11' of github.com:leanprover-commu… 

    …nity/mathlib4 into bump/nightly-2024-03-11
    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    dd230fb View commit details
    Browse the repository at this point in the history

  46. cleanup

    @semorrison
    semorrison committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    477fd6c View commit details
    Browse the repository at this point in the history

  47. lint

    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    60f150f View commit details
    Browse the repository at this point in the history

  48. Merge remote-tracking branch 'refs/remotes/origin/bump/nightly-2024-0… 

    …3-11' into bump/nightly-2024-03-11
    @mattrobball
    mattrobball committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    33eaca8 View commit details
    Browse the repository at this point in the history

Commits on Mar 13, 2024

  1. fix: patch for std4#579

    @fgdorais
    fgdorais committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    cdcb0ad View commit details
    Browse the repository at this point in the history

  2. cleanup

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    7bdcaa7 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'bump/v4.8.0' into bump/nightly-2024-03-11

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    09b5587 View commit details
    Browse the repository at this point in the history

  4. fix tests

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    66347a3 View commit details
    Browse the repository at this point in the history

  5. fix tests

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    ac499c5 View commit details
    Browse the repository at this point in the history

  6. shake

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    a83ef92 View commit details
    Browse the repository at this point in the history

  7. bump Std

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    4fc25a9 View commit details
    Browse the repository at this point in the history

  8. revert merge'

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    1ae214e View commit details
    Browse the repository at this point in the history

  9. merge bump-Std-2024-03-13

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    5f261fb View commit details
    Browse the repository at this point in the history

  10. comment more

    @mattrobball
    mattrobball committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    e31222f View commit details
    Browse the repository at this point in the history

  11. add comment

    @mattrobball
    mattrobball committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    b77d858 View commit details
    Browse the repository at this point in the history

  12. cleanup

    @semorrison
    semorrison committed Mar 13, 2024
    Configuration menu
    Copy the full SHA
    992b550 View commit details
    Browse the repository at this point in the history