The Coq mailing list

[James Smith <jecs AT imperial.ac.uk>]

Hi,

I have a collaborative proof assistant (I use these last two words very 
reservedly) here:

http://florence-cpa.org

I've been reaching out to a few academics lately to see if I can find a 
way to possibly use Florence as a front end for an existing proof 
assistant and one of them suggested I subscribe to this list. Literally 
the second email I've received is about JsCoq. I'm glad to learn that 
there is at least one JavaScript implementation of an established proof 
assistant out there.

There is much I could write, however it's probably best instead that 
anyone who is interested in the possibility of another front end for 
JsCoq should just get in touch.

Kind regards,

James

P.S. @Benjamin Pierce, this is the first use of the Concur algorithm I 
contacted you about.

P.P.S. Even a glance at the Mathematics-Core project will show you that 
the vernacular and reasoning is in an embryonic state, to put it mildly. 
Please don't judge this harshly, it is all experimental, not a priority, 
and very difficult to get right. The Propositional folder in the 
Mathematics-Logic project is at least in a presentable state and this is 
the best place to start if you want to have a root around.


On 20/06/16 13:25, Benjamin C. Pierce wrote:
> Hi Emilio,
>
> Do you have automation there to automatically generate a jscoq instance for 
> SF?  I’d love to be able to point SF users to jscoq, as soon as it is ready 
> (= as soon as someone can just follow one link and start doing exercises from 
> the newest SF in their browser)...
>
>     - B
>
>
>
> > On Jun 13, 2016, at 11:56 AM, Emilio Jesús Gallego Arias 
> > <e+coq-club AT x80.org>
> >  wrote:
> >
> > Dear Coq Users,
> >
> > we are happy to announce the release of jsCoq 0.8 and SerAPI 0.02.
> >
> > JsCoq 0.8
> > ---------
> >
> > - https://github.com/ejgallego/jscoq
> >
> > jsCoq has seen many improvements and should be much faster now. It now
> > ships with the following addons:
> >
> > - math-comp mtac coquelicot flocq tlc color sf cpdt hott dsp
> >   coq-ext-lib mirror-core hott
> >
> > In its current status, it is not hard to embed jsCoq into your own
> > blog, web page, or book.
> >
> > 0.9 development will track Coq 8.6 and will be mainly focused on
> > completing the (much needed) new panel user interface.
> >
> > SerAPI 0.02
> > -----------
> >
> > The Coq SerAPI project provides a new communication protocol for
> > Coq based on ppx serializers.
> >
> > - https://github.com/ejgallego/coq-serapi
> >
> > Originally started as the jsCoq toplevel, the project has become
> > independent as we feel it can be useful on its own.
> >
> > The 0.02 release is the first alpha public release; use at your own
> > risk!
> >
> > In the future, jsCoq will consist of a browser user interface plus a
> > js_of_ocaml compiled sertop running in a browser thread.
> >
> > I'd to thank the participants of the Coq Implementors Workshop plus
> > Clément Pit--Claudel, Valentin Robert, and Gabriel Scherer for their
> > help and comments wrt this project.
> >
> > Best regards,
> > Emilio