Skip to content
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

Add command line option to treat batch files as individual lines in interactive mode #1006

Closed
benjaminselfridge opened this issue Dec 10, 2020 · 2 comments · Fixed by #1010
Closed
Assignees
Labels
feature request Asking for new or improved functionality

Comments

@benjaminselfridge
Copy link
Contributor

benjaminselfridge commented Dec 10, 2020

This would add an additional flag for the -b FILE batch mode for cryptol, which would have the effect of reverting to the old behavior. That behavior includes both:

  • using <interactive> as the file name in error messages
  • not tracking line numbers in error messages (so any error is reported as occurring on "line 1", regardless of where it appeared in the file)

The reason I need this is to keep the error messages in Programming Cryptol consistent with what the actual error message output would be.

As an example, suppose we have a file in.cry containing the following:

  True
  false
  False : Bit
  if True && False then 0x3 else 0x4
  False || True
  (True && False) ^ True
  ~False
  ~(False || True)

When I run cryptol -b in.cry, I get the following output:

True
[error] at in.icry:2:1--2:6 Value not in scope: false
False
0x4
True
True
True
False

I'd like this flag to have the effect of changing the above output to:

True
[error] at <interactive>:1:1--1:6 Value not in scope: false
False
0x4
True
True
True
False
@benjaminselfridge benjaminselfridge added the feature request Asking for new or improved functionality label Dec 10, 2020
@robdockins
Copy link
Contributor

What if we add a separate --interactive-batch = <FILE> option instead of having another option that changes the semantics of -b? I don't think it makes much difference, but is maybe a little bit cleaner.

@benjaminselfridge
Copy link
Contributor Author

Yeah, I like that better.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature request Asking for new or improved functionality
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants