Skip to content

corwin-of-amber/jscoq

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Run the Coq Proof Assistant in your browser!

Build Status Gitter

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:

https://jscoq.github.io

jsCoq is written to conform to ES2017, any recent standard-compliant browser. No servers or external programs are needed. See the Troubleshooting section if you have problems.

jsCoq is community-developed 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 math-comp, 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
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:

Shortcut Action
Ctrl-S Save file (with the last name provided, or untitled.v)
Ctrl-Shift-S Save file as (prompts for file name)
Ctrl-Alt-S Save file to disk (using the browser's Save dialog, or preset destination)
Ctrl-O Open file (prompts for file name, supports tab completion)
Ctrl-Alt-O 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 pastebin-like 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/haste-server/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 beta-status 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:

Outdated examples [but still working]

jsCoq Users:

Incomplete list of places where jsCoq has been used:

jsCoq in the press

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 coq-addons repository. We recommend you use one of the existing files as a model.

Also, you need to define a jsCoq package by editing the coq-jslib/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/user-agent and command line options.

Contact and on-line help

What is broken

  • Loading ML modules is slow.
  • Loading .vo files is slow.
  • There surely are threading and performance problems.
  • vm_compute and native_compute fall back to regular compute.

Documents

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

Credits

Core developer team

Past Contributors

Acknowledgements

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.

About

A port of Coq to Javascript -- Run Coq in your Browser

Resources

License

Code of conduct

Stars

Watchers

Forks

Packages

No packages published

Languages

  • JavaScript 60.5%
  • OCaml 16.1%
  • TypeScript 8.2%
  • CSS 7.5%
  • Makefile 3.5%
  • HTML 2.0%
  • Other 2.2%