Original bug ID: 5049
Reporter: @glondu
Assigned to: @alainfrisch
Status: closed (set by @xavierleroy on 2013-08-31T10:46:23Z)
Resolution: not a bug
Priority: normal
Severity: feature
Platform: ARM
Category: ~DO NOT USE (was: OCaml general)
Monitored by: mehdi "Julien Signoles"
Bug description
Hello,
While rebuilding all Debian packages (armel port) with ocamlopt enabled (using trunk r10396), ssreflect failed to build. The full build log is available at [1].
The following command crashes with a segmentation fault:
/usr/bin/coqc -dump-glob theories/ssreflect.glob -q -R src Ssreflect -R theories Ssreflect theories/ssreflect
It uses (nat)dynlink. The bytecode counterpart (by adding "-byte") doesn't segfault. Generating a Coq toplevel with ssreflect statically linked in (with "coqmktop -opt -o ssrcoq src/ssreflect.cmx"), and then using it (by adding "-image ./ssrcoq" to the command above) doesn't segfault either.
Running ocsigen in native code on arm also segfaults:
root@daribow:/tmp# ocsigen.opt -V
-- Dependencies of ocsigen.ext.staticmod: ocsigen.commandline, camlp4, ocsigen.ext.staticmod
-- Needed: /usr/lib/ocaml/ocsigen/parsecommandline.cmxs, /usr/lib/ocaml/ocsigen/staticmod.cmxs
Loading extension /usr/lib/ocaml/ocsigen/parsecommandline.cmxs
Loading extension /usr/lib/ocaml/ocsigen/staticmod.cmxs
Segmentation fault
These errors don't happen on amd64.
Cheers,
--
Stéphane
Additional information
[1] http://ocaml.debian.net/debian/ocaml3120dev23r10396/failures/ssreflect_1.2%2Bdfsg-4%2B3.12.0%2Bdev23%2B10396%2B1_armel.build
Original bug ID: 5049
Reporter: @glondu
Assigned to: @alainfrisch
Status: closed (set by @xavierleroy on 2013-08-31T10:46:23Z)
Resolution: not a bug
Priority: normal
Severity: feature
Platform: ARM
Category: ~DO NOT USE (was: OCaml general)
Monitored by: mehdi "Julien Signoles"
Bug description
Hello,
While rebuilding all Debian packages (armel port) with ocamlopt enabled (using trunk r10396), ssreflect failed to build. The full build log is available at [1].
The following command crashes with a segmentation fault:
/usr/bin/coqc -dump-glob theories/ssreflect.glob -q -R src Ssreflect -R theories Ssreflect theories/ssreflect
It uses (nat)dynlink. The bytecode counterpart (by adding "-byte") doesn't segfault. Generating a Coq toplevel with ssreflect statically linked in (with "coqmktop -opt -o ssrcoq src/ssreflect.cmx"), and then using it (by adding "-image ./ssrcoq" to the command above) doesn't segfault either.
Running ocsigen in native code on arm also segfaults:
These errors don't happen on amd64.
Cheers,
--
Stéphane
Additional information
[1] http://ocaml.debian.net/debian/ocaml3120dev23r10396/failures/ssreflect_1.2%2Bdfsg-4%2B3.12.0%2Bdev23%2B10396%2B1_armel.build