jsCoq and SerAPI releases

Announcements
1

Dear Coq users and developers,

we are happy to announce the releases of jsCoq 0.9.3 and SerAPI 0.6.1 for Coq 8.9.

jsCoq and SerAPI are free software, please don’t hesitate to report issues and contribute at:

jsCoq 0.9:

jsCoq allows interacting with Coq developments as standard-compliant HTML documents using a browser. The project aims to ease the development of interactive Coq documents and teaching material, to improve the accessibility of the platform, and to explore new user interaction possibilities.

jsCoq 0.9 has been three years in the making, and it features a long list of improvements, most of them due to the incredible work of Shachar Itzhaky, who managed to stabilize the Web Worker version and provided countless usability and display improvements including “Company-Coq”-like contextual information display facilities.

While there are still some minor bugs, we feel that this is the first release that seems ready for wider testing and exposure; in particular, as Coq now runs in a separate browser thread, the overall experience is much smoother than before. Keep in mind that jsCoq’s primary target is introductory Coq material, thus it is expected to struggle with heavy developments.

You can see some examples including the “Software Foundations” suite in the links below:

See more examples and information in the project’s web page https://github.com/ejgallego/jscoq, the full list of changes is at https://github.com/ejgallego/jscoq/blob/v8.9%2Bworker/CHANGES.md

SerAPI 0.6.1

SerAPI provides an S-expression based API suitable for machine interaction with Coq. Capabilities include full round-trip serialization of Coq’s AST and most internal structures, easy access to the document build and checking API, and facilities for querying Coq’s environment and proof state.

The 0.6.1 release brings many improvements and features on the serialization front. Thanks to the awesome efforts of Karl Palmskog and Ahmet Celik, SerAPI is now able to serialize/deserialize large Coq developments reliably, and we have improved the sercomp command-line tool for batch (de)serialization of Coq files.

See more information and examples on the project’s website https://github.com/ejgallego/coq-serapi, the full list of changes is at https://github.com/ejgallego/coq-serapi/blob/v8.9/CHANGES.md

Best regards,
Emilio & all contributors to these projects

7 Likes