diff --git a/CHANGES.md b/CHANGES.md index 8bce6e5f..c0d7e515 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,7 +22,7 @@ (closes #167 thanks to @corwin-of-amber for the report) * [serapi ] (!) Add bullet suggest information to goal query (@corwin-of-amber) * [sertop ] Add `--no_prelude` option (closes #176, @ejgallego, request of @darbyhaller) - * [serlib ] (!) Add index to `MBId` serialization` (fixes #150, @ejgallego) + * [serlib ] (!) Add index to `MBId` serialization (fixes #150, @ejgallego) * [serapi ] (!) Add `sid` parameter to `Print` (helps #150, @ejgallego, reported by @cpitclaudel) * [sertop ] Add `sertok` program for batch serialization of tokens and their source locations (@palmskog) * [serapi ] (!) Add string-formatted messages to `CoqExn` and `Message` diff --git a/notes/announce-0.7.0.md b/notes/announce-0.7.0.md new file mode 100644 index 00000000..df1b1880 --- /dev/null +++ b/notes/announce-0.7.0.md @@ -0,0 +1,34 @@ +Subject: [ANNOUNCE] SerAPI 0.7.0 + +Dear Coq users and developers, + +we are happy to announce the release SerAPI 0.7.0 for Coq 8.10. + +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. + +SerAPI is developed by Emilio J. Gallego Arias, Karl Palmskog, and +many other contributors. SerAPI is free software. please don't +hesitate to report issues and contribute at: + +- https://github.com/ejgallego/coq-serapi + +## SerAPI 0.7.0 + +The 0.7.0 release provides brings many small improvements, bugfixes, +and tweaks; two highlights of the 0.7.0 release are: + + - it is now possible to serialize from/to `JSON` using the `Serlib` API + - `sertok` command-line tool provides batch tokenization of Coq documents + +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.10/CHANGES.md + +Items marked with `(!)` are protocol-breaking changes. + +Best regards, +Emilio, Karl & all contributors