Bring IDEs to the browsers?
Enrich documents with provers!

Outline JsCoq @github

1. JsCoq Story
2. Demos
3. Inside JsCoq
4. Protocols
5. Conclusion and Future Work

Some Context

1. The initial experiment.
   Using Coq for audio DSL Faust development (ANR FEEVER).
   Compiling Coq to JavaScript.
2. Viability!
   It worked! What do we do now?
3. First functional prototype.
   Public release: where to go now?
4. Second generation and protocol.
   The SerAPI protocol is born.
5. Third generation, beyond JsCoq.
   Who knows?

Browser Platforms and js_of_ocaml

Coq ~ 200.000 lines of OCaml code (with some C)

js_of_ocaml: OCaml bytecode to JavaScript compiler

Will it work?

What Can Jscoq Bring to ITP?

The status:

• Hard awkward interfaces and platforms (emacs).
• Highly non-standard protocols and formats.
• Problems with distribution, high abandonware ratio ("Try to run a Coq development older than...").
• Interfaces not appealing to students: low coolness factor for the Youtube Epoch.
• Literate programming widely used but poorly supported.
• Few alternatives: Edukera, non-free, others...
• Online tools that interface with a server (security hell, state issues, protocols, etc.).

JsCoq is Born

A Serverless, Opinionated Project

... targeting an existing user base, while developing proper foundations.

HTML5, as the future of UI, excellent support for interaction.

What we "didn't" want to do:

1. Fork Coq.
2. Invent anything.
3. Look like an IDE.
4. Write code or user interfaces.
5. Deal with protocols.

... and yet, we've done a bit of all of the above.

Brief Demo Time!

You can try it yourself!

• Demo I (the infinitude of primes)
• Demo II (collacoq)
• Demo III (Software Foundations)
• Demo IV (DFT)
• Demo V (Mathematical Components)

More developments supported, but all looking similar (expected to change, with more advanced media).

This is Work-in-Progress™

How Does it Work?

Four modular components:

The Document Provider

Document extraction:

• Code Providers (user-selected), such as editor widgets, textareas, ... yielding a stream of Coq sentences.
  May query the prover.
• CodeMirror, our smart provider of choice (key to success).

Document-level model:

• Provider Containers, presenting a set of Code Providers as a single document (with focus management invalidation, next/previous).
• Delegation, where Provider Containers talk to the manager on behalf of the providers.

The Document Manager

Responsible of communication with the prover-level model.

• Main Task: keep coherence between the two models.
• Written in ES2015 JavaScript, with minimal OCaml help.
• Becomes thinner as Coq's view of the world is improved (current size ~ 500 JS lines)
• Should work with different providers/panels.

The Panel

• Prover-related UI (note the difference with Code Providers).
• Designed to wrap over an existing document.
• Responsible to interpret "lateral" prover data, i.e., search results, configuration parameter, goals...
• Usually queries the prover for data.
• New panel in progress, using Jupyter JS UI.

What About the Coq Part?

Notes on the first prototype:

• Non-standard enviroment (with its own toplevel).
• Use of Coq 100% as an OCaml library, with no protocol.
• At that stage, most of the related work didn't apply.
• Strong focus on "real-world" examples, e.g., libraries (with small package manager).
• Low-level access enabled experiments that would shape future directions.
• Interaction with the JS side required some kind of encoding or protocol.

Related Work

PIDE, Coq XML protocol (main contenders):

• Mundane data encoding and serialization, a significant part of papers.
• Much worse code-wise!
• Choice of format embedded in the code.
• Impedance problems.
• Example use case: check if the current goal is an application.

Idea: use metaprogramming and automate.

Serialization

Promising initial experiments with PPX!

... but what about the real case?

Large scale serialization: SerAPI was born!

type vernac_expr =
  [%import: Vernacexpr.vernac_expr]
  [@@deriving sexp yojson]

val vernac_expr_of_sexp : Sexp.t -> vernac_expr
val sexp_of_vernac_expr : vernac_expr -> Sexp.t
val vernac_exp_to_yojson : vernac_expr -> json
val vernac_exp_of_yojson : json ->
                        (vernac_expr, string) Result.result 

Automatic canonical schema (328 Coq datatypes serialized).

Towards a New Protocol

OCaml limitations:

• Serialization for data; what for RPC?
• Favor direct export of the OCaml API.
• How to take profit of the serialization technology?

Solution: Export the API as a small DSL

• Available methods as a datatype, with a small intepreter for execution.
• Basic RPC over many channels.
• Reasonable introspection/reflection enabled.

A (brief) Visit to the Protocol Zoo

• Coq-STM: Initial OCaml API for JsCoq, influenced from PIDE. Calls to add, edit, and execute statements. Doc level low. Initial base for SerAPI.
• Coq-XML: A non-exact encoding of the STM API. Issues with usability and features. Doc level low.
• PIDE: Private API to Isabelle. Two Coq implementations. Seemed quite complex and advanced for our goals. Adequacy for some Coq use cases?

Evolving the STM API

The first steps of SerAPI:

• Addressing some usability goals, which gathered some interest.
• Need to introduce some modifications to the way the STM API works.
• (From the JsCoq point of view) Lack of a systematic data-query API.
• (From the UI point of view) Clément Pit-Claudel's suggestions to the control protocol.

An evolved protocol appeared.

The SerAPI Protocol

Assumptions: Reliable, order-preserving, fully-asynchronous channels.

Goals: Lightweight, document-oriented, asynchronous, lock-free.

Modularity: Control Protocol, Query Protocol, Parsing Protocol.

Advanced Features: Whole document parsing, concurrent editing, rich layout.

The SerAPI Control Protocol

Simplified version

type jscoq_cmd =
  | Add     of stateid * stateid * string
  | Cancel  of stateid
  | Exec    of stateid
  | SetOpt  of bool option * string list * gvalue
  | GetOpt  of string list
  | ...
type jscoq_answer =
  | Message   of stateid * level * richpp
  | ParseInfo of stateid * loc
  | Cancelled of stateid list
  | Processed of stateid
      

Click for the GitHub version

The SerAPI Query Protocol

Non-final version

type query_opt =
{ preds   : query_pred sexp_list;
  limit   : int sexp_option;
  stateid : Stateid.t [@default Stm.get_current_state()];
  pp      : print_opt [@default
            { pp_format=PpSexp; pp_depth=0; pp_elide="..." }];
}
type query_cmd =
  | Option
  | Goals
  | Ast
  | ...
type coq_object =
  | CoqRich of Richpp.richpp
  | CoqAst  of Loc.t * Vernacexpr.vernac_expr
  | CoqGoal of (constr * (idlist * constr option * constr) list) Proof.pre_goals

Click for the GitHub version

SerAPI Interfaces

Web Worker:

• A self-contained generic Coq Web Worker.
• Serialization to JSON.
• Size ~ 3 MiB, time to load < 1 sec, libraries between 3 and 300 MiB (lots of space for Coq modules).

• Unix style.
• For machine use, but human-friendly
• Serialization to S-EXPs.
• Advanced uses, such as full asynchronous support, native code performance.

JsCoq as a Coq Memory Profiler

JsCoq as a Coq CPU Profiler

Conclusion and Future Work

JsCoq/SerAPI@github

• Usable state, 1.0 release expected soon.
• UI work needed.
• More than 1000 users (ballpark estimate), 4 courses.
• udoc, a replacement for coqdoc.
• Other clients: elcoq / ProofGeneral by Clément Pit-Claudel; PeaCoq by Valentin Robert; CoqIDE; Jupyter.

Coq Upstream Changes

• STM.
• Print model, closer to HTML, client-side reflowing (CEP009)