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

Are seq supported? #21

Closed
pkriens opened this issue Jun 11, 2020 · 7 comments
Closed

Are seq supported? #21

pkriens opened this issue Jun 11, 2020 · 7 comments
Labels
bug Something isn't working temporal
Milestone

Comments

@pkriens
Copy link

pkriens commented Jun 11, 2020

I was trying to use 'seq' and ran into the following syntax error on sequniv.als:

image

class edu.mit.csail.sdg.alloy4.ErrorSyntax: There are 38 possible tokens that can appear here:
! # ( * @ Int NAME NUMBER STRING String Time ^ after all always before disj eventually fun historically iden int let lone no none once one pred seq set some sum this univ { } ~ 
edu.mit.csail.sdg.parser.CompParser.syntax_error(CompParser.java:2823)
edu.mit.csail.sdg.parser.CompParser.parse(CompParser.java:2670)
edu.mit.csail.sdg.parser.CompParser.alloy_parseStream(CompParser.java:2865)
edu.mit.csail.sdg.parser.CompUtil.parse(CompUtil.java:497)
edu.mit.csail.sdg.parser.CompUtil.parseRecursively(CompUtil.java:255)
edu.mit.csail.sdg.parser.CompUtil.parseRecursively(CompUtil.java:299)
edu.mit.csail.sdg.parser.CompUtil.parseEverything_fromFile(CompUtil.java:444)
edu.mit.csail.sdg.alloy4whole.SimpleReporter$SimpleTask1.run(SimpleReporter.java:672)
edu.mit.csail.sdg.alloy4.WorkerEngine$5.run(WorkerEngine.java:462)
java.base/java.lang.Thread.run(Unknown Source)
@grayswandyr grayswandyr added the bug Something isn't working label Jul 24, 2020
@grayswandyr
Copy link
Collaborator

The issue here is that we must substitute all ' characters in legacy models (including those from util/, and seq relies on util/sequniv). Once this is done, we think seq should work but we still have to check more thoroughly.

@nmacedo nmacedo added this to the Electrum 2.1 milestone Jul 30, 2020
@nmacedo
Copy link
Member

nmacedo commented Jul 30, 2020

932943f fixed the legacy util models.

@nmacedo nmacedo closed this as completed Jul 30, 2020
@pkriens
Copy link
Author

pkriens commented Jul 31, 2020

It is a bit late but I also got some more experience now ...

I am starting to wonder if we should actually use the ' in the first place. I know people are familiar with it but I am becoming afraid that this is going to kill a lot of models out there since this is a pretty big part of Daniel's conventions in his book.

Couldn't we use a backtick (`) for the use in Electrum?

@grayswandyr
Copy link
Collaborator

As this will be a major version, I think it's acceptable to make a breaking change. But we will discuss the situation internally and see what we can do, please just be patient.

@pkriens
Copy link
Author

pkriens commented Jul 31, 2020

I am very patient :-) However, this change is larger than I thought and by using another character we bypass these issues for, imho, a very small cost.

@grayswandyr
Copy link
Collaborator

I wouldn't base my choice on this, but backticks wouldn't play nice with Markdown 😄

@pkriens
Copy link
Author

pkriens commented Jul 31, 2020

Only in the non-alloy parts. But that is an issue :-)

Although, you double the backticks in the text section:

               ``Use `code` in your Markdown file.``

Use `code` in your Markdown file.

@nmacedo nmacedo mentioned this issue Nov 13, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working temporal
Projects
None yet
Development

No branches or pull requests

3 participants