[Why3-club] Problems in compiling Why3 for Windows with Cygwin

Vyacheslav Napadovsky napadovskiy at gmail.com
Tue Nov 5 09:17:39 CET 2013


Hello.

I have a problem after I've successfully compiled Why3ide for Windows.
After running the IDE with, for example, krakatoa 1.java, I have no data
into bottom right textbox.
Moreover, there is an error appears every time I want to select any item to
proof.
https://dl.dropboxusercontent.com/u/39984835/why3ide/error_capture.jpg
This error differs from time to time, depending on what item I try to
select in the project tree.
https://dl.dropboxusercontent.com/u/39984835/why3ide/error_capture2.JPG

Please, can you give me any instructions about how I can debug this error?
I've already using --debug-all flag for why3ide, but information provided
via that flag is not enough.
I've also noticed that Printexc.print_backtrace doesn't print the function
calls history inside why3ide.
And the error appears somewhere around here in ide\gmain.ml (line 536):

let intro_transformation = "introduce_premises"
let update_task_view a =
  let text =
  match a with
    | S.Goal g ->
      if (Gconfig.config ()).intro_premises then
        let trans =
          Trans.lookup_transform intro_transformation (env_session()).S.env
        in
        task_text (try Trans.apply trans (S.goal_task g) with
          e -> eprintf "@.%a at ." Exn_printer.exn_printer e; raise e)
      else
        task_text (S.goal_task g)

Does it related to missing text into right-bottom textbox?

Ocaml version used is 4.00.1.
I'm newbie in Ocaml, so any advices would be great!

P.S. I've also posted this question at
http://stackoverflow.com/questions/19743889/ocaml-bugs-during-why3-usage

Regards,
Vyacheslav Napadovsky
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131105/6681e2f6/attachment.html>


More information about the Why3-club mailing list