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.

Sign up for GitHub

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

Jump to bottom

Deprecate recognizing unicode versions of logical and relational symbols in the parser #3755

Closed
davidcok opened this issue Mar 17, 2023 · 1 comment · Fixed by #4023
Closed

Deprecate recognizing unicode versions of logical and relational symbols in the parser #3755

davidcok opened this issue Mar 17, 2023 · 1 comment · Fixed by #4023
Assignees
@davidcok
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: parser First phase of Dafny's pipeline

Comments

@davidcok
Copy link
Collaborator

Summary

No response

Background and Motivation

We say only ASCII text is supported in a dafny program (other than comments, strings and characters).
So we should take out this complexity.

Proposed Feature

Deprecate the symbols in the parser and eventually remove them.

Alternatives

No response
@davidcok davidcok added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Mar 17, 2023
@MikaelMayer
Copy link
Member

To the best of my knowledge, Emacs renders the symbols as icons, do you know if it actually stores them as such? I've seen someone pasting Dafny code on Stack overflow with these symbols.

@MikaelMayer MikaelMayer added the part: parser First phase of Dafny's pipeline label Mar 20, 2023
@davidcok davidcok self-assigned this Mar 21, 2023
@davidcok davidcok mentioned this issue May 16, 2023
Merged
davidcok added a commit that referenced this issue May 17, 2023
@davidcok
Removing unicode representations of mathematical symbols from the par…
12d310f 
…ser (#4023)

Fixes #3755

The documentation has long stated that only ACSII symbols are allowed in
Dafny source text (outside of strings. characters and comments). This PR
removes the representations of math symbols from the input parser.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: davidcok <[email protected]>
@ZhongRuoyu ZhongRuoyu mentioned this issue Jul 20, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@davidcok davidcok

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: parser First phase of Dafny's pipeline
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Removing unicode representations of mathematical symbols from the parser davidcok/dafny
2 participants
@MikaelMayer @davidcok