[coq 8.7] [serious] errors don't block `proof-assert-next` and we can continue asserting after error. #175

ejgallego · 2017-04-07T00:16:37Z

I would reopen #173 but I don't have the rights.

After coq/coq#530, Coq will always wrap errors in the markers, and put position information before. However, PG fails with this setting as now errors don't stop the buffer anymore.

So it seems I tried to guess wrong here; I am OK implementing whatever error output specification you want for -emacs, just let me know.

The text was updated successfully, but these errors were encountered:

ejgallego · 2017-04-08T12:47:23Z

Indeed removing the "emacs specific quoting" around the error fixed this problem:

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index ee55366..0b8d3a5 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -259,7 +259,7 @@ let init_color_output () =
    - Warning/Error: emacs_quote_err
    - Notice: unquoted
  *)
-let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+let emacs_logger = gen_logger emacs_quote_info (fun x -> x)
 
 (* Output to file, used only in extraction so a candidate for removal *)
 let ft_logger old_logger ft ?loc level mesg =

still waiting to see what you folks want before committing any further change to Coq.

cpitclaudel · 2017-04-12T20:31:55Z

I'm not sure I understand the problem, unfortunately. @Matafou, do you know what the issue is?

ejgallego · 2017-04-12T22:29:59Z

@cpitclaudel I think the issue is simple: what is the error format PG expects from Coq?

Once you let us know, we will implement that in Coq. In the past, Coq emitted errors in 2 different ways when -emacs was enabled, sometimes without "quoting" , and sometimes with it.

@JasonGross has suggested that maybe the markers maybe should not be present, but I am not sure anymore.

Thanks for having a look to this.

ejgallego · 2017-04-12T22:47:34Z

BTW I'll be happy to chat on Coq's gitter if you folks think we can make progress that way.

cpitclaudel · 2017-04-12T23:36:09Z

Ah, got it. Pierre introduced these markers, IIRC, so he'll know better than me. My understanding was that some things were to be displayed in real time, and other were to be displayed once processing was complete, and that was why there were two kinds?

ejgallego · 2017-04-12T23:45:28Z

I can't tell. Al Coq error messages in -emacs currently follow the pattern:

(location_info\n)?
(program_caret\n)?
MARKER[254]Error: msgMARKER[255]

where A? is an optional component (may not be present) and MARKER[X] is ASCII X. We can tweak that as needed. location_info is the typical

Toplevel input, characters 5-6:

and program_caret is:

> Goal I.
>      ^

Note that in the past, such messages where also produced without the markers (*), hence the bug as PG seems to handle only those correctly.

(*) Whether an error message contained the marker used to depend on the Coq component originating it.

cpitclaudel · 2017-04-12T23:50:37Z

Ok. I don't know enough about this then. Let's wait for @Matafou

Matafou · 2017-04-13T22:51:50Z

Sorry guys I am in holidays currently. Will have a look next week. P Le mer. 12 avr. 2017 à 16:50, Clément Pit-Claudel <notifications@github.com> a écrit :

…

Ok. I don't know enough about this then. Let's wait for @Matafou <https://github.com/Matafou> — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#175 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEsl6gpjWAuqkjt5S7PCJEoI6N1GFNaaks5rvWNNgaJpZM4M2UTU> .

ejgallego · 2017-04-19T00:02:20Z

A good example of the discrepancy in 8.6 is Print a vs Print Module a.

Matafou · 2017-04-19T16:53:43Z

OK I am currently looking at this.

They are two different issues IIUW:

detecting error messages
parsing error location for highlighting the source

point 2) should rework once 1) is solved but it uses space counting whereas now toplevel gives a position which is easier to parse. So I may switch to this and let the space counting code for compatibility. No hurry though.

point 1) is broken because indeed error where not tagged at all before (It was only for warnings). The regexp detecting errors are not triggered anymore because they assume that for instance "Error:" appears at the beginning of a line, but now the special character is make this fail.

So yes removing the special characters is OK.

By the way @ejgallego why is "really painful" in topfmt.ml?

(* XXX: This is really painful! *)
module Emacs = struct

  (* Special chars for emacs, to detect warnings inside goal output *)
  let emacs_quote_start = String.make 1 (Char.chr 254)
  let emacs_quote_end   = String.make 1 (Char.chr 255)

  let emacs_quote_err g =
    hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)

  let emacs_quote_info_start = "<infomsg>"
  let emacs_quote_info_end = "</infomsg>"

  let emacs_quote_info g =
    hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)

end

ejgallego · 2017-04-19T17:00:39Z

@Matafou ok, let me know the desired specification in terms of the components I described in my previous messages and I'll update the printing system immediately.

why is "really painful"

This comment was added back in 8.5 -> 8.6 , but IIRC it was not particularly aimed at the emacs stuff but indeed at the general feedback/pp situation at the time. -emacs mode was indeed problematic to handle for:

no documentation or specification wrt to what emacs expects,
same errors printed in different ways (see again Print vs Print Module),
global flag print_emacs scattered over all the system,
the quoting is arbitrary (special chars vs tags vs nothing) and doesn't follow message structure,
emacs output format is not designed to be parsed back, (what happens if the error msg contains ^Error ?)
duplicate loggers.

Matafou · 2017-04-20T10:07:30Z

@Matafou ok, let me know the desired specification in terms of the components I described in my previous messages and I'll update the printing system immediately.

Thanks Emilio.

You mean this?:

(location_info\n)?
(program_caret\n)?
MARKER[254]Error: msgMARKER[255]

Please just remove MARKER[254] and MERGKER[255] for now.

I will ask for removal of program_caret once I have implement the parsing of location_info.

I may ask for a special tag ahead of Error: but I need to modify pg generic code to hide it from response buffer first.

why is "really painful"
This comment was added back in 8.5 -> 8.6 , but IIRC it was not particularly aimed at the emacs stuff but indeed at the general feedback/pp situation at the time. -emacs mode was indeed problematic to handle for:

no documentation or specification wrt to what emacs expects,

Indeed it is poorly documented. You can find a bit in coqloop@193 about prompts.

same errors printed in different ways (see again Print vs Print Module),

Indeed, currently pg regexp for coq errors is:

"^\\(In nested Ltac call\\|Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"

If you simplify this i am all for it.

global flag print_emacs scattered over all the system,

True.

the quoting is arbitrary (special chars vs tags vs nothing) and doesn't follow message structure,

The generic mechanism of pg needs tags around warnings if one wants to see them when scritping several commands at once. On the contrary errors are considered to stop at the next prompt so we only need to recognize the beginning of an error message. Again this comes from he minimlity principle.

emacs output format is not designed to be parsed back

Indeed, only the content of goals and response buffers try to be parseable, not the content of coq session.

, (what happens if the error msg contains ^Error ?)

Not sure to understand what you mean here. If you mean that error message are not recognizable enough I agree.

duplicate loggers.

Isn't the whole point of loggers to have several ones?

Matafou · 2017-04-20T15:32:26Z

Sorry now that I tested things by myself I think we need to do something a bit more complex because the current behaviour of pg is not satisfying concerning the display of all kinds of messages.

In loggers there are 5 kinds of messages. Debug, Info, Notice, Warning and Error.

In pg we have 3 levels of messages:

messages that correspond to a real error that interrupted pg script processing, always display everything from that message to the next prompt.
warning messages that must be printed even during the processing of several commands
Other informational messages that should be hidden when not processing the last command of a group of commands.

Let us make this clean on pg side and adapt the emacs logger to that, I propose that the 5 coq levels are displayed like this 3 pg levels:

Errors:
(location_info\n)?
(program_caret\n)?
Error: msg
Warnings:
(location_info\n)?
(program_caret\n)?
Error: msg
Notice and info and debug:
(location_info\n)?
(program_caret\n)?
Error: msg

@ejgallego I can do it if you want.

@ejgallego what is the meaning of these negative locations? I have seen acomment about that elsewhere but can't remember

Matafou · 2017-04-20T15:44:42Z

Should info be hidden when "Set Silent" is set? Currently I see these messages.

Matafou · 2017-04-20T16:42:52Z

Eeeeh and why are goals diplayed as "Debug" messages???

Sorry but I am a bit puzzled by the current state of loggers...

Matafou · 2017-04-20T16:57:18Z

@ejgallego I think we need to meet IRL for this. I will be at Sophie Germain friday 28 maybe we can have 30 minutes discussion at that moment?

ejgallego · 2017-04-20T17:14:26Z

Indeed, currently pg regexp for coq errors is:

"^\\(In nested Ltac call\\|Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)"
If you simplify this i am all for it.

Indeed now all the errors are of that form, and always include the header Error: .

The generic mechanism of pg needs tags around warnings if one wants to see them when scritping several commands at once.

Note again that some errors (such as Print Module a where quoted as warnings, this is where the problem originates, as in resolving the duality of errors I chose to follow the behavior of Print Module a.

Not sure to understand what you mean here. If you mean that error message are not recognizable enough I agree.

I meant this. This is in fact the reason I resolved the ambiguity opting to add the markers. I didn't realize PG was already buggy for errors with markers (such as Print Module a).

Isn't the whole point of loggers to have several ones?

Well that has to be handled with care, in the past in particular we had several loggers and different paths were taken for errors even under the same flags. There are some examples in the bugzilla.

Let us make this clean on pg side and adapt the emacs logger to that, I propose that the 5 coq levels are displayed like this 3 pg levels:

Sorry I don't understand what you mean here as all the levels are similar, note that PG in the past used at least 4 modes not 3. [<infomsg> tag, nothing, marker, Error + misc headers]

Feel free to submit a PR of course.

@ejgallego what is the meaning of these negative locations? I have seen acomment about that elsewhere but can't remember

This is due to ltac semantics reporting the error in the definition of tactics. Previously these messages were reported as unlocated or with the wrong location. Now the offset to the current sentence is computed accurately wrt the input buffer.

Should info be hidden when "Set Silent" is set? Currently I see these messages.

That is a good question, do you have an example illustrating a change of behavior wrt 8.6?

Eeeeh and why are goals diplayed as "Debug" messages???

Are you sure you are in trunk?

@ejgallego I think we need to meet IRL for this. I will be at Sophie Germain friday 28 maybe we can have 30 minutes discussion at that moment?

I think 28 may work for me.

Matafou · 2017-04-20T20:03:49Z

Eeeeh and why are goals diplayed as "Debug" messages???
Are you sure you are in trunk?

This one was my fault.

ejgallego · 2017-04-20T21:38:06Z

This one was my fault.

Well, it was my fault but I fixed it quickly :D anyways we've merged quite a few commits trying to consolidate the printing structure and indeed some new bugs have been exposed, please bear with us, it is basically very hard to test this kind of interactive use.

In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. This fixes ProofGeneral for trunk users. c.f. ProofGeneral/PG#175

ejgallego · 2017-04-21T13:20:31Z

Ok I've submitted coq/coq#581 so Coq trunk becomes usable to PG users. IMHO the current rules are pretty clear from the code itself:

let gen_logger dbg warn ?pre_hdr level msg = match level with
  | Debug   -> msgnl_with !std_ft (make_body dbg   dbg_hdr ?pre_hdr msg)
  | Info    -> msgnl_with !std_ft (make_body dbg  info_hdr ?pre_hdr msg)
  | Notice  -> msgnl_with !std_ft (make_body noq  info_hdr ?pre_hdr msg)
  | Warning -> Flags.if_warn (fun () ->
               msgnl_with !err_ft (make_body warn warn_hdr ?pre_hdr msg)) ()
  | Error   -> msgnl_with !err_ft (make_body noq   err_hdr ?pre_hdr msg)

that is to say, Debug and Info get treated by the dbg quoter, warnings by the warn one, and Error and Notice are left untreated.

Matafou · 2017-04-21T17:09:00Z

Looks good to me. Thanks @ejgallego !

Now that we are back to previous behavour (fixed and more uniform), I must say that don't like those special chars because they may confuse emacs in presence of unicode. I would like to replace them by <warning></warning>.

ejgallego · 2017-04-21T18:34:10Z

Your call folks, I thought that the quoting behavior of the past would make more sense.

I would like to replace them by .

by?

Matafou · 2017-04-22T22:48:45Z

Sorry, edited my last message.

ejgallego · 2017-04-23T00:37:33Z

<warning></warning> sounds fine, do you want that change pushed now?

Matafou · 2017-04-23T08:07:37Z

Yes please. P. Le dim. 23 avr. 2017 à 02:37, Emilio Jesús Gallego Arias < notifications@github.com> a écrit :

…

<warning></warning> sounds fine, do you want that change pushed now? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#175 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEsl6p7hvcfsXUgyh19UemG2rVKDgEquks5ryp1NgaJpZM4M2UTU> .

In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. This fixes ProofGeneral for trunk users. c.f. ProofGeneral/PG#175

In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. We also update the warnings quoter to use a warning tag instead of a non-printable char. This fixes ProofGeneral for trunk users. c.f. ProofGeneral/PG#175

ejgallego · 2017-04-23T12:36:33Z

PR updated.

In 8.6 + emacs, errors were quoted sometimes with special markers (e.g. `Print Module foo.` for a non-existing `foo`) In 8.7 we uniformized error handling and now all errors are quoted, however, this behavior confuses emacs as it seems that the quotes are meant to be applied only to warnings. We thus reflect the de-facto situation, removing quoting for errors and updating the code so it is clear that the quoter is a warnings quoter. We also update the warnings quoter to use a warning tag instead of a non-printable char. This fixes ProofGeneral for trunk users. c.f. ProofGeneral/PG#175

Matafou · 2017-04-24T09:29:48Z

Ready for merging imho.

ejgallego · 2017-04-24T09:47:30Z

@Matafou did you mean to comment on coq/coq#581 ?

Matafou · 2017-04-24T09:58:55Z

Yes sorry.

ejgallego · 2017-04-24T15:33:47Z

Ok so I think we can consider this fixed for now, it works for me! However you may want to update the warning detection code in PG I guess.

Matafou · 2017-04-24T15:44:33Z

It is already updated in PG/master. People will have to update their pg to see all warning. This desreves a word in CHANGE probably. P. 2017-04-24 17:33 GMT+02:00 Emilio Jesús Gallego Arias < notifications@github.com>:

…

Closed #175 <#175>. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#175 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEsl6kdpYF1uv5HpitaK51wR81VqBEFyks5rzMDcgaJpZM4M2UTU> .

ejgallego · 2017-04-24T15:49:19Z

Cool thanks. There is still time to improve -emacs if you feel like needing some other stuff.

Matafou · 2017-04-24T16:31:25Z

Hopefully Proofgeneral/xml will replace -emacs soon and we may remove -emacs option in a near future.

ejgallego changed the title ~~In coq 8.7, errors don't proof-assert-next~~ In coq 8.7, errors don't block proof-assert-next and we can continue asserting after error. Apr 7, 2017

ejgallego changed the title ~~In coq 8.7, errors don't block proof-assert-next and we can continue asserting after error.~~ [coq 8.7] [serious] errors don't block proof-assert-next and we can continue asserting after error. Apr 7, 2017

ejgallego mentioned this issue Apr 21, 2017

[toplevel] [emacs] Don't quote errors in emacs mode. coq/coq#581

Merged

ejgallego closed this as completed Apr 24, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[coq 8.7] [serious] errors don't block `proof-assert-next` and we can continue asserting after error. #175

[coq 8.7] [serious] errors don't block `proof-assert-next` and we can continue asserting after error. #175

ejgallego commented Apr 7, 2017 •

edited

Loading

ejgallego commented Apr 8, 2017

cpitclaudel commented Apr 12, 2017

ejgallego commented Apr 12, 2017

ejgallego commented Apr 12, 2017

cpitclaudel commented Apr 12, 2017

ejgallego commented Apr 12, 2017 •

edited

Loading

cpitclaudel commented Apr 12, 2017

Matafou commented Apr 13, 2017 via email

ejgallego commented Apr 19, 2017

Matafou commented Apr 19, 2017 •

edited

Loading

ejgallego commented Apr 19, 2017 •

edited

Loading

Matafou commented Apr 20, 2017 •

edited

Loading

Matafou commented Apr 20, 2017

Matafou commented Apr 20, 2017

Matafou commented Apr 20, 2017

Matafou commented Apr 20, 2017

ejgallego commented Apr 20, 2017

Matafou commented Apr 20, 2017

ejgallego commented Apr 20, 2017

ejgallego commented Apr 21, 2017 •

edited

Loading

Matafou commented Apr 21, 2017 •

edited

Loading

ejgallego commented Apr 21, 2017

Matafou commented Apr 22, 2017

ejgallego commented Apr 23, 2017

Matafou commented Apr 23, 2017 via email

ejgallego commented Apr 23, 2017

Matafou commented Apr 24, 2017

ejgallego commented Apr 24, 2017 •

edited

Loading

Matafou commented Apr 24, 2017

ejgallego commented Apr 24, 2017

Matafou commented Apr 24, 2017 via email

ejgallego commented Apr 24, 2017

Matafou commented Apr 24, 2017

[coq 8.7] [serious] errors don't block proof-assert-next and we can continue asserting after error. #175

[coq 8.7] [serious] errors don't block proof-assert-next and we can continue asserting after error. #175

Comments

ejgallego commented Apr 7, 2017 • edited Loading

ejgallego commented Apr 8, 2017

cpitclaudel commented Apr 12, 2017

ejgallego commented Apr 12, 2017

ejgallego commented Apr 12, 2017

cpitclaudel commented Apr 12, 2017

ejgallego commented Apr 12, 2017 • edited Loading

cpitclaudel commented Apr 12, 2017

Matafou commented Apr 13, 2017 via email

ejgallego commented Apr 19, 2017

Matafou commented Apr 19, 2017 • edited Loading

ejgallego commented Apr 19, 2017 • edited Loading

Matafou commented Apr 20, 2017 • edited Loading

Matafou commented Apr 20, 2017

Matafou commented Apr 20, 2017

Matafou commented Apr 20, 2017

Matafou commented Apr 20, 2017

ejgallego commented Apr 20, 2017

Matafou commented Apr 20, 2017

ejgallego commented Apr 20, 2017

ejgallego commented Apr 21, 2017 • edited Loading

Matafou commented Apr 21, 2017 • edited Loading

ejgallego commented Apr 21, 2017

Matafou commented Apr 22, 2017

ejgallego commented Apr 23, 2017

Matafou commented Apr 23, 2017 via email

ejgallego commented Apr 23, 2017

Matafou commented Apr 24, 2017

ejgallego commented Apr 24, 2017 • edited Loading

Matafou commented Apr 24, 2017

ejgallego commented Apr 24, 2017

Matafou commented Apr 24, 2017 via email

ejgallego commented Apr 24, 2017

Matafou commented Apr 24, 2017

[coq 8.7] [serious] errors don't block `proof-assert-next` and we can continue asserting after error. #175

[coq 8.7] [serious] errors don't block `proof-assert-next` and we can continue asserting after error. #175

ejgallego commented Apr 7, 2017 •

edited

Loading

ejgallego commented Apr 12, 2017 •

edited

Loading

Matafou commented Apr 19, 2017 •

edited

Loading

ejgallego commented Apr 19, 2017 •

edited

Loading

Matafou commented Apr 20, 2017 •

edited

Loading

ejgallego commented Apr 21, 2017 •

edited

Loading

Matafou commented Apr 21, 2017 •

edited

Loading

ejgallego commented Apr 24, 2017 •

edited

Loading