Lean update

[siddhartha-gadgil]

Thanks @0art0 : lake build works.

However, the command line programs like bulkelab, chkthms etc are broken as the manually specified path should now include std, Qq and aesop.

[0art0]

There also seems to be a subtle formatting issue here that I am not sure how to fix.

[siddhartha-gadgil]

There also seems to be a subtle formatting issue here that I am not sure how to fix.

This we should ask on Zulip. This is Leo de Moura's code.

[0art0]

I changed it according to the original code here.

[siddhartha-gadgil]

I will rerun the "safe prompts" generation to see there are no regressions. But I see that in "Scratch.lean" some stuff is broken due to the port (for example, "Prime" becoming "Nat.Prime").

[0art0]

I have fixed a few of the errors, but some of them seem unfixable currently (such as DivisionRing, which throws an error because of an unknown attribute in the source files). Shall we delete Scratch.lean for now and programmatically port it to the latest Lean4 using MathPort from Lean3 when needed?

[siddhartha-gadgil]

I have fixed a few of the errors, but some of them seem unfixable currently (such as DivisionRing, which throws an error because of an unknown attribute in the source files). Shall we delete Scratch.lean for now and programmatically port it to the latest Lean4 using MathPort from Lean3 when needed?

Scratch is a good test. It seems best we maintain two main branches, "main" and "lean-update", at least for a while. We may need to update translation, suggest imports etc here.

[siddhartha-gadgil]

@0art0 as I suspected there are many statements that do not elaborate. A diff is here: https://github.com/siddhartha-gadgil/LeanAide/commit/1d48c66e2c59dd7c5c56cf88a1d876e157195371#diff-77bc4cbe789c26e037630e64b90c11fb004db8fa5aea7bf31a0d61ee963835cb

We should try to figure out if we can make changes so these work again. Maybe some imports, or a different name change. ertainly #7 has a role in improving numbers.

[siddhartha-gadgil]

For this, we need a helper to give all translation/auto-correction outputs and which ones succeeded. This is the elaboration part only of translateWithDataM, i.e., without querying Codex and assuming we are given a completion.

This should be implemented in main and then pulled.

[0art0]

I will also take a look at #4 to see if it is feasible to do a Syntax -> Syntax translation that keeps up with the special name changes.

[siddhartha-gadgil]

For this, we need a helper to give all translation/auto-correction outputs and which ones succeeded. This is the elaboration part only of translateWithDataM, i.e., without querying Codex and assuming we are given a completion.

This should be implemented in main and then pulled.

I realized that the script I just made (and the function it calls) does the needed. For example, in main:

$ build/bin/chkelab "{α : Type u} [pseudo_metric_space α] (x y z : α) : has_nndist.nndist x z ≤ has_nndist.nndist x y + has_nndist.nndist y z"
{"theorem": "∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), nndist x z ≤ nndist x y + nndist y z", "success": true, "all-elabs": [" {  α :  Type  u } ->  [  PseudoMetricSpace  α ] ->  (  x y z : α ) ->   HasNndist.nndist  x z ≤   HasNndist.nndist  x y +  HasNndist.nndist  y z"]}

But in lean-update the statement does not elaborate. Specifcally, if I use the translation in Scratch I see that PseudoMetricSpace is no longer recognized.

[siddhartha-gadgil]

Yes, that would be useful. But it looks like the main issue is bits of Binport allowed to break for the sake of Synport, because of upstream changes as per Mario's comment on Zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/dropping.20.60import.20Mathbin.60.20support/near/305078886

If that is the case then we should keep this branch separate and experiment with shrunk prompts but the use of Aesop and other things. It looks like definitions are getting broken in binport but are not yet in mathlib4. As they come in we can see how to pick them up.

On Fri, 11 Nov 2022 at 16:51, Anand Rao @.***> wrote:

I will also take a look at #4 https://github.com/siddhartha-gadgil/LeanAide/issues/4 to see if it is feasible to do a Syntax -> Syntax translation that keeps up with the special name https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Mathport/SpecialNames.lean changes.

— Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LeanAide/pull/17#issuecomment-1311571180, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA3K3JDFUNKGAUP3UI5KKG3WHYT35ANCNFSM6AAAAAAR4D3VVU . You are receiving this because your review was requested.Message ID: @.***>

[0art0]

I checked locally and it seems to be a part of a series of issues that I encountered yesterday: PseudoMetricSpace is actually recognised in Mathbin, but it no longer takes in a type as an argument.

On my set-up,

example {A : Type} : PseudoMetricSpace A := sorry

throws a cryptic error, but

example {A : Type} : PseudoMetricSpace := sorry

works fine.

[siddhartha-gadgil]

That may be a false positive. I believe in the second case auto-implicits are being used. Check with these off.

On Fri, 11 Nov 2022 at 17:15, Anand Rao @.***> wrote:

I checked locally and it seems to be a part of a series of issues that I encountered yesterday: PseudoMetricSpace is actually recognised in Mathbin, but it no longer takes in a type as an argument.

On my set-up,

example {A : Type} : PseudoMetricSpace A := sorry

throws a cryptic error, but

example {A : Type} : PseudoMetricSpace := sorry

works fine.

— Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LeanAide/pull/17#issuecomment-1311595603, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA3K3JCFCQOTPPM7VSUEJ23WHYWVHANCNFSM6AAAAAAR4D3VVU . You are receiving this because your review was requested.Message ID: @.***>

[0art0]

The second one is working even with auto-implicits off:

set_option autoImplicit false
set_option relaxedAutoImplicit false

example {A : Type} : PseudoMetricSpace := sorry

[0art0]

I had noticed this for DivisionRing, IsClosed and Polynomial.aeval yesterday (the first two were of type Prop and the last one gave a "Unit" error, which I think may be related to what Mario mentioned in the Zulip thread).

[siddhartha-gadgil]

That seems to be it. Lot of things are compiled but interpreted as Units

On Fri, 11 Nov 2022 at 17:38, Anand Rao @.***> wrote:

I had noticed this for DivisionRing, IsClosed and Polynomial.aeval yesterday (the first two were of type Prop and the last one gave a "Unit" error, which I think may be related to what Mario mentioned in the Zulip thread).

— Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LeanAide/pull/17#issuecomment-1311618077, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA3K3JGC3JWO3BVDIQKWZQ3WHYZKRANCNFSM6AAAAAAR4D3VVU . You are receiving this because your review was requested.Message ID: @.***>

[siddhartha-gadgil]

@0art0 I was planning to merge - have created a branch and tag to be safe. Do you see any danger?

[0art0]

No, I do not foresee any issues with the merge.