[serapi] (!) support for Coq 8.14, see upstream changes; nothing too remarkable other than NewDoc will now ignore loadpaths due to new init setup upstream. (#253, @ejgallego)
[ci] SerAPI branches should be able to build now against Coq rc packages as to better integrate with Coq's platform beta release; thanks to Érik Martin-Dorel, Karl Palmskog and Théo Zimmermann for feedback.
Version 0.13.1:
[serapi] New query (Query () (LogicalPath file)) which will return the logical path for a particular .v file (@ejgallego, see also https://github.com/cpitclaudel/alectryon/pull/25)
[serapi] new (SaveDoc opts) command supporting saving of .vo files even when from interactive mode; note that using --topfile is required (fixes #238, @ejgallego, reported by Jason Gross)
[sertop] we don't link the OCaml num library anymore, this could have some impact on plugins (@ejgallego)
[nix] Added Nix support (#249, fixes #248, @Zimmi48, reported by @nyraghu)
[serapi] Fix COQPATH support: interpret paths as absolute (#249, @Zimmi48)
[serlib] Ignore env parameter in certain exceptions (#254, fixes #250, @ejgallego, reported by @cpitclaudel)
[sertop] New option --omit_env that will disable the serialization of Coq's super heavy global environments (#254 @ejgallego)
[build] Test OCaml 4.12 (#257 @ejgallego)
[sertop] Async mode was not working due to passing -no-glob to workers
Version 0.13.0:
[serapi] (!) support for Coq 8.13, see upstream changes; in particular there are changes in the kernel representation of terms [pattern matching, new caseinvert, primitive arrays] (#232, fixes #227, @ejgallego)
Version 0.12.1:
[serapi] (!) Bump public library versioning [breaking change]
[opam] Bump upper bound on ppx_sexp_conv to 0.15, allowing SerAPI to work with the 0.14 set of Jane Street packages.
[sertop ] New (Fork (fifo_in file) (fifo_out file)) command, that will (hard) fork a new SerAPI process and redirect the input / output towards the given Unix FIFOs. This API is experimental but should allow quite a few advantages to some users willing to perform speculative execution. (#210 , improves #202 , @ejgallego)
[serapi] Fix missing newline to separate goals (#235, fixes #231, @ejgallego)
Version 0.12.0:
[general] (!) support Coq 8.12, main changes upstream related to the representation of numerals and notations. The rest of the interface does remain relative stable. (@ejgallego).
Version 0.11.1:
[general] Require dune >= 2.0 (@ejgallego, ??)
[serapi] New query Comments to return all comments in a document (@ejgallego, #20? , (partially) fixes #191 , #200 )
[general] Coq's error recovery is now disabled by default (@ejgallego , fixes #201)
[general] New option --error-recovery to enable error recovery (@ejgallego , #203)
[general] Bump sexplib dependency to v0.13 (@ejgallego , #204) Fixes incorrect change in #194.
[sertop] Set default value of allow-sprop to be true in agreement with upstream coq v8.11 and added option '--disallow-sprop' to optionally switch it off (--disallow-sprop forbids using the proof irrelevant SProp sort) (#199, @pestun)
[sertop] Set default value of allow-sprop to be true in agreement with upstream coq v8.11 and added option '--disallow-sprop' to optionally switch it off (--disallow-sprop forbids using the proof irrelevant SProp sort) (@pestun , #199)
[sertop] Added option --topfile to sertop to set top name from a filename (#197, @pestun)
[sertop ] Fix "Stack overflow in main loop" (@pestun , #216)
Version 0.11.0:
[general] (!) support Coq 8.11, a few datatypes have changed, in particular CoqAst handles locations as an AST node, and the kernel type includes primitive floats (@ejgallego).
[general] (!) Now the sertop and serapi OCaml libraries are built packed, we've also bumped their compat version number (#192 @ejgallego)
Version 0.7.1:
[sertop ] Add sername program for batch serialization elaborated terms Note that this utility will be deprecated in future versions, to be subsumed by Query. (#207, @palmskog, with help from @ejgallego)
[serlib ] Expose QueryUtil.info_of_id and gen_pp_obj in serapi_protocol.mli to enable using them in sername to retrieve serialized body-type pairs (@palmskog)
[general] Improved compat with Jane Street v0.13 toolchain
[serlib ] Only use ssreflect from Coq in tests (@ejgallego)
Version 0.7.0:
[general] (!) support Coq 8.10,
[serapi] (!) Goals query return type has been modified due to upstream changes. (@ejgallego)
[serlib] Complete (hopefully) serialization for ssreflect ASTs. (#73 @ejgallego)
[general] Drop support for OCaml < 4.07 (#140 @ejgallego)
[serlib ] JSON serialization for kernel and AST terms (@ejgallego)
[serapi ] Add Complete support (@ejgallego c.f. https://github.com/coq/coq/pull/8766)
[serlib ] Serlib is now built as a wrapped module (@ejgallego)
[serapi ] (!) Goals info has been extended to print name metadata if available, cc #151 (@ejgallego , suggested by @cpitclaudel)
[serlib ] JSON support for vernac_expr (@ejgallego)
[sertop ] (!) Do as Coq upstream and load Coq's stdlib with -R (closes #56)
[sertop ] Follow Coq upstream and unset indices_matter (closes #157, thanks to @palmskog for the report)
[serapi ] (!) Improve CoqExn answer to have pretty-printed message (improves #162, thanks to @cpitclaudel for the request)
[serlib ] (!) Fix capitalization conventions for a few types in Names (closes #167 thanks to @corwin-of-amber for the report)
[serapi ] (!) Add bullet suggest information to goal query (@corwin-of-amber)
[done] Basic Sentence splitting (Parse num string)), retuns the first num end of the sentences without executing them. This has pitfalls as parsing is very stateful.
[done] Basic completion-oriented Search support (Query () Names)
[done] Better command line parsing (Cmdliner, Core ?)
[partial] Print Grammar tactic. (Query ... (Tactics)). Still we need to decide on: Coq.Init.Notations.instantiate vs instantiate, the issue of Nametab.shortest_qualid_of_global is a very sensible one for IDEs