Zulip Chat Archive
Stream: lean4
Topic: Nondeterminism during compilation
Henrik Böving (Mar 30 2022 at 23:38):
In my mathlib4 fork to port SlimCheck to Lean 4 I'm experiencing some weird issues, if I comment the following line out: https://github.com/hargoniX/mathlib4/blob/slim_check/Mathlib/Testing/SlimCheck/Testable.lean#L374 the LSP will sometimes hang on this and sometimes produce proper output (I reload the file with C-c C-d in emacs to achieve this effect), example:
successful run: image.png
hanging run: image.png
Lake and thus the compiler are rather consistently convinced this code is broken image.png so my question would be...what on earth is going on?
Mario Carneiro (Mar 30 2022 at 23:47):
It sounds like your random number generator is nondeterministic
Mario Carneiro (Mar 30 2022 at 23:48):
if the state is not being stored in the environment then this is expected
Mario Carneiro (Mar 30 2022 at 23:49):
that is, every time the command is elaborated you will get new random numbers
Henrik Böving (Mar 30 2022 at 23:52):
Pinning the randomSeed does indeed help the consistency so I guess I'll start to look around for where im doing too much recursion then
Mario Carneiro (Mar 30 2022 at 23:53):
recursion?
Henrik Böving (Mar 30 2022 at 23:53):
Well its complaining that there might be a stackoverflow during execution no?
Mario Carneiro (Mar 30 2022 at 23:54):
oh I see
Henrik Böving (Mar 30 2022 at 23:55):
I can in fact already pin point it to a certain instance from above that is misbehaving so I'll keep digging there, thanks!
Henrik Böving (Mar 31 2022 at 00:09):
Huh, I did include one of the failing seeds (Testable.check (∀ (x y z a : Nat) (h1 : 3 < x) (h2 : 3 < y), x - y = y - x) { Configuration.verbose with randomSeed := some 1000}) in a binary and it segfaulted
Henrik Böving (Mar 31 2022 at 00:09):
after running for a little at least
Henrik Böving (Mar 31 2022 at 00:10):
How does one debug segfaults in Lean generated code the best way?
Leonardo de Moura (Mar 31 2022 at 00:11):
I use gdb and then bt to print the stack trace.
Leonardo de Moura (Mar 31 2022 at 00:12):
The function names are mangled, but readable.
Henrik Böving (Mar 31 2022 at 00:13):
(gdb) bt
#0 0x00000000029a4d74 in lean_apply_1 ()
#1 0x00000000006ea373 in l_SlimCheck_TestResult_combine___rarg ()
#2 0x00000000006eb7cf in l_SlimCheck_TestResult_imp___rarg ()
#3 0x00000000006ebb9c in l_SlimCheck_TestResult_addInfo___rarg ()
#4 0x0000000000667feb in l_SlimCheck_Testable_runSuiteAux___at_main___spec__4___lambda__5 ()
#5 0x000000000066881e in l_SlimCheck_Testable_runSuiteAux___at_main___spec__4___lambda__6 ()
#6 0x0000000000668dd1 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__4___lambda__7 ()
#7 0x000000000066b2a7 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__2 ()
#8 0x000000000066bac9 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__3 ()
#9 0x00000000029a519c in lean_apply_1 ()
#10 0x00000000006fbbc1 in l_SlimCheck_retry___rarg ()
#11 0x000000000066bbb3 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 ()
#12 0x000000000066c21d in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 ()
#13 0x000000000066be01 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 ()
#14 0x000000000066c21d in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 ()
#15 0x000000000066be01 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 ()
#16 0x000000000066c21d in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 ()
#17 0x000000000066be01 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 ()
#18 0x000000000066c21d in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 ()
#19 0x000000000066be01 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 ()
#20 0x000000000066c21d in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 ()
#21 0x000000000066be01 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 ()
#22 0x000000000066c21d in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 ()
#23 0x000000000066c300 in l_SlimCheck_Testable_runSuite___at_main___spec__6 ()
#24 0x00000000029a4e80 in lean_apply_1 ()
#25 0x000000000077cf2e in l_IO_runRandWith___rarg ()
#26 0x000000000066c417 in l_SlimCheck_Testable_checkIO___at_main___spec__2 ()
#27 0x000000000066c471 in l_SlimCheck_Testable_check___at_main___spec__1 ()
#28 0x000000000066cb75 in _lean_main ()
#29 0x000000000066d77e in main ()
So apparently: https://github.com/hargoniX/mathlib4/blob/slim_check/Mathlib/Testing/SlimCheck/Testable.lean#L55 this one is evil...but only for certain inputs of course?
Leonardo de Moura (Mar 31 2022 at 00:14):
For "panic" messages, I use LEAN_ABORT_ON_PANIC=1 gdb <path-to-build-dir>/stage1/bin/lean, run file.lean, bt.
Henrik Böving (Mar 31 2022 at 00:18):
(gdb) list
693 {
694 lean_object* x_9; lean_object* x_10; lean_object* x_11;
695 x_9 = lean_ctor_get(x_2, 0);
696 lean_inc(x_9);
697 lean_dec(x_2);
698 x_10 = lean_apply_1(x_5, x_9);
699 x_11 = lean_alloc_ctor(1, 1, 0);
700 lean_ctor_set(x_11, 0, x_10);
701 return x_11;
702 }
(gdb) info locals
x_9 = 0x1
x_10 = 0x7ffff7bd80c8
x_11 = 0x7fffffffb580
x_5 = 0x1
x_6 = 1 '\001'
(gdb)
I'm certainly not well versed with how lean does stuff in C under the hood but applying 0x1 to 0x1 does not sound like something that should be happening right? (line 698 is the line that is the exit point according to a build with debug info)
Leonardo de Moura (Mar 31 2022 at 00:21):
combine looks harmless. Try to take a look at the other functions on the stack. dbg_trace is also helpful in this kind situation.
Leonardo de Moura (Mar 31 2022 at 00:22):
I'm certainly not well versed with how lean does stuff in C under the hood but applying 0x1 to 0x1 does not sound like something that should be happening right?
Yes, the memory looks corrupted at this point.
Henrik Böving (Mar 31 2022 at 00:27):
Here's the trace with debug info so one can see the arguments...it seems like this 0x1 value is first introduced in the call from #8 to #7?
#0 0x00000000029922b4 in lean_apply_1 ()
#1 0x00000000006e4a53 in l_SlimCheck_TestResult_combine___rarg (x_1=0x7ffff7bd80c8, x_2=0x7ffff7bd8118) at ./../mathlib4/./build/ir/Mathlib/Testing/SlimCheck/Testable.c:698
#2 0x00000000006e5dcf in l_SlimCheck_TestResult_imp___rarg (x_1=0x7ffff7bd8108, x_2=0x7ffff7bd80c8) at ./../mathlib4/./build/ir/Mathlib/Testing/SlimCheck/Testable.c:1166
#3 0x00000000006e619c in l_SlimCheck_TestResult_addInfo___rarg (x_1=0x7ffff7bdf178, x_2=0x1, x_3=0x7ffff7bd8108, x_4=0x7ffff7bd80c8) at ./../mathlib4/./build/ir/Mathlib/Testing/SlimCheck/Testable.c:1283
#4 0x0000000000664e9b in l_SlimCheck_Testable_runSuiteAux___at_main___spec__4___lambda__5 (x_1=1 '\001', x_2=0x7ffff7bef268, x_3=0xb, x_4=0xb, x_5=0x1, x_6=0xb, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:921
#5 0x00000000006656ce in l_SlimCheck_Testable_runSuiteAux___at_main___spec__4___lambda__6 (x_1=1 '\001', x_2=0x7ffff7bef268, x_3=0xb, x_4=0xb, x_5=0x1, x_6=0xb, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:1093
#6 0x0000000000665c81 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__4___lambda__7 (x_1=0x7ffff7bef238, x_2=0xb, x_3=0x7ffff7bef268, x_4=0x7ffff7a6c5d8, x_5=0xb, x_6=0x1, x_7=0xb, x_8=0x7ffff7a6c5f0) at ./build/ir/Main.c:1234
#7 0x0000000000668157 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__2 (x_1=0x7ffff7bef238, x_2=0xb, x_3=0x7ffff7bef268, x_4=0x1, x_5=0xb, x_6=0x7ffff7a6c5f0) at ./build/ir/Main.c:2004
#8 0x0000000000668979 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__3 (x_1=0x7ffff7bef238, x_2=0xb, x_3=0x7ffff7bef268, x_4=0x7ffff7a6c5f0) at ./build/ir/Main.c:2159
#9 0x00000000029926dc in lean_apply_1 ()
#10 0x00000000006f60b1 in l_SlimCheck_retry___rarg (x_1=0x7ffff7bef208, x_2=0x7ffff7bef268, x_3=0x7, x_4=0x7ffff7a6c5f0) at ./../mathlib4/./build/ir/Mathlib/Testing/SlimCheck/Testable.c:7552
#11 0x0000000000668a63 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 (x_1=0x7ffff7bef238, x_2=0xb, x_3=0x7ffff7bef268, x_4=0x7ffff7bd80d8, x_5=0xbd, x_6=0x1, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:2176
#12 0x00000000006690cd in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7bd80d8, x_4=0xbf, x_5=0x7ffff7a6c5f0) at ./build/ir/Main.c:2324
#13 0x0000000000668cb1 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 (x_1=0x7ffff7bef238, x_2=0x9, x_3=0x7ffff7bef268, x_4=0x7ffff7bd80d8, x_5=0xbf, x_6=0x1, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:2235
#14 0x00000000006690cd in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7bd80d8, x_4=0xc1, x_5=0x7ffff7a6c5f0) at ./build/ir/Main.c:2324
#15 0x0000000000668cb1 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 (x_1=0x7ffff7bef238, x_2=0x7, x_3=0x7ffff7bef268, x_4=0x7ffff7bd80d8, x_5=0xc1, x_6=0x1, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:2235
#16 0x00000000006690cd in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7bd80d8, x_4=0xc3, x_5=0x7ffff7a6c5f0) at ./build/ir/Main.c:2324
#17 0x0000000000668cb1 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 (x_1=0x7ffff7bef238, x_2=0x5, x_3=0x7ffff7bef268, x_4=0x7ffff7bd80d8, x_5=0xc3, x_6=0x1, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:2235
#18 0x00000000006690cd in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7bd80d8, x_4=0xc5, x_5=0x7ffff7a6c5f0) at ./build/ir/Main.c:2324
#19 0x0000000000668cb1 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 (x_1=0x7ffff7bef238, x_2=0x3, x_3=0x7ffff7bef268, x_4=0x7ffff7bd80d8, x_5=0xc5, x_6=0x1, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:2235
#20 0x00000000006690cd in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7bd80d8, x_4=0xc7, x_5=0x7ffff7a6c5f0) at ./build/ir/Main.c:2324
#21 0x0000000000668cb1 in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7___lambda__4 (x_1=0x7ffff7bef238, x_2=0x1, x_3=0x7ffff7bef268, x_4=0x7ffff7bd80f8, x_5=0xc7, x_6=0x1, x_7=0x7ffff7a6c5f0) at ./build/ir/Main.c:2235
#22 0x00000000006690cd in l_SlimCheck_Testable_runSuiteAux___at_main___spec__7 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7bd80f8, x_4=0xc9, x_5=0x7ffff7a6c5f0) at ./build/ir/Main.c:2324
#23 0x00000000006691b0 in l_SlimCheck_Testable_runSuite___at_main___spec__6 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x7ffff7a6c5f0) at ./build/ir/Main.c:2349
#24 0x00000000029923c0 in lean_apply_1 ()
#25 0x0000000000771d9e in l_IO_runRandWith___rarg (x_1=0x7d1, x_2=0x7ffff7bf1000, x_3=0x1) at ./../mathlib4/./build/ir/Mathlib/Control/Random.c:835
#26 0x00000000006692c7 in l_SlimCheck_Testable_checkIO___at_main___spec__2 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x1) at ./build/ir/Main.c:2377
#27 0x0000000000669321 in l_SlimCheck_Testable_check___at_main___spec__1 (x_1=0x7ffff7bef238, x_2=0x7ffff7bef268, x_3=0x1) at ./build/ir/Main.c:2420
#28 0x00000000006699e5 in _lean_main (x_1=0x1) at ./build/ir/Main.c:2673
#29 0x000000000066a5ee in main (argc=1, argv=0x7fffffffd638) at ./build/ir/Main.c:2948
so that might be the culprit?
Henrik Böving (Mar 31 2022 at 00:33):
Either way I'm off to bed, if someone wants to investigate further there is a reproducible example over here: https://github.com/hargoniX/lean4-c-bug, maybe I will just wake up and it will be magically fixed :sparkles:
Leonardo de Moura (Mar 31 2022 at 01:10):
@Henrik Böving The problem is that PSum can store data and proofs. Recall that proofs are erased by the code generator. This is where the 0x1 is coming from. An easy fix is to modify apply_* to check its arguments have been erased, but this would impact the performance of all Lean programs that never need this feature. A better fix is to have two sets of apply_* functions: the current one; and another for places that can take proofs and data (e.g., your combine function). We don't have cycles for this kind of modification right now. So, could you please rewrite your code and replace PSum with a type such as
inductive Semidecidable (p : Prop) where
| isTrue (h : p)
| unknown
This one would be making clear to Lean that the argument stored there is always a proof. You could also try to rewrite combine as
def combine {p q : Prop} : PSum Unit (p → q) → PSum Unit p → PSum Unit q
| PSum.inr f, PSum.inr proof => PSum.inr $ f proof
| _, _ => PSum.inl ()
In your current implementation, p and q can be any type.
I did not read your code carefully. So, you might have other places where the code can be used to process proofs and data.
BTW, I think it is worth replacing PSum because it will make the code more readable.
Leonardo de Moura (Mar 31 2022 at 01:20):
Here is a mwe for this issue
def combine : PSum Unit (p → q) → PSum Unit p → PSum Unit q
| PSum.inr f, PSum.inr proof => PSum.inr $ f proof
| _, _ => PSum.inl ()
def tst : String :=
let f : PSum Unit (True → True) := .inr id
let v : PSum Unit True := .inr .intro
match combine f v with
| .inr _ => "inr"
| .inl _ => "inl"
#evat tst
The crash goes away if add {p q : Prop} to combine. Example:
def combine {p q : Prop} : PSum Unit (p → q) → PSum Unit p → PSum Unit q
| PSum.inr f, PSum.inr proof => PSum.inr $ f proof
| _, _ => PSum.inl ()
Leonardo de Moura (Mar 31 2022 at 01:28):
Added an issue for this https://github.com/leanprover/lean4/issues/1087
Leonardo de Moura (Mar 31 2022 at 01:50):
I pushed the "easy" fix for the issue above. I am hoping the performance impact will be small.
Henrik Böving (Mar 31 2022 at 07:51):
It did indeed get magically fixed^^ But the explanation very much makes sense yes, I'll just keep it like combine {p q : Prop} to make this explicit
Last updated: Dec 20 2023 at 11:08 UTC