[Why3-club] Problems in compiling Why3 for Windows with Cygwin
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club