nikswamy
commented
4 years ago We've made lots of progress on warning numbers, warn_error etc.
We also have profiling knobs to control per component of the typechecker.
We still don't have a principled internal debug log facility. But, this is a facility for a better developer experience rather than a user experience.
Closing this issue
original title: An error reporting and diagnostics logging framework, with tunable levels
CH: we could take some inspiration from the F5 type derivation viewer, some screenshots here: http://www.infsec.cs.uni-saarland.de/projects/F5 Generally, I think a tree view is much better suited for displaying this kind of data than a huge sequential log.
NS: Doing something like those screenshots would be terrific! It sounds like a BIG effort though and is likely to take a while, including some invasive work on the type-checker to make sure that such contexts are made available. I'd prefer to do that after we stabilize the checker for the school (and would be happy to make this kind of visualization a priority thereafter).
NS: in the short term, I was just thinking that it would be good to clean up the way in which we're reporting errors. For example, assign unique error codes to all of them; classify some as errors, others as warnings; provide flags to disable certain warnings; etc. On the diagnostic side, the code is littered with (if debug env Options.Low/Med/High then printf "...") ... which is really ugly. Can we adopt some more principled logging framework?
CH: I'll have a look at the existing logging frameworks for OCaml and F# [..] and then report back. I've started a Google Doc about this here: https://docs.google.com/document/d/16Y_kl9yx505siu8BWh7Hc7xDR0UeX-OLX9ZS4HemH0Q/edit?usp=sharing Please let me know if you want edit access to it.