Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ANN: jsCoq 0.8 / SerAPI 0.02

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ANN: jsCoq 0.8 / SerAPI 0.02


Chronological Thread 
  • From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] ANN: jsCoq 0.8 / SerAPI 0.02
  • Date: Mon, 20 Jun 2016 21:19:40 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT fox.seas.upenn.edu
  • Ironport-phdr: 9a23:netgOh2sXQcksO7SsmDT+DRfVm0co7zxezQtwd8ZsegSLPad9pjvdHbS+e9qxAeQG96LurQV1aGK4+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6DyZXpnLzis7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGEGl630eW2AXlFJjRUD97RzgVZq7+n/wvfJ81TORMOX9TKtyRCyv6aEtRRP13nRUfwUl+X3a35QjxJlQpwis8kRy

How about once that’s fixed (and the POPL deadline is past :-) we have a go
at generating everything automatically from the SF Makefile…

- B

> On Jun 20, 2016, at 11:04 AM, Emilio Jesús Gallego Arias
> <e+coq-club AT x80.org>
> wrote:
>
> e+coq-club AT x80.org
> (Emilio Jesús Gallego Arias) writes:
>
>> I think it is not yet ready to the point you can fully replace
>> Emacs/CoqIDE, however it is a start and the thing can serve as backup.
>
> Indeed there is a very annoying bug that prevents the whole book
> working fine: braces as in:
>
> assert H.
> { now tac. }
>
> are not handled correctly by the editor. Fixed manually in few first
> chapters, bug was already in my TODO list.
>
> Also coqdoc tool sometimes likes to eat random tokens, but that is
> usually easy to fix.
>
> E.




Archive powered by MHonArc 2.6.18.

Top of Page