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

Update Alloy DSL for Alloy 6 #1963

Closed
wants to merge 33 commits into from
Closed

Update Alloy DSL for Alloy 6 #1963

wants to merge 33 commits into from

Conversation

hwayne
Copy link
Contributor

@hwayne hwayne commented Nov 17, 2021

Last Tuesday Alloytools released a new, backwards-incompatible version. The biggest change is that ' is now an operator and no longer a valid identifier token. The team is encouraging people to use " instead, which the current Pygments lexer assumes automatically starts a string.

This change adds the new keywords, modifies how the lexer handles ", and closes an edge case in using strings for fact definitions. See commit messages for further details on each.

not-my-profile and others added 18 commits November 17, 2021 10:19
Accessibility by default is important.

The colors with a too low contrast were adjusted just
so much that they match the required contrast of 4.5.

Part of pygments#1718.
* Correctly identify whitespace.
* Merge consecutive tokens where possible.
* Consistently use String.Double for the opening and closing quotation
  marks
Correctly identify whitespace.
Use a simpler expression to match comments in HTML/XML.
wcag-contrast-ratio is now a build-time dependency for the docs.
Some dark styles did not define a color for every token type,
resulting in black text (the browser default for text) on dark
backgrounds (defined by the styles) unless the web page had some
CSS to remedy that like:

  body { color: white; background: black; }

We however don't want the readability of styles to rely on external CSS.

Part of pygments#1718. Fixes some unreadable styles reported in pygments#1526.
@hwayne
Copy link
Contributor Author

hwayne commented Nov 22, 2021

Ooop, looks like I didn't notice the Alloy tests, will fix

Alloy (http://alloytools.org/) facts can take a string token in addition
to an identifier. This is because the name isn't actually used for
facts, it's just for readability.

This is technically undocumented behavior, but it's widely used in
legacy specs and is handled this way in the official Alloy IDE.
Alloy 6 adds temporal logic to Alloy. This includes the following
keywords:

* Three new symbols: `'` (prime), `..` (step interval), and `;` (sequential composition)
* Five future-time keywords: `always`, `after`, `eventually`, `until`,
  `releases`
* Five past-time keywords: `historically`, `before`, `once`, `since`,
  `triggered`
* A new `steps` keyword for specifying a range to model check.

See here for full changes: https://alloytools.org/alloy6.html
Legacy alloy uses `'` to distinguish variables:

    all b, b': Foo | bar

But since Alloy 6 makes `'` into an operator, the new recommendation is
to use `"`:

    all b, b": Foo | bar

See
https://alloytools.org/alloy6.html#compatibility-with-pre-6-models.

The lexer currently reads `b"` as starting a string. This commit fixes
this by only having `"` begin a string if it's the start of a token.

Additionally, `'` is removed from identifiers.
Alloy 6 recommends changing `'` in legacy specs to `"`. Since this is a
breaking change, the golden test is updated to reflect that.
@hwayne
Copy link
Contributor Author

hwayne commented Dec 15, 2021

Running regexlint locally doesn't seem to trigger an error. Is there a specific way I should be running it?

@Anteru
Copy link
Collaborator

Anteru commented Dec 27, 2021

@birkenfeld Do you have an idea what might be going on here?

@jeanas
Copy link
Contributor

jeanas commented Mar 7, 2022

I get the error locally with an up-to-date checkout of regexlint:

/home/jean/repos/pygments/pygments/lexers/dsls.py:641: (AlloyLexer:root:pat#17) E105: Potential out of order alternation between '\\.' and '\\.\\.'
              (r'!|#|&&|\+\+|<<|>>|>=|<=>|<=|\.|\.\.|->', Operator),
                                                ^ here

It seems sensible because this regex will never match .. as the first . already matches \..

@jeanas jeanas added the update needed Waiting for an update from the PR/issue creator label Mar 16, 2022
Alloy (http://alloytools.org/) facts can take a string token in addition
to an identifier. This is because the name isn't actually used for
facts, it's just for readability.

This is technically undocumented behavior, but it's widely used in
legacy specs and is handled this way in the official Alloy IDE.
Alloy 6 adds temporal logic to Alloy. This includes the following
keywords:

* Three new symbols: `'` (prime), `..` (step interval), and `;` (sequential composition)
* Five future-time keywords: `always`, `after`, `eventually`, `until`,
  `releases`
* Five past-time keywords: `historically`, `before`, `once`, `since`,
  `triggered`
* A new `steps` keyword for specifying a range to model check.

See here for full changes: https://alloytools.org/alloy6.html
Legacy alloy uses `'` to distinguish variables:

    all b, b': Foo | bar

But since Alloy 6 makes `'` into an operator, the new recommendation is
to use `"`:

    all b, b": Foo | bar

See
https://alloytools.org/alloy6.html#compatibility-with-pre-6-models.

The lexer currently reads `b"` as starting a string. This commit fixes
this by only having `"` begin a string if it's the start of a token.

Additionally, `'` is removed from identifiers.
Alloy 6 recommends changing `'` in legacy specs to `"`. Since this is a
breaking change, the golden test is updated to reflect that.
As mentioned in pygments#1963 (comment), the problem is that the rule matched . before .., so .. would never be matched. Fixed here.
@hwayne
Copy link
Contributor Author

hwayne commented Nov 18, 2022

Only a year late, but I fixed the regexlint issue, let's see if this passes the check!

@birkenfeld birkenfeld removed the update needed Waiting for an update from the PR/issue creator label Nov 19, 2022
@birkenfeld
Copy link
Member

Tests are fine. Since there were tons of unrelated changes and conflicts in the branch, I manually cherry-picked the changes and pushed them in f1283e6.

@birkenfeld birkenfeld closed this Nov 19, 2022
@hwayne hwayne deleted the alloy branch March 12, 2023 17:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

6 participants