• Ltac: Where did my idtac debug output go?

    When debugging Ltac tactics in Coq, one can use idtac to print debug messages. However, when a tactic invocation fails, ProofGeneral will not display any of the debug output in the *response* buffer, so in order to read our debug output, we have to read the *coq* buffer or precede the failing command with Fail.

    Read on →

  • Default inlinings of Coq Extraction

    While working with Coq’s JSON extraction, Thomas and I were quite puzzled when the AST generated by extraction did not match the original Gallina syntax: Some functions were silently unfolded, even though we never told Coq to do so. With Tej’s help, we figured out what’s going on, and after some thinking, it all started to make sense.

    Read on →

  • A quick hack to ask any SMT solver if my Coq goal is true

    This is (roughly) the transcript of a 5 minute lightning talk I gave at the DeepSpec workshop at PLDI’18.

    Read on →

  • Coq's Search command and other tricks

    Between 2014 and 2016, I was using Coq regularly, but did not know that its Search command accepts patterns. If only I had learnt this earlier, this would have saved me so much time!

    Read on →

  • A non-technical reminder to my future self

    If you ever hesitate whether you should buy a crazy expensive trans-atlantic plane ticket, shift your biological clock by 6 hours for just a three day stay, miss a meeting of your research group and reschedule another one:

    Read on →