[new release] coq-serapi (8.11.0+0.11.1)

[ejgallego]

CHANGES:

• [general] Require dune >= 2.0 (@ejgallego, ??)
• [serapi] New query Comments to return all comments in a document
  (@ejgallego, Evar support rocq-archive/coq-serapi#20? , (partially) fixes [sercomp] Print mode strips out comments from .v rocq-archive/coq-serapi#191 , Feature request: split comments, not just code ejgallego/coq-lsp#353 )
• [general] Coq's error recovery is now disabled by default
  (@ejgallego , fixes Out-of-order error messages rocq-archive/coq-serapi#201)
• [general] New option --error-recovery to enable error recovery
  (@ejgallego , [serapi] New option --error-recovery to enable error recovery. rocq-archive/coq-serapi#203)
• [general] Bump sexplib dependency to v0.13 (@ejgallego , [build] Bump minimum sexplib version to v0.13 rocq-archive/coq-serapi#204)
  Fixes incorrect change in [sexplib] Bump min version to v0.12.0 , fix deprecated data types. rocq-archive/coq-serapi#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)
  (* set allow-sprop true by default at the init of coq  rocq-archive/coq-serapi#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 , * set allow-sprop true by default at the init of coq  rocq-archive/coq-serapi#199)
• [sertop] Added option --topfile to sertop to set top name from
  a filename (added sertop option --topfile <filename> rocq-archive/coq-serapi#197, @pestun)
• [deps] Require sexplib >= 0.12 , fixed deprecation warnings
  ([sexplib] Bump min version to v0.12.0 , fix deprecated data types. rocq-archive/coq-serapi#194, @ejgallego)
• [general] SerAPI is now tested with OCaml 4.08 and 4.09 ([travis] Test with OCaml 4.08 , Ocaml 4.09 rocq-archive/coq-serapi#195 , @ejgallego)
• [sertop ] Forward port sername from 0.7.1 (@ejgallego)
• [serlib ] Fix Segfault rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , [serlib] Fix segfault in univs.ml rocq-archive/coq-serapi#214)
• [serapi ] Fix Respect COQPATH in sertop rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , [serapi] Fix #221 "Support COQPATH" rocq-archive/coq-serapi#224)
• [sertop ] Fix Support for -indices-matter rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , [sertop] Fix #222 "Support --indices-matter" rocq-archive/coq-serapi#223)
• [sertop ] Fix "Stack overflow in main loop" (@pestun , fixed stack overflow bug in sertop main loop rocq-archive/coq-serapi#216)

[camelus]

Commit: cb00c63

@ejgallego has posted 42 contributions.

☀️ All lint checks passed cb00c63

• These packages passed lint tests: coq-serapi.8.11.0+0.11.1

---

☀️ Installability check (+1)

• new installable packages (1): coq-serapi.8.11.0+0.11.1

[mseri]

I get two failures. The CI seems to fail because it dfoes not recognise pinned as package filter, while Travis fails with:

#=== ERROR while compiling coq-serapi.8.11.0+0.11.1 ===========================#
# context     2.0.7 | linux/x86_64 | ocaml-system.4.09.1 | file:///home/travis/build/ocaml/opam-repository
# path        ~/.opam/ocaml-system/.opam-switch/build/coq-serapi.8.11.0+0.11.1
# command     ~/.opam/opam-init/hooks/sandbox.sh build dune build -p coq-serapi -j 1
# exit-code   1
# env-file    ~/.opam/log/coq-serapi-24825-60459a.env
# output-file ~/.opam/log/coq-serapi-24825-60459a.ou
### output ###
# [...]
# File "serlib/plugins/ssrmatching/dune", line 6, characters 12-35:
# 6 |  (libraries coq.plugins.ssrmatching serlib serlib_ltac sexplib))
#                 ^^^^^^^^^^^^^^^^^^^^^^^
# Error: Library "coq.plugins.ssrmatching" not found.
# Hint: try:
#   dune external-lib-deps --missing -p coq-serapi -j 1 @install
# File "serlib/dune", line 6, characters 12-19:
# 6 |  (libraries coq.stm sexplib))
#                 ^^^^^^^
# Error: Library "coq.stm" not found.
# Hint: try:
#   dune external-lib-deps --missing -p coq-serapi -j 1 @install

[ejgallego]

while Travis fails with

That's also due to Coq not being installed, I'll fix this but still unclear what to do w.r.t. rocq-archive/coq-serapi#208

[mseri]

Thanks!