Show diffs in some error messages

[jfehrle]

Kind: feature.
Fixes: #8366

• Corresponding documentation was added (including any warning and error messages added).
• Entry added in CHANGES.md.

Show diffs for error messages that compare 2 similar values (when diffs are enabled).

For example, instead of:

it will be easier to pick out the differences between the "Unable to unify" expressions if they're highlighted:

In CoqIDE:

[ejgallego]

That's a very cool feature, however I'm afraid that we must rethink the diffing strategy; this kind of state in Lexer will be frowned upon in 8.10.

I can try to have a look later, but going back to my question on the first ever diff PR: why are we not doing diffs over a Pp.t ? Maybe you want to implement a different rendering method Pp.t -> diff_structure, what would be fine. However, having to re-lex seems indeed problematic [and will get more] as the lexer is not designed for this use case.

[jfehrle]

I was more looking for comments on changing Xmlprotocol--what that entails, how to do that cleanly without breaking, say, PG.

Of course, let's discuss the lexer stuff, but if it requires much change to the diff code, I'll drop this idea. It's not worth the trouble to me. The concept was to do diffs on a token basis; Pp.t isn't necessarily grouped by tokens.

[ejgallego]

Is it reasonable to change Xmlprotocol.pr_value_gen so the Fail case returns a Pp.t? That would mean PG and other clients would need some changes.

I think you could extend the return message so you send both the Pp.t and the string version. This may not be too optimal tho, but at least it is easy to be compatible that way.

Regarding the lexer I guess you could build a special entry point if you still want to diff at the token level, but I guess I'd be better if you could avoid this special mode.

Why you need it anyways?

[jfehrle]

I think you could extend the return message so you send both the Pp.t and the string version. This may not be too optimal tho, but at least it is easy to be compatible that way.

If the client and server negotiate what protocol version to use, I would create a new Fail2 return type with a Pp.t. I see there is a protocol_version field in Xmlprotocol.ml, but I didn't see a negotiation.

Suppose I modify Coq to return (string, Pp.t) for a Fail. I expect an old, unmodified PG will not understand that and so won't show any error message for a Fail. That seems like a crippling issue. One approach to address this is for the client to announce what version of the XML protocol it wants to use, and then the server uses that version or tells the client it can't communicate with it. (One could also infer that if the client doesn't announce what protocol version it wants, it must want the old protocol.) Only 2 versions need to be supported in any version of Coq--just enough decoupling of software versions so you don't need to simultaneously update both Coq and PG (and any other clients using the protocol).

Is there such a mechanism already? If not, I don't know how much work this would require for Coq--or whether we expect to enhance the XML protocol for other purposes (which might help justify the effort, if significant). I think this is the bigger part of the work needed to complete this PR.

Why you need it anyways?

Diffing at the token level is a much better match for how users read and think about these expressions than diffing at the character level. If a step replaces x with x0, you would want to see x0 marked as as changed rather than just the 0 as changed. Nor do you want the variable name i matched to the middle character of a new reference to min (marking only m and n as changed).

A Pp.t can contain an arbitrary series of strings; there's no guarantee that a Ppcmd_string contains a single token. It could contain part of one token or multiple tokens. Passing it through the lexer gives you tokens.

The changes to the lexer shown here are quite small. I would expect providing the additional entry point in a new lexer would be similarly small. Is it necessary to delay any work on this until this new lexer is available--which I expect would be several to many months from now? When will the new lexer be available?

Do other developers agree that rewriting the lexer is a priority?

[ejgallego]

I mean why do you need this specific change in the lexer.

[ppedrot]

I agree with @ejgallego that we should not increase the technical debt by adding more imperative state to the lexer. I also agree that we should perform the diff at the level of the pretty-printing AST, the current situation is clearly a hack. More generally, the diff feature is very hacky. I was not against inclusion for the end-users to quickly take advantage of it, but it would be great to polish it and remove many ugly details.

[Zimmi48]

Just to be clear in passing: PG (the version that most users rely on anyways) does not use the XML protocol. There is a branch which uses it but it's hard to know what its future will be given that the person who developed it is not around anymore. So while greater stability of the protocol would be an improvement, it's not something that matters much right now.

[jfehrle]

I pushed a new version that removes the additional state, instead passing a flag when initializing the lexer.

I mean why do you need this specific change in the lexer.

When adding the diff highlights to the Pp.t, the code needs to have the character sequence of the tokens match (ignoring white space) the character sequence of the string passed to the lexer. That's so it can match the diff output to the Pp.t and, if necessary, split Pp.t strings that don't correspond to a single token.

For example, passing the quoted string "abc" returns the token abc, which doesn't match because it omits the " marks. The changed code will return tokens ", abc and ", which does match.

[jfehrle]

it would be great to polish it and remove many ugly details.

I would be interested to hear your suggestions for improvements. As I've said before, I'm new to OCaml. I've not found any useful style guidelines for OCaml--if you know of such, please let me know.

(On the other hand, there are many things in Coq that deserve to be improved. Is it better to address some of those other areas or to perfect the diffs code?)

[jfehrle]

Just to be clear in passing: PG (the version that most users rely on anyways) does not use the XML protocol.

OK, then we can change the XML protocol freely, assuming CoqIDE is the only client?

Nonetheless I'd also want to look at the PG interface and make sure it can handle Pp.t's in error messages. Would you point me to the protocol code PG uses?

[ppedrot]

I've not found any useful style guidelines for OCaml--if you know of such, please let me know.

It is not so much about the OCaml style than the specific guidelines of the Coq codebase, which unluckily are not quite written down but mostly passed by oral tradition in the PR comments and heated discussions on gitter or IRL. Note that they do change from a dev to another, even though we try to be somewhat consensual. As a general rule of thumb regarding your recent PRs, I'd highlight that:

• we try to be as pure as possible (in particular care is taken not to introduce global variables except if there is a very good reason),
• glob_constr should only be used internally or as an intermediate representation
• UI specific features should not contaminate lower layers, and more generally one should stick to maximal separation of concerns

OK, then we can change the XML protocol freely, assuming CoqIDE is the only client?

I'd personally say that indeed you can. So far we didn't care about compatibility of the protocol across Coq versions.

[gares]

Nonetheless I'd also want to look at the PG interface and make sure it can handle Pp.t's in error messages. Would you point me to the protocol code PG uses?

PG master branch uses no protocol, it just calls coqtop and parses the output using regexes, eg to detect when a goal is printer rather than when an error is. Yes, you have not misunderstood...

PG server-protocol branch (IIRC the name) uses the very same XML protocol of CoqIDE. The code is known to work but also to have some bugs. If you are fluent in emacs lisp, you are surely welcome working/fixing on that code, but beware it is not the code most people run when they say PG.

[gares]

I'd personally say that indeed you can.

I agree too. If it is not the case, please add a version number to the protocol. I think I did it. Or maybe I forgot it. There is an init message, the version could go in there.

[Zimmi48]

The protocol is documented here and indeed it contains a version number.

[gares]

Thanks for helping my bad memory, About tells you the protocol version.

[jfehrle]

Please review. I updated the description. I was able to do this without changing the lexer (I'll make that a separate PR). Also, xmlprotocol.md already passes a Pp.t for Fail--I was mistaken on that.

[Zimmi48]

I am not sure what is the point of requiring the user to turn diffs on (most users probably won't most of the time) to see diffs in error messages. It seems useful even to users who do not want diffs between successive goals (and it definitely sounds like two unrelated things).

[ejgallego]

A problem with the diff code is that it likes to die on quite a few inputs, it seems.

[Zimmi48]

Yes but if there are such issues we will be more likely to detect them before 8.10 if this is activated by default. If this code path is never used in our tests, it is more likely to bitrot quickly.

[ejgallego]

IMHO the code needs significant work before is activated by default; also, it has the potential to increase compile time largely, so I guess we would be best served by specific tests.

[Zimmi48]

In any case, it doesn't make sense to use the same option for diffs between successive goals and diffs in error messages, because the former should never be made the default while the latter should (as soon as it is realistic to do so).

[jfehrle]

I am not sure what is the point of requiring the user to turn diffs on (most users probably won't most of the time) to see diffs in error messages.

That makes sense; I would do that, though I would hope that users turn on diffs more often. In coqtop, we would need to check that -color on was specified on the command line.

A problem with the diff code is that it likes to die on quite a few inputs, it seems.

No. I'm pretty careful about not breaking things for users:

1. The values that are being compared in proof steps and in messages are terms and are unlikely to include the few input sequences that are not handled yet. Make diffs work for more input strings #8734 addresses those.
2. In the unlikely case that the diff fails, it prints the message without diff highlighting and an additional message saying that diff failed. The user impact is negligible.

I guess we would be best served by specific tests.

Automatic testing is an interesting challenge. I included a .v file that generates an example message (for a manual test). Do we have a mechanism in place to verify that coqtop output contains the message?

IMHO the code needs significant work before is activated by default

Specifics please?

it has the potential to increase compile time largely

Huh?

[jfehrle]

If the user enters Set Diffs "on"when color is not enabled, no textual markers will appear in the output. If coqtop accepts the command in this case, the user will not see any diffs or any change in behavior at all, likely causing confusion and creating the impression that diffs don't work. Not a good result. It's much friendlier to give a message explaining why diffs can't be enabled. Proof_diffs only looks at the color setting for this specific purpose; the diff algorithm is color-blind.

Surely there is some reasonable way to show the warning message "Enabling Diffs requires setting the \"-color\" command line argument to "on" or "auto"." in this case. I've tried to suggest alternatives that you might find palatable. Or is a minor wart in the code more important to you than a better user experience? @ejgallego, what are your thoughts?

[jfehrle]

@ejgallego Would you respond to my last comments, which are from 4 weeks ago? Thanks.

[jfehrle]

Ping @herbelin, @ejgallego

This PR has been waiting for two months for a response from Emilio to my last comments. If there's no response within a week or so, would it be reasonable to proceed to merging this?

[ejgallego]

This PR has been waiting for two months for a response from Emilio to my last comments. If there's no response within a week or so, would it be reasonable to proceed to merging this?

My comments still hold AFAICS, I am not happy with Proff_diffs learning about the existence of terminal-specific data.

[jfehrle]

Would you respond more specifically to what I said? I was not just repeating myself in my last comment. My comment deserves a bit more thought and more of a response.

From the very long delay and your terse comments, one might think that you don't value the proposal or my comments very highly. Or perhaps you're just too busy?

[ejgallego]

I do value your proposal a lot @jfehrle , in fact I'd like to provide some more detailed feedback, but I am just too busy as to get a long enough slot for it to happen sorry :( :(

[ejgallego]

I wish I could provide you with a date but I'm afraid I can't at the moment :S

[herbelin]

@jfehrle: I'm trying to understand the status of the PR. At the level of the user interaction, the current status is:

• -color on or -color auto, and -diffs on: diff for error messages is used
• -color off, and -diffs on: error -color on needed

Otherwise, at the level of the code, could it be possible to use less references so that the possible interaction between flags is easier to follow. Ideally, could we have global references (such as term_color or diff_option) set only at the level of Coqtop.init_toplevel and having even init_color be purely functional?

I mean, this is per se more general than this PR, but could this PR not add more side effects than there is already (e.g. no write_color_enabled but instead write_diffs_option taking the status of color as an extra explicit argument)?

PS: As a side example of having little structure in option, if I do, say, coqc -list-tags foo.v, or coqtop -list-tags -where, the command line options after -list-tags are silently ignored. Shouldn't it be an error instead? It seems that Coqargs.t should instead be somewhere a type of the form:

type t = coq_init_pre * coq_init_main * coq_init_post
type coq_batch_action = Query of coq_query_option | DeprecatedCompile of string list
type coq_action = Batch of coq_bacth_action | Interactive

[jfehrle]

@herbelin The unresolved issue is how Coq can generate an error message if the user enters Set Diffs "on" when -color was not enabled on the command line. If color is not enabled and the user turns on diffs, they won't see anything highlighted, which would make them think the feature is broken. It would not be obvious that they should enable -color.

Implementing this requires preserving the state of -color in a global variable so it can be accessed later when the user enters Set Diffs "on". @ejgallego seemed to be against the idea of preserving this state at all. (In an earlier version of the code, the diff code would skip computing diffs if -color was not enabled. My last change removed that dependency--diffs are now computed regardless of -color and the terminal layer decides what to do with the diff highlights.)

The color-enabled variable should be set to true when Coq is run from CoqIDE since CoqIDE assumes color; there is no command-line setting for color.

The options for such a global variable are:

1. Put it in coqtop.ml. I believe referencing the global from proof_diffs.ml would create a prohibited circular linking relationship between the source files, so not feasible.
2. Create a new source file to hold the color setting that can be set from coqtop.ml and accessed by proof_diffs.ml. This is workable, though I'm not eager to create a new one-line source file.
3. Put the global in proof_diffs.ml, which is what's in the current code.

I'm agnostic about the details of the code as long as there's a way to generate the error message in this use case.

could we have global references (such as term_color or diff_option) set only at the level of Coqtop.init_toplevel and having even init_color be purely functional?

diffs_option holds the setting for the Set Diffs command. It needs to be set whenever the user changes that setting. init_color could be made purely functional but then the caller(s) would still need to save the info about whether color is enabled--just moving the problem up one level.

could this PR not add more side effects than there is already (e.g. no write_color_enabled but instead write_diffs_option taking the status of color as an extra explicit argument)?

write_diffs_option is called by the standard option-setting code. I expect adding an additional argument would not work with the option-setting code.

Let me know your thoughts, thanks.

[herbelin]

The options for such a global variable are:

1. Put it in coqtop.ml. I believe referencing the global from proof_diffs.ml would create a prohibited circular linking relationship between the source files, so not feasible.
2. Create a new source file to hold the color setting that can be set from coqtop.ml and accessed by proof_diffs.ml. This is workable, though I'm not eager to create a new one-line source file.
3. Put the global in proof_diffs.ml, which is what's in the current code.

I'm agnostic about the details of the code as long as there's a way to generate the error message in this use case.

Question (a naive one because I did not investigate all places from where the diff mode is called): would it work to have if Proof_diffs.show_diffs () then ... in coqloop.ml turned into if Proof_diffs.show_diffs () && terminal_enable_diff () then ... be possible, with terminal_enable_diff defined somewhere, in coqtop.ml or terminal.ml?

Would this answer @ejgallego's argument (with which I sympathetize) that diffing should not know about color?

Let me know your thoughts, thanks.

I have otherwise more general thoughts.

On one side, options are already stored in references dispatched in several files such as Flags, Dumpglob, System, Mltop, ... and I feel we should rather target a functional view at options rather than adding new indirect dependences into global variables. Now, I would need more than 5 minutes to propose a solution. So, I understood that @ejgallego want to eventually make a proposal within a couple of weeks, so maybe can we wait for his proposal.

If ever it takes more time, merging the PR as it is seems to be a good solution, keeping in mind that a model where options are treated functionally and generically may eventually be adopted (see #9585 which I just created about this), avoiding in particular proof_diffs.ml to know about colors.

[jfehrle]

Question (a naive one because I did not investigate all places from where the diff mode is called): would it work to have if Proof_diffs.show_diffs () then ... in coqloop.ml turned into if Proof_diffs.show_diffs () && terminal_enable_diff () then ... be possible, with terminal_enable_diff defined somewhere, in coqtop.ml or terminal.ml?

No, this wouldn't help--I already changed the code so the compute/print diffs part doesn't examine the color setting at all. The color setting is used only to generate a warning to the user when they try to Set Diffs "on".

On one side, options are already stored in references dispatched in several files such as Flags, Dumpglob, System, Mltop, ... and I feel we should rather target a functional view at options rather than adding new indirect dependences into global variables.

I'd be interested in seeing any proposal.

So, I understood that @ejgallego want to eventually make a proposal within a couple of weeks, so maybe can we wait for his proposal.

If ever it takes more time, merging the PR as it is seems to be a good solution

I'll wait to hear from @ejgallego in early March. We can consider merging as-is after that if the substantive discussion doesn't happen. In any case, let's get some form of this PR into master before 8.10 starts--a one-year delay (if it's not in 8.10) on shipping this seems unreasonable.

[ejgallego]

Hi @jfehrle , sorry for the delay on handling this, I had the impression that it would take me more than than it did; I still have some wishes w.r.t. general code organization of the diffs feature, but IMHO they should not block this patch which can be merged now.

I still believe that the diffs code should be agnostic to the output device, and the algorithm's domain changed, but surely these concerns can be addressed later [some of them will hopefully be when I get a slot to rebase #8728