Run the Coq Proof Assistant in your browser!
jsCoq is an Online Integrated Development Environment for the Coq proof assistant and runs in your browser! We aim to enable new UI/interaction possibilities and to improve the accessibility of the Coq platform itself. Current stable version is jsCoq v8.11+0.11.0 supporting Coq 8.11.1, try it:
jsCoq is written to conform to ES2017, any recent standardcompliant browser. No servers or external programs are needed. See the Troubleshooting section if you have problems.
jsCoq is communitydeveloped by a team of contributors.
Are you a jsCoq user?
Have you developed or taught a course using jsCoq? Do you have some feedback for us?
If so, please submit a pull request or an issue so we can add your lectures to the list of jsCoq users. This is essential to guarantee future funding of the project.
Basic Usage
The main page showcases jsCoq by walking through a proof for the infinitude of primes using mathcomp
, due to Georges Gonthier.
Once jsCoq finishes loading, you can step through the proof using the arrow buttons on the toolbar (top right), or using these keyboard shortcuts:
Shortcut  Action 

AltN or Alt↓  Go to next 
AltP or Alt↑  Go to previous 
AltEnter or Alt→  Go to cursor 
You can open a blank editor and experiment with your own Coq developments using the scratchpad. The same keyboard shortcuts apply here.
The scratchpad's contents are saved in your browser's local storage (IndexedDB, specifically), so they are not lost if you close the browser window or refresh the page. You can, in fact, store more than one document using the local open/save file dialogs:
Shortcut  Action 

CtrlS  Save file (with the last name provided, or untitled.v ) 
CtrlShiftS  Save file as (prompts for file name) 
CtrlAltS  Save file to disk (using the browser's Save dialog, or preset destination) 
CtrlO  Open file (prompts for file name, supports tab completion) 
CtrlAltO  Open file from disk (using the browser's Open dialog) 
On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.
How to build your own jsCoq documents
See the dedicated page for information on advanced options and jsCoq HTML embedding API. A quick setup can be done with:
$ npm install jscoq
then copy and adapt the template page page to your needs.
For a more detailed tutorial and information, refer to docs/embedding.md.
Collacoq
A small pastebinlike server based on haste is available at https://x80.org/collacoq. Note that this service is experimental, data loss is guaranteed as we don't backup the server.
The haste
branch we use is available at https://github.com/ejgallego/hasteserver/tree/collacoq Help with Collacoq is very welcome!
Contributing and Developer Information
See the dedicated page for developer information as well as links to past versions and tools.
This is a betastatus project, but any contribution or comment is really welcome! See the contributing guide for more information.
Publications
See the dedicated file
Examples
The main page includes a proof of the infinitude of primes by G. Gonthier. We provide some more examples as a showcase of the tool:

The Logical Foundations suite:

dft.v: https://x80.org/rhinocoq/v8.11/examples/dft.html
A small development of the theory of the Fourier Transform following Julius Orion Smith III's "The Mathematics of the Discrete Fourier Transform"

equations: https://x80.org/rhinocoq/v8.11/examples/equations_intro.htmla
Introduction to the Coq Equations package from the official documentation.

Stlc: The "Simply Typed Lambda Calculus" chapter from Software Foundations by Benjamin Pierce et al:

Mike's Nahas Tutorial: https://corwinofamber.github.io/jscoq/tut/nahas/nahas_tutorial.html
Outdated examples [but still working]

The IRIS program logic, by Robbert Krebbers et al.

Mtac: The Mtac tutorial by Beta Zilliani:

StackMachine: The First chapter of the book "Certified Programming with Dependent Types" by Adam Chlipala:
https://x80.org/rhinocoq/v8.5/examples/Cpdt.StackMachine.html

MirrorCore:

A simple demo: https://x80.org/rhinocoq/v8.5/examples/mirrorcore.html

A demo of developing a cancellation algorithm for commutative monoids: https://x80.org/rhinocoq/v8.5/examples/mirrorcorertacdemo.html

jsCoq Users:
Incomplete list of places where jsCoq has been used:
 Coq Winter School 2016: “Advanced Software Verification And Computer Proof”. Sophia Antipolis https://team.inria.fr/marelle/en/advancedcoqwinterschool2016/
 Coq Winter School 20162017 (SSReflect & MathComp) “Advanced Software Verification And Computer Proof”. Sophia Antipolis https://team.inria.fr/marelle/en/advancedcoqwinterschool20162017/
 Mathematical Components, an Introduction, Satellite workshop of the ITP 2016 conference, August 27th, Nancy, France https://github.com/mathcomp/wiki/wiki/tutorialitp2016
 Several examples of the "Mathematical Components Book" https://mathcomp.github.io/mcb/
 School on "Preuves et Programmes" at l'École de Mines https://wwwsop.inria.fr/marelle/mines/
 Mini Corso di Coq a Pavoda: http://wwwsop.inria.fr/members/Enrico.Tassi/padova2017/
 Elpi Tutorial / Demo at CoqPL 2017 Los Angeles https://lpcic.github.io/coqelpiwww/tutorialdemo_CoqPL2018.html
 Coq Winter School 20172018 (SSReflect & MathComp) Sophia Antipolis https://team.inria.fr/marelle/en/coqwinterschool20172018ssreflectmathcomp/
 Lectures at the "Journées Nationales du Calcul Formel" by Assia Mahboubi: https://specfun.inria.fr/amahboub/Jncf18/cours2.html
 Types Summer School: http://wwwsop.inria.fr/teams/marelle/types18/
 Coq Winter School 20182019 (SSReflect & MathComp) https://team.inria.fr/marelle/en/coqwinterschool20182019ssreflectmathcomp/
 CASS 2020, Coq Andes Summer School https://cass.pleiad.cl/
 Lectures on Separation Logic by JeanMarie Madiot in MPRI's course "Proofs of programs", using Arthur Charguéraud's material. See it in action!
jsCoq in the press
 http://www.minesparistech.fr/Actualites/jsCoqouCoqdansunnavigateur/2118
 https://news.ycombinator.com/item?id=9836900
Addon Packages:
One of jsCoq's strengths is its support for bundling addon packages. In order to add your Coq package to jsCoq, you need to add a definition file in the coqaddons
repository. We recommend you use one of the existing files as a model.
Also, you need to define a jsCoq package by editing the coqjslib/dftlibs.ml
file. Once that is done, call make jscoq
again.
Troubleshooting
Are you getting a StackOverflow
exception? Unfortunately these are hard to fix; you may be stuck with them for a while.
 Clearing the browser cache usually solves lots of issues.
 Change browser, if using Firefox try Chrome, if using Chrome try Firefox.
Reporting Bugs
Feel free to use the issue tracker. Please include your browser/OS/useragent and command line options.
Contact and online help

jsCoq's gitter: main developer chat

The jsCoq mailing list: https://x80.org/cgibin/mailman/listinfo/jscoq
The list archives should be also available through Gmane at group:
gmane.science.mathematics.logic.coq.jscoq
you can post to the list using nntp. 
Coq's discourse [use the jscoq tag] https://coq.discourse.group/

StackOverflow [use the jscoq tag] https://stackoverflow.com/
What is broken
 Loading ML modules is slow.
 Loading
.vo
files is slow.  There surely are threading and performance problems.
vm_compute
andnative_compute
fall back to regularcompute
.
Documents
See the etc/notes/
directory for some random notes about the project.
Credits
Core developer team
 Emilio Jesús Gallego Arias , Inria, Université de Paris, IRIF
 Shachar Itzhaky , Technion
Past Contributors
 Benoît Pin, CRI, MINES ParisTech
Acknowledgements
jsCoq was made possible thanks to funding by the FEEVER project and support from MINES ParisTech
We want to strongly thank the js_of_ocaml
developers. Without their great and quick support jsCoq wouldn't have been possible.
CodeMirror has played a crucial role in the project, we are very happy with it, thanks a lot!
Please consider supporting the development of CodeMirror with a donation.