You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Although I'm working on Windows, I generally set up my git repositories to use unix line endings.
Trying to translate the following from pluscal to tlaplus:
--------------------------- MODULE foo ---------------------------
(*--algorithm upgrade
begin
skip;
end algorithm;*)
=============================================================================
gives "Unrecoverable error: Text on same line following *) that ends the comment containing the algorithm". Which is puzzling, partly because it's rather awkwardly phrased so that I'm not completely sure what it's trying to tell me - but mostly because I think that whatever it is trying to tell me is not true.
As I say, I set up my git to commit with LF endings. So I've also had fun where I write a spec that's valid, commit it, and then find that it doesn't work any more. The error that I see then is usually "Unrecoverable error: No line containing `END TRANSLATION". But I can see quite clearly that there is such a line.
This has all been very confusing to debug.
It would be great if the toolbox was agnostic about line endings; if that's not possible, it would be helpful if it could give more useful errors in such cases.
The text was updated successfully, but these errors were encountered:
It looks as though the toolbox now re-dos-es the file before performing translation - is that what you're expecting?
While that's not completely ideal - I'd prefer that the toolbox was truly agnostic about the line endings and would leave my file using whichever format it found - it's certainly a huge improvement on the cryptic errors that I was seeing when I reported this.
I'm using version 1.57 of the toolbox.
Although I'm working on Windows, I generally set up my git repositories to use unix line endings.
Trying to translate the following from pluscal to tlaplus:
gives "Unrecoverable error: Text on same line following
*)
that ends the comment containing the algorithm". Which is puzzling, partly because it's rather awkwardly phrased so that I'm not completely sure what it's trying to tell me - but mostly because I think that whatever it is trying to tell me is not true.As I say, I set up my git to commit with LF endings. So I've also had fun where I write a spec that's valid, commit it, and then find that it doesn't work any more. The error that I see then is usually "Unrecoverable error: No line containing `END TRANSLATION". But I can see quite clearly that there is such a line.
This has all been very confusing to debug.
It would be great if the toolbox was agnostic about line endings; if that's not possible, it would be helpful if it could give more useful errors in such cases.
The text was updated successfully, but these errors were encountered: