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

Detect VSCode Remote-SSH when using --visualize #1292

Merged
merged 4 commits into from
Jun 22, 2022

Conversation

tedinski
Copy link
Contributor

Description of changes:

Add a quick suggestion for how to view a visualize report when using VS Code Remote-SSH.

  • I also updated some of the cheat-sheets in docs. I:
    • Removed old cheat sheets that aren't relevant now that we're not a fork
    • Added a new one reminding how to fix "I committed to main"

Resolved issues:

Resolves #1263

Call-outs:

See it in action:

Screen Shot 2022-06-20 at 5 18 40 PM

Testing:

  • How is this change tested? Manually - We could check for the appearance of this line, but it's not a meaningful test.

  • Is this a refactor change? no

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@tedinski tedinski requested a review from a team as a code owner June 20, 2022 22:20
&& std::env::var("SSH_CONNECTION").is_ok()
{
println!(
"VSCode Remote-SSH port forwards for you. Try: python3 -m http.server --directory {}/html",
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please improve this message? It's not clear to me what the message is here.

I'm assuming you are trying to say that there is a VSCode remote-ssh session running and the user might be able to see the trace by running the command above.

Also, do we have a more detailed documentation that we can provide a link to?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, the message I struggled with.

One the one hand, we want to prompt users with the command and give them a clue why they should run it, but on the other hand this gets printed on every run, so we don't want paragraphs explaining the feature every time, it quickly becomes noise.

I could try to explain more or... I could try to explain less? What if it was just "Try: "

I suppose we could tolerate two lines?

Report written to: target/etc
VS Code automatically forwards ports for locally hosted servers. To view the report remotely,
Try: <cmd>

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's better, thanks!

@tedinski tedinski merged commit 8a5e579 into model-checking:main Jun 22, 2022
@tedinski tedinski deleted the vscode-help branch June 22, 2022 22:23
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.

Detect VS code remote ssh when using visualize
2 participants