Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
119
Issues
119
List
Boards
Labels
Service Desk
Milestones
Merge Requests
16
Merge Requests
16
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
b0c5c8d7
Commit
b0c5c8d7
authored
Jul 16, 2012
by
Andrei Paskevich
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
IDE: reorganize debug output
parent
75871d67
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
74 additions
and
57 deletions
+74
-57
src/ide/gconfig.ml
src/ide/gconfig.ml
+13
-12
src/ide/gconfig.mli
src/ide/gconfig.mli
+2
-0
src/ide/gmain.ml
src/ide/gmain.ml
+53
-36
src/util/debug.ml
src/util/debug.ml
+1
-1
src/util/debug.mli
src/util/debug.mli
+5
-8
No files found.
src/ide/gconfig.ml
View file @
b0c5c8d7
...
...
@@ -24,6 +24,8 @@ open Util
open
Rc
open
Whyconf
let
debug
=
Debug
.
register_flag
"ide_info"
let
()
=
Debug
.
set_flag
debug
(* config file *)
...
...
@@ -138,7 +140,7 @@ let load_ide section =
ide_error_color
=
get_string
section
~
default
:
default_ide
.
ide_error_color
"error_color"
;
ide_iconset
=
ide_iconset
=
get_string
section
~
default
:
default_ide
.
ide_iconset
"iconset"
;
ide_default_editor
=
...
...
@@ -239,6 +241,7 @@ let load_config config original_config =
*)
(*
let debug_save_config n c =
let coq = { prover_name = "Coq" ; prover_version = "8.3pl3";
prover_altern = "" } in
...
...
@@ -246,9 +249,10 @@ let debug_save_config n c =
let time = Whyconf.timelimit (Whyconf.get_main c) in
Format.eprintf "[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
n time p.editor
*)
let
save_config
t
=
eprintf
"[Info] saving IDE config file@."
;
Debug
.
dprintf
debug
"[Info] saving IDE config file@."
;
(* taking original config, without the extra_config *)
let
config
=
t
.
original_config
in
(* copy possibly modified settings to original config *)
...
...
@@ -298,9 +302,9 @@ let config,read_config =
|
None
->
invalid_arg
"configuration not yet loaded"
|
Some
conf
->
conf
)
,
(
fun
conf_file
extra_files
->
eprintf
"[Info] reading IDE config file...@?"
;
(*Debug.dprintf debug "[Info] reading config file...@?";*)
let
c
=
read_config
conf_file
extra_files
in
eprintf
" done.@."
;
(*Debug.dprintf debug " done.@.";*)
config
:=
Some
c
)
let
save_config
()
=
save_config
(
config
()
)
...
...
@@ -349,7 +353,7 @@ let why_icon = ref !image_default
let
image
?
size
f
=
let
main
=
get_main
()
in
let
n
=
let
n
=
Filename
.
concat
(
datadir
main
)
(
Filename
.
concat
"images"
(
f
^
".png"
))
in
...
...
@@ -466,11 +470,11 @@ let resize_images size =
()
let
init
()
=
eprintf
"[Info] reading icons...@?"
;
Debug
.
dprintf
debug
"[Info] reading icons...@?"
;
load_icon_names
()
;
why_icon
:=
image
"logo-why"
;
resize_images
20
;
eprintf
" done.@."
Debug
.
dprintf
debug
" done.@."
let
show_legend_window
()
=
let
dialog
=
GWindow
.
dialog
~
title
:
"Why3: legend of icons"
()
in
...
...
@@ -837,7 +841,7 @@ let editors_page c (notebook:GPack.notebook) =
try
Meditor
.
find
s
map
with
Not_found
->
assert
false
in
(*
Format.eprintf
"prover %a : selected editor '%s'@." *)
(*
Debug.dprintf debug
"prover %a : selected editor '%s'@." *)
(* print_prover p data; *)
let
provers
=
Whyconf
.
get_provers
c
.
config
in
c
.
config
<-
...
...
@@ -905,7 +909,7 @@ let run_auto_detection gconfig =
()
*)
(*
let () = eprintf "[Info] end of configuration initialization@."
*)
(*
let () = Debug.dprintf debug "[Info] end of configuration initialization@."
*)
let
uninstalled_prover
c
eS
unknown
=
try
...
...
@@ -1080,9 +1084,6 @@ let replace_prover c to_be_removed to_be_copied =
res
*)
let
read_config
conf_file
extra_files
=
read_config
conf_file
extra_files
;
init
()
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
...
...
src/ide/gconfig.mli
View file @
b0c5c8d7
...
...
@@ -48,6 +48,8 @@ type t =
val
read_config
:
string
option
->
string
list
->
unit
(** None use the default config *)
val
init
:
unit
->
unit
val
save_config
:
unit
->
unit
val
config
:
unit
->
t
...
...
src/ide/gmain.ml
View file @
b0c5c8d7
...
...
@@ -21,20 +21,14 @@
open
Format
let
()
=
eprintf
"[Info] Init the GTK interface...@?"
;
ignore
(
GtkMain
.
Main
.
init
()
);
eprintf
" done.@."
open
Why3
open
Whyconf
open
Gconfig
open
Util
open
Debug
module
C
=
Whyconf
let
debug
=
register_flag
"gui"
let
debug
=
Debug
.
register_flag
"ide_info"
let
()
=
Debug
.
set_flag
debug
(************************)
(* parsing command line *)
...
...
@@ -42,9 +36,11 @@ let debug = register_flag "gui"
let
includes
=
ref
[]
let
file
=
ref
None
let
opt_parser
=
ref
None
let
opt_version
=
ref
false
let
opt_config
=
ref
None
let
opt_extra
=
ref
[]
let
opt_list_formats
=
ref
false
let
spec
=
Arg
.
align
[
(
"-L"
,
...
...
@@ -62,6 +58,12 @@ let spec = Arg.align [
" same as -C"
;
"--extra-config"
,
Arg
.
String
(
fun
s
->
opt_extra
:=
!
opt_extra
@
[
s
])
,
"<file> Read additional configuration from <file>"
;
"-F"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
"<format> Select input format (default:
\"
why
\"
)"
;
"--format"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
" same as -F"
;
"--list-formats"
,
Arg
.
Set
opt_list_formats
,
" List known input formats"
;
(*
("-f",
Arg.String (fun s -> input_files := s :: !input_files),
...
...
@@ -98,6 +100,24 @@ let () =
let
()
=
Gconfig
.
read_config
!
opt_config
!
opt_extra
let
()
=
C
.
load_plugins
(
get_main
()
)
let
()
=
Debug
.
Opt
.
set_flags_selected
()
;
if
Debug
.
Opt
.
option_list
()
then
exit
0
let
()
=
if
!
opt_list_formats
then
begin
let
print1
fmt
s
=
fprintf
fmt
"%S"
s
in
let
print
fmt
(
p
,
l
)
=
fprintf
fmt
"%s [%a]"
p
(
Pp
.
print_list
Pp
.
comma
print1
)
l
in
printf
"@[<hov 2>Known input formats:@
\n
%a@]@."
(
Pp
.
print_list
Pp
.
newline
print
)
(
List
.
sort
Pervasives
.
compare
(
Env
.
list_formats
()
));
exit
0
;
end
let
fname
=
match
!
file
with
|
None
->
Arg
.
usage
spec
usage_str
;
...
...
@@ -105,6 +125,12 @@ let fname = match !file with
|
Some
f
->
f
let
()
=
Debug
.
dprintf
debug
"[Info] Init the GTK interface...@?"
;
ignore
(
GtkMain
.
Main
.
init
()
);
Debug
.
dprintf
debug
" done.@."
;
Gconfig
.
init
()
let
(
why_lang
,
any_lang
)
=
let
main
=
get_main
()
in
let
load_path
=
Filename
.
concat
(
datadir
main
)
"lang"
in
...
...
@@ -116,7 +142,7 @@ let (why_lang, any_lang) =
let
why_lang
=
match
languages_manager
#
language
"why"
with
|
None
->
Format
.
eprintf
"language file for 'why' not found in directory %s@."
eprintf
"language file for 'why' not found in directory %s@."
load_path
;
exit
1
|
Some
_
as
l
->
l
in
...
...
@@ -150,14 +176,6 @@ let gconfig =
*)
c
let
()
=
C
.
load_plugins
(
get_main
()
)
let
()
=
Debug
.
Opt
.
set_flags_selected
()
;
if
Debug
.
Opt
.
option_list
()
then
exit
0
(***************)
(* Main window *)
(***************)
...
...
@@ -356,7 +374,7 @@ let () =
view_time_column
#
set_visible
true
let
goals_model
,
goals_view
=
eprintf
"[Info] Creating tree model...@?"
;
Debug
.
dprintf
debug
"[Info] Creating tree model...@?"
;
let
model
=
GTree
.
tree_store
cols
in
let
view
=
GTree
.
view
~
model
~
packing
:
scrollview
#
add
()
in
let
()
=
view
#
selection
#
set_mode
(* `SINGLE *)
`MULTIPLE
in
...
...
@@ -364,7 +382,7 @@ let goals_model,goals_view =
ignore
(
view
#
append_column
view_name_column
);
ignore
(
view
#
append_column
view_status_column
);
ignore
(
view
#
append_column
view_time_column
);
eprintf
" done@."
;
Debug
.
dprintf
debug
" done@."
;
model
,
view
...
...
@@ -699,17 +717,19 @@ let project_dir, file_to_read =
begin
if
Sys
.
is_directory
fname
then
begin
eprintf
"[Info] found directory '%s' for the project@."
fname
;
Debug
.
dprintf
debug
"[Info] found directory '%s' for the project@."
fname
;
fname
,
None
end
else
begin
eprintf
"[Info] found regular file '%s'@."
fname
;
Debug
.
dprintf
debug
"[Info] found regular file '%s'@."
fname
;
let
d
=
try
Filename
.
chop_extension
fname
with
Invalid_argument
_
->
fname
in
eprintf
"[Info] using '%s' as directory for the project@."
d
;
Debug
.
dprintf
debug
"[Info] using '%s' as directory for the project@."
d
;
d
,
Some
(
Filename
.
concat
Filename
.
parent_dir_name
(
Filename
.
basename
fname
))
end
...
...
@@ -720,8 +740,8 @@ let project_dir, file_to_read =
let
()
=
if
not
(
Sys
.
file_exists
project_dir
)
then
begin
eprintf
"[Info] '%s' does not exists. Creating directory of that name
\
for the project@."
project_dir
;
Debug
.
dprintf
debug
"[Info] '%s' does not exists.
\
Creating directory of that name
for the project@."
project_dir
;
Unix
.
mkdir
project_dir
0o777
end
...
...
@@ -762,7 +782,7 @@ let () =
let
sched
=
try
eprintf
"[Info] Opening session...@
\n
@[<v 2>
"
;
Debug
.
dprintf
debug
"@[<hov 2>[Info] Opening session...@
\n
"
;
let
session
=
if
Sys
.
file_exists
project_dir
then
S
.
read_session
project_dir
else
S
.
create_session
project_dir
in
...
...
@@ -773,7 +793,7 @@ let sched =
let
sched
=
M
.
init
(
Whyconf
.
running_provers_max
(
Whyconf
.
get_main
gconfig
.
config
))
in
dprintf
debug
"@]@
\n
[Info] Opening session: done@."
;
Debug
.
dprintf
debug
"@]@
\n
[Info] Opening session: done@."
;
session_needs_saving
:=
false
;
current_env_session
:=
Some
env
;
sched
...
...
@@ -783,7 +803,6 @@ let sched =
exit
1
(**********************************)
(* add new file from command line *)
(**********************************)
...
...
@@ -793,10 +812,10 @@ let () =
|
None
->
()
|
Some
fn
->
if
S
.
PHstr
.
mem
(
env_session
()
)
.
S
.
session
.
S
.
session_files
fn
then
dprintf
debug
"[Info] file %s already in database@."
fn
Debug
.
dprintf
debug
"[Info] file %s already in database@."
fn
else
try
dprintf
debug
"[Info] adding file %s in database@."
fn
;
Debug
.
dprintf
debug
"[Info] adding file %s in database@."
fn
;
ignore
(
M
.
add_file
(
env_session
()
)
fn
)
with
e
->
eprintf
"@[Error while reading file@ '%s':@ %a@.@]"
fn
...
...
@@ -804,8 +823,6 @@ let () =
exit
1
(*****************************************************)
(* method: run a given prover on each unproved goals *)
(*****************************************************)
...
...
@@ -908,7 +925,7 @@ let select_file () =
|
None
->
()
|
Some
f
->
let
f
=
Sysutil
.
relativize_filename
project_dir
f
in
eprintf
"Adding file '%s'@."
f
;
Debug
.
dprintf
debug
"Adding file '%s'@."
f
;
try
ignore
(
M
.
add_file
(
env_session
()
)
f
)
with
e
->
...
...
@@ -956,7 +973,7 @@ let (_ : GMenu.image_menu_item) =
(*
Mprover.iter
(fun p pi ->
Format.eprintf
"editor for %a : %s@." Whyconf.print_prover p
Debug.dprintf debug
"editor for %a : %s@." Whyconf.print_prover p
pi.editor)
(Whyconf.get_provers gconfig.config);
*)
...
...
@@ -966,7 +983,7 @@ let (_ : GMenu.image_menu_item) =
let
add_refresh_provers
f
_msg
=
(*
eprintf
"[Info] recording '%s' for refresh provers@." msg;
Debug.dprintf debug
"[Info] recording '%s' for refresh provers@." msg;
*)
let
rp
=
!
refresh_provers
in
refresh_provers
:=
(
fun
()
->
rp
()
;
f
()
)
...
...
@@ -980,7 +997,7 @@ let (_ : GMenu.image_menu_item) =
let
save_session
()
=
if
!
session_needs_saving
then
begin
eprintf
"[Info] saving session@."
;
Debug
.
dprintf
debug
"[Info] saving session@."
;
S
.
save_session
gconfig
.
config
(
env_session
()
)
.
S
.
session
;
session_needs_saving
:=
false
;
end
...
...
@@ -1529,7 +1546,7 @@ let edit_selected_row r =
let c = e.Session.whyconf in
let p = Mprover.find coq (get_provers c) in
let time = Whyconf.timelimit (Whyconf.get_main c) in
Format.eprintf
Debug.dprintf debug
"[debug] save_config %d: timelimit=%d ; editor for Coq=%s@."
0 time p.editor;
*)
...
...
src/util/debug.ml
View file @
b0c5c8d7
...
...
@@ -94,7 +94,7 @@ module Opt = struct
if
stop
then
Format
.
fprintf
fmt
"%s *"
p
else
Format
.
pp_print_string
fmt
p
in
Format
.
printf
"@[<hov 2>Known debug flags \
(
* mark flags which change the behavior)
:@
\n
%a@]@."
(
`*' marks the flags that change Why3 behavior)
:@
\n
%a@]@."
(
Pp
.
print_list
Pp
.
newline
print
)
(
List
.
sort
Pervasives
.
compare
list
);
end
;
...
...
src/util/debug.mli
View file @
b0c5c8d7
...
...
@@ -22,14 +22,12 @@ type flag
(* Flag used for debugging only part of Why3 *)
val
register_flag
:
string
->
flag
(** Register a new flag. If someone try to register two times the same
flag the same one is used *)
(** Register a new flag. It is allowed to register twice the same flag *)
val
register_stop_flag
:
string
->
flag
(** Register a new stop flag. If someone try to register two times the same
flag the same one is used.
A stop flag should be used when a flag change the behavior of the program.
It is not setted by debug-all *)
(** Register a new stop flag. It is allowed to register twice the same flag.
A stop flag should be used when a flag changes the behavior of Why3.
Such flags are not set by --debug-all. *)
val
lookup_flag
:
string
->
flag
val
list_flags
:
unit
->
(
string
*
flag
*
bool
)
list
...
...
@@ -69,8 +67,7 @@ module Opt : sig
val
option_list
:
unit
->
bool
(** Print the list of debug flag if requested (in this case return [true]).
You should run this function after the plugins have been started.
*)
You should run this function after the plugins have been loaded. *)
val
desc_debug_all
:
spec
(** Option for setting all the debug flags except the stopping one *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment