--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on October 2013 ---
Here's an update on this issue. I re-did everything with Ocaml 4.01.0. No difference. Then I tried with a 64-bit Lubuntu virtual machine, set up identically to the 32-bit version (with Ocaml 4.00.1). Then it worked. So there seems to be some defect with some module (Zarith?) in a 32-bit environment, that only comes up in very specific situations like this one. By the way, in the 64-bit linux, there was some problem with opam install building the documentation for Coq. I removed the tex packages to avoid the documentation building altogether, but there does seem to be a little bug there that someone might need to fix. -Steve On Oct 13, 2013, at 1:07 PM, Stephen Siegel <siegel at UDel.Edu> wrote: > I started with a fresh Lubtutu 32-bit VM, installed opam and everything I could using opam, using 4.00.1, still getting the same error. What I have installed: > > user at 614v5:~/examples/basic$ ocaml -version > The OCaml toplevel, version 4.00.1 > user at 614v5:~/examples/basic$ ocamlopt -version > 4.00.1 > > user at 614v5:$ more ~/.opam/4.00.1/installed > alt-ergo 0.95.2 > base-bigarray base > base-threads base > base-unix base > camlp5 6.11 > conf-gnomecanvas 2 > conf-gtksourceview 2 > coq 8.4pl2 > frama-c 20130601 > lablgtk 2.16.0 > ocamlfind 1.4.0 > ocamlgraph 1.8.3 > why 2.33 > why3 0.81 > zarith 1.2 > > > Weirdly, the example works fine on Mac OS X, even though I installed everything almost exactly the same way: > > basic$ ocaml -version > The OCaml toplevel, version 4.00.1 > basic$ ocamlopt -version > 4.00.1 > basic$ > > basic$ more ~/.opam/4.00.1/installed > alt-ergo 0.95.2 > base-bigarray base > base-threads base > base-unix base > camlp5 6.11 > conf-gnomecanvas 2 > conf-gtksourceview 2 > coq 8.4pl2 > frama-c 20130601 > lablgtk 2.16.0 > ocamlfind 1.4.0 > ocamlgraph 1.8.3 > why 2.33 > why3 0.81 > zarith 1.2 > > > The Mac is 64-bit, if that could make any difference. > > -Steve > > > On Oct 11, 2013, at 8:49 AM, Nanci Naomi <nnarai at gmail.com> wrote: > >> Hi Stephen, >> >> I have not run the example and I cannot help you, but I can say the ocaml version is old. >> >> I have the version 4.01.0 >> >> Regards >> >> Nanci Naomi >> >> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ >> Treat the Earth well. It was not given to you by your parents, >> it was loaned to you by your children. (Kenyan proverb) >> ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ >> >> >> >> On Thu, Oct 10, 2013 at 10:53 AM, Stephen Siegel <siegel at udel.edu> wrote: >> I'm doing this in linux (Ubuntu), where I do have why 2.33, and every other example I have tried works fine. But I guess I have an older ocaml? >> >> user at cisc614:~/614/frama-c/examples/basic$ ocaml -version >> The Objective Caml toplevel, version 3.12.1 >> user at cisc614:~/614/frama-c/examples/basic$ ocamlopt -version >> 3.12.1 >> >> This is what got installed by apt-get ocaml ocaml-native-compilers. apt-get thinks all these are up-to-date. >> >> -s >> >> >> >> >> >> On Oct 10, 2013, at 8:56 AM, Claude March? <Claude.Marche at inria.fr> wrote: >> >> > >> > I can't reproduce the problem. I've seen this error message in the past >> > a long time ago. (e.g. http://bts.frama-c.com/view.php?id=1003) >> > >> > >> > This may also depend on the version of OCaml. >> > I hope it will disappear when you will install why 2.33 >> > >> > - Claude >> > >> > Le 09/10/2013 22:53, Stephen Siegel a ?crit : >> >> Uncaught exception: Invalid_argument("equal: abstract value") >> > >> > -- >> > Claude March? | tel: +33 1 72 92 59 69 >> > INRIA Saclay - ?le-de-France | >> > Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ >> > F-91405 ORSAY Cedex | >> -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131016/23aeb165/attachment-0001.html>