Zulip Chat Archive

Stream: lean4

Topic: server error

Patrick Massot (Dec 14 2022 at 15:26):

In https://github.com/leanprover-community/mathlib4/pull/998/commits/d1012b892e0d1f8c87dae113607b6ab37d4aadf0, opening the file data.rat.defs reliably gives a weird error message 

Error: invalid `Name.append`, both arguments have macro scopes, consider using `eraseMacroScopes`

The error output is 400 lines long and can be found at https://gist.github.com/PatrickMassot/fcc633c44014e25fb458bfd620ec2a13

Sebastian Ullrich (Dec 14 2022 at 15:40):

Yep, that's a bug in conv congr. As it was a simple case of "called the wrong function", I've taken the liberty to push the fix directly without test case.

Mario Carneiro (Dec 14 2022 at 15:42):

oops, I have a PR coming with test case

Sebastian Ullrich (Dec 14 2022 at 15:42):

Happy to merge that :)

Patrick Massot (Dec 14 2022 at 15:42):

Thanks to both of you!

Sebastian Ullrich (Dec 14 2022 at 16:15):

I think that fixed it fwiw

$ nix build nale+github:leanprover-community/mathlib4/pull/998/head#Mathlib.mods.\"Mathlib.Data.Rat.Defs\" --override-input lean github:leanprover/lean4 -L
warning: not writing modified lock file of flake 'nale+github:leanprover-community/mathlib4/pull/998/head':
• Updated input 'lean':
    'github:leanprover/lean4-nightly/88c8cd5cf29a74a7cdb21db78791644e52401b95' (2022-12-13)
  → 'github:leanprover/lean4/d5fb32a393010e03aa13c7bfe453123cb3278e26' (2022-12-14)
Mathlib.Data.Rat.Defs> Mathlib/Data/Rat/Defs.lean:125:4: error: tactic 'injection' failed, equality of constructor applications expected
Mathlib.Data.Rat.Defs> case mk
Mathlib.Data.Rat.Defs> a✝ b✝ : ℤ
Mathlib.Data.Rat.Defs> b0 : b✝ ≠ 0
Mathlib.Data.Rat.Defs> h✝ : a✝ /. b✝ = 0
Mathlib.Data.Rat.Defs> a : ℤ
Mathlib.Data.Rat.Defs> b : ℕ
Mathlib.Data.Rat.Defs> h : 0 < b
Mathlib.Data.Rat.Defs> e : mkPNat a { val := b, property := h } = 0
Mathlib.Data.Rat.Defs> ⊢ a = 0
...

Patrick Massot (Dec 15 2022 at 15:58):

I think I have a new one, and it's pretty spectacular in its use of stderr:
bug.gif

Kevin Buzzard (Dec 15 2022 at 16:00):

What did you do to trigger it? I can't quite see from the video (I was trying to reproduce)

Patrick Massot (Dec 15 2022 at 16:01):

Opening a file...

Patrick Massot (Dec 15 2022 at 16:01):

I'll push in one minute

Sebastian Ullrich (Dec 15 2022 at 16:01):

Not aborting on panics for general Lean programs was a conscious decision, but I'm starting to wonder whether it's the right decision for lean itself

Kevin Buzzard (Dec 15 2022 at 16:01):

Aah OK -- I was wondering if I'd missed some subtlety.

Sebastian Ullrich (Dec 15 2022 at 16:02):

(which would make sure you get one message at most)

Patrick Massot (Dec 15 2022 at 16:02):

See https://github.com/leanprover-community/mathlib4/pull/1053

Kyle Miller (Mar 29 2023 at 01:41):

It looks like there's a similar "invalid Name.append" bug in tagUntaggedGoals: https://github.com/leanprover/lean4/blob/8650804b025c9e69cd7f491eeb1ba988e6969367/src/Lean/Elab/Tactic/Basic.lean#L406

Here's a mathlib4 run with a stacktrace pointing to this function: https://github.com/leanprover-community/mathlib4/actions/runs/4535703933/jobs/8020167679

It's triggered by the placeholder in the convert before this diff, which is consistent with it being tagUntaggedGoals. @Matthew Ballard checked that filling in the placeholder causes the error to go away.

Matthew Ballard (Mar 29 2023 at 01:52):

I also conveniently pushed my failure test case in addition to the success. The diff

Matthew Ballard (Mar 29 2023 at 02:07):

Naive question: https://github.com/leanprover/lean4/blob/8650804b025c9e69cd7f491eeb1ba988e6969367/src/Lean/Elab/Tactic/Match.lean#L31 also?

Last updated: Dec 20 2023 at 11:08 UTC