coq-breakpoints /

Filename Size Date modified Message
2.0 KB
5.9 KB
6.0 KB
        Coq breakpoints library.


  Big and complex functions sometimes appearing during
developement may contain bugs.  Proving their correctness
can be very hard, especially when Coq is used as a programming
language with rich types, not as proof assistant.

    What is suggested?

  This library allows one to prevent reduction of expressions
of interest.  This is achieved by wrapping them in so called
"breakpoints", either modifying source code of function or
"on fly".
  Then programmer can look at partial reduction's results, allow
reduction of some/all breakpoint(s), list present breakpoints,
watch at what these breakpoints are "waiting for"
(beta/delta/iota/zeta reduction), apply conversion tactic to
expression under some/all breakpoint(s).

    Why not <alternative>?

  Usual alternatives are:

  - debug with eyes, paper and pencil.  Hard for big functions
    and deep recursion.

  - add debug prints in extracted code.  Requires extraction
    and patching extracted sources manually.  Repeat when
    function's body is changed.

  - use "writer monad".  Programmer must change types, use monadic
    bind instead of some function applications, monadic return
    instead of simply returning function's value.  However this
    approach is useful when debug information should be present
    in extracted code.

  (know more?  Please tell me about them!)

    How it works?

  Internally breakpoint is represented as an opaque wrapper
containing expression.  Coq doesn't unfold breakpoints until
programmer won't tell him to do this.

  There are two modules, for named and for nameless breakpoints.
Names are not required sometimes, since they can clutter the
output.  However it's impossible to manipulate specific nameless
breakpoints, only "for all breakpoints" commands.

    How to use it?


        Require Import Breakpoints.

  Then, for named breakpoints:

        Import Named.
        Open Scope string_scope.  (* for convenience *)

  For nameless breakpoints:

        Import Nameless.


  (note: file "Bp_examples.v" contains examples on how to use
   these definitions/tactics.)

  This section contains documentation on both named and nameless
breakpoints.  Each description states on what kind of breakpoints
the definition/tactic is applicable.  Don't mix named breakpoints
with nameless ones.

  - DEBUG <expr>
      is an expression of sort Type, useful to start a debug
      session using vernacular 'Goal DEBUG <expr>.'
      ("Lemma somelemma : DEBUG <expr>." is fine too -- just
      enter the proof mode with breakpoints in the goal,
      "DEBUG" is just a convenience keyword.)

  - BREAK "name" <expr>
      for named breakpoints it is a wrapper for <expr> that
      won't be unfolded by Coq until 'pass "name".' or
      'pass_all.' (see below).

  - BREAK <expr>
      same as 'BREAK "name" <expr>', but for nameless breakpoints.

  Following commands can be used in proof mode:

  - breaks.
      for named breakpoints: lists breakpoints present in the
      current goal.
      for nameless breakpoints: shows presence/absence of
      breakpoints in the current goal.

  - waits.
      lists breakpoints and their positions in the goal:
      - "beta"
          breakpoint is an argument of some function
      - "delta"
          breakpoint is a function
      - "iota"
          breakpoint present in match construction as a
          "match_item" -- expression that will be "destructed"
          by "match"
      - "zeta"
          breakpoint is a right-hand side of some
          "let lhs := rhs in expr" expression

  - under_break "name" ltac:(fun e => eval <redexp> in e).
      reduces expression wrapped in breakpoint "name" with
      conversion tactic <redexp> (like "simpl", "cbv ..."
      and so on).

  - under_all_breaks ltac:(fun e => eval <redexp> in e).
      same as 'under_break "name" ...", but for all named

  - under_break ltac:(fun e => eval <redexp> in e).
      same as 'under_break "name" ...', but for nameless

  - pass-like commands:
      allow some/all breakpoints to be reduced by Coq:

      - pass "name".
          for breakpoint with name "name"

      - pass_all.
          for all breakpoints (named/nameless)

      - pass.
          for all nameless breakpoints

  - set_break "name" <expr>.
      sets named breakpoint "on fly".

  - set_break <expr>.
      sets nameless breakpoint "on fly".

      Finishes the debug session, allows one to store it for
      later debugging, with "Defined." / "Qed".

  Coq "conversion tactics" are very useful during debug
session, most notably "cbv" tactic which can be fine-tuned
to make Coq do only needed reductions.


  See the file "Bp_examples.v".

    Known bugs.

  Breakpoints that use fixpoint's arguments can't be manipulated:
they are not seen in "breaks", "waits", can't be "pass"'ed.

  Why?  Take a look at an example:

        Goal (fix f (x : nat) := id x) 1 = 1.
        match goal with
        | |- appcontext [@id] => idtac "works"
        | _ (* match failback *) => idtac "doesn't work"

  It's a Coq bug probably, it is already reported:

  vm_compute doesn't respect opacity of definitions:

  so one can't use breakpoints with vm_compute in useful manner.

  'waits.' won't show breakpoint in beta-position when there are
more than 12 arguments between function and breakpoints.  It can
be easily fixed, look at "waits_beta_loop" code in Breakpoints.v.
Why it happens?  Author doesn't know.  Take a look at discussion
in coq-club:


    - Dmitry Grebeniuk <>

    - Robbert Krebbers
    - AUGER C├ędric