Being able to jump to definition even if F* not loaded in current buffer

jaybosamiya commented 5 years ago

Some preliminary work towards being able to jump to a definition even when we don't have F* loaded up in the current buffer. Will update this PR as I make progress. The reason I am opening a WIP PR though is because I would appreciate feedback on feasibility (or if a better/easier approach exists for this already).

The way this works is by first looking for another buffer where there is an available free F process (this is likely to be the case if you are jumping many layers deep- the first process will remain free). If not, then it just complains. If it can find one, then by using that buffer's F process, it finds the place to jump to, and then performs the jump.

TODOs before merging:

[x] Find the first free F* process
- [x] Suggestion by @cpitclaudel : Use parent buffer if possible first (if current buffer is not possible), and fall back on search only if parent is unavailable.
[x] Give current buffer highest priority
[x] Improve this and fallback on old behavior if unable to find a free F* process
[x] Pass along process details to the jump/continuation, so that we can actually make the jump
[x] Make sure that the current buffers/windows are changed/updated by a jump
[x] Think about what if some module is accessible by one free F* process but not by another?
- In this case we just ignore doing stuff. Not sure how else to handle it better.

msftclas commented 5 years ago

All CLA requirements met.

cpitclaudel commented 5 years ago

I think this is a great idea, and I've been wanting this for a while.

There's a slightly better approach than looking for an F* buffer, though: you could introduce a buffer-local variable called fstar--parent-buffer, which M-. would set to the original buffer when opening a new buffer. Then, when pressing M-. again, the process of the parent buffer would be used, and the value of fstar--parent would be propagated. Any buffer in which a process is already running can be its own parent.

If there's no parent set, we can then look for an F buffer to use as the parent (this way we can handle e.g. buffers opened through grep). Ideally, any buffer sharing the same 'project root' would work, but I don't think we have a notion of project root right now, do we? So when no parent is set looking for any F process and prompting would be good.

jaybosamiya commented 5 years ago

Makes sense. I've added that to the TODO list above.

jaybosamiya commented 5 years ago

As long as we get a CI green, this is in a state where I'm satisfied with the usability of the code. I would love a code review as it currently stands, and if you are happy with it, feel free to merge :)

cpitclaudel commented 5 years ago

Very nice. The patch looks pretty small, and this is a great feature to have. I'm traveling until tomorrow, so the review might linger until this weekend; I hope that's OK!

jaybosamiya commented 5 years ago

No worries, take your time! :)

cpitclaudel commented 5 years ago

Btw, this PR will close #97 :)

jaybosamiya commented 5 years ago

Made and pushed changes as per your comments. Additionally, I added a change that helps use (xref-pop-marker-stack) better. In particular, earlier it would jump back to the F* buffer that was running, instead of jumping back to the buffer from where M-. was called. Now, with the change, it jumps back to the place where M-. was called (as expected).

jaybosamiya commented 5 years ago

Resolved comments above

cpitclaudel commented 5 years ago

Super. Any objection if I squash the commits before merging?

jaybosamiya commented 5 years ago

No objections. Makes sense to clean up the intermediate work. :)

cpitclaudel commented 5 years ago

:tada: Merged, thanks a lot for the work.

I pushed a few small tweaks (mostly whitespace, as the PR contained a mix of tabs and spaces; I recommend setting indent-tabs-mode to nil).

I also realize now that fstar-subp--pos-check-wrapper doesn't work quite right with this PR: indeed, we save the (point) in the parent buffer, and compare to that when the query returns. It would be better to save the value of point in the current buffer, and compare against that. Do you want to give that a try?

jaybosamiya commented 5 years ago

I took a look at the tweaks. Thanks for fixing them up! I realized that I had the "fail will proper error message" behavior before, but it somehow got missed during the change over to cl-loop. As for indent-tabs-mode to nil, maybe we can add that in as an emacs file local variable so that future contributors will automatically do the right thing?)

I agree that it would be better to store in the current buffer and compare against that, but at the moment, it seemed to be a pretty significant set of changes to be made to make that feasible, so I didn't do them as part of this PR.

I can try to take a look at doing that at some point of time later when I can spare a few extra cycles.

Thanks for merging! :smile_cat:

cpitclaudel commented 5 years ago

The file local variable is a good idea. You can push that directly, I think :) Storing the current buffer is a bit complicated, but I think we should at least have a FIXME in there to point out the issue. We could then attach a buffer to queries so that instead of executing all callbacks in the 'source' buffer (the one that started the process) we execute them in the buffer that caused the query to run. If we make the query constructor default to using the current buffer, it should DTRT in most cases.

jaybosamiya commented 5 years ago

Pushed the change for the file local var. Can you please add in the FIXME where you feel it'd best explain what is necessary? Thanks!

cpitclaudel commented 5 years ago

Done, see https://github.com/FStarLang/fstar-mode.el/commit/d63d1c48573c82317e5b5991486d1595094bcccd

FStarLang / fstar-mode.el

Being able to jump to definition even if F* not loaded in current buffer #105

TODOs before merging: