Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Segfault #212

Closed
cpitclaudel opened this issue Jun 19, 2020 · 1 comment · Fixed by #214 or ocaml/opam-repository#17070
Closed

Segfault #212

cpitclaudel opened this issue Jun 19, 2020 · 1 comment · Fixed by #214 or ocaml/opam-repository#17070
Labels
kind: bug kind: serialization
Milestone
0.11.1

Comments

@cpitclaudel
Copy link
Collaborator

Hi @ejgallego,

The following example reliably causes a segfault on my machine:

$ sertop
("query0"("Add"()"Require Coq.Vectors.Vector.\nRequire Import Coq.Strings.String Coq.Arith.PeanoNat.\nImport EqNotations Vector.VectorNotations."))
("query1"("Exec""2"))
("query2"("Query"(("sid""2"))"EGoals"))
("query3"("Exec""3"))
("query4"("Query"(("sid""3"))"EGoals"))
("query5"("Exec""4"))
("query6"("Query"(("sid""4"))"EGoals"))
("query7"("Add"()"Lemma map_snoc_1234 :\n  Vector.map (fun x => 2 * x) (cons 1 [2; 3; 4]) = [2; 4; 6; 8].\nProof.\n  cbv -[Vector.map Nat.mul].\n  Fail destruct (Nat.add_1_r 3). (* .messages *)\nAbort."))
("query8"("Exec""5"))

Here's the backtrace:

#0  camlSerlib__Ser_univ__sexp_of_t_1094 () at serlib/ser_univ.ml:30
#1  0x0000555556070a01 in camlSerlib__Ser_univ__sexp_of__t_1224 () at serlib/ser_univ.ml:43
#2  0x00005555561fc10c in camlSexplib0__Sexp_conv__sexp_of_array_840 () at sexp_conv.ml:71
#3  0x0000555556071557 in camlSerlib__Ser_univ__sexp_of__t_2109 () at serlib/ser_univ.ml:90
#4  0x00005555561fbeb6 in camlSexplib0__Sexp_conv__sexp_of_pair_823 () at sexp_conv.ml:59
#5  0x000055555609ea7c in camlSerlib__Ser_declarations__sexp_of_universes_1858 () at serlib/ser_univ.ml:129
#6  0x00005555560a0f32 in camlSerlib__Ser_declarations__sexp_of_constant_body_2111 () at kernel/declarations.ml:105
#7  0x00005555560aabff in camlSerlib__Ser_declarations__sexp_of_structure_field_body_3986 () at serlib/ser_declarations.ml:132
#8  0x00005555560b844f in camlSerlib__Ser_declarations__fun_6568 () at serlib/ser_declarations.ml:136
#9  0x000055555673955b in camlStdlib__list__rmap_f_231 () at list.ml:103
#10 0x00005555561fc029 in camlSexplib0__Sexp_conv__sexp_of_list_837 () at sexp_conv.ml:66
#11 0x00005555560a69d4 in camlSerlib__Ser_declarations__sexp_of_functorize_2511 () at kernel/declarations.ml:236
#12 0x00005555560b6c48 in camlSerlib__Ser_declarations__sexp_of_generic_module_body_3991 () at serlib/ser_declarations.ml:140
#13 0x00005555561fbe76 in camlSexplib0__Sexp_conv__sexp_of_pair_823 () at sexp_conv.ml:59
#14 0x000055555673955b in camlStdlib__list__rmap_f_231 () at list.ml:103
#15 0x00005555561fc029 in camlSexplib0__Sexp_conv__sexp_of_list_837 () at sexp_conv.ml:66
#16 0x00005555560be196 in camlSerlib__Ser_environ__sexp_of__t_2142 () at serlib/ser_environ.ml:66
#17 0x00005555560bed72 in camlSerlib__Ser_environ__sexp_of_env_2371 () at serlib/ser_environ.ml:69
#18 0x0000555556159df0 in camlSerlib__Ser_pretype_errors__sexp_of_unification_error_883 () at pretyping/pretype_errors.mli:25
#19 0x000055555615c50c in camlSerlib__Ser_pretype_errors__sexp_of_pretype_error_2363 () at pretyping/pretype_errors.mli:44
#20 0x00005555560315f3 in camlSertop__Sertop_ser__fun_6259 () at sertop/sertop_ser.ml:63
#21 0x00005555561fc77f in camlSexplib0__Sexp_conv__find_auto_3050 () at sexp_conv.ml:161
#22 0x00005555561fc85d in camlSexplib0__Sexp_conv__sexp_of_exn_3063 () at sexp_conv.ml:174
#23 0x000055555602d9b0 in camlSertop__Sertop_ser__sexp_of_t_4688 () at serapi/serapi_protocol.mli:461
#24 0x000055555602e7bc in camlSertop__Sertop_ser__sexp_of_answer_kind_4770 () at serapi/serapi_protocol.mli:478
#25 0x000055555603111f in camlSertop__Sertop_ser__sexp_of_answer_4980 () at serapi/serapi_protocol.mli:515
#26 0x0000555556033fb5 in camlSertop__Sertop_sexp__fun_1253 () at sertop/sertop_sexp.ml:98
#27 0x000055555603431a in camlSertop__Sertop_sexp__ser_lock_850 () at sertop/sertop_sexp.ml:109
#28 0x00005555567395c1 in camlStdlib__list__iter_236 () at list.ml:110
#29 0x0000555556034555 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:156
#30 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#31 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#32 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#33 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#34 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#35 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#36 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#37 0x0000555556034583 in camlSertop__Sertop_sexp__loop_1179 () at sertop/sertop_sexp.ml:157
#38 0x000055555600cd73 in caml_curry17_16 ()
#39 0x00005555566c18b8 in camlCmdliner_term__fun_177 () at cmdliner_term.ml:25
#40 0x00005555566c4a2d in camlCmdliner__run_389 () at cmdliner.ml:117
#41 0x00005555566c4d60 in camlCmdliner__term_eval_412 () at cmdliner.ml:147
#42 0x00005555566c564e in camlCmdliner__eval_771 () at cmdliner.ml:221
#43 0x0000555556011ee7 in camlSertop_bin__main_343 () at sertop/sertop_bin.ml:79
#44 0x0000555556012149 in camlSertop_bin__entry () at sertop/sertop_bin.ml:83
#45 0x000055555600bf59 in caml_program ()
#46 0x00005555567c5ae0 in caml_start_program ()
#47 0x00005555567a7ac5 in caml_startup_common (argv=0x7fffffffe078, pooling=<optimized out>, pooling@entry=0) at startup_nat.c:160
#48 0x00005555567a7b0b in caml_startup_exn (argv=<optimized out>) at startup_nat.c:170
#49 caml_startup (argv=<optimized out>) at startup_nat.c:170
#50 0x000055555600951c in main (argc=<optimized out>, argv=<optimized out>) at main.c:44

And here's the full session. The segfault happens a few seconds after sending the last command:

$ gdb sertop
GNU gdb (Ubuntu 8.2-0ubuntu1~18.04) 8.2
Copyright (C) 2018 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from sertop...done.
(gdb) run
Starting program: /home/clement/.opam/4.09.0/bin/sertop 
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Prelude /home/clement/.opam/4.09.0/lib/coq/theories/Init/Prelude.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Notations /home/clement/.opam/4.09.0/lib/coq/theories/Init/Notations.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Logic /home/clement/.opam/4.09.0/lib/coq/theories/Init/Logic.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Datatypes /home/clement/.opam/4.09.0/lib/coq/theories/Init/Datatypes.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Logic_Type /home/clement/.opam/4.09.0/lib/coq/theories/Init/Logic_Type.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Specif /home/clement/.opam/4.09.0/lib/coq/theories/Init/Specif.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Decimal /home/clement/.opam/4.09.0/lib/coq/theories/Init/Decimal.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Nat /home/clement/.opam/4.09.0/lib/coq/theories/Init/Nat.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Byte /home/clement/.opam/4.09.0/lib/coq/theories/Init/Byte.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Peano /home/clement/.opam/4.09.0/lib/coq/theories/Init/Peano.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Wf /home/clement/.opam/4.09.0/lib/coq/theories/Init/Wf.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Tactics /home/clement/.opam/4.09.0/lib/coq/theories/Init/Tactics.vo))))
(Feedback((doc_id 0)(span_id 0)(route 0)(contents(FileLoaded Coq.Init.Tauto /home/clement/.opam/4.09.0/lib/coq/theories/Init/Tauto.vo))))
(Feedback((doc_id 0)(span_id 1)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 1)(route 0)(contents Processed)))
("query0"("Add"()"Require Coq.Vectors.Vector.\nRequire Import Coq.Strings.String Coq.Arith.PeanoNat.\nImport EqNotations Vector.VectorNotations."))
("query1"("Exec""2"))
("query2"("Query"(("sid""2"))"EGoals"))
("query3"("Exec""3"))
("query4"("Query"(("sid""3"))"EGoals"))
("query5"("Exec""4"))
("query6"("Query"(("sid""4"))"EGoals"))
("query7"("Add"()"Lemma map_snoc_1234 :\n  Vector.map (fun x => 2 * x) (cons 1 [2; 3; 4]) = [2; 4; 6; 8].\nProof.\n  cbv -[Vector.map Nat.mul].\n  Fail destruct (Nat.add_1_r 3). (* .messages *)\nAbort."))
("query8"("Exec""5"))

(Answer query0 Ack)
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 1)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Vectors.Vector /home/clement/.opam/4.09.0/lib/coq/theories/Vectors/Vector.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Bool.Bool /home/clement/.opam/4.09.0/lib/coq/theories/Bool/Bool.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Program.Basics /home/clement/.opam/4.09.0/lib/coq/theories/Program/Basics.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.Init /home/clement/.opam/4.09.0/lib/coq/theories/Classes/Init.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Program.Tactics /home/clement/.opam/4.09.0/lib/coq/theories/Program/Tactics.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Relations.Relation_Definitions /home/clement/.opam/4.09.0/lib/coq/theories/Relations/Relation_Definitions.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.RelationClasses /home/clement/.opam/4.09.0/lib/coq/theories/Classes/RelationClasses.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.Morphisms /home/clement/.opam/4.09.0/lib/coq/theories/Classes/Morphisms.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.CRelationClasses /home/clement/.opam/4.09.0/lib/coq/theories/Classes/CRelationClasses.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.CMorphisms /home/clement/.opam/4.09.0/lib/coq/theories/Classes/CMorphisms.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.Morphisms_Prop /home/clement/.opam/4.09.0/lib/coq/theories/Classes/Morphisms_Prop.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.Equivalence /home/clement/.opam/4.09.0/lib/coq/theories/Classes/Equivalence.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Classes.SetoidTactics /home/clement/.opam/4.09.0/lib/coq/theories/Classes/SetoidTactics.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.ssr.ssrclasses /home/clement/.opam/4.09.0/lib/coq/plugins/ssr/ssrclasses.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.ssr.ssrunder /home/clement/.opam/4.09.0/lib/coq/plugins/ssr/ssrunder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.ssr.ssrsetoid /home/clement/.opam/4.09.0/lib/coq/plugins/ssr/ssrsetoid.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Setoids.Setoid /home/clement/.opam/4.09.0/lib/coq/theories/Setoids/Setoid.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Structures.Equalities /home/clement/.opam/4.09.0/lib/coq/theories/Structures/Equalities.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Relations.Relation_Operators /home/clement/.opam/4.09.0/lib/coq/theories/Relations/Relation_Operators.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Relations.Operators_Properties /home/clement/.opam/4.09.0/lib/coq/theories/Relations/Operators_Properties.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Relations.Relations /home/clement/.opam/4.09.0/lib/coq/theories/Relations/Relations.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Structures.Orders /home/clement/.opam/4.09.0/lib/coq/theories/Structures/Orders.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NumPrelude /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NumPrelude.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Structures.OrdersTac /home/clement/.opam/4.09.0/lib/coq/theories/Structures/OrdersTac.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Structures.OrdersFacts /home/clement/.opam/4.09.0/lib/coq/theories/Structures/OrdersFacts.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Structures.GenericMinMax /home/clement/.opam/4.09.0/lib/coq/theories/Structures/GenericMinMax.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZAxioms /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZAxioms.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZBase /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZBase.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZAdd /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZAdd.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZMul /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZMul.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Logic.Decidable /home/clement/.opam/4.09.0/lib/coq/theories/Logic/Decidable.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZOrder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZAddOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZAddOrder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZMulOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZMulOrder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZParity /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZParity.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZPow /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZPow.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZSqrt /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZSqrt.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZLog /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZLog.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZDiv /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZDiv.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZGcd /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZGcd.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZBits /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZBits.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NAxioms /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NAxioms.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.NatInt.NZProperties /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/NatInt/NZProperties.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NBase /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NBase.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NAdd /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NAdd.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NOrder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NAddOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NAddOrder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NMulOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NMulOrder.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NSub /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NSub.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NMaxMin /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NMaxMin.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NParity /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NParity.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NPow /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NPow.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NSqrt /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NSqrt.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NLog /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NLog.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NDiv /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NDiv.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NGcd /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NGcd.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NLcm /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NLcm.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NBits /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NBits.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Numbers.Natural.Abstract.NProperties /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Natural/Abstract/NProperties.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.PeanoNat /home/clement/.opam/4.09.0/lib/coq/theories/Arith/PeanoNat.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Le /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Le.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Lt /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Lt.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Plus /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Plus.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Gt /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Gt.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Minus /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Minus.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Mult /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Mult.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Between /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Between.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Logic.EqdepFacts /home/clement/.opam/4.09.0/lib/coq/theories/Logic/EqdepFacts.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Logic.Eqdep_dec /home/clement/.opam/4.09.0/lib/coq/theories/Logic/Eqdep_dec.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Peano_dec /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Peano_dec.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Compare_dec /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Compare_dec.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Factorial /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Factorial.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.EqNat /home/clement/.opam/4.09.0/lib/coq/theories/Arith/EqNat.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Wf_nat /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Wf_nat.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Arith.Arith_base /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Arith_base.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Vectors.Fin /home/clement/.opam/4.09.0/lib/coq/theories/Vectors/Fin.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Vectors.VectorDef /home/clement/.opam/4.09.0/lib/coq/theories/Vectors/VectorDef.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Vectors.VectorSpec /home/clement/.opam/4.09.0/lib/coq/theories/Vectors/VectorSpec.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents(FileLoaded Coq.Vectors.VectorEq /home/clement/.opam/4.09.0/lib/coq/theories/Vectors/VectorEq.vo))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 2)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Strings.String /home/clement/.opam/4.09.0/lib/coq/theories/Strings/String.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.BinNums /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/BinNums.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.PArith.BinPosDef /home/clement/.opam/4.09.0/lib/coq/theories/PArith/BinPosDef.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.PArith.BinPos /home/clement/.opam/4.09.0/lib/coq/theories/PArith/BinPos.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.NArith.BinNatDef /home/clement/.opam/4.09.0/lib/coq/theories/NArith/BinNatDef.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.NArith.BinNat /home/clement/.opam/4.09.0/lib/coq/theories/NArith/BinNat.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.PArith.Pnat /home/clement/.opam/4.09.0/lib/coq/theories/PArith/Pnat.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.NArith.Nnat /home/clement/.opam/4.09.0/lib/coq/theories/NArith/Nnat.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.Ring_theory /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/Ring_theory.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Lists.List /home/clement/.opam/4.09.0/lib/coq/theories/Lists/List.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.BinList /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/BinList.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZAxioms /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZAxioms.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZBase /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZBase.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZAdd /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZAdd.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZMul /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZMul.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZLt /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZLt.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZAddOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZAddOrder.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZMulOrder /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZMulOrder.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZMaxMin /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZMaxMin.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZSgnAbs /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZSgnAbs.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZParity /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZParity.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZPow /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZPow.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZDivTrunc /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZDivTrunc.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZDivFloor /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZDivFloor.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZGcd /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZGcd.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZLcm /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZLcm.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZBits /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZBits.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Numbers.Integer.Abstract.ZProperties /home/clement/.opam/4.09.0/lib/coq/theories/Numbers/Integer/Abstract/ZProperties.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.BinIntDef /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/BinIntDef.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.BinInt /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/BinInt.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.Ring_polynom /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/Ring_polynom.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Lists.ListTactics /home/clement/.opam/4.09.0/lib/coq/theories/Lists/ListTactics.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.Zeven /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/Zeven.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.Zcompare /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/Zcompare.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.Zorder /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/Zorder.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Bool.Sumbool /home/clement/.opam/4.09.0/lib/coq/theories/Bool/Sumbool.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.ZArith_dec /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/ZArith_dec.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.ZArith.Zbool /home/clement/.opam/4.09.0/lib/coq/theories/ZArith/Zbool.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.InitialRing /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/InitialRing.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.Ring_tac /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/Ring_tac.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.Ring_base /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/Ring_base.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.Ring /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/Ring.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.setoid_ring.ArithRing /home/clement/.opam/4.09.0/lib/coq/plugins/setoid_ring/ArithRing.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Arith.Arith /home/clement/.opam/4.09.0/lib/coq/theories/Arith/Arith.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Strings.Byte /home/clement/.opam/4.09.0/lib/coq/theories/Strings/Byte.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents(FileLoaded Coq.Strings.Ascii /home/clement/.opam/4.09.0/lib/coq/theories/Strings/Ascii.vo))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 4)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 3)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 4)(route 0)(contents Processed)))
(Answer query0(Added 2((fname ToplevelInput)(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 0)(ep 27))NewTip))
(Answer query0(Added 3((fname ToplevelInput)(line_nb 2)(bol_pos 28)(line_nb_last 2)(bol_pos_last 28)(bp 28)(ep 81))NewTip))
(Answer query0(Added 4((fname ToplevelInput)(line_nb 3)(bol_pos 82)(line_nb_last 3)(bol_pos_last 82)(bp 82)(ep 124))NewTip))
(Answer query0 Completed)
(Answer query1 Ack)
(Feedback((doc_id 0)(span_id 2)(route 0)(contents Processed)))
(Answer query1 Completed)
(Answer query2 Ack)
(Answer query2(ObjList()))
(Answer query2 Completed)
(Answer query3 Ack)
(Feedback((doc_id 0)(span_id 3)(route 0)(contents Processed)))
(Answer query3 Completed)
(Answer query4 Ack)
(Answer query4(ObjList()))
(Answer query4 Completed)
(Answer query5 Ack)
(Feedback((doc_id 0)(span_id 4)(route 0)(contents Processed)))
(Answer query5 Completed)
(Answer query6 Ack)
(Answer query6(ObjList()))
(Answer query6 Completed)
(Answer query7 Ack)
(Answer query7(Added 5((fname ToplevelInput)(line_nb 1)(bol_pos 0)(line_nb_last 2)(bol_pos_last 22)(bp 0)(ep 86))NewTip))
(Answer query7(Added 6((fname ToplevelInput)(line_nb 3)(bol_pos 87)(line_nb_last 3)(bol_pos_last 87)(bp 87)(ep 93))NewTip))
(Answer query7(Added 7((fname ToplevelInput)(line_nb 4)(bol_pos 94)(line_nb_last 4)(bol_pos_last 94)(bp 96)(ep 122))NewTip))
(Answer query7(Added 8((fname ToplevelInput)(line_nb 5)(bol_pos 123)(line_nb_last 5)(bol_pos_last 123)(bp 125)(ep 155))NewTip))
(Answer query7(Added 9((fname ToplevelInput)(line_nb 6)(bol_pos 172)(line_nb_last 6)(bol_pos_last 172)(bp 172)(ep 178))NewTip))
(Answer query7 Completed)
(Answer query8 Ack)
(Feedback((doc_id 0)(span_id 5)(route 0)(contents(ProcessingIn master))))
(Feedback((doc_id 0)(span_id 4)(route 0)(contents Processed)))
(Feedback((doc_id 0)(span_id 5)(route 0)(contents(Message(level Error)(loc(((fname ToplevelInput)(line_nb 2)(bol_pos 22)(line_nb_last 2)(bol_pos_last 22)(bp 60)(ep 69))))(pp(Pp_glue((Pp_box(Pp_hovbox 0)(Pp_glue((Pp_string"The term")(Pp_print_break 1 1)(Pp_box(Pp_hbox 0)(Pp_glue((Pp_string"\"")(Pp_box(Pp_hovbox 0)(Pp_glue((Pp_tag constr.notation(Pp_string"["))(Pp_string 2)(Pp_tag constr.notation(Pp_string";"))(Pp_print_break 1 0)(Pp_string 3)(Pp_tag constr.notation(Pp_string";"))(Pp_print_break 1 0)(Pp_string 4)(Pp_tag constr.notation(Pp_string"]")))))(Pp_string"\""))))(Pp_print_break 1 0)(Pp_string"has type")(Pp_print_break 1 1)(Pp_box(Pp_hbox 0)(Pp_glue((Pp_string"\"")(Pp_box(Pp_hovbox 2)(Pp_glue((Pp_tag constr.path(Pp_string Vector))(Pp_string .)(Pp_tag constr.reference(Pp_string t))(Pp_print_break 1 0)(Pp_tag constr.variable(Pp_string nat))(Pp_print_break 1 0)(Pp_string 3))))(Pp_string"\""))))(Pp_print_break 1 0)(Pp_string"while it is expected to have type")(Pp_print_break 1 1)(Pp_box(Pp_hbox 0)(Pp_glue((Pp_string"\"")(Pp_box(Pp_hovbox 2)(Pp_glue((Pp_tag constr.variable(Pp_string list))(Pp_print_break 1 0)(Pp_tag constr.variable(Pp_string nat)))))(Pp_string"\""))))(Pp_string .)))))))(str"The term \"[2; 3; 4]\" has type \"Vector.t nat 3\"\nwhile it is expected to have type \"list nat\".")))))

Program received signal SIGSEGV, Segmentation fault.
camlSerlib__Ser_univ__sexp_of_t_1094 () at serlib/ser_univ.ml:30
30	serlib/ser_univ.ml: No such file or directory.

I'm on 8.11.0+0.11.0
@ejgallego
Copy link
Collaborator

Thanks, fix in #214 ; a test has been added.

However, a further issue appears here, namely that the verbose error serialization is way too verbose as it will include a huge env in this case, this should be likely addressed separately.

I guess we want to reify errors upstream so these carrying the context can be handled in a more modular way, for now we will have to filter those by hand.

ejgallego added a commit that referenced this issue Jun 19, 2020
@ejgallego
[serlib] Fix segfault in univs.ml
0e4ae0e 
Fixes #212 ; there was an error in the manual syncing of code.

We have added a test, but still this is a problem.

Moreover, in the report in #212 a further issue appears, namely that
the verbose error serialization is _way_ too verbose, this should be
likely addressed separately.
@ejgallego ejgallego mentioned this issue Jun 19, 2020
Merged
@ejgallego ejgallego added this to the 0.11.1 milestone Jun 19, 2020
cpitclaudel added a commit to cpitclaudel/alectryon that referenced this issue Jun 26, 2020
@cpitclaudel
core: Work around rocq-archive/coq-serapi#212
1239b24
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Aug 26, 2020
@ejgallego
[new release] coq-serapi (8.11.0+0.11.1)
b688d42 
CHANGES:

* [general] Require dune >= 2.0 (@ejgallego, ??)
 * [serapi]  New query `Comments` to return all comments in a document
             (@ejgallego, rocq-archive/coq-serapi#20? , (partially) fixes rocq-archive/coq-serapi#191 , ejgallego/coq-serapi#200 )
 * [general] Coq's error recovery is now disabled by default
             (@ejgallego , fixes rocq-archive/coq-serapi#201)
 * [general] New option `--error-recovery` to enable error recovery
             (@ejgallego , rocq-archive/coq-serapi#203)
 * [general] Bump sexplib dependency to v0.13 (@ejgallego , rocq-archive/coq-serapi#204)
             Fixes incorrect change in 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)
             (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 , rocq-archive/coq-serapi#199)
 * [sertop]  Added option `--topfile` to `sertop` to set top name from
             a filename (rocq-archive/coq-serapi#197, @pestun)
 * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
             (rocq-archive/coq-serapi#194, @ejgallego)
 * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (rocq-archive/coq-serapi#195 , @ejgallego)
 * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
 * [serlib ] Fix rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#214)
 * [serapi ] Fix rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#224)
 * [sertop ] Fix rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#223)
 * [sertop ] Fix "Stack overflow in main loop" (@pestun , rocq-archive/coq-serapi#216)
@ejgallego ejgallego mentioned this issue Aug 26, 2020
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Aug 27, 2020
@ejgallego
[new release] coq-serapi (8.11.0+0.11.1)
cb00c63 
CHANGES:

* [general] Require dune >= 2.0 (@ejgallego, ??)
 * [serapi]  New query `Comments` to return all comments in a document
             (@ejgallego, rocq-archive/coq-serapi#20? , (partially) fixes rocq-archive/coq-serapi#191 , ejgallego/coq-serapi#200 )
 * [general] Coq's error recovery is now disabled by default
             (@ejgallego , fixes rocq-archive/coq-serapi#201)
 * [general] New option `--error-recovery` to enable error recovery
             (@ejgallego , rocq-archive/coq-serapi#203)
 * [general] Bump sexplib dependency to v0.13 (@ejgallego , rocq-archive/coq-serapi#204)
             Fixes incorrect change in 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)
             (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 , rocq-archive/coq-serapi#199)
 * [sertop]  Added option `--topfile` to `sertop` to set top name from
             a filename (rocq-archive/coq-serapi#197, @pestun)
 * [deps]    Require sexplib >= 0.12 , fixed deprecation warnings
             (rocq-archive/coq-serapi#194, @ejgallego)
 * [general] SerAPI is now tested with OCaml 4.08 and 4.09 (rocq-archive/coq-serapi#195 , @ejgallego)
 * [sertop ] Forward port sername from 0.7.1 (@ejgallego)
 * [serlib ] Fix rocq-archive/coq-serapi#212 "Segfault on universes" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#214)
 * [serapi ] Fix rocq-archive/coq-serapi#221 "Support COQPATH" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#224)
 * [sertop ] Fix rocq-archive/coq-serapi#222 "Support --indices-matter" (@ejgallego, reported by @cpitclaudel , rocq-archive/coq-serapi#223)
 * [sertop ] Fix "Stack overflow in main loop" (@pestun , rocq-archive/coq-serapi#216)
@agrarpan agrarpan mentioned this issue Sep 20, 2022
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug kind: serialization
Projects
None yet
Milestone
0.11.1
2 participants
@ejgallego @cpitclaudel