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

[FEATURE] PrettyWriter should extend the standard modules #137

Closed
konnov opened this issue Apr 24, 2020 · 1 comment · Fixed by #786
Closed

[FEATURE] PrettyWriter should extend the standard modules #137

konnov opened this issue Apr 24, 2020 · 1 comment · Fixed by #786
Assignees
@konnov
Labels
Alpha Centauri The first public alpha release new New issue to be triaged. usability UX improvements
Milestone
May iteration

Comments

@konnov
Copy link
Collaborator

konnov commented Apr 24, 2020

Currently, PrettyWriter prints the user-defined operators. This is not sufficient for being parsed back by SANY. It is quite easy to detect the standard modules that are used by the user-defined operators. We should add these modules in the EXTENDS clause when writing the TLA+ file.
@konnov konnov added the new New issue to be triaged. label Apr 24, 2020
@konnov konnov added this to the v0.7-dev-integration milestone Apr 24, 2020
@konnov konnov modified the milestones: v0.7-dev-integration, v1.0-release-ux Jun 26, 2020
@konnov konnov modified the milestones: v1.0-release-ux, backlog2020 Dec 6, 2020
@konnov konnov added the usability UX improvements label Dec 11, 2020
@konnov konnov modified the milestones: backlog2020, backlog2021 Dec 11, 2020
@konnov konnov self-assigned this Apr 18, 2021
@konnov konnov modified the milestones: backlog2021, April iteration Apr 18, 2021
@konnov konnov added the Alpha Centauri The first public alpha release label Apr 18, 2021
@konnov
Copy link
Collaborator Author

konnov commented Apr 18, 2021

We should fix that to make the user reports reproducible.

@konnov konnov mentioned this issue Apr 29, 2021
Merged
8 tasks
@apalache-bot apalache-bot mentioned this issue May 3, 2021
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@konnov konnov

Labels
Alpha Centauri The first public alpha release new New issue to be triaged. usability UX improvements
Projects
None yet
Milestone
May iteration
Development

Successfully merging a pull request may close this issue.

Fix pretty printer: write annotations correctly and extend the standard modules apalache-mc/apalache
2 participants
@konnov @shonfeder