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(*): switch to lean 3.6.1 #2064

Merged
merged 57 commits into from Mar 5, 2020
Merged

chore(*): switch to lean 3.6.1 #2064

merged 57 commits into from Mar 5, 2020

Commits on Feb 27, 2020

  1. chore(*): switch to lean 3.6.0

    @gebner
    gebner committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    e6f4901 View commit details
    Browse the repository at this point in the history

  2. Port src/linear_algebra to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    5350fd8 View commit details
    Browse the repository at this point in the history

  3. Port src/ring_theory to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    fc34d93 View commit details
    Browse the repository at this point in the history

  4. Port src/algebra and its dependencies to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    158db65 View commit details
    Browse the repository at this point in the history

  5. Port src/group_theory to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    1a5d95f View commit details
    Browse the repository at this point in the history

  6. WIP: Ports part of src/data to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    185f76d View commit details
    Browse the repository at this point in the history

Commits on Feb 28, 2020

  1. Port src/data (and dependencies) to Lean 3.6

    @Vierkantor
    Vierkantor committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    561696f View commit details
    Browse the repository at this point in the history

  2. fix set_theory.lists

    @robertylewis
    robertylewis committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    29aa9ee View commit details
    Browse the repository at this point in the history

  3. fix ring2

    @robertylewis
    robertylewis committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    9d66ac2 View commit details
    Browse the repository at this point in the history

  4. fix pell.lean 

    these aren't the cleanest proofs, but pell.lean is kind of a standalone thing.
    @robertylewis
    robertylewis committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    0e44d29 View commit details
    Browse the repository at this point in the history

  5. fix dioph.lean

    @robertylewis
    robertylewis committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    1b5508d View commit details
    Browse the repository at this point in the history

  6. Port src/number_theory/sum_four_squares.lean to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    389d5f4 View commit details
    Browse the repository at this point in the history

  7. Port src/field_theory to Lean 3.6

    @Vierkantor
    Vierkantor committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    4fcd626 View commit details
    Browse the repository at this point in the history

  8. Port src/computability to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    82bd7bb View commit details
    Browse the repository at this point in the history

  9. Port src/measure_theory (and dependencies) to Lean 3.6c

    @Vierkantor
    Vierkantor committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    8427582 View commit details
    Browse the repository at this point in the history

  10. fix manifold/real_instances

    @robertylewis
    robertylewis committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    a4a51e9 View commit details
    Browse the repository at this point in the history

  11. fix analysis/complex/polynomial

    @robertylewis
    robertylewis committed Feb 28, 2020
    Configuration menu
    Copy the full SHA
    767ecc7 View commit details
    Browse the repository at this point in the history

Commits on Mar 2, 2020

  1. Merge remote-tracking branch 'origin/master' into lean36

    @urkud
    urkud committed Mar 2, 2020
    Configuration menu
    Copy the full SHA
    73f5a7e View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of git://github.com/leanprover-community/mathli… 

    …b into lean36
    @urkud
    urkud committed Mar 2, 2020
    Configuration menu
    Copy the full SHA
    f8bc1c4 View commit details
    Browse the repository at this point in the history

Commits on Mar 3, 2020

  1. Fix some compile errors in real_inner_product

    @urkud
    urkud committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    a9ec482 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into lean36

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    15f49bd View commit details
    Browse the repository at this point in the history

  3. Upgrade to Lean 3.6.1

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    9eae01a View commit details
    Browse the repository at this point in the history

  4. perf: speed up calls to linarith

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    23c858e View commit details
    Browse the repository at this point in the history

  5. Reduce instance priorities for potentially noncomputable instances.

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    eebb008 View commit details
    Browse the repository at this point in the history

  6. Remove cyclic instance.

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    0768fc0 View commit details
    Browse the repository at this point in the history

  7. Make arguments {implicit} in instances where they can be filled in vi… 

    …a unification.
    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    88a084f View commit details
    Browse the repository at this point in the history

  8. Make inner_product_space compile.

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    38d32c8 View commit details
    Browse the repository at this point in the history

  9. Style.

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    2810d3d View commit details
    Browse the repository at this point in the history

  10. Port data.nat.modeq

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    5c917ef View commit details
    Browse the repository at this point in the history

  11. Port data.int.parity

    @gebner
    gebner committed Mar 3, 2020
    Configuration menu
    Copy the full SHA
    0e3081b View commit details
    Browse the repository at this point in the history

Commits on Mar 4, 2020

  1. Port data.int.modeq

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    e184dd1 View commit details
    Browse the repository at this point in the history

  2. Port data.real.hyperreal

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    72cf4e1 View commit details
    Browse the repository at this point in the history

  3. fix(ci): always run git setup step 

    closes #2079

(cherry picked from commit 8a0157d)
    @robertylewis @gebner
    robertylewis authored and gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    d275e43 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into lean36

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    f809761 View commit details
    Browse the repository at this point in the history

  5. Remove pre-3.6 legacy code.

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    778d9d1 View commit details
    Browse the repository at this point in the history

  6. Fix test/monotonicity.lean

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    b7d560b View commit details
    Browse the repository at this point in the history

  7. Fix test/ring_exp.lean

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    3e282a5 View commit details
    Browse the repository at this point in the history

  8. Fix test/conv.lean

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    b6072a5 View commit details
    Browse the repository at this point in the history

  9. Fix archive/imo1988_q6.lean

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    bceed17 View commit details
    Browse the repository at this point in the history

  10. Fix docs/tutorial/Zmod37.lean

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    8f9b6c6 View commit details
    Browse the repository at this point in the history

  11. Fix archive/sensitivity.lean

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    9e38477 View commit details
    Browse the repository at this point in the history

  12. refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    83b9a20 View commit details
    Browse the repository at this point in the history

  13. remove unused argument

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

  14. add doc-string to instance that became a def

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

  15. add docstring

    @semorrison
    semorrison committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    3beb5f7 View commit details
    Browse the repository at this point in the history

  16. Fix linting error ☺

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    b1daf12 View commit details
    Browse the repository at this point in the history

  17. Fix data.real.irrational

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    72af113 View commit details
    Browse the repository at this point in the history

  18. Merge remote-tracking branch 'origin/master' into lean36

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    23f1ff7 View commit details
    Browse the repository at this point in the history

  19. Merge remote-tracking branch 'origin/lie-algebra' into lean36

    @gebner
    gebner committed Mar 4, 2020
    Configuration menu
    Copy the full SHA
    2d4f527 View commit details
    Browse the repository at this point in the history

Commits on Mar 5, 2020

  1. fixing a proof

    @semorrison
    semorrison committed Mar 5, 2020
    Configuration menu
    Copy the full SHA
    748a257 View commit details
    Browse the repository at this point in the history

  2. cleaning up proof

    @semorrison
    semorrison committed Mar 5, 2020
    Configuration menu
    Copy the full SHA
    706ecea View commit details
    Browse the repository at this point in the history

  3. fix broken proof

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

  4. Merge remote-tracking branch 'origin/master' into lean36

    @semorrison
    semorrison committed Mar 5, 2020
    Configuration menu
    Copy the full SHA
    78dccce View commit details
    Browse the repository at this point in the history

  5. fix proof

    @semorrison
    semorrison committed Mar 5, 2020
    Configuration menu
    Copy the full SHA
    7bceaee View commit details
    Browse the repository at this point in the history

  6. fix some more proofs

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

  7. fix

    @semorrison
    semorrison committed Mar 5, 2020
    Configuration menu
    Copy the full SHA
    9e3332a View commit details
    Browse the repository at this point in the history

  8. fix proofs

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