strange stack overflow when parsing(?) tactics

Stream: lean4

[Jakob von Raumer]

I have a command which takes in a block of tactic syntax which it runs on a certain sets on goals. I do this with the following line:

        let ⟨_, s⟩ ← (Tactic.evalTacticSeq termination { main := totMVars.get! 0, elaborator := Name.anonymous }).run { goals := totMVars }
        unless s.goals.length = 0 do throwError "tactic block didn't solve all goals"

where termination is the Syntax of the tactics. So far it always magically worked, that I get the goal view when I put the cursor among the tactics. Now the tactics still work as intended, but clicking anywhere among the tactic block gives me Stack overflow detected. Aborting. instead of an output. This just changes when I put set_option pp.all true. Then everything displays correctly. Any ideas on what's happening here?

[Jakob von Raumer]

Sometimes™ it also give me a bit of more helpful output:

[Error - 10:19:52] Request textDocument/documentHighlight failed.
  Message: Server process for file:///data1/jakob/iit/Examples/ConTy.lean crashed, likely due to a stack overflow in user code.
  Code: -32603

[Jakob von Raumer]

It's also strange that having

set_option pp.explicit true
set_option pp.universes true
set_option pp.notation false

doesn't help, only pp.all makes it work :confused:

[Sebastian Ullrich]

pp.analyze is already off? (defaults to off since 10/8)

[Jakob von Raumer]

Oh, that's the culprit, I think? It crashes when it's on

[Jakob von Raumer]

FWIW no matter the option, what's definitely not working anymore is the syntax highlighting, which did work with the June version

[Leonardo de Moura]

@Jakob von Raumer Could you please create an issue with a mwe?

[Jakob von Raumer]

I'll try, not so easy to separate it from the rest

[Leonardo de Moura]

@Jakob von Raumer Thanks a bunch!

[Sebastian Ullrich]

In particular, it only happened on hover/in the goal view, not at e.g. a done :scream:

[Jakob von Raumer]

The thing is, there are no overflows when I make the example smaller...

[Jakob von Raumer]

But then, the goals in totMVars aren't "broken", I can solve them...

[Jakob von Raumer]

#41852 0x00007f50f10facfe in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuick () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41853 0x00007f50f10fda5d in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41854 0x00007f50f10facfe in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuick () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41855 0x00007f50f10fda5d in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41856 0x00007f50f10facfe in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuick () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41857 0x00007f50f1123229 in l_Lean_Meta_isExprDefEqAuxImpl___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41858 0x00007f50f112beda in l_Lean_Meta_isExprDefEqAuxImpl___lambda__2 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41859 0x00007f50f1049257 in lean_is_expr_def_eq () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41860 0x00007f50f10625ee in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_checkTypesAndAssign () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41861 0x00007f50f10cdbad in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_process___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41862 0x00007f50f10d2eff in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_process () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41863 0x00007f50f10d3b27 in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41864 0x00007f50f10d5d40 in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41865 0x00007f50f10d97e9 in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_processAssignment_x27 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41866 0x00007f50f10ffcda in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther___lambda__2 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41867 0x00007f50f10ffa34 in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuickOther () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41868 0x00007f50f10facfe in l___private_Lean_Meta_ExprDefEq_0__Lean_Meta_isDefEqQuick () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41869 0x00007f50f11251f6 in l_Lean_Meta_isExprDefEqAuxImpl___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41870 0x00007f50f112beda in l_Lean_Meta_isExprDefEqAuxImpl___lambda__2 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41871 0x00007f50f1049257 in lean_is_expr_def_eq () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41872 0x00007f50f16846a5 in l_Lean_Meta_checkpointDefEq___at_Lean_Meta_isExprDefEq___spec__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41873 0x00007f50f16879ec in l_Lean_Meta_isExprDefEq () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41874 0x00007f50f22ac2c0 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_tryUnify () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41875 0x00007f50f22b1c68 in l_Std_Range_forIn_loop___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_canBottomUp___spec__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41876 0x00007f50f22b5140 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_canBottomUp___lambda__3 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41877 0x00007f50f22b71d4 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_canBottomUp___lambda__4 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41878 0x00007f50f22b32a3 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_canBottomUp () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41879 0x00007f50f22c92a0 in l_Std_Range_forIn_loop___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore_collectBottomUps___spec__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41880 0x00007f50f22cb6ff in l_List_forIn_loop___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore_collectBottomUps___spec__2 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41881 0x00007f50f22cc1d5 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore_collectBottomUps () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41882 0x00007f50f22f27a2 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyzeAppStagedCore () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41883 0x00007f50f22f17c2 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeAppStaged___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41884 0x00007f50f22f6011 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeAppStaged () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41885 0x00007f50f24f123a in lean_apply_7 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41886 0x00007f50f22b7774 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_withKnowing___rarg () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41887 0x00007f50f230a4a4 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeApp___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41888 0x00007f50f230ad78 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeApp___lambda__1___boxed () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41889 0x00007f50f24f4109 in lean_apply_9 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41890 0x00007f50f22ec05d in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeApp () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41891 0x00007f50f22e9e3b in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze___lambda__1 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41892 0x00007f50f22ee721 in l_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41893 0x00007f50f24f1a36 in lean_apply_7 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41894 0x00007f50f22e8799 in l_Lean_PrettyPrinter_Delaborator_SubExpr_descend___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze___spec__2 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41895 0x00007f50f24f280b in lean_apply_8 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41896 0x00007f50f24ef45a in lean_apply_6 () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41897 0x00007f50f1620321 in l___private_Lean_Meta_Basic_0__Lean_Meta_withNewFVar___rarg () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41898 0x00007f50f1620712 in l___private_Lean_Meta_Basic_0__Lean_Meta_withLocalDeclImp___rarg () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so
#41899 0x00007f50f22f06e8 in l_Lean_Meta_withLocalDecl___at_Lean_PrettyPrinter_Delaborator_TopDownAnalyze_analyze_analyzeLam___spec__3___rarg () from /home/javra2/.elan/toolchains/leanprover--lean4---nightly-2021-09-08/bin/../lib/lean/libleanshared.so

[Kevin Buzzard]

I can't comment about Lean 4, but for Lean 3 debugging even a gigantic #mwe is better than no mwe

[Jakob von Raumer]

Kevin Buzzard said:

I can't comment about Lean 4, but for Lean 3 debugging even a gigantic #mwe is better than no mwe

Well in that sense https://github.com/javra/iit/blob/main/Examples/ConTy.lean is a gigantic "M"NWE.

[Kevin Buzzard]

and how do I reproduce?

[Jakob von Raumer]

Load the file and put your cursor after e.g. the first repeat assumption

[Kevin Buzzard]

leanpkg print-paths` failed:

stderr:
configuring iit 0.1
no such file or directory (error code: 2)
  file: ./IIT/InfoviewBug.lean

[Jakob von Raumer]

fixed

[Kevin Buzzard]

yeah I can reproduce the stack overflow here

[Jakob von Raumer]

Sebastian helped me to get the above call, so it's definitely an issue of Lean.Meta.ExprDefEq.isDefEqQuick and Lean.Meta.ExprDefEq.isDefEqQuickOther looping. The lines above look like the first two.