coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
- To: coq-club AT inria.fr
- Subject: [Coq-Club] [ANNOUNCE] jsCoq preview release
- Date: Thu, 03 Mar 2016 01:39:15 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT boipeva.ensmp.fr
- Ironport-phdr: 9a23:88vB6x3+44kPGIfdsmDT+DRfVm0co7zxezQtwd8ZsegSIvad9pjvdHbS+e9qxAeQG96LtLQb0KGM7ejJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZvsnLrss7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGAbM7XwFF24SjxBgE1idqhbgUd+xny77sut6kAuXJl/tBZ89XTCv4KAjYQXpgTxGZG1xy33elsEl1PETmxmmvREqm4M=
- Organization: X80 Heavy Industries
Dear Coq Club,
we are happy to announce the first experimental release of jsCoq, a
port of Coq to HTML5/Javascript ES2015.
jsCoq needs a *pretty recent* browser, either Chrome (>= 48.0) or
Firefox (>= 45.0). The online demo is at:
https://x80.org/rhino-coq/
The project aims to ease the development of interactive Coq documents
and teaching material, improve the accessibility of the platform, and
explore new user interaction possibilities.
This is the first public release; it provides a mostly functional
basic Coq environment. While basically untested, we feel that the tool
has reached a point where it could be useful to others.
Some code is hacky and needs to be reworked, there are known pitfalls,
expect bugs and problems. More info below.
Best regards,
Emilio
Try & Download:
---------------
jsCoq is free software, source and build instructions are available
from:
https://github.com/ejgallego/jscoq/
Building is a bit involved, there are pre-built versions at:
https://github.com/ejgallego/jscoq-builds/
Enabling jsCoq in an existing webpage roughly amounts to adding:
<script src="js/jscoq-loader.js" type="text/javascript"></script>
<script type="text/javascript">
loadJsCoq('./').then( () => new CoqManager (list_of_ids, [options]) );
</script>
YMMV, we would be very happy to help or hear from your experience!
Current structure is fairly UI independent, so this could be a good
base to build a different IDE try ideas out!
Libraries available:
--------------------
jsCoq can build against Coq 8.5 or trunk. Our current build is based
on 8.5 + several hand-picked fixes, we include the following
libraries:
CoLoR, cpdt (free parts), coquelicot, flocq, math-comp, mtac,
relation-algebra, sf, and TLC.
Let us know if you would like to add your own library to our builds.
Colla&Coq
---------
We provide a pastebin-like service at:
https://x80.org/collacoq/
it allows to paste and share runnable Coq snippets, it's status is
extremely experimental, so expect you pastes to be gone.
Custom build for HoTT:
----------------------
We provide an experimental custom build for HoTT:
- using the HoTT library:
https://x80.org/rhino-hott/
A very experimental optimized build for the math-comp library is also
available (contact me in private).
Coqdoc to jsCoq:
---------------
Experimental support for generating jsCoq webpages from a coqdoc
document is available; see the README for more details.
Users:
------
jsCoq was used at the "Advanced Coq Winter School 2016":
https://team.inria.fr/marelle/en/advanced-coq-winter-school-2016/
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:
+ dft.v: https://x80.org/rhino-coq/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"
+ Mtac: The Mtac tutorial by Beta Zilliani:
https://x80.org/rhino-coq/examples/mtac_tutorial.html
+ Stlc: The "Simply Typed Lambda Calculus" chapter from Software
Foundations by Benjamin Pierce et al:
https://x80.org/rhino-coq/examples/Stlc.html
+ StackMachine: The First chapter of the book "Certified Programming
with Dependent Types" by Adam Chlipala:
https://x80.org/rhino-coq/examples/Cpdt.StackMachine.html
Acknowledgments:
----------------
jsCoq development has been funded by the ANR/FEEVER project.
jsCoq has been written by Emilio Jesús Gallego Arias and Benoît Pin,
with special thanks to:
Yves Bertot
Maximé Dènés
Hugo Heuzard
Pierre Jouvelot
Pierre-Marie Pédrot
Gabriel Scherer
Arnaud Spiwack
Enrico Tassi
Jérome Vouillon
Future plans/TODO:
------------------
A better panel layout is coming soon. It will allow different
placement, resizing. Goal history and diffs should also happen soon,
as well as a much improved search/logging support.
There are potentially many useful things to improve, here's a small
brainstorming:
+ Improve .vo load time: This requires non-trivial, but we could make
.vo loading an order of magnitude faster.
+ Better CSS/HTML styles: we are lacking in web design manpower so the
current style could be easily improved.
+ Web editor (CodeMirror) support for Coq still needs a lot of work.
+ Better UI: Current UI is a prototype and may not be flexible enough.
Better proof display, user queries, an improved search command,
better display of math would be great.
+ More of Coq's API and data structures could be exported to JS (via
json_ppx_deriving).
+ Extraction to JavaScript.
+ Better support for html slides/deck.js.
+ Running jsCoq in a separate browser thread (worker).
+ Static vs dynamic linking of .cma plugins is to be considered.
+ Makefile of addons/package format need work.
+ Fixing vm_compute could be done using emscripten.
- [Coq-Club] [ANNOUNCE] jsCoq preview release, Emilio Jesús Gallego Arias, 03/03/2016
- Re: [Coq-Club] [ANNOUNCE] jsCoq preview release, Arthur Azevedo de Amorim, 03/03/2016
- Re: [Coq-Club] [ANNOUNCE] jsCoq preview release, Clément Pit--Claudel, 03/03/2016
- Re: [Coq-Club] [ANNOUNCE] jsCoq preview release, Arthur Azevedo de Amorim, 03/03/2016
Archive powered by MHonArc 2.6.18.