Should we we kill msg_info? What is the legitimate use case? (wondering about making its type different, to avoid confusion)

Should we we kill msg_info?

I don't think so.

What is the legitimate use case?

The one described in the API, that is information meant to be displayed in verbose mode (typically when running coqtop).

(wondering about making its type different, to avoid confusion)

The two functions are essentially doing the same thing, but correspond to different degrees of verbosity. I don't see what distinguishing them by typing would mean, TBH.

The two functions are essentially doing the same thing, but correspond to different degrees of verbosity. I don't see what distinguishing them by typing would mean, TBH.

My impression is that one of the two is used rarely, so maybe a single function with a ?if_verbose flag so that, in case you don't know, you pass the default value.

Anyway, the few examples of msg_notice you gave me (in a private chat) were variants of "foo is defined" that is not very useful, hence my questioning the entire thing.

Maybe the debug output in auto and even in ltac_profile should be priority "debug", certainly at most Info not Notice.

You mean the output of debug auto? I thought they were not Coq debug info, but rather a query to help users debug their scripts.

As per documentation, "info" essentially means that it will be displayed by coqtop's verbose mode only. Why wouldn't IDEs want to show the result of the ltac profiler?

Indeed I guess that having both notice and info is a bit confusing, OK then for notice in this case.

Ultimately trace information seems specialized enough as to have it's own request.

Indeed I guess that having both notice and info is a bit confusing

Most protocols tend to have a single information notification, however depending how you set the verbose level in the server more messages are generated then. This is normal as otherwise now all the info call are wasteful in the sense that they shouldn't run in the first place.

Ultimately trace information seems specialized enough as to have it's own request.

I agree with that, but for now it seems a "notice" is the closest indeed.

Most protocols tend to have a single information notification, however depending how you set the verbose level in the server more messages are generated then.

I also agree. It is sometimes done this way today, but via ad-hoc guards to printer calls (testing if we are in verbose/debug mode, etc). It should certainly be consolidated, but it is out of scope for this modest PR.

Any takers? @ejgallego maybe?

@gares can you take this one?