Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006329OCamlOCaml runtime systempublic2014-02-18 10:392014-07-08 11:30
Reportergmelquiond 
Assigned Toshinwell 
PrioritylowSeveritymajorReproducibilityalways
StatusfeedbackResolutionopen 
PlatformOSOS Version
Product Version4.01.0 
Target Version4.03.0+devFixed in Version 
Summary0006329: File "camlinternalMod.ml", line 63, characters 6-12: Assertion failed.
DescriptionThere is an assertion failed in the OCaml runtime when dynamically loading a recursive module. Unfortunately, the bug is highly sensitive to conditions: changing the size of the code segment, changing the size of the data segment, changing the size of the read-only data segment, changing the number of relocations, etc, all cause the bug to vanish. As a consequence, we were unable to produce a small testcase, sorry. This bug report is mostly for the record. That said, it is perfectly reproducible and we were able to trigger it on three systems with OCaml 4.01.0 and Coq 8.4pl3.
Steps To Reproducegit clone git://scm.gforge.inria.fr/why3/why3.git [^]
cd why3
git checkout a8c13660788c726a134fab9109e384592881e8d7
autoconf
./configure
cat > src/util/config.ml << EOF
let version = "1234567812345678123456781234567812345678123456781234567812345678123456781234567"
let builddate = ""
let libdir = ""
let datadir = ""
let localdir = Some ""
let compile_time_support = [ "", ""; "", "" ]
EOF
make src/coq-tactic/.why3-vo-opt
Tagsrecmod
Attached Files

- Relationships

-  Notes
(0010963)
frisch (developer)
2014-02-20 11:36

Could it be the case that two units of the same name where dynlinked in the same process? Do you use -pack?
(0010964)
frisch (developer)
2014-02-20 11:59

$ make src/coq-tactic/.why3-vo-opt
...
...
Ocamldep src/util/extmap.ml
Ocamldep src/util/strings.ml
Ocamldep src/util/lists.ml
Ocamldep src/util/opt.ml
Ocamldep src/util/util.ml
Ocamldep src/util/config.ml
make: *** No rule to make target `src/coq-tactic/.why3-vo-opt'. Stop.


Do we need to install anything else in addition to OCaml itself?
(0010965)
gmelquiond (reporter)
2014-02-20 12:20

I don't think there are two units with the same name. (Any way to make sure?) We are using -pack, so that all our modules are submodules of Why3.

Also, you need Coq, since the dynamically-loaded module is actually a Coq plugin and it depends on various Coq modules. Due to the high sensitivity on the size of the segments and the number of relocations, I was unfortunately not able to remove Coq from the equation.
(0011590)
shinwell (developer)
2014-05-30 13:02

I tried to reproduce this, building a clean 4.01 OCaml installation, and then compiling coq-8.4pl3 from the distribution tarball. With both of the installation directories on my PATH, the configure script for why3 said:

                 Summary
-----------------------------------------
Verbose make : no
OCaml compiler : yes
    Version : 4.01.1+dev2-2013-12-18+CLOSED
    Library path : /home/mark/dev/pr/6329/ocaml/lib/ocaml
    Native compilation : yes
    Profiling : no
IDE : no (lablgtk2 not found)
Bench tool : no (sqlite3 not found)
Documentation : no (rubber not found)
Coq support : yes
    Version : 8.4pl3
    Library path : /home/mark/dev/pr/6329/coq-install/lib/coq
    "why3" tactic : no (camlp5o not found)
    Realization support : yes
        FP arithmetic : no (Flocq >= 2.2 not found)
PVS support : no (pvs not found)
Isabelle support : no (isabelle not found)
Frama-C support : no
Hypothesis selection : no (ocamlgraph not found)
Installable : yes
    Binary path : ${exec_prefix}/bin
    Lib path : ${exec_prefix}/lib/why3
    Data path : ${prefix}/share/why3
    Ocaml Library : /home/mark/dev/pr/6329/ocaml/lib/ocaml/why3
    Relocatable : no

However, I still get the same error "make: *** No rule to make target `src/coq-tactic/.why3-vo-opt'. Stop.". I think it might be because some dependency of lib/coq-tactic/why3tac.cmxs can't or won't build.

Could you please adjust the repro instructions, and then we can try again? Thanks.
(0011591)
shinwell (developer)
2014-05-30 13:17

Ah, the error was caused by missing camlp5...
(0011592)
shinwell (developer)
2014-05-30 13:55
edited on: 2014-05-30 13:58

OK, so I managed to get that make command to complete successfully.

Maybe you could prepare a tarball that includes all of the sources and objects from a tree where this bug has been observed.

Also, it would be useful if you could get this to fail having altered your OCaml source tree such that instead of just bombing out with an assertion failure, it prints the values of:
- n
- Obj.tag n
- Obj.size n
- Array.length comps


- Issue History
Date Modified Username Field Change
2014-02-18 10:39 gmelquiond New Issue
2014-02-19 20:46 doligez Tag Attached: recmod
2014-02-20 11:36 frisch Note Added: 0010963
2014-02-20 11:59 frisch Note Added: 0010964
2014-02-20 12:20 gmelquiond Note Added: 0010965
2014-05-30 13:02 shinwell Note Added: 0011590
2014-05-30 13:17 shinwell Note Added: 0011591
2014-05-30 13:55 shinwell Note Added: 0011592
2014-05-30 13:55 shinwell Assigned To => shinwell
2014-05-30 13:55 shinwell Status new => feedback
2014-05-30 13:58 shinwell Note Edited: 0011592 View Revisions
2014-07-08 11:30 doligez Target Version => 4.03.0+dev


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker