Stream: Coq users

Topic: Debugging a hanging Definition


view this post on Zulip Raphael Sofaer (Feb 20 2024 at 13:51):

Hello,

I'm a Coq beginner currently trying out the InteractionTrees library, and I am having some difficulty. I have a Definition which hangs indefinitely (100% cpu and expanding memory) until it is killed. I believe this occurs in the process of trying to resolve implicit arguments.

Is there a way to enable debugging output which shows what Coq is doing in general during evaluation of a Gallina statement? Also, is there a way to specifically enable debugging output for what implicit argument Coq is trying to solve? I've found information about debugging in proofs and in Eval, but not in the context of Definition.

Thank you,
Raphael

My 'minimal' example right now is still 60 lines.
ImpHangDemo.v

view this post on Zulip Gaëtan Gilbert (Feb 20 2024 at 13:53):

I'm not sure what you call "resolve implicit arguments"
You can try Set Debug "unification". and Typeclasses eauto := debug.

view this post on Zulip Karl Palmskog (Feb 20 2024 at 13:56):

see here for an example of how this problem arises and can be addressed: https://github.com/damien-pous/coinduction/pull/14

TLDR: the root cause is missing Hint Mode declarations for InteractionTree typeclasses (cc: @Yannick Zakowski)

view this post on Zulip Karl Palmskog (Feb 20 2024 at 13:57):

(I can move this topic to the #Interaction Trees stream, but since the issue very general, it may fit best here)

view this post on Zulip Raphael Sofaer (Feb 20 2024 at 15:00):

Gaëtan Gilbert said:

I'm not sure what you call "resolve implicit arguments"
You can try Set Debug "unification". and Typeclasses eauto := debug.

Thank you for the suggestion. That gives helpful output.

@Karl Palmskog How would I figure out what Hint Mode declaration is missing?

I am currently looking at the following example, in which the Definition hangs because of a missing instance of RelDec for the string type:

(* This Imp language is from the InteractionTrees tutorial. *)
Require Import String.
From ITree Require Import ITree Events.MapDefault.
From ExtLib Require Import Structures.Monad
    Data.Map.FMapAList
    Structures.Maps.
Import Monads.
Import MonadNotation.
Local Open Scope monad_scope.
Local Open Scope string_scope.

Definition var : Set := string.
Definition value : Type := nat.

Inductive expr : Type :=
| Var (_ : var)
.

Inductive stmt : Type :=
| Assign (x: var) (e: expr) (* x = e *)
.

Variant ImpState : Type -> Type :=
| GetVar (x: var) : ImpState value
| SetVar (x : var) (v: value) : ImpState unit.

Section Denote.
  Context {eff : Type -> Type}.
  Context {HasImpState : ImpState -< eff}.

  Definition denote_expr (e : expr) : itree eff value :=
    match e with
    | Var v => trigger (GetVar v)
    end.

    (* Statements are distinct from expressions.  They don't return anything.
       Since they don't return anything, they give itree eff unit. *)
    Definition denote_imp (s: stmt) : itree eff unit :=
      match s with
      | Assign x e => v <- denote_expr e ;; trigger (SetVar x v)
      end.
End Denote.

Definition handle_ImpState {E: Type -> Type} `{mapE var 0 -< E}: ImpState ~> itree E :=
fun _ e =>
match e with
| GetVar x => lookup_def x
| SetVar x v => insert x v
end.

Definition env := alist var value.

(* From ExtLib Require Import Data.String. *)
Set Debug "unification".
(*Without Data.String this hangs*)
(* Alternately, this is the part of Data.String that fixes it *)
(* Require Import ExtLib.Core.RelDec.
Global Instance RelDec_string : RelDec (@eq string) :=
{| rel_dec := String.eqb |}. *)
Definition interp_imp {E A} (t: itree (ImpState +' E) A) : stateT env (itree E) A :=
  let t' := interp (bimap handle_ImpState (id_ E)) t in interp_map t'.

Definition eval_imp (s: stmt) : itree void1 (env * unit) :=
  interp_imp (denote_imp s) empty.

The problem is 'fixed' by uncommenting "From ExtLib Require Import Data.String. With Set Debug "unification" the following message is repeated:

[unification]
  ReaderMonad.readerT|ZApp(?S,
                           ReaderMonad.readerT ?S0
                             (ReaderMonad.readerT
                                ?S1
...
                                                 ?S19
                                                 (ReaderMonad.readerT ... ...)))))))))))))))))))),
                           A)
  itree|ZApp(mapE ?K ?d +' E, A)

With the "Data.String" require, I get the following output:

[unification] forall T : Type, ImpState T -> itree ?E0 T|
              ?C|ZApp(?a, ?c)

[unification] ?C0|ZApp(E, E)
              ?C|ZApp(?b, ?d)

[unification] ?C|ZApp(?bif ?a E, ?bif ?c E)
              forall T : Type, ?E T -> ?M T|

[unification] itree|ZApp(ImpState +' E, A)
              itree|ZApp(?E, ?T)

[unification] ?M|ZApp(A)
              itree|ZApp(mapE ?K ?d +' ?E0, ?T)

[unification] stateT|ZApp(?map, itree ?E0, ?T)
              stateT|ZApp(env, itree E, A)

[unification] itree|ZApp(?E0)
              itree|ZApp(E)

[unification] Heuristic:
              ?M A
              itree (mapE ?K ?d +' E) A

[unification]
  Heuristic:
  ?C (?bif ?a E) (?bif ?c E)
  forall T : Type, (ImpState +' E) T -> itree (mapE ?T ?y +' E) T

[unification] Heuristic:
              ?C0
              ?C

[unification] Heuristic:
              forall T : Type, ImpState T -> itree ?E T
              ?C ?a ?c

[unification] Heuristic:
              forall T : Type, ImpState T -> itree ?E T
              ?C ?a ?c

[unification]
  Heuristic:
  ?C (?bif ?a E) (?bif ?c E)
  forall T : Type, (ImpState +' E) T -> itree (mapE ?T ?y +' E) T

[unification] itree|ZApp(?E0, A)
              itree|ZApp(mapE ?K ?d +' E, A)

[unification]
  Handler|ZApp(?bif ?a E, ?bif ?c E)
  forall T : Type, (ImpState +' E) T -> itree (mapE ?T ?y +' E) T|

[unification]
  forall T : Type, ?bif ?a E T -> itree (?bif ?c E) T|
  forall T : Type, (ImpState +' E) T -> itree (mapE ?T ?y +' E) T|

[unification]
  ?bif ?a E T -> itree (?bif ?c E) T|
  (ImpState +' E) T -> itree (mapE ?T ?y +' E) T|

[unification] ?bif|ZApp(?a, E, T)
              sum1|ZApp(ImpState, E, T)

[unification] itree|ZApp(?bif ?c E, T)
              itree|ZApp(mapE ?T ?y +' E, T)

[unification] ?bif|ZApp(?c, E)
              sum1|ZApp(mapE ?T ?y, E)

[unification] forall T : Type, ImpState T -> itree ?E T|
              Handler|ZApp(?a, ?c)

[unification]
  forall T : Type, ImpState T -> itree ?E T|
  forall T : Type, ?a T -> itree ?c T|

[unification] ImpState T -> itree ?E T|
              ?a T -> itree ?c T|

[unification] ImpState|ZApp(T)
              ?a|ZApp(T)

[unification] itree|ZApp(?E, T)
              itree|ZApp(?c, T)

[unification] sum1|ZApp(?c, E)
              sum1|ZApp(mapE ?T ?y, E)

Typeclasses eauto := debug also gives helpful output which includes 7.1-1: no match for (RelDec.RelDec ?R), 0 possibilities, but then devolves into repeated:

4.1-1: no match for (Cat ?C), 2 possibilities
3.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2-1.2:

My question here is really, how do I tell what's missing? Look for that 'no match, 0 possibilities' in the Typeclasses eauto debug output?

Thanks again.

view this post on Zulip Karl Palmskog (Feb 20 2024 at 15:01):

unfortunately, figuring out the typeclass with the "missing" Hint Mode requires domain-specific knowledge of the library that I don't have. Perhaps @Yannick Zakowski or @Li-yao could weigh in.

view this post on Zulip Karl Palmskog (Feb 20 2024 at 15:35):

@Raphael Sofaer one thing to try is to prefix any definition that diverges with @ so the typeclass machinery doesn't run awry. For example, if you have Definition x := y arg you could try Definition x := @y arg. (and you might have to insert a bunch of _ between @y and arg to make it typecheck at all.

view this post on Zulip Raphael Sofaer (Feb 20 2024 at 16:43):

I ended up just changing the definition I was writing to use 'lower level' types from the library that were a little easier to understand. I think the problem had something to do with Cat_Handler but I seem to have bypassed it for now. Thank you!

view this post on Zulip Li-yao (Feb 20 2024 at 17:28):

Thanks for reporting this. I'm going to add a Hint Mode so that at least this doesn't keep looping.


Last updated: Jun 23 2024 at 05:02 UTC