## Stream: PR reviews

### Topic: lean#229

#### Johan Commelin (May 15 2020 at 16:44):

I think this one is ready.
I'm still worried about what happens to mathlib after we merge this PR. But if others don't mind... we can lump it in the same release as all the other PRs that are merged into core.

#### Gabriel Ebner (May 15 2020 at 17:06):

As long as you volunteer to update mathlib. You're also the one who knows best what has been removed. I don't think any of the other changes breaks anything in mathlib.

#### Johan Commelin (May 15 2020 at 17:07):

As long as none of the other PRs breaks anything in mathlib...

#### Johan Commelin (May 15 2020 at 17:07):

I will work on the algebra part

#### Gabriel Ebner (May 15 2020 at 17:09):

Oh, there was one breaking change:

diff --git a/src/tactic/simps.lean b/src/tactic/simps.lean
index 3a986891..46831659 100644
--- a/src/tactic/simps.lean
+++ b/src/tactic/simps.lean
@@ -29,8 +29,9 @@ meta def simps_add_projection (nm : name) (type lhs rhs : expr) (args : list exp
let decl_value := refl_ap.lambdas args,
let decl := declaration.thm decl_name univs decl_type (pure decl_value),
-  when add_simp $- set_basic_attribute simp decl_name tt >> set_basic_attribute _refl_lemma decl_name tt + when add_simp$ do
+    set_basic_attribute _refl_lemma decl_name tt,
+    set_basic_attribute simp decl_name tt

/-- Derive lemmas specifying the projections of the declaration.
If todo is non-empty, it will generate exactly the names in todo. -/


#### Bryan Gin-ge Chen (May 15 2020 at 17:16):

@Mario Carneiro had a question about default_dec_tac that was hidden in a resolved comment. Was that settled?

#### Johan Commelin (May 15 2020 at 17:26):

A thanks. I didn't see that one.

#### Johan Commelin (May 15 2020 at 17:27):

We don't need to do that in this PR. At some point I thought that it depended on algebra, but it didn't.

#### Johan Commelin (May 15 2020 at 17:45):

@Gabriel Ebner Does

constant foo_rec (n : ℕ) (k : Type) [group k]  : Prop

lemma stupid (k : Type) [group k] (n : ℕ) :
foo_rec nat.zero k ↔ foo_rec nat.zero k :=
by simp only [nat.nat_zero_eq_zero]

open tactic
#eval do
cgr ← mk_congr_lemma_simp (foo_rec),
type_check cgr.proof


depend on group. Not really, right? I can change it to preorder if I want, right?

#### Johan Commelin (May 15 2020 at 17:46):

Or has_one

Yes.

Ok, pushed

#### Johan Commelin (May 15 2020 at 19:59):

Hooray! It passed the linter. CI is now at the leanchecker stage.

#### Bryan Gin-ge Chen (May 15 2020 at 20:17):

Approved. Thanks for the hard work everyone!

#### Kevin Buzzard (May 15 2020 at 20:17):

Can someone exactly what has been going on recently?

#### Johan Commelin (May 15 2020 at 20:17):

See the commit message

#### Johan Commelin (May 15 2020 at 20:18):

But basically: {x} is now what you want it to be. And the associativity for {x,y,z} also changed, so it's better now.

#### Bryan Gin-ge Chen (May 15 2020 at 20:18):

Can someone check whether this will conflict with #2646 or #2689?

#### Bryan Gin-ge Chen (May 15 2020 at 20:18):

Those two are also in the queue.

#### Johan Commelin (May 15 2020 at 20:19):

I fear that I won't be able to check before bed time

#### Bryan Gin-ge Chen (May 15 2020 at 20:19):

OK, we can also just let bors tell us if something breaks.

#### Yury G. Kudryashov (May 15 2020 at 22:00):

I mean copyrights on files moved from core to mathlib, especially ones we merge their contents in our files.

#### Kevin Buzzard (May 15 2020 at 22:01):

I did not ask him anything. If someone wants to tell me what to ask him this would be great. I am not really following what is going on here

#### Kevin Buzzard (May 15 2020 at 22:01):

All I know is that people are super-excited about v3.13

#### Jalex Stark (May 15 2020 at 22:29):

Kevin Buzzard said:

I did not ask him anything. If someone wants to tell me what to ask him this would be great. I am not really following what is going on here

I was half-following, and I think the question is:
"We're moving stuff from core to mathlib. A bunch of it is copyrighted by (Leo? Microsoft?). Do you / Microsoft have any particular ideas on what we should or should not do about the copyright declarations in the files?"

#### Jalex Stark (May 15 2020 at 22:30):

and maybe someone had a specific suggestion, so the question could be extended with "Our first thought was to do this, is that okay or should we do something different?"

#### Mario Carneiro (May 15 2020 at 22:32):

Lean is apache licensed, so attribution is required but otherwise reuse should be fine

#### Yury G. Kudryashov (May 16 2020 at 00:20):

So, what are we going to do:

• add Microsoft to (c) line of every file with code from Lean core;
• add Microsoft to Authors: line of ...;
• something else?

#### Yury G. Kudryashov (May 16 2020 at 00:21):

BTW, (c) one author followed by "Authors: ..." looks strange to me.

#### Kevin Buzzard (May 16 2020 at 00:22):

Jalex Stark said:

Kevin Buzzard said:

I did not ask him anything. If someone wants to tell me what to ask him this would be great. I am not really following what is going on here

I was half-following, and I think the question is:
"We're moving stuff from core to mathlib. A bunch of it is copyrighted by (Leo? Microsoft?). Do you / Microsoft have any particular ideas on what we should or should not do about the copyright declarations in the files?"

I am happy to ask Leo about this but I need to know what the exact question is. I don't really want to say "copyright you or MS or something" and I don't know which files we're talking about.

#### Yury G. Kudryashov (May 16 2020 at 00:24):

We are talking about files removed from core in lean#229, mainly algebraic definitions/theorems.

#### Yury G. Kudryashov (May 16 2020 at 00:24):

They are copyright MS in lean 3.4.2

#### Yury G. Kudryashov (May 16 2020 at 00:25):

Clearly, if we just resurrect a file in mathlib, then we preserve the copyright header.

#### Kevin Buzzard (May 16 2020 at 00:26):

I see, I can see both kinds of file.

#### Kevin Buzzard (May 16 2020 at 00:27):

What happens to e.g. src/library/arith_instance.cpp? It's C++ code. Surely that's not going into mathlib?

#### Yury G. Kudryashov (May 16 2020 at 00:30):

C++ definitely doesn't go to mathlib

#### Yury G. Kudryashov (May 16 2020 at 00:31):

@Johan Commelin Why did you have to change app builder in this PR?

#### Kevin Buzzard (May 16 2020 at 00:31):

Is there an example of a lean file which will go essentially unchanged into mathlib, and which has "copyright Microsoft" written in it?

#### Yury G. Kudryashov (May 16 2020 at 00:33):

init/algebra/group`?

#### Yury G. Kudryashov (May 16 2020 at 00:34):

/me is going to the kitchen

#### Kevin Buzzard (May 16 2020 at 00:37):

And is the question simply "do you mind if we move a file unchanged from Lean 3.12 into mathlib" or are there some more subtle questions?

#### Yury G. Kudryashov (May 16 2020 at 00:48):

There is a more subtle question: what should we do when we merge code from this file with our code in mathlib?

#### Yury G. Kudryashov (May 16 2020 at 00:48):

According to Apache License, we clearly may move code to mathlib without asking.

#### Yury G. Kudryashov (May 16 2020 at 00:49):

The only question is what sort of attribution is OK.

#### Johan Commelin (May 16 2020 at 04:01):

Yury G. Kudryashov said:

Johan Commelin Why did you have to change app builder in this PR?

I have no idea. Gabriel did that so that I could move forward again :oops:

#### Keeley Hoek (May 16 2020 at 18:18):

@Yury G. Kudryashov From a cursory glance it seems to me it was entirely just deleting (unused) c++ functions which reference removed lemmas, barring a single change here: https://github.com/leanprover-community/lean/pull/229/files?file-filters%5B%5D=.cpp&file-filters%5B%5D=.h#diff-672f44b0651a1af0d7da661a06ca7295L926
which is presumably non-functional.

Last updated: May 06 2021 at 12:15 UTC