Re: any news about commit emails?
Radu Grigore
> Verbose mode seems to be broken on master - could you fix it?
> (and other debug messages)
Debug messages are activated from utils/debug.ml.
1. I'm now writing a small frontend that lets you turn almost any command
javac ARGS
into
jStar ARGS
and get something that works (running soot, looking up specs and
logics, bla-bla).
2. Next thing on my TODO is splitting backend and frontend.
3. Third is fixing error reporting. Let me know if you really need this faster.
I don't like how it works now, so I'm inclined to changed. As it is
possible I'll change it to something *you* won't like, I'll describe
briefly my plan below so you can provide feedback.
It is none of the backend's business to print *anything* to the
console; that's the frontend's job. The backend should build a list of
errors and, as a courtesy to the frontendS, provide a function
(report_error : formatter -> error -> unit) that uses some standard
format (a la gcc). There's a good practical reason too: The user
interface is important and we shouldn't need to go through the whole
code to fix it. For example, the change with json reporting for
eclipse could have been done by changing *one* file, rather that going
thru piles of files to add print statements. Since no new
functionality was added to the symbolic execution engine, one should
simply not need to touch anything in that package just so that errors
are reported in a new format as well!
That said, debugging is another matter. For debugging, print
statements through the code are useful. The mechanism used in
utils/debug.ml has the disadvantage that it requires the developer to
recompile, but has the advantage that it removes debugging code
completely from the executable when debugging is turned off. Let me
know if you prefer to allow users to debug jStar.
Finally, as it was obvious during the last meeting, I seem to have a
different opinion of what constitutes "debug info" and what
constitutes "verbose info". I didn't check, but it's likely that your
assessment of verbose/debug being "broken" really comes from me
treating as debug info what you consider verbose info. Briefly, my
opinion is that anything which can't be reported on a couple of lines
is not for the console, so I chucked it in the "debug info" category.
I'd like to know your opinion about
(1) debug info vs verbose info vs normal info
(2) Whether requiring recompilation to include/exclude debugging code
is acceptable. (Debugging code means (a) code for reporting debug info
and (b) expensive sanity/invariant checks.)
regards,
radu
Mike Dodds
Your plan for handling error reporting sounds sensible; please feel free to implement it. I'm also happy for debugging flags to be turned on / off through compilation.
My assessment of verbose mode being broken comes from the fact that -v doesn't dump the proof trace, as it used to.
My feeling is:
- verbose mode is for output useful when developing proofs, so dumping extended proof scripts during proof search is verbose mode.
- debug mode is for things that are only useful when finding bugs in the jstar code itself. So traffic between the SMT solver and the prover is debug info because it isn't ever going to be useful to end users (it either works or it doesn't).
Mike.
Radu Grigore
> verbose mode is for output useful when developing proofs,
> so dumping extended proof scripts during proof search is verbose mode.
OK, I'll move this back. In the meantime please use the seting in debug.ml.
Thanks for the feedback.