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

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


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
This error differs from time to time, depending on what item I try to
select in the project tree.

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
        task_text (try Trans.apply trans (S.goal_task g) with
          e -> eprintf "@.%a at ." Exn_printer.exn_printer e; raise e)
        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

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