Deeper IDE Integration

[rasenmaeher92]

Hey, thanks for this awesome addon for VS Code to use CrossHair! I was wondering whether a deeper VS Code integration would be possible, is intented or is already planned?

For example

• Output
  • It would be nice if issues found by crosshair commands are listed in the "Problems" tab or show as a CodeLens directly above the function definition.
  • In combination with the live updates through crosshair watch this could really be helpful and interactive tool whilst coding, that continuously suggests counterexamples to the currently implemented code & contracts.
• Reruns
  • Afaik crosshair watch currently relies on changed last edited times. Maybe VS Code could trigger reruns instead after a short delay after the last key was pressed (like it is the case with many other actions, e.g. pylance).
• Command Naming
  • The crosshair watch command in the command palette is currently not searchable with the keyword watch.
  • In a similar vein, maybe it would be nice if all commands are prefixed with Crosshair: such that they are searchable with the keyword Crosshair.
• Settings
  • It would be nice if some crosshair settings could be set via the VS Code settings dialog.
• Status
  • The output of crosshair watch (e.g. Analyzed <XYZ> paths) could be shown in the status bar at the bottom.

Many of the features above are inspired by other addons (mostly linters), but unfortunately I am not much of a TypeScript programmer :/.

Cheers!

[mristin]

Hi @rasenmaeher92 , Thanks a lot for your suggestions! We indeed considered some of them already, especially the output point. The problem is that CrossHair currently does not provide a server/client split, but we can interact with it only through invoking a command in the terminal.

@pschanely what do you think about adding a server option so that we could steer CrossHair more tightly and listen somehow on the outputs?

@rasenmaeher92 I imagine that this would be a lot of work both on crosshair-vscode side as well as on CrossHair side. Is there any way you could gather ~5 people so that we can discuss the requirements in more detail? @pschanely Do you know if somebody else might want to use CrossHair as a server? Perhaps some of the educational platforms for learning programming might want to integrate it in their offerings and might be interested to contribute somehow?

[pschanely]

Hi all! I am open to the idea of giving CrossHair an option to run as an LSP server, and could implement it. On rare occasions, I've had someone ask about using CrossHair programmatically. Though so far people have been content to write a file and parse a crosshair check result. I'll ask around anyway.

As a side note, vscode-python has recently been working on breaking out the various python linters into their own extensions, so we now have examples to draw from, for instance vscode-pylint.

[pschanely]

I'm looking into whether I could attempt some of this myself. LSP appears to be a nice platform for CrossHair, which really wants to be able to sit in the background and chew on things.

@rasenmaeher92 Gotcha, no TypeScript! But any chance you're available to help out in some fashion? (e.g. to QA, perhaps make minor tweaks?)

@mristin I know you don't really have spare cycles to support this plugin; LMK if you're ready for me to officially inherit! (or, if you are interested at some level; code reviews, etc)

[mristin]

@pschanely please do take over the ownership! I'm indeed swamped with tasks in the forseeable future.

[pschanely]

@pschanely please do take over the ownership! I'm indeed swamped with tasks in the forseeable future.

@mristin Sounds good. I think you can either try that big red "transfer ownership" button, or just add me as a collaborator and I'll act as owner.

[mristin]

@pschanely I tried to transfer the ownership, but it says that pschanely/crosshair-vscode already exists. I suppose you made a fork? I added you as collaborator -- please let me know if you want to delete your personal fork so that I can transfer the repository to you.

[pschanely]

Ah! Adding me as a contributor is certainly enough (but I've also just deleted my fork if you'd like to do the full transfer).

As for the actual requests: I don't plan to implement all of these right away. The main piece of work I'd like to implement is the watch-in-background, inline errors, and problems tab (and commands to pause/resume the background watch). But I'll probably implement a few of the other ideas too.

[rasenmaeher92]

Sorry for the long delay on my answer, if possible I will certainly try to help out here and there (e.g. QA, beta testing) :).

[pschanely]

I have a new pre-release version out. Finally! Here are the subset of requested changes that I've implemented:

• Output

  • The extension now optionally runs something very much like crosshair watch in the background. Counterexamples discovered from the background running show both with the red underlines and in the "Problems" tab!

• Command Naming

  • The crosshair watch command in the command palette is now searchable with the keyword watch.

• Settings

  • Contract type and autostart is now configurable as a real vscode setting!

• Status

  • For now, I just show whether CrossHair is running in the status bar. (I am not sure whether the path count would be overly distracting ... or not)

Marko has transferred ownership of this project to me; consequently, the extension "upgrade" has to be performed manually: uninstall the current extension and install my pre-release version of the extension. In addition, please update the crosshair-tool python package in the environment you're using, e.g. pip install crosshair-tool -U.

@rasenmaeher92 : I know it's probably long since fallen off your radar, but it'd be incredibly helpful if you were able to give this a try and let us know how it works for you, whether you have suggestions, etc.

[rasenmaeher92]

Actually I haven't forgotten about this (I was just a bit busy)! It is great to see this crosshair tooling improvement for VS Code! There was a little notification that pygls was also required, so I installed that (maybe it could be listed in the readme of this extension if it is always required).

Apart form that, it is really great to see the counter examples and errors in the Problems tab as one is live coding! It allows to write a function, write a few pre/post-contracts and then iteratively refine the required pre-contracts and the implemention as crosshair discovers counterexamples.

I am still wondering whether there should be any kind of information on much effort crosshair has spent to check a function. I guess what I am looking for is a positive confirmation, which code is being checked by crosshair and which isn't. As I understand it crosshair is good at finding counterexamples rather than proving that there are none, so I use the paths checked value as proxy to gauge whether I can move on, but it could be any other value or measure

[pschanely]

@rasenmaeher92 Thank you for trying this out, and I'm glad it's working for you! I'd love to continue to get feedback/problems/suggestions from you as you continue.

Ooops! Indeed, I didn't update the README about the pygls dependency - just added some text about that now. I'll probably decide to just bundle it further down the road.

Having some sort of confirmation about what CrossHair is doing doing sounds like a great idea! I need to look into what's possible/feasible (I think I can show "informational" or "hint" messages, but I'm not sure whether that'll make some parts of the interface too noisy). Right now, I'm deep in some optimization work, but I'll revisit this hopefully in the next month or two.

Thanks again, and especially for reporting back about how it's going - feedback is SO important for a project at this phase.