Definition of User Interface?

• IDEs: Development Enviroments
• Analysis / Refactoring tools
• Code browsing / Documentation

Important Considerations:

• Data models.
• Data representation.
• Protocols.
• Communication channels.
• Maintenance / documentation.

The Read-Eval-Print-Loop

1. User inputs command.
2. Prover executes the command.
3. Prover prints results.
4. GOTO 1

The Edit-Check (Search) Cycle

User edits proof documents, continously.

Hales estimates that almost 50% of his time formalising the Jordan curve theorem and working on Flyspeck was spent looking up theorems in the HOL Light library.

Coq's User Interface API

A bit of (incomplete) history:

• Original Coq REPL ⇒ Terminal based, humans.
• Proof-General ⇒ Terminal based, regular expressions.
• PIDE / STM ⇒ Custom Protocols, XML-based.
• ? ⇒ ???? ????

It's all about the state

Typical REPL

let rec loop (st : state) =
  let cmd      = read ()     in
  let st', res = exec cmd st in
  print res; loop st'

Typical REPL with backtracing

let rec loop (sts : state list) =
  let cmd      = read ()       in
  let sts', res = exec cmd sts in
  print res; loop sts'

Many variations of this scheme

Doesn't work well for documents

Coq: Current Architecture

type st = Stateid.t
val parse_sentence : st -> parsable -> vernac_expr
val add : ontop:st -> ?newtip:st -> vernac_expr -> st
val edit_at : Stateid.t -> `NewTip | `Focus of focus
val observe : Stateid.t -> unit

Writing a New Coq Toplevel

1. Initialize the STM
2. ? ≡ you define interaction
3. Profit !

A Closer Look at the STM

type state = {
  system : States.state;       (* summary + libstack *)
  proof : Proof_global.state;  (* proof state *) }
type transaction =         type vernac_type =
  | Cmd    of cmd_t          | VtStartProof of vernac_start
  | Fork   of fork_t         | VtSideff of vernac_sideff_type
  | Qed    of qed_t          | VtQed of vernac_qed_type
  | Sideff of seff_t         | VtProofStep of proof_step
  | Alias  of alias_t        | VtProofMode of string
type vernac_when =           | VtQuery of report_with
  | VtNow                    | VtUnknown
  | VtLater
val process_transaction : ast -> vernac_type * when -> unit
val reach : Stateid.t -> unit

Where is the document?

Let's have a look