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

Display infobox when .cfg is missing #336

Merged
merged 1 commit into from
Sep 27, 2024

Conversation

FedericoPonzi
Copy link
Collaborator

When running command "TLA+: Check model with TLC", if the .cfg file is missing, we don't get a warning or anything. This can be
source of confusion. Removed the warn parameter as it was already defaulting to true. This will lead in more consistent behavior as well.

Solves: #331
Ref: #335 and commit: 2092aeb

New behavior when running "TLA+: Check model with TLC":
image

When running command "TLA+: Check model with TLC", if the .cfg file
is missing, we don't get a warning or anything. This can be
source of confusion. Removed the warn parameter as it was already
defaulting to true. This will lead in more consistent behavior as
well.

Signed-off-by: Federico Ponzi <me@fponzi.me>
@lemmy
Copy link
Member

lemmy commented Sep 27, 2024

Given a model Foo, the extension will look for an MCFoo.tla and MCFoo.cfg and run TLC on those if they exist. I have found this to be pretty useful, if one adopts the convention of prefixing TLC configs with MC.

@FedericoPonzi FedericoPonzi merged commit b042ac5 into tlaplus:master Sep 27, 2024
4 checks passed
@FedericoPonzi FedericoPonzi deleted the issue-331 branch September 27, 2024 20:36
@lemmy
Copy link
Member

lemmy commented Oct 3, 2024

I get the two popup boxes now on every editor save when editing auxiliary modules, i.e. not the root module.

FedericoPonzi added a commit to FedericoPonzi/vscode-tlaplus that referenced this pull request Oct 4, 2024
FedericoPonzi added a commit to FedericoPonzi/vscode-tlaplus that referenced this pull request Oct 4, 2024
This reverts commit b042ac5, reversing
changes made to 2e5780c.

Signed-off-by: Federico Ponzi <me@fponzi.me>
lemmy pushed a commit that referenced this pull request Oct 4, 2024
This reverts commit b042ac5, reversing
changes made to 2e5780c.

Signed-off-by: Federico Ponzi <me@fponzi.me>
@FedericoPonzi
Copy link
Collaborator Author

FedericoPonzi commented Oct 5, 2024

I get the two popup boxes now on every editor save when editing auxiliary modules, i.e. not the root module.

Do you have specific hooks on save? I tried and failed to reproduce it. Also, the code path seems to be triggered only from check, debug or evaluate expression commands; so I'm not sure how they are showing up on save.

@lemmy
Copy link
Member

lemmy commented Oct 6, 2024

image

@FedericoPonzi
Copy link
Collaborator Author

Can you also include the settings you've added?

@lemmy
Copy link
Member

lemmy commented Oct 6, 2024

  "tlaplus.smoke.prefix.path": "../.smoke/",
  "tlaplus.smoke.prefix.name": "Smoke",
  "[tlaplus]": {
    "editor.codeActionsOnSave": {
      "source": "explicit"
    }
  },

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

2 participants