Stream: Coq devs & plugin devs

Topic: ✔ debugging segfaults


view this post on Zulip Jason Gross (Feb 10 2022 at 17:47):

How do I get a backtrace when coqc segfaults?

view this post on Zulip Gaëtan Gilbert (Feb 10 2022 at 17:48):

run it in gdb

view this post on Zulip Jason Gross (Feb 10 2022 at 17:49):

backtrace is

#0  camlMicromega_plugin__Coq_micromega__xhyps_of_cone_4480 () at plugins/micromega/coq_micromega.ml:2144
#1  0x00007fffe715eee3 in camlMicromega_plugin__Coq_micromega__xhyps_of_cone_4480 () at plugins/micromega/coq_micromega.ml:2151
#2  0x00007fffe715eee3 in camlMicromega_plugin__Coq_micromega__xhyps_of_cone_4480 () at plugins/micromega/coq_micromega.ml:2151
#3  0x00007fffe715f05a in camlMicromega_plugin__Coq_micromega__xhyps_4499 () at plugins/micromega/coq_micromega.ml:2159
#4  0x00007fffe715c6a8 in camlMicromega_plugin__Coq_micromega__fun_7637 () at plugins/micromega/coq_micromega.ml:1724
#5  0x00005555560cd0cc in camlStdlib__list__fold_left_272 () at list.ml:121
#6  0x00007fffe715c595 in camlMicromega_plugin__Coq_micromega__micromega_tauto_3724 () at plugins/micromega/coq_micromega.ml:1715
#7  0x00007fffe715c7ba in camlMicromega_plugin__Coq_micromega__micromega_tauto_3762 () at plugins/micromega/coq_micromega.ml:1764
#8  0x00007fffe715cadb in camlMicromega_plugin__Coq_micromega__fun_7657 () at plugins/micromega/coq_micromega.ml:1804
#9  0x0000555555f36c51 in camlProofview__fun_5347 () at engine/proofview.ml:1120
#10 0x0000555555f2641f in camlLogic_monad__fun_910 () at engine/logic_monad.ml:192
#11 0x0000555555f271a7 in camlLogic_monad__fun_1111 () at engine/logic_monad.ml:260
#12 0x0000555555c09c2c in caml_apply2 ()
#13 0x0000555555f25aaa in camlLogic_monad__fun_823 () at engine/logic_monad.ml:67
#14 0x0000555555f25aaa in camlLogic_monad__fun_823 () at engine/logic_monad.ml:67
#15 0x0000555555f25aaa in camlLogic_monad__fun_823 () at engine/logic_monad.ml:67
#16 0x0000555555f26266 in camlLogic_monad__run_283 () at engine/logic_monad.ml:117
#17 0x0000555555f30a80 in camlProofview__apply_1565 () at engine/proofview.ml:236
#18 0x0000555555db379e in camlProof__run_tactic_1220 () at proofs/proof.ml:381
#19 0x0000555555db4472 in camlProof__solve_1463 () at proofs/proof.ml:490
#20 0x0000555555d00fad in camlComTactic__fun_734 () at vernac/comTactic.ml:46
#21 0x0000555555c93e03 in camlDeclare__map_fold_endline_4857 () at vernac/declare.ml:1447
#22 0x0000555555d00ef6 in camlComTactic__solve_core_263 () at vernac/comTactic.ml:43
#23 0x0000555555ce8410 in camlVernacextend__fun_3242 () at vernac/vernacextend.ml:163
#24 0x0000555555cfb4cc in camlVernacinterp__interp_typed_vernac_148 () at vernac/vernacinterp.ml:20
#25 0x0000555555cfc90a in camlVernacinterp__fun_1403 () at vernac/vernacinterp.ml:207
#26 0x000055555607a073 in camlFlags__with_modified_ref_inner_288 () at lib/flags.ml:17
#27 0x0000555555cfcfa3 in camlVernacinterp__fun_1519 () at vernac/vernacinterp.ml:257
#28 0x0000555555cfcef5 in camlVernacinterp__interp_gen_1073 () at vernac/vernacinterp.ml:255
#29 0x0000555555c28bd5 in camlStm__f_8889 () at stm/stm.ml:2169
#30 0x0000555555c28736 in camlStm__step_8821 () at stm/stm.ml:2111
#31 0x0000555555c21794 in camlStm__define_inner_10052 () at stm/stm.ml:964
#32 0x0000555555c28485 in camlStm__reach_inner_10921 () at stm/stm.ml:2320
#33 0x0000555555c2a519 in camlStm__observe_6900 () at stm/stm.ml:2421
#34 0x0000555555c0b453 in camlVernac__interp_vernac_233 () at toplevel/vernac.ml:68
#35 0x000055555607a073 in camlFlags__with_modified_ref_inner_288 () at lib/flags.ml:17
#36 0x0000555555c0ba64 in camlVernac__loop_442 () at lib/flags.ml:64
#37 0x0000555555c0b83b in camlVernac__load_vernac_core_262 () at toplevel/vernac.ml:116
#38 0x0000555555c0c022 in camlVernac__load_vernac_1169 () at toplevel/vernac.ml:172
#39 0x0000555555c0d02c in camlCcompile__compile_936 () at toplevel/ccompile.ml:146
#40 0x0000555555c0d4e3 in camlCcompile__compile_file_1144 () at toplevel/ccompile.ml:210
#41 0x0000555555c11f3a in camlCoqc__coqc_main_120 () at toplevel/coqc.ml:48
#42 0x0000555555c120c6 in camlCoqc__coqc_run_234 () at toplevel/coqc.ml:67
#43 0x0000555555c09c84 in camlDune__exe__Coqc_bin__entry () at toplevel/coqc.ml:90
#44 0x0000555555c01f89 in caml_program ()
#45 0x000055555616ac6c in caml_start_program ()
#46 0x000055555614737c in caml_startup_common (argv=0x7fffffffd938, pooling=<optimized out>, pooling@entry=0) at startup_nat.c:160
#47 0x00005555561473cf in caml_startup_exn (argv=<optimized out>) at startup_nat.c:165
#48 caml_startup (argv=<optimized out>) at startup_nat.c:170
#49 0x00005555561473f9 in caml_main (argv=<optimized out>) at startup_nat.c:177
#50 0x0000555555c00110 in main (argc=<optimized out>, argv=<optimized out>) at main.c:44

view this post on Zulip Jason Gross (Feb 10 2022 at 17:49):

I guess this is https://github.com/coq/coq/issues/15629

view this post on Zulip Notification Bot (Feb 10 2022 at 17:54):

Jason Gross has marked this topic as resolved.


Last updated: Feb 06 2023 at 18:03 UTC