feat: implement have this

[digama0]

This builds on #2246, to make use of the hygieneInfo parser in have and suffices. It also allows _ binders for have and let (rather than treating them as patterns), superseding part of #2105.

[Kha]

It also allows _ binders for have and let (rather than treating them as patterns)

I'm assuming you combined these changes to avoid another update-stage0 dance, but it held me back from merging the PR immediately. @leodemoura Are you on board with consistently moving towards binderIdent for binders where it makes sense? I'm willing to review #2105 if Mario is interested in updating and finishing it.

[leodemoura]

@leodemoura Are you on board with consistently moving towards binderIdent for binders where it makes sense? I'm willing to review #2105 if Mario is interested in updating and finishing it.

I am onboard if it does not create a "snowball" of new issues.

[digama0]

Hm, I am not sure what I can do to determine how likely it is to create a cascade of other issues. What I can do concretely is fix it up so it passes all the tests, and try bumping std and mathlib to make sure they also don't break. (I'll need to wait until just after an actual nightly bump to do that test.) Hopefully the changes to the code and any test changes made as a result will help answer the question of what the concrete fallout will be.

I am optimistic that will have essentially no effects on user code, although it will involve changing some tactics to handle the hole case.

(I can also back out the _ change from this PR; the reason I added it is because without it have _ := foo is interpreted as have this _ := foo instead of have _x := foo.)

[Kha]

the reason I added it is because without it have _ := foo is interpreted as have this _ := foo instead of have _x := foo

Hmm, don't we have the same issue with any other kind of pattern then? have \<x, y\> should not mean have this \<x, y\> either

[Kha]

If we do rebootstrap the PR, one remark and one question:

• We should probably use mkAntiquotation (anonymous := false), we really don't want to capture an invisible piece of syntax by default
• Is it clear why we need two update-stage0s? Did you try using parseQuotWithCurrentStage like described in bootstrap.md?

[digama0]

Hmm, don't we have the same issue with any other kind of pattern then? have \<x, y\> should not mean have this \<x, y\> either

No, because \<x, y\> is not a binder. You can't write have foo \<x, y\> := ..., it needs to be have foo | \<x, y\> => ... or something.

[digama0]

If we do rebootstrap the PR,

I'm not sure exactly what you mean by this. I have (unfortunately) quite some experience doing this dance, and I can rebase this PR if required via a script, although it takes a while (I think it's around 25 minutes per update-stage0 since you have to build lean again from scratch)

• We should probably use mkAntiquotation (anonymous := false), we really don't want to capture an invisible piece of syntax by default

Sure, I'll add that

• Is it clear why we need two update-stage0s? Did you try using parseQuotWithCurrentStage like described in bootstrap.md?

I tried my best to optimize it, and I am using parseQuotWithCurrentStage in the middle stage. The current staging looks like this:

• Part 1: Prepare have to not break when seeing hygieneInfo. This is useless in the first stage but it prevents breakage in stage 2.
• Update stage 0: now the builtin have understands hygieneInfo
• Part 2: Main implementation. parseQuotWithCurrentStage is enabled, the new grammar productions are added, and the new have implementation uses the new grammar productions. Because of parseQuotWithCurrentStage, various things are using the new syntax and passing it through the builtin have implementation, which is why we needed part 1.
  • There is a use of have inside the DecidableEq handler, which is parsed using the old grammar and will cause errors in stage 3. The easiest way to get around this is to just swap out the implementation for something else temporarily.
• Update stage 0: now the new notation is fully installed
• Part 3: cleanup staging effects, fix tests

[Kha]

No, because \<x, y\> is not a binder.

Ah, of course. Then I don't have any remaining reservations on this PR anymore.

I'm not sure exactly what you mean by this

Just regenerating the stage0 updates.

via a script

Does it use git rebase --exec? Would be nice to contribute and document!

[Kha]

I just checked out the PR, it builds fine without the stage0 updates except for the deriving DecidableEq issue. Changing a built-in syntax like haveDecl that is depended on by non-builtin syntax like tactic have is an unfortunate known issue.

[digama0]

I just checked out the PR, it builds fine without the stage0 updates except for the deriving DecidableEq issue. Changing a built-in syntax like term have that is depended on by non-builtin syntax like tactic have is an unfortunate known issue.

are you saying you can build it if you merge part 1 & 2? I'm pretty sure I tried that, it fails right at the start of part 3.

via a script

Does it use git rebase --exec? Would be nice to contribute and document!

Actually it's a bit less than this, I use git rebase --interactive and replace all the update-stage0 commits with x ./x0.sh which is a script that calls make update-stage0 and commits the result. Usually I also want to stop and edit one or more commits at the same time, so it works okay for my use case.

[Kha]

Yes, all I did was remove the two update-stage0 commits. Stage 1 builds fine, then the tests and stage 2 fail on the deriving issue.

[digama0]

right, if you just don't do any staging then you won't be able to bootstrap, that's what a failure in stage 2 is. If you run update-stage0 then the Init package can't be parsed. The work in part 1 is to make sure that the part 3 build (after the bootstrap) doesn't crash while reading Init.

[Kha]

I don't see why parsing would be affected. I get a very late error due to the deriving issue after rebootstrapping:

Lean/Meta/Tactic/LinearArith/Solver.lean:130:22: error: tactic 'rfl' failed, equality lhs
  x✝
is not definitionally equal to rhs
  y✝
x✝ y✝ : CnstrKind
h✝ : CnstrKind.toCtorIdx x✝ = CnstrKind.toCtorIdx y✝
⊢ x✝ = y✝

[Kha]

Just to be perfectly clear, this is my history:

[digama0]

what happens if you put the update stage0 between part 2 and part 3? The main thing that part 3 does is to take out the have -> let_fun hack which was done to get around the issue that you are reporting.

[Kha]

what happens if you put the update stage0 between part 2 and part 3?

Right, that makes more sense. But it builds and tests fine.

[digama0]

Okay, I updated it with only two stages and added the (anonymous := false) (which is actually part of the other PR), and rebased both PRs on master.

[Kha]

Thanks!

[Kha]

@digama0 Ah, do you want to add a release note as well describing the user-level changes?

[digama0]

is there a special syntax that I put in the PR description?

[Kha]

No, feel free to open a new PR adjusting RELEASES.md