Zulip Chat Archive

Stream: new members

Topic: 2006 STEP 3 Question 8


view this post on Zulip Shing Tak Lam (Mar 23 2020 at 02:53):

Hello, I was trying to formalise my solution to this question in lean, but I'm getting an error saying the my result contains meta variables.

image.png

So far I have

import data.polynomial
       data.real.basic

open polynomial

variable Δ : polynomial   polynomial 
variables f g : polynomial 
variable k : 

axiom Δ1 : Δ X = C 1
axiom Δ2 : Δ(f + g) = Δ f + Δ g
axiom Δ3 : Δ(C k * f) = C k * Δ f
axiom Δ4 : Δ(f * g) = f * Δ g + g * Δ f

lemma ΔXcubed : Δ (X^3) = 3*X^2 := begin
    have h1 : X^3 = X * X^2 := begin
        have h11 : 3 = 2 + 1 := rfl,
        rw h11,
        rw pow_succ,
    end -- Error Here
end

I've highlighted where the error is occuring, the error message is

tactic failed, result contains meta-variables
state:
no goals
state:
6 goals
Δ : polynomial ℝ → polynomial ℝ
⊢ Δ (X ^ 3) = 3 * X ^ 2

Δ : polynomial ℝ → polynomial ℝ
⊢ Type ?

Δ : polynomial ℝ → polynomial ℝ
⊢ comm_semiring ?m_1

Δ : polynomial ℝ → polynomial ℝ
⊢ has_pow (polynomial ?m_1) ℕ

Δ : polynomial ℝ → polynomial ℝ
⊢ has_mul (polynomial ?m_1)

Δ : polynomial ℝ → polynomial ℝ
⊢ has_pow (polynomial ?m_1) ℕ

I think I know why the error is occurring, as I didn't specify the type of X, so lean doesn't know that it has pow mul, etc. But I'm not sure how or where I could add the type annotations?

Also, when I use the axioms, rw \Delta4 doesn't work, I need to specify rw \Delta4 \Delta. Making \Delta a constant fixes this, but then it still doesn't fix the error message above. In this case, should \Delta be variable or constant? Since I don't care what Delta is, as long as it satisfies those axioms.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 02:59):

those axioms should be variables. If you make them axioms then they will implicitly quantify over all Delta, meaning that you are adding an axiom to lean that says that all functions are derivations. Since this is false, the axiom will make lean inconsistent

view this post on Zulip Yury G. Kudryashov (Mar 23 2020 at 03:01):

And you probably want to include all these variables so that they will be available in tactic proofs.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 03:30):

Alright thank you, I've edited it with your suggestions. However, I still have an issue with the results contains meta-variables.

view this post on Zulip Yury G. Kudryashov (Mar 23 2020 at 03:33):

Can't help without looking at your code...

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 03:36):

Apologies. The error message is basically the same after changing the axioms to variables. I've also changed f g and k to be in foralls instead of variables.

import data.polynomial
       data.real.basic

open polynomial

variable Δ : polynomial   polynomial 
include Δ

variable Δ1 : Δ X = C 1
variable Δ2 :  (f g : polynomial ), Δ(f + g) = Δ f + Δ g
variable Δ3 :  (k : ) (f : polynomial ), Δ(C k * f) = C k * Δ f
variable Δ4 :  (f g : polynomial ), Δ(f * g) = f * Δ g + g * Δ f
include Δ1 Δ2 Δ3 Δ4

lemma ΔXcubed : Δ (X^3) = 3*X^2 := begin
    have h1 : X^3 = X * X^2 := begin
        have h11 : 3 = 2 + 1 := rfl,
        rw h11,
        rw pow_succ,
    end -- ERROR HERE
end

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 03:38):

Nevermind, I've figured it out. I needed to add the type annotation in the inner have statement, as the X in the inner statement is different to the one in the theorem statement.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 03:41):

you can prove h1 by ring

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 03:49):

Alright, Thanks!

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:07):

Did you try recover?

This is a great question for Lean!

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:45):

I think you might be better off proving lemma Δ_one : Δ 1 = 0 first, and then lemma ΔX_pow_succ (n : ℕ) : Δ (X ^ (n + 1)) = (n + 1) * X ^ n

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:47):

I'm sorry, but I'm not sure what you mean by using recover.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:47):

I've already proved that \Delta c = 0 for all c.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:47):

I've already proved that \Delta c = 0 for all c.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:47):

I'm sorry, but I'm not sure what you mean by using recover.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:48):

And I did prove the general case of X^n, although I used X^n and not X^(n+1), which had an interesting base case

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:48):

Oh, recover was when your goal contained metavariables.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:48):

Ah. I see

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:49):

The problem with X^n directly is that when n=1 the inductive hypothesis involves 0 - 1 so has to be dealt with as a special case.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:50):

Yeah, when I was doing this question for STEP prep I thought it would be interesting to do in lean, as the steps revolved around these 4 rules. Now that no one even knows what's gonna happen with A Levels/STEP I had a bit of free time so I thought I'd give it a shot in Lean.

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:51):

My son is in the same position -- sitting on a Cambridge offer with no idea what's going to happen next.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:51):

That makes sense, I did it on paper first and tried a direct translation. In retrospect X^(n+1) makes more sense. I'm gonna refactor it.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:52):

Yeah, Cambridge sent out an email like hours before the Government announcement, which wasn't that helpful.

(Not that any of my other Universities seem to know what is happening, do you know anything about Imperial?)

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 07:52):

No decisions have been made yet.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:53):

Alright. Just that they haven't said anything since January, which was slightly worrying.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 07:53):

Thank you very much for all of your help

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 08:17):

lemma Δ_one : Δ 1 = 0 :=
begin
  -- the standard trick
  suffices H : Δ 1 + Δ 1 = Δ 1,
    rwa add_left_eq_self at H,
  conv begin to_rhs,
    rw (show (1 : polynomial ) = 1 * 1, by ring),
  end,
  rw Δ4,
  ring,
end

lemma ΔX_pow_succ (n : ) : Δ (X ^ (n + 1)) = (n + 1) * X ^ n := begin
  induction n with d hd,
  { -- base case
    rw [pow_one, Δ1, nat.cast_zero],
    ring,
  },
  rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ,
    nat.cast_add, nat.cast_one],
  ring,
end

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 08:22):

It helps a lot knowing what ring can and cannot do.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 08:31):

Again, thank you very much.

This (once again) reminds me I should probably read TPIL. show is nicer than what I've been doing, which is have then rw, which clutters up my local context a lot, and I end up with a lot of local hypotheses which are only used once.

For the final part of the question, the proof that \Delta f = df/dx for all polynomial f, I did it (on paper) by arguing that it's true for a polynomial of degree 1 (and 0), and then using induction, assuming that it is true for a polynomial of degree n then showing that it's true for a polynomial of degree n+1, therefore it is true for all polynomials. I've tried looking in data.polynomial, but I don't think I've seen this functionality in there. So I might have to do it another way.

I'm gonna look ring (and probably what a ring is first).

view this post on Zulip Mario Carneiro (Mar 23 2020 at 08:54):

This is just induction on natural numbers

view this post on Zulip Mario Carneiro (Mar 23 2020 at 08:55):

I'm pretty sure there is a degree function on polynomials

view this post on Zulip Mario Carneiro (Mar 23 2020 at 08:56):

The question I have about this problem is, do we have the definition of the derivative of a polynomial yet? Do we know it is a polynomial? I'm not sure how you intend to write the theorem statement

view this post on Zulip Johan Commelin (Mar 23 2020 at 08:58):

Mario Carneiro said:

I'm pretty sure there is a degree function on polynomials

Yes, and there is also nat_degree which is a natural number. (degree 0 is not natural)

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 08:59):

So induction on degree p where p is the polynomial? The degree function returns an option nat though, so I'll have to look at that further.

I haven't written it yet, but there is a polynomial.derivative function, so I think it'll just be forall (p : polynomial R), derivative p = \Delta p.

view this post on Zulip Johan Commelin (Mar 23 2020 at 08:59):

We have the formal derivative of a polynomial, and also a proof that as a function it coincides with the analytical derivative (if you work over a normed field or something)

view this post on Zulip Mario Carneiro (Mar 23 2020 at 08:59):

nice

view this post on Zulip Sebastien Gouezel (Mar 23 2020 at 09:26):

There is a function polynomial.induction_on that is designed precisely for this kind of induction. You can for instance have a look at analysis/calculus/deriv, line 1116.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 09:36):

Ok. Thank you all very much. I'll give that a shot when I have some more time to look at this.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 11:43):

I've had some free time just then and I tried Kevin's solution from above. However when i pasted it into lean I got a (deterministic) timeout. Seems like the rings are taking too long. I doubt my laptop is too slow, but that is a possibility.

Any suggestions to how I can fix this?

view this post on Zulip Mario Carneiro (Mar 23 2020 at 11:44):

ring performs very fast on almost all not-contrived examples, so that's not likely to be the problem

view this post on Zulip Mario Carneiro (Mar 23 2020 at 11:44):

it could be typeclass inference or something else

view this post on Zulip Mario Carneiro (Mar 23 2020 at 11:44):

code plz

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 11:47):

Minimum Working Example

import data.polynomial
       data.real.basic
       tactic

open polynomial

variable Δ : polynomial   polynomial 
include Δ

variable Δ1 : Δ X = C 1
variable Δ2 :  (f g : polynomial ), Δ(f + g) = Δ f + Δ g
variable Δ3 :  (k : ) (f : polynomial ), Δ(C k * f) = C k * Δ f
variable Δ4 :  (f g : polynomial ), Δ(f * g) = f * Δ g + g * Δ f
include Δ1 Δ2 Δ3 Δ4

lemma ΔXn (n : ) : Δ (X^(n+1)) = (n+1)*X^n := begin
    induction n with d hd,
  { -- base case
    rw [pow_one, Δ1, nat.cast_zero],
    ring,
  },
  rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ,
    nat.cast_add, nat.cast_one],
  ring,
end

The lemma is just the one Kevin posted above, so it probably worked on his machine.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 11:48):

It might be of use: #eval lean.version is (3, (6, 1)), mathlib is mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "093ac77ac9d27ce83ebf4e76ca5bd9b3eaebedaa"}

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 11:49):

The lemma checks almost immediately if I comment out the ring in the inductive case (the one at the end of the lemma)

view this post on Zulip Mario Carneiro (Mar 23 2020 at 11:57):

The goal you gave to ring is

 X * ((d + 1) * X ^ d) + X * X ^ d * C 1 = (d + 1 + 1) * (X * X ^ d)

which is not an equality that is valid from the axioms of rings alone (because of the C 1)

view this post on Zulip Mario Carneiro (Mar 23 2020 at 11:59):

I think ring is probably taking forever because it does some processing to see if different looking expressions are defeq, and it is unfolding C 1

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:00):

IIRC there is an option to disable that, but then it will just fail in this case

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:01):

This works

lemma ΔXn (n : ) : Δ (X^(n+1)) = (n+1)*X^n := begin
    induction n with d hd,
  { -- base case
    rw [pow_one, Δ1, nat.cast_zero],
    ring,
  },
  rw [nat.succ_eq_add_one, pow_succ, Δ4, Δ1, hd, pow_succ,
    nat.cast_add, nat.cast_one, C_1],
  ring,
end

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 12:01):

Huh... Alright. (I didn't write this).

Adding rw (show C (1:ℝ) = 1, by simp), before ring fixed this.

Thank you very much.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:02):

Alternatively you can probably use simp instead of rw since half of those equations are simp lemmas

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 12:03):

I see. I thought I saw somewhere that it's best to only use simp as the last tactic in a proof. That's why I didn't use it there.

view this post on Zulip Johan Commelin (Mar 23 2020 at 12:04):

That's right

view this post on Zulip Johan Commelin (Mar 23 2020 at 12:04):

But simp only is fine

view this post on Zulip Johan Commelin (Mar 23 2020 at 12:04):

Write squeeze_simp to get some help

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:04):

lemma ΔXn (n : ) : Δ (X^(n+1)) = (n+1)*X^n := begin
    induction n with d hd,
  { -- base case
    rw [pow_one, Δ1, nat.cast_zero],
    ring,
  },
  rw [pow_succ, Δ4, hd], simp [Δ1, pow_succ],
  ring,
end

view this post on Zulip Mario Carneiro (Mar 23 2020 at 12:05):

using simp before a tactic that doesn't care too much about the shape of the input, like ring, is okay

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 12:06):

Ok. Thank you.

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 12:24):

Another question, when I try to rw ΔXn, it doesn't work. But rw ΔXn Δ works. But then it puts all of Δ1 Δ2 Δ3 Δ4 as new goals. Why? It's easy to solve (repeat {assumption}), but I'd still like to know why this is the case.

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:16):

Because you used variables

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:17):

The theorems you're proving are "if Delta satisfies all these axioms then..." and the proofs are hence all functions which demand proofs of all the axioms as input

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:18):

One way around this would probably be to make some sort of structure to carry the variables around in

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:20):

You can probably also use parameters but it doesn't take much to stumble on places where they don't work very well

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:22):

If you used parameters you would probably be able to avoid this issue in this one particular lean file, but if someone were to import your file because they wanted to use your work, the extra assumptions would be back by default

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:22):

And the user could probably try to include them but then they have to remember to exclude them later. This set up happens very little in mathlib

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:23):

I think that's what you want in this case though. There are two or three intermediate lemmas and you don't want to refer to the assumptions since they are fixed, but once you reach the goal, you discharge everything and it becomes a regular theorem with a bunch of hypotheses

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:24):

Here's how it would work with structures. You could define delta-structure on a ring R to be a function called Delta from polynomial R to polynomial R which satisfied the axioms. Just like the definition of a group in the group theory game.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:25):

I think it has a name, it's called a derivation

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:26):

And then you want to prove that if Delta is any delta-structure then the underlying map Delta.to_fun must agree with differentiation

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:27):

A general derivation goes from R to another ring A and there is no Delta 1 axiom

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:28):

The advantage of the structure approach is that you have easy access to the axioms: Delta.map_add is Delta2 for the function Delta.to_fun for example

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:29):

Delta4 will be called Delta.map_mul

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:30):

And someone better at knowing Lean's naming convention can figure out what Delta3 is called

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:30):

something with smul?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:34):

Oh is it not in canonical form??

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:35):

I understand this canonical form/naming convention far worse than I would like to

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:43):

No, I think it's fine to write C k * p instead of k \bu p since it's an algebra

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:43):

I just meant that something like map_smul could be used for the name

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:43):

but since it isn't written with \bu that's a bit of a lie, so perhaps map_C_mul is better

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:52):

The correct theorem from the point of view of derivations is that if we have a structure satisfying the last three axioms then there exists a unique polynomial g such that Delta (f) = g*f', and that g can be taken to be Delta(X)

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:52):

This has the original question as a special case

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:54):

Do we have a theory of derivations in Lean already? @Johan Commelin ?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 13:55):

I think it would be quite fun to prove the universal property of derivations in general.

view this post on Zulip Mario Carneiro (Mar 23 2020 at 13:59):

pretty sure we don't

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:02):

@Shing Tak Lam so there's your homework while your teachers go through all the people in your year awarding them A-levels. I wonder if they'll do it anonymously?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:02):

Feel free to ask if you need help

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:03):

But let's make a new thread because this one has a silly name. It can go in #maths

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 14:05):

I had a meeting with my teachers earlier, and as I'm doing International A Levels, apparently my exams are still going ahead... It's just STEP that's a maybe...

Apparently the exam boards think that it's safe to go ahead (even though IB has cancelled for everyone as well).

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 14:05):

So I guess I still have to revise...

view this post on Zulip Shing Tak Lam (Mar 23 2020 at 14:06):

(deleted)

view this post on Zulip Johan Commelin (Mar 23 2020 at 14:11):

Kevin Buzzard said:

Do we have a theory of derivations in Lean already? Johan Commelin ?

Not yet, but @Kenny Lau looked into it at some point, I htink.

view this post on Zulip Kenny Lau (Mar 23 2020 at 14:12):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/derivation/near/170730598

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:17):

Has enough API been extracted?

view this post on Zulip Johan Commelin (Mar 23 2020 at 14:17):

What are you thinking of?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:18):

Did we locate the characteristic predicate yet?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:18):

I think this has something to do with transfer.

view this post on Zulip Johan Commelin (Mar 23 2020 at 14:19):

No, I don't think much happened so far.

view this post on Zulip Johan Commelin (Mar 23 2020 at 14:19):

Also, didn't we switch to calling it the "characteristic predicate"?

view this post on Zulip Kevin Buzzard (Mar 23 2020 at 14:20):

Somehow the bare minimum API is the universal property, and then there is the problem of isolating the characteristic predicate and proving that a module satisfies the characteristic predicate iff it's the differentials

view this post on Zulip Kevin Buzzard (Mar 24 2020 at 13:47):

@Kenny Lau

import data.polynomial

open polynomial

structure delta_structure (R : Type) [comm_ring R] :=
(to_fun : polynomial R  polynomial R)
(map_X' : to_fun X = 1)
(map_add' :  (f g : polynomial R), to_fun (f + g) = to_fun f + to_fun g)
(map_C_mul' :  (k : R) (f : polynomial R), to_fun (C k * f) = C k * to_fun f)
(map_mul' :  (f g : polynomial R), to_fun (f * g) = f * to_fun g + g * to_fun f)

namespace delta_structure

variables {R : Type} [comm_ring R] (Δ : delta_structure R)

instance : has_coe_to_fun (delta_structure R) := ⟨_, to_fun

@[simp] theorem map_X (Δ : delta_structure R) : Δ X = 1 := Δ.map_X'

@[simp] theorem map_add (Δ : delta_structure R) :  {f g : polynomial R}, Δ (f + g) = Δ f + Δ g := Δ.map_add'

@[simp] theorem map_C_mul :  (k : R) (f : polynomial R), Δ (C k * f) = C k * Δ f := Δ.map_C_mul'

@[simp] theorem map_mul :  (f g : polynomial R), Δ (f * g) = f * Δ g + g * Δ f := Δ.map_mul'

end delta_structure

What do you think of my structure?

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 12:46):

@Shing Tak Lam now has a github repo where this question is solved using derivations on a polynomial ring. @Patrick Massot at the time of writing I see that he only has one branch, which is lean-3.4.2. Is this something to do with the tooling? Shing -- did you use leanproject to make this repo?

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 12:50):

the linter doesn't like the simps above but now I have a much better understanding of what is going on there.

view this post on Zulip Shing Tak Lam (Mar 27 2020 at 12:58):

Yes I did use leanproject. Just to check I made a new project.

$ leanproject new test
> mkdir -p test
> cd test
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring test 0.1
Adding mathlib

I'm kinda confused now as that shouldn't be happening...

Looking at the repo at https://github.com/leanprover-community/mathlib-tools/blob/96734b3f6e7b1b6d69f86e18f4fee9c4c3e8bfff/mathlibtools/lib.py#L435 the branch should be called master.

view this post on Zulip Shing Tak Lam (Mar 27 2020 at 12:59):

For what it's worth

$ pip list | grep mathlibtools
mathlibtools                       0.0.4

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 12:59):

The tooling is brand new, much better than what we had before, but still contains a few minor glitches. It has already transformed my workflow though.

view this post on Zulip Kevin Buzzard (Mar 27 2020 at 12:59):

Yeah, that number is an indication of how new it is :-)

view this post on Zulip Patrick Massot (Mar 27 2020 at 13:35):

leanproject still uses leanpkg to create new projects. And leanpkg uses the default elan toolchain. We should change that, but that requires finding time to do it.

view this post on Zulip Patrick Massot (Mar 27 2020 at 13:36):

Also note that every complain or feature request about leanproject that is expressed here but not in a GitHub issue currently falls into a black hole.

view this post on Zulip Shing Tak Lam (Mar 27 2020 at 14:22):

Mhm... I found

https://github.com/leanprover-community/mathlib-tools/issues/26

and

https://github.com/leanprover-community/mathlib-tools/commit/5768b8fdf7de059eb8d4d663bd42fc8f9809190c

So this should be fixed...

view this post on Zulip Patrick Massot (Mar 27 2020 at 14:32):

The lean-3.4.2 exists in your repository, but the master branch also exist. Did you need to manually merge one branch into the other?

view this post on Zulip Shing Tak Lam (Mar 27 2020 at 14:36):

That was me renaming the branch locally from lean-3.4.2 to master then pushing it.

view this post on Zulip Shing Tak Lam (Mar 27 2020 at 14:37):

lean-3.4.2 now only exists on github but not on my local copy. I can probably delete it.

view this post on Zulip Patrick Massot (Mar 27 2020 at 14:50):

I'm sorry I can't reproduce this locally.

$ leanproject new test
$ git a leanpkg.toml
$ git commit
$ git branch
* master

view this post on Zulip Shing Tak Lam (Mar 27 2020 at 14:52):

No problem. I have a few ideas on what may have caused this, I'll give it a go tomorrow. If I find anything then I'll report back.


Last updated: May 08 2021 at 18:17 UTC