Zulip Chat Archive

Stream: general

Topic: how to debug a server crash?


Eric Rodriguez (Apr 04 2021 at 12:11):

For some reason, cc crashes the server, but when I try lean --make, it's fine! From a little look, I can't find any server logs -- are there any anywhere?

For reference, the crashing code:

import combinatorics.simple_graph.basic

variables {α: Type*} (G : simple_graph α)

structure my_struct :=
(f : α  α)
(f_pred:  a b : α, ¬G.adj a b  f a = f b)

def my_instance (hg : my_struct G) (H : simple_graph α)
  (h :  a b : α, G.adj a b  H.adj a b) : my_struct H :=
{
  f := hg.f,
  f_pred := λ a b nadj, begin
    have := hg.f_pred a b, --cc
    -- uncomment `cc` to see a crash
    -- (I was fooling around to see what would finish this by modus tollens)
  end
}

Eric Rodriguez (Apr 04 2021 at 12:11):

I found this with the same error code (3221225477), but it seems to be a different issue as it was supposedly resolved


Last updated: Dec 20 2023 at 11:08 UTC