Zulip Chat Archive

Stream: PR reviews

Topic: lean#229


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 15 2020 at 17:07):

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

view this post on Zulip Johan Commelin (May 15 2020 at 17:07):

I will work on the algebra part

view this post on Zulip 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),
   add_decl decl <|> fail format!"failed to add projection lemma {decl_name}.",
-  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`. -/

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 15 2020 at 17:26):

A thanks. I didn't see that one.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 15 2020 at 17:46):

Or has_one

view this post on Zulip Gabriel Ebner (May 15 2020 at 17:47):

Yes.

view this post on Zulip Johan Commelin (May 15 2020 at 17:47):

Ok, pushed

view this post on Zulip Johan Commelin (May 15 2020 at 19:59):

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

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 20:17):

Approved. Thanks for the hard work everyone!

view this post on Zulip Kevin Buzzard (May 15 2020 at 20:17):

Can someone exactly what has been going on recently?

view this post on Zulip Johan Commelin (May 15 2020 at 20:17):

See the commit message

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 20:18):

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

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 20:18):

Those two are also in the queue.

view this post on Zulip Johan Commelin (May 15 2020 at 20:19):

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

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 20:19):

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

view this post on Zulip Yury G. Kudryashov (May 15 2020 at 21:59):

Did we hear from Leo about copyrights?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 15 2020 at 22:01):

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

view this post on Zulip 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?"

view this post on Zulip 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?"

view this post on Zulip Mario Carneiro (May 15 2020 at 22:32):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:21):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:24):

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

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:24):

They are copyright MS in lean 3.4.2

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:25):

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

view this post on Zulip Kevin Buzzard (May 16 2020 at 00:25):

So is the question about files copyright Leo, copyright MS, or both?

view this post on Zulip Kevin Buzzard (May 16 2020 at 00:26):

I see, I can see both kinds of file.

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:26):

Wait a minute. I'm looking at the copyright headers.

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:30):

C++ definitely doesn't go to mathlib

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:31):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:33):

init/algebra/group?

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:34):

/me is going to the kitchen

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:48):

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

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 00:49):

The only question is what sort of attribution is OK.

view this post on Zulip Kevin Buzzard (May 16 2020 at 01:14):

Ok I asked him something

view this post on Zulip 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:

view this post on Zulip 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