segfault apparently due to dynlink'ed code (both native and bytecode) #4707
Comments
|
Comment author: @xavierleroy Thanks for the nice repro case. I had no problems observing the crash on Linux/amd64. The "value_interp" function in tacinterp.ml receives as argument the integer 0 while it expects a block. Since I'm old and experienced, I grepped "Obj.magic" in contrib/subtac, and lo and behold I found one in subtac_obligations.ml: let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) Naughty, naughty boys :-) Replacing this line with let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId []) causes the compilation of RelationClasses.v not to segfault, but report a more meaningful error: File "/home/estephe/xleroy/coq-11875/theories/Classes/RelationClasses.v", My guess is that Subtac_obligations.set_default_tactics is not called at the right times when dynamic loading is activated. I don't know whether that's a bug in Coq's sources or whether it points out to an unwanted semantic difference between Caml's static and dynamic linking. Could you please investigate on Coq's side and let me know what you find? |
|
Comment author: letouzey Hi Xavier, Thanks for the help with this issue, which is indeed 100% due to our stuff, Additionally, naughty boys will be dully notified of your discovery of this Sorry for the disturbance... Pierre |
Original bug ID: 4707
Reporter: letouzey
Assigned to: @xavierleroy
Status: closed (set by @xavierleroy on 2009-02-05T09:54:02Z)
Resolution: not a bug
Priority: normal
Severity: major
Version: 3.11.0
Category: ~DO NOT USE (was: OCaml general)
Bug description
Hi
While converting some parts of the Coq system into dynlink'able
plugins, I've encountered the following issue: while other plugins
work great, the one containing Subtac (the work of Matthieu Sozeau,
also known as Program) triggers a segfault when processing one of the
file of the Coq Standard Library. The same Subtac code works well when
compiled statically into Coq. This segfault appears to be
reproducible both with native and bytecode ocaml 3.11, either on amd64
or x86. I haven't tried yet with (bytecode) dynlink of earlier
versions of ocaml.
For the moment, to reproduce the bug, I'm afraid I can only point to
the Coq source, see below. I plan to investigate more the issue, so I
might be able to exhibit later a smaller testcase. Anyway D. Doliguez
encouraged me to report this matter early. Last disclaimer: it may
perfectly happen that my construction of subtac_plugin.cma does
something wrong (or some part of Matthieu's code ?), but if it is the
case, an error message nicer than segfault would be nice...
Steps to reproduce:
for instance today's svn revision 11875) :
svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk/ -r 11875
cd trunk
by applying the small patch attached to this bug-report
patch -p1 < activate_subtac_as_plugin.patch
./configure -local -debug -opt
check that (nat)dynlink has been selected :
grep HASNATDYNLINK config/Makefile
launch the build:
make
This currently fails on file theories/Classes/RelationClasses.v
By default, the build is done via native coqtop.opt. The bytecode version
can be build via "make bin/coqtop.byte" and then used via:
bin/coqtop.byte -l theories/Classes/RelationClasses.v
Best regards,
Pierre Letouzey
File attachments
The text was updated successfully, but these errors were encountered: