-
Notifications
You must be signed in to change notification settings - Fork 86
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
bug: newlines misparsed as space in string litterals #773
Comments
FYI the culprit is this line: Lines 968 to 970 in cb23709
the upside is that this behavior is customizable. FYI, without changing PG, the following minimal-working-example fixes the issue: (*
* M-: (setq proof-shell-strip-crs-from-input nil) RET
*)
Definition foo': string :=
" a
".
Set Printing All.
Compute foo'.
(* = String (Ascii.Ascii false false false false false true false false) *)
(* (String (Ascii.Ascii true false false false false true true false) *)
(* (String (Ascii.Ascii false true false true false false false false) EmptyString)) *)
(* : string *) So as a proper fix @aa755, you can just run: M-: (customize-save-variable 'proof-shell-strip-crs-from-input nil) RET to automatically save this setting in your init file. |
Cc @ProofGeneral/core I see that the custom https://proofgeneral.github.io/doc/master/userman/Variable-Index/#Variable-Index I also see that easycrypt sets this custom to nil by default: Line 143 in cb23709
So two questions: Q1. should we just change the default to nil for Coq as well? and look for possible issues in the CI and/or from users? Q2. should we document this custom in PG's userman? saying e.g. "nil" is recommended for String-related formalizations. Other thoughts? |
This setting dates back the times when coqtop would duplicate its prompt after each newline input ad de-synch PG. |
OK thanks @Matafou ! FYI I did the following test: Running to download and run the oldest coq prebuilt in Docker-Coq, namely Coq 8.4pl6 as of April 2015. Then proving a trivial lemma while inserting spurious newlines:
And I didn't get any duplicate Does this check looks enough to you? Kind regards |
Yes. Let us test what the ci says about that. |
FYI: @vzaliva just reported a regression on Zulip that seems to indicate that my bugfix #774 was incomplete. Namely, regarding error reporting for commands that don't fit in a single line. @ProofGeneral/core I'll try to take a closer look on Monday, but feel free to investigate meanwhile if you can/wish. |
I can't have look now but it is strange: replacing each |
I can't have look now but it is strange: replacing each `\n` by a space
should not change the computation of (char) positions of errors...
Could it be some CRLF conversion biting us?
|
Had a quick look. Here are the elements:
<prompt>Coq < 12 || 0 < </prompt>Eval compute in
x * trois * trois.
Toplevel input, characters 18-19:
> x * trois * trois.
> ^
Error: The reference x was not found in the current environment. We need to delete the hackish legacy code for error location (which was using the number of spaces preceding the "^^^" and use the the "characters x-y:" information instead. Which is better anyways. |
The error location is now parsed as said above (PR #781) we can close this issue again I guess. |
Reported by @aa755 on Coq-Club:
The text was updated successfully, but these errors were encountered: