Add message format cli option

[W95Psp]

This PR adds a --message_format option to the CLI that can be human or JSON, defaulting to human.

When --message_format is set to JSON, error reports and profiling messages are done in JSON.

[mtzguido]

Hi Lucas, this looks great! I'll take a deeper look soon (I'm phone-only right now) and merge it.

Wondering, is this for the Hax playground?

[W95Psp]

Thanks! I've actually just forced push this, made it a little better and I added support for JSON-output for profiling-related messages.

Ah :) this is both for the playground and for something I've wanted to make for such a long time: a build system & package manager for F* 😄

[mtzguido]

Hi Lucas, took another look and this seems perfect to me. (I want to add a jsonable class which would be useful here btw.)

Just one thing, I noticed this also changes the format for the output of profiling info.

$ ./bin/fstar.exe X.fst --message_format json --profile X --profile_component '*'
{"tag":"Prims","counter":{"id":"FStar.Universal.extend_tcenv","total_time":5,"running":false,"undercount":false}}
{"tag":"Prims","counter":{"id":"FStar.CheckedFiles","total_time":1,"running":false,"undercount":false}}
{"tag":"Prims","counter":{"id":"FStar.Parser.Dep.discover","total_time":0,"running":false,"undercount":false}}
{"tag":"Prims","counter":{"id":"FStar.Parser.Dep.topological_dependences_of","total_time":0,"running":false,"undercount":false}}
{"tag":"FStar.Pervasives.Native","counter":{"id":"FStar.Universal.extend_tcenv","total_time":14,"running":false,"undercount":false}}
{"tag":"FStar.Pervasives.Native","counter":{"id":"FStar.CheckedFiles","total_time":10,"running":false,"undercount":false}}
{"tag":"FStar.Pervasives","counter":{"id":"FStar.Universal.extend_tcenv","total_time":18,"running":false,"undercount":false}}
{"tag":"FStar.Pervasives","counter":{"id":"FStar.CheckedFiles","total_time":6,"running":false,"undercount":false}}
{"msg":["Expected expression of type Prims.int\ngot expression ()\nof type Prims.unit"],"level":"Error","range":{"def":{"file_name":"X.fst","start_pos":{"line":3,"col":12},"end_pos":{"line":3,"col":14}},"use":{"file_name":"X.fst","start_pos":{"line":3,"col":12},"end_pos":{"line":3,"col":14}}},"number":189,"ctx":["While typechecking the top-level declaration `let uu___0`"]}
1 error was reported (see above)

Would a field like kind in each json message be useful to distinguish what each line represents? I guess clients can look at the presence of "counter" or "level" instead. Maybe that less-structured convention is fine in the json world? : )

[W95Psp]

Ah, I wanted to make a jsonable class as well!

Same thing, I was thinking about that and was thinking having unstructured JSON data was pretty bad.
I was a bit too shy to make big changes, but I was roughly thinking about the following design:

• introduce a FStar.Diagnostics module
• in that module have a diagnostic type where each variant is a kind of diagnostic (profiling, error, "proof done message", etc.)
• the variants of diagnostic should carry the data that represent the message, not the message itself: rendering of messages should be made by FStar.Diagnostics, not by anything else
• have one function print (or something) of type diagnostics -> unit, that prints the error and takes care of the JSON/human logic

Things would be much nicer, we could move from mostly string/document based errors and messages to well structured ADT messages. What do you think?

[mtzguido]

Yeah I had in mind something very similar to that, modularizing all output into a single module that takes care of formatting, coloring, etc. But I think that's for another PR... probably pretty invasive.

I pushed a patch here to also try --message_format json in tests/error-messages. If you think this looks good, I can rebase and merge it, and then we can brainstorm about improvements.

[W95Psp]

Yes, let's do a follow up PR, but indeed, would love to see all those ad-hoc reports go away in favor of a single ADT the stores all the information.

Great, thank you, that's a great idea, that looks good :) let's merge then!