chore(*): switch to lean 3.6.1 #2064

gebner · 2020-02-27T10:00:50Z

The only remaining build failure is a class instance resolution failure in real_inner_product.

There's still lots of stuff to fix, but I'm not sure if I'll have time to do it until next week. I got as far as derivatives.

There's roughly 4 different kinds of breakage:

Some lemmas relied on add_comm, add_left_comm, sub_eq_add_neg being in the simp set. @semorrison suggested to just add an attribute [simp] for the moment, but I'm not sure if this makes porting much easier. It's pretty easy to modify the simp invocation, and there's other breakage you need to fix anyhow.
field no longer implies decidable_eq, so you need to add classical, open_locale classical, etc., as necessary.
field no longer has the inv_mul_cancel field, so you need to remove it from the instances.
Lots of lemmas in core got renamed / changed / have fewer arguments now due to the field change.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

robertylewis · 2020-02-27T19:35:58Z

2. field no longer implies decidable_eq, so you need to add classical, open_locale classical, etc., as necessary.

I haven't looked closely at the changes yet, but the fix should often be to add a [decidable_eq T] hypothesis instead of open_locale classical, no? I'll look more carefully in the office tomorrow.

these aren't the cleanest proofs, but pell.lean is kind of a standalone thing.

gebner · 2020-02-28T17:00:53Z

src/analysis/complex/polynomial.lean

@@ -56,7 +56,7 @@ have hF₁ : F.eval z' = f.eval z₀ - f.eval z₀ * (g.eval z₀).abs * δ ^ n
      neg_mul_eq_neg_mul_symm, mul_one, div_eq_mul_inv];
    simp only [mul_comm, mul_left_comm, mul_assoc],
 have hδs : (g.eval z₀).abs * δ ^ n / (f.eval z₀).abs < 1,
-  by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← inv_inv' (complex.abs _ * _), mul_inv',
+  by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← @inv_inv' _ _ (complex.abs _ * _), mul_inv',


Suggested change

by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← @inv_inv' _ _ (complex.abs _ * _), mul_inv',

by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← inv_inv'' (complex.abs _ * _), mul_inv',

urkud · 2020-03-02T08:57:42Z

BTW, should we increase mathlib version here so that people will be able to easily stick to lean-3.5.1 version for some time?

…b into lean36

urkud · 2020-03-02T14:42:10Z

field no longer implies decidable_eq, so you need to add classical, open_locale classical, etc., as necessary.

I haven't looked closely at the changes yet, but the fix should often be to add a [decidable_eq T] hypothesis instead of open_locale classical, no? I'll look more carefully in the office tomorrow.

As far as I understand, it should be [deciddable_eq T] in definitions and classical in theorems.

urkud · 2020-03-02T14:54:39Z

src/algebra/field.lean


-lemma inv_involutive' [discrete_field α] : function.involutive (has_inv.inv : α → α) :=
+lemma inv_inv'' [division_ring α] (x : α) : x⁻¹⁻¹ = x :=
 inv_inv'


What's the difference between inv_inv' and inv_inv''? Why do we need both?

As far as I can see, the only difference is that inv_inv' takes x as an implicit argument. I think, this should be fixed in the stdlib.

urkud · 2020-03-02T16:18:59Z

I wonder why class instance resolution fails in real_inner_product.

jcommelin · 2020-03-04T14:12:08Z

test/monotonicity.lean

@@ -299,7 +299,7 @@ example (x y z k m n i j : ℕ)
 : (m + x + n + i) * z + k = z * (j + n + m + y) + k :=


It seems that there are a lot of : at the beginning of lines in this file...

gebner · 2020-03-05T10:00:43Z

Wow, it builds!!

* chore(*): switch to lean 3.6.0 * Port `src/linear_algebra` to Lean 3.6c * Port `src/ring_theory` to Lean 3.6c * Port `src/algebra` and its dependencies to Lean 3.6c * Port `src/group_theory` to Lean 3.6c * WIP: Ports part of `src/data` to Lean 3.6c * Port `src/data` (and dependencies) to Lean 3.6 * fix set_theory.lists * fix ring2 * fix pell.lean these aren't the cleanest proofs, but pell.lean is kind of a standalone thing. * fix dioph.lean * Port `src/number_theory/sum_four_squares.lean` to Lean 3.6c * Port `src/field_theory` to Lean 3.6 * Port `src/computability` to Lean 3.6c * Port `src/measure_theory` (and dependencies) to Lean 3.6c * fix manifold/real_instances * fix analysis/complex/polynomial * Fix some compile errors in `real_inner_product` * Upgrade to Lean 3.6.1 * perf: speed up calls to linarith * Reduce instance priorities for potentially noncomputable instances. * Remove cyclic instance. * Make arguments {implicit} in instances where they can be filled in via unification. * Make inner_product_space compile. * Style. * Port data.nat.modeq * Port data.int.parity * Port data.int.modeq * Port data.real.hyperreal * fix(ci): always run git setup step closes leanprover-community#2079 (cherry picked from commit 8a0157d) * Remove pre-3.6 legacy code. * Fix test/monotonicity.lean * Fix test/ring_exp.lean * Fix test/conv.lean * Fix archive/imo1988_q6.lean * Fix docs/tutorial/Zmod37.lean * Fix archive/sensitivity.lean * refactor(algebra/lie_algebra): lie_algebra should not extend lie_ring * remove unused argument * add doc-string to instance that became a def * add docstring * Fix linting error ☺ * Fix data.real.irrational * fixing a proof * cleaning up proof * fix broken proof * fix proof * fix some more proofs * fix * fix proofs Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Scott Morrison <scott@tqft.net>

chore(*): switch to lean 3.6.0

e6f4901

robertylewis mentioned this pull request Feb 27, 2020

feat(tactic): command for adding tactic, command, and attribute documentation (RFC) #1963

Closed

7 tasks

gebner added enhancement help-wanted The author needs attention to resolve issues WIP Work in progress labels Feb 27, 2020

Vierkantor added 5 commits February 27, 2020 15:46

Port src/linear_algebra to Lean 3.6c

5350fd8

Port src/ring_theory to Lean 3.6c

fc34d93

Port src/algebra and its dependencies to Lean 3.6c

158db65

Port src/group_theory to Lean 3.6c

1a5d95f

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

185f76d

Vierkantor and others added 11 commits February 28, 2020 10:56

Port src/data (and dependencies) to Lean 3.6

561696f

fix set_theory.lists

29aa9ee

fix ring2

9d66ac2

fix pell.lean

0e44d29

these aren't the cleanest proofs, but pell.lean is kind of a standalone thing.

fix dioph.lean

1b5508d

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

389d5f4

Port src/field_theory to Lean 3.6

4fcd626

Port src/computability to Lean 3.6c

82bd7bb

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

8427582

fix manifold/real_instances

a4a51e9

fix analysis/complex/polynomial

767ecc7

gebner commented Feb 28, 2020

View reviewed changes

urkud added 2 commits March 2, 2020 09:06

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

73f5a7e

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

f8bc1c4

…b into lean36

urkud reviewed Mar 2, 2020

View reviewed changes

Fix some compile errors in real_inner_product

a9ec482

gebner added 2 commits March 4, 2020 12:55

Fix docs/tutorial/Zmod37.lean

8f9b6c6

Fix archive/sensitivity.lean

9e38477

jcommelin reviewed Mar 4, 2020

View reviewed changes

gebner and others added 16 commits March 4, 2020 18:13

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

83b9a20

remove unused argument

e7823d1

add doc-string to instance that became a def

b37f486

add docstring

3beb5f7

Fix linting error ☺

b1daf12

Fix data.real.irrational

72af113

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

23f1ff7

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

2d4f527

fixing a proof

748a257

cleaning up proof

706ecea

fix broken proof

5ad2c87

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

78dccce

fix proof

7bceaee

fix some more proofs

bad47c3

fix

9e3332a

fix proofs

f6649a8

gebner added awaiting-review The author would like community review of the PR and removed WIP Work in progress help-wanted The author needs attention to resolve issues labels Mar 5, 2020

jcommelin approved these changes Mar 5, 2020

View reviewed changes

jcommelin added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Mar 5, 2020

mergify bot merged commit 78ffbae into master Mar 5, 2020

mergify bot deleted the lean36 branch March 5, 2020 13:17

YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 15, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore(*): switch to lean 3.6.1 #2064

chore(*): switch to lean 3.6.1 #2064

gebner commented Feb 27, 2020 •

edited by urkud

robertylewis commented Feb 27, 2020 •

edited

gebner Feb 28, 2020

urkud commented Mar 2, 2020

urkud commented Mar 2, 2020

urkud Mar 2, 2020

urkud Mar 2, 2020

urkud commented Mar 2, 2020

jcommelin Mar 4, 2020

gebner commented Mar 5, 2020

	by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← @inv_inv' _ _ (complex.abs _ * _), mul_inv',
	by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← inv_inv'' (complex.abs _ * _), mul_inv',

		@@ -299,7 +299,7 @@ example (x y z k m n i j : ℕ)
		: (m + x + n + i) * z + k = z * (j + n + m + y) + k :=

chore(*): switch to lean 3.6.1 #2064

chore(*): switch to lean 3.6.1 #2064

Conversation

gebner commented Feb 27, 2020 • edited by urkud

robertylewis commented Feb 27, 2020 • edited

gebner Feb 28, 2020

Choose a reason for hiding this comment

urkud commented Mar 2, 2020

urkud commented Mar 2, 2020

urkud Mar 2, 2020

Choose a reason for hiding this comment

urkud Mar 2, 2020

Choose a reason for hiding this comment

urkud commented Mar 2, 2020

jcommelin Mar 4, 2020

Choose a reason for hiding this comment

gebner commented Mar 5, 2020

gebner commented Feb 27, 2020 •

edited by urkud

robertylewis commented Feb 27, 2020 •

edited