Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

jscoq/jscoq

A port of Coq to Javascript -- Run Coq in your Browser
Source code at GitHub https://jscoq.github.io
jscoq/jscoq.json
{
  "createdAt": "2015-05-12T20:29:34Z",
  "defaultBranch": "v8.20",
  "description": "A port of Coq to Javascript -- Run Coq in your Browser",
  "fullName": "jscoq/jscoq",
  "homepage": "https://jscoq.github.io",
  "language": "TypeScript",
  "name": "jscoq",
  "pushedAt": "2025-11-21T15:35:50Z",
  "stargazersCount": 535,
  "topics": [
    "coq",
    "integrated-development-environment",
    "javascript",
    "proof-assistant"
  ],
  "updatedAt": "2025-11-21T15:35:54Z",
  "url": "https://github.com/jscoq/jscoq"
}

Run the Coq Proof Assistant in your browser!

Section titled “Run the Coq Proof Assistant in your browser!”

Build Status

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.

The current stable version is jsCoq 0.17.1 supporting Coq 8.17.1, try it:

https://coq.vercel.app

The easiest way to use jsCoq 0.17.1 for your classes is to use our coqdoc template.

Don’t hesitate to get in touch with us at the jsCoq’s Zulip Room for any question or help request you may have.

jsCoq is written to conform to ES2017; any recent standard-compliant browser should be able to run it. No servers or external programs are needed. See the [Troubleshooting]!(#Troubleshooting) section if you have problems.

jsCoq is community-developed by a [team of contributors]!(#Credits). We are in need of help, in particular with documentation, funding, and fine tuning the project, see the [contributing]!(#Contributing-and-Developer-Information) section for more information.

Development version

Section titled “Development version”

The current development version is jsCoq 1.99.1, targeting Coq 8.17 to Coq 8.21. The current development version is based on the new Flèche document manager and has significant changes. If you are interested in helping with this effort, please get in touch with us.

Contributing and Developer Information

Section titled “Contributing and Developer Information”

See our [contributing guide]!(CONTRIBUTING.md) for more information.

The jsCoq is in need of funding, as of today, it is fully run by unpaid volunteers. If you think you could help with funding, don’t hesitate to get in touch with us.

Are you a jsCoq user? Let us know!

Section titled “Are you a jsCoq user? Let us know!”

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]!(#jsCoq-Users). This is essential to guarantee future funding of the project.

Basic Usage

Section titled “Basic Usage”

The main page showcases jsCoq with a variety of proofs, available from the Examples drop-down menu.

Once jsCoq finishes loading, you can step through the proof using the arrow buttons on the toolbar (top right), or using these keyboard shortcuts:

ShortcutAction
Alt-N or Alt-↓Go to next
Alt-P or Alt-↑Go to previous
Alt-Enter 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:

ShortcutAction
Ctrl-SSave file (with the last name provided, or untitled.v)
Ctrl-Shift-SSave file as (prompts for file name; also has options to download or share the content)
Ctrl-Alt-SSave file to disk (using the browser’s Save dialog, or preset destination)
Ctrl-OOpen file (prompts for file name, supports tab completion)
Ctrl-Alt-OOpen file from disk (using the browser’s Open dialog)

On Mac, replace Ctrl with ⌘ (command) and Alt with ⌥ (option), as is traditional.

Drag .v files from your local drive onto the scratchpad to open them. You can also drag multiple files, which will open up a project pane to the left of the editor, allowing you to switch between them; this functionality is still experimental.

Sharing your development

Section titled “Sharing your development”

A small pastebin-like server based on Hastebin is available for sharing .v files between users. Open the save dialog (Ctrl-Shift-S) and click “Share”; then share the URL from your browser’s location bar with anyone you like. The URL represents the state of the document at the moment it was shared, and this state is read-only. Every time you click “Share”, a fresh URL is generated. Shared content is not saved forever, though; documents are typically available for a period of ~30 days.

How to build your own jsCoq documents

Section titled “How to build your own jsCoq documents”

See the [dedicated page]!(docs/embedding.md) 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]!(docs/embedding.md).

Publications

Section titled “Publications”

See the [dedicated file]!(docs/papers.md)

Examples

Section titled “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:

Outdated examples [but still working]

Section titled “Outdated examples [but still working]”

jsCoq Users:

Section titled “jsCoq Users:”

Incomplete list of places where jsCoq has been used, more or less in reverse chronological order:

jsCoq in the press

Section titled “jsCoq in the press”

Addon Packages

Section titled “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 compile it with jsCoq’s version of Coq. Head over to jscoq/addons for pointers to some well-known packages that have been compiled for jsCoq and are bundled with every version of jsCoq. You can use these as examples for bundling your own libraries.

Troubleshooting

Section titled “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

Section titled “Reporting Bugs”

Feel free to use the issue tracker. Please include your browser/OS/user-agent and any command-line options.

Contact and on-line help

Section titled “Contact and on-line help”

What is broken

Section titled “What is broken”
  • Loading ML modules is slow (not anymore actually).
  • Loading .vo files is slow (not anymore actually).
  • There are surely are threading and performance problems.
  • vm_compute and native_compute fall back to regular compute.

Documents

Section titled “Documents”

See the etc/notes/ directory for some random notes about the project.

Credits

Section titled “Credits”

Core developer team

Section titled “Core developer team”

Past Contributors

Section titled “Past Contributors”

Acknowledgements

Section titled “Acknowledgements”

![FEEVER Logo]!(/frontend/classic/images/feever-logo.png?raw=true “Feever Logo”)

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.