Zulip Chat Archive

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),
   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`. -/

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

Gabriel Ebner (May 15 2020 at 17:47):

Yes.

Johan Commelin (May 15 2020 at 17:47):

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 21:59):

Did we hear from Leo about copyrights?

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.