Supporting #info requests

[nikswamy]

Hi Clement,

The latest master version of F* now supports a new feature that I would like to make available from fstar-mode.el.

In response to an "#info filename row col" request, fstar --in will reply with either

<info> identifier : type (defined at filename:(row, col))</info>

Or

No information found at filename:(row, col)

I'm hoping to provide a feature where the user hovers the mouse over an identifier in the current buffer and fstar-mode.el floats the information returned by fstar for that identifier, if any.

Ideally, through some other option, it would be possible also jump to the source location that defines this identifier.

If there are any easy hints you can provide about how to implement this functionality in fstar-mode.el (or thoughts about how to improve my proposed design) that would be most helpful!

Thanks! -Nik

PS: Thanks to @leodemoura for suggesting some of this.

[cpitclaudel]

Hey Nik,

Sounds useful :) Some thoughts about the design first:

• This seems to require that the file be saved before calling #info; is that the case? If so, will there also be a story for parts of the file that haven't been processed or saved yet? (To clarify: should there be a variant — something like #info-name — to query F* about an identifier, rather than a particular position? It may be less precise, but possibly more useful)
• Is this command synchronous ? That is, if F is busy proving something, will the query hang until F returns? If so, we need to check whether F* is busy before making such a query.
• How large do F* types get, when printed?

And about the implementation:

• This sounds like a special case of eldoc, and it could plug nicely into that framework. See C-h f eldoc-mode and C-h v eldoc-documentation-function.
• There's a framework for jumping to definition in Emacs >= 25 called xref. If some F* users are still on Emacs 24 we can do it in an ad-hoc way, too. The usual keybinding is M-..

Happy to help with either of these, though I'm a bit time-constrained for the next month. Do I just need to rebuild F* to get the feature?

[nikswamy]

Hi Clement,

About saving a file: The current buffer does not have to be saved. It's a request for information about either (a) the current buffer (which need not be saved) or (b) any saved file in the the current buffer's dependence graph. The user interface I propose doesn't make it particularly easy to make a query in class (b). However, I could imagine a scenario where on starts in the current buffer, jumps to a definition in another file, and asks F* for information about some symbol in that file.

About #info-name: I'm not sure what scope one would use to resolve the name. Any suggestions?

About (a)synchrony: The command I'm proposing is synchronous. But, an async variant is clearly more useful. However, that would require some re-architecting of fstar --in

About size of types: Current they can be very large if printed in full detail. However, I would expect this info request to, by default, print only "lax" types, which are smaller (e.g., usually less than a line but sometimes up to 10 lines in source formatting---see, for example, https://github.com/FStarLang/FStar/blob/master/examples/low-level/crypto/Crypto.AEAD.Decrypt.fst#L83 up to line 92). We would also allow the user to ratchet up detail based on verbosity options already available using the #set-options directive in an F* file. Also, @kyod, @qunyanm and others are working on better pretty printers fro F* terms, so this should keep improving.

About implementation:

Thanks for the tips. Totally understand that you're busy with other stuff. These tips may already be enough to get me started ... I should dig into the code of fstar-mode.el anyway.

The latest master version of F* supports this feature. However, it has not been tested much yet ... I was expecting to do that as part of editor integration.

[kkohbrok]

Hey guys,

More info on types in fstar-mode sounds like a great idea!

I'm not too familiar with the inner workings of the interactive mode, but if the interactive mode is remodelled, could this also be a possibility to enable the retraction of busy sections? That would mean that I don't have to kill the whole process every time and work with a shifting --lax option.

[s-zanella]

A rudimentary way of achieving this is to kill the underlying Z3 process. F and the Emacs mode can recover from this and revert to the last checkpoint. Having a way of killing the Z3 process from within Emacs will be convenient and won't need any remodelling on the F side.

On Tue, Mar 21, 2017 at 4:54 PM, kkohbrok notifications@github.com wrote:

Hey guys,

More info on types in fstar-mode sounds like a great idea!

I'm not too familiar with the inner workings of the interactive mode, but if the interactive mode is remodelled, could this also be a possibility to enable the retraction of busy sections? That would mean that I don't have to kill the whole process every time and work with a shifting --lax option.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/50#issuecomment-288144384, or mute the thread https://github.com/notifications/unsubscribe-auth/AHG0bWgdXDKxDeXwmD66O4tAtrTKCI6Zks5roADegaJpZM4Mi9Cf .

[nikswamy]

Also, you don't have to have a shifting "--lax" option.

C-x C-l will lax-check the chunk you sent to F*.

And that chunk will be highlighted in grey rather than blue, so you know which parts of a buffer have been lax checked and which verified.

Adding #set-option "--lax" to a file should be avoided.

[kkohbrok]

Thanks for the hint, I'll try that. I still think that retracting busy sections would be a nice feature. However, I did not come up with the sliding --lax. If it is not recommended, it should probably be removed from here: https://github.com/FStarLang/FStar/wiki/Pragmas-(%23set-options%2C-%23reset-options) Alternatively, a "best practices" page might be good, subjective as that may be. Sorry for getting a bit off-topic here.

[cpitclaudel]

Hi all,

The current buffer does not have to be saved. It's a request for information about either (a) the current buffer (which need not be saved) or (b) any saved file in the the current buffer's dependence graph.

Got it. What happens if the query is about a symbol in an unprocessed region ?

About #info-name: I'm not sure what scope one would use to resolve the name. Any suggestions?

Probably the current global scope; we could add a position to the query, and F* could try to use that; but it would also fall back to the global scope when nothing better is available.

The latest master version of F* supports this feature. However, it has not been tested much yet ... I was expecting to do that as part of editor integration.

Makes sense :) Can you give me a small example of how it works? I tried this, but I think I probably did something wrong.

$ /build/fstar/bin/fstar.exe "/home/clement/.emacs.d/lisp/fstar.el/test.fst" "--in"
#push 1 0
module Test

let a = 1
#end #done-ok #done-nok

#done-ok
#info "/home/clement/.emacs.d/lisp/fstar.el/test.fst" 3 4
#end ok nok
<input>(1,2-1,2): (Error) Syntax error: Parsing.Parse_error
nok

[cpitclaudel]

Woops, wrong version of F*. Now I just see "no information found at (...)." (and the subprocess exits after that) Nik, could this command accept and print the usual #end #done-ok #done-nok markers? This would help with parsing the response.

[cpitclaudel]

Also (this may be unrelated), it seems that F* now accepts repeated definitions?

module Test

let a = 1

let a = 1

It used to say "Duplicate top-level names [Test.a]; previously declared at …".

[nikswamy]

Not sure about this change for repeated definitions ... @protz, is it related to support for interfaces in interactive mode?

[nikswamy]

Also, I managed to get this to work using the master version of F*

$ cat transcript  | fstar test.fst --in

#done-ok
<info>a : int (defined at <input>(3,8-3,9))</info>/n

Where

$ cat transcript
#push 1 0
module Test
let a = 1
let f = a
#end #done-ok #done-nok
#info <input> 3 8

Seems that the current buffer is called "" rather than the current file name. Also, while the output type is accurate, but the defining location is not. Like I said, not tested at all yet. Will work a bit more on debugging this stuff later today.

[msprotz]

Surprised about the double definition thing, this indeed seems to happen only in the interactive mode, as it's rejected in batch mode.

[cpitclaudel]

Also, I managed to get this to work using the master version of F*

Thanks, works for me too ! It would be awesome if it could return results as either

(at filename:(row, col)) identifier : type
#done-ok

when a location and definition are available, and as

#done-nok

otherwise. With that, the current response parsing mechanism should work just fine (and putting the filename and (row, column) information first will improve response parsing times).

If you have time to make these changes before tonight (EST), I should be able to whip a prototype together tonight.

[cpitclaudel]

A rudimentary way of achieving this is to kill the underlying Z3 process.

@s-zanella How hard would it be for F* to listen to signals (say ^C and abort the current Z3 when/if it gets such a signal?)

[cpitclaudel]

@s-zanella @kkohbrok Moved the interruption part to a separate thread (#51), with a question.

[cpitclaudel]

Ok, I have a prototype at https://github.com/FStarLang/fstar-mode.el/tree/50-info-queries . It had to apply the following to F* itself:

From 7c90899617f72f4bc5583b5b75c1e9b8a6dd7baa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= <clement.pitclaudel@live.com>
Date: Wed, 22 Mar 2017 23:14:15 -0400
Subject: [PATCH] Adjust #info syntax to make it easier to parse the output

Also make sure to call (go) after processing an Info message.
---
 src/fstar/FStar.Interactive.fs              | 8 ++++----
 src/typechecker/FStar.TypeChecker.Common.fs | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/fstar/FStar.Interactive.fs b/src/fstar/FStar.Interactive.fs
index aa2cdc1..e86595a 100644
--- a/src/fstar/FStar.Interactive.fs
+++ b/src/fstar/FStar.Interactive.fs
@@ -377,10 +377,10 @@ let rec go (line_col:(int*int))
     let iopt = FStar.TypeChecker.Common.info_at_pos file row col in
     (match iopt with
      | None ->
-       Util.print3 "No information found at %s:(%s, %s)\n" 
-            file (Util.string_of_int row) (Util.string_of_int col)
-     | Some s -> 
-       Util.print1 "<info>%s</info>/n" s)
+       Util.print_string "\n#done-nok\n"
+     | Some s ->
+       Util.print1 "%s\n#done-ok\n" s);
+    go line_col filename stack curmod env ts
   | Pop msg ->
       // This shrinks all internal stacks by 1
       pop env msg;
diff --git a/src/typechecker/FStar.TypeChecker.Common.fs b/src/typechecker/FStar.TypeChecker.Common.fs
index 89c2c44..ace2ee1 100644
--- a/src/typechecker/FStar.TypeChecker.Common.fs
+++ b/src/typechecker/FStar.TypeChecker.Common.fs
@@ -105,8 +105,8 @@ let info_as_string info =
     let id_string, range = match info.identifier with 
         | Inl bv -> Print.bv_to_string bv, FStar.Syntax.Syntax.range_of_bv bv
         | Inr fv -> Print.lid_to_string (FStar.Syntax.Syntax.lid_of_fv fv), FStar.Syntax.Syntax.range_of_fv fv in
-    BU.format3 "%s : %s (defined at %s)"
-        id_string (Print.term_to_string info.identifier_ty) (Range.string_of_range range)
+    BU.format3 "(defined at %s) %s : %s"
+        (Range.string_of_range range) id_string (Print.term_to_string info.identifier_ty)
 let rec insert_col_info col info col_infos =
     match col_infos with 
     | [] -> [col, info]
-- 
2.7.4

[nikswamy]

This is awesome ... Thanks so much for jumping into the fray! My day got filled up before I could get to this ...

[nikswamy]

oh sweet lord!! This is incredible : )

I have some bug fixes to do on my end to print stuff better. But even in this form, this extra information is very useful to have.

[cpitclaudel]

Cool. Let me know if you need further help :) If you merge the patch above and bump the version number I can make #info queries conditional on the version number and enable them by default.

[nikswamy]

0.9.4.1 is now the version reported by fstar master. Thanks!

[cpitclaudel]

Thanks! I merged the info branch into master, and it should only kick in on versions >= 0.9.4.1. Btw, when I build locally, I don't see a version number:

# Built from the release tarball
$ /build/fstar/bin/fstar.exe --version
F* 0.9.4.0
platform=Linux_x86_64
compiler=OCaml 4.03.0
date=2017-02-02T11:54:08+01:00
commit=9fc07cf

# Built from source
$ /build/FStar/bin/fstar.exe --version
F* 
platform=
compiler=
date=
commit=

Maybe the second one should say 0.9.4.2-git, or something similar?

Implementing the "jump-to-definition" thing should be easy too. I'll look into it tonight, if you don't beat me to it :)

[nikswamy]

Ah, you need to build the ocaml version by saying 'make -C src/ocaml-output'. That should report the right version number.

Also, I get this quite often now:

QUERY [#info <input> 6 0
]
eldoc error: (void-function nil)
OUTPUT [
#done-nok
]
eldoc error: (void-function nil)
RESPONSE [nil] []
eldoc error: (void-function nil)
Queue is empty (processed processed)
eldoc error: (void-function nil)
Mark set

Any idea what's going on?

[nikswamy]

Also, for jump to definition, I noticed the source position reported by in the "(defined at )" to be inaccurate. I'll look into fixing that on the F* side. If there's an easy way to implement jumping part on the emacs side, that'll be most welcome. As always, many thanks!

[cpitclaudel]

Any idea what's going on?

Not from a quick look at the code. Can you M-x toggle-debug-on-error and post the stack trace once an error happens again?

[nikswamy]

Debugger entered--Lisp error: (void-function nil)

  nil()
  apply(nil nil)
  #[128 "\301\302\300!\"\207" [eldoc-documentation-function apply default-value] 4 "\n\n(fn &rest ARGS)"]()
  apply(#[128 "\301\302\300!\"\207" [eldoc-documentation-function apply default-value] 4 "\n\n(fn &rest ARGS)"] nil)
  #[128 "\300\301\"\206

[nikswamy]

is that helpful? seems a bit mangled

[cpitclaudel]

I think it got truncated (there was probably a \0 in there which confused your clipboard) :/

[nikswamy]

backtrace.txt

[cpitclaudel]

Thanks!

[cpitclaudel]

Wild guess: running (default-value 'eldoc-documentation-function) with M-: returns nil on your machine, and you're using Emacs 24.5. If so, try running (setq-local eldoc-documentation-function #'fstar-subp--eldoc-function) (with M-:) in an F* buffer. That should make the error go away.

[nikswamy]

wild guess is wildly successful! Thanks!

[cpitclaudel]

Excellent. I'll push a fix.

[cpitclaudel]

If there's an easy way to implement jumping part on the emacs side, that'll be most welcome.

Done in https://github.com/FStarLang/fstar-mode.el/commit/3d5f332e374dbacb9d11788433b7d90523b0596f. Pressing M-. should now jump to the location reported by F*, though I couldn't test it much :)

[nikswamy]

I fixed the reported definition locations in my branch of F*.

Using that branch M-. works well for jumping to definitions within the same file. Thanks!

However, I get stuff like this when the location refers to another file:

QUERY [#info <input> 3 39
]
OUTPUT [(defined at C:\Users\nswamy\workspace\FStar\bin\..\ulib\prims.fst(209,11-209,27)) int : Type

#done-ok

]
RESPONSE [t] [(defined at C:\Users\nswamy\workspace\FStar\bin\..\ulib\prims.fst(209,11-209,27)) int : Type]
error in process filter: if: File not found: "C:\\Users\\nswamy\\workspace\\FStar\\bin\\..\\ulib\\prims.fst"
error in process filter: File not found: "C:\\Users\\nswamy\\workspace\\FStar\\bin\\..\\ulib\\prims.fst"
Queue is empty (processed processed processed)
error in process filter: File not found: "C:\\Users\\nswamy\\workspace\\FStar\\bin\\..\\ulib\\prims.fst"

[cpitclaudel]

Thanks; indeed, I didn't test it much at all. I'll look to see what's happening :)

[cpitclaudel]

Works for me when I build on your branch. Do you have an example? Could it be that you're using a cygwin Emacs with a native F*, and that's getting Emacs confused?

[nikswamy]

After a session with @protz, we figured out that if you're using Cygwin emacs, you should also install https://www.emacswiki.org/emacs/windows-path.el

In fact, for uniformity, if you're running emacs on windows and want to use fstar-mode.el, installing that windows-path.el package is probably a good idea.

Jump to definitions works! : )

[nikswamy]

I added a note to the README.md about windows-path.el.

Could the melpa package for fstar-mode.el automatically grab this package also, when on windows?

[cpitclaudel]

Jump to definitions works! : )

Yay :)

In fact, for uniformity, if you're running emacs on windows and want to use fstar-mode.el, installing that windows-path.el package is probably a good idea.

I'm not too sure, actually: that package doesn't seem to be on MELPA (right?), which suggests that it isn't commonly used.

Could the melpa package for fstar-mode.el automatically grab this package also, when on windows?

Not unless someone put the windows-path package only on MELPA, IIUC, and not conditionally either — this sounds like something better installed separately.

I think the issue is a bit more general, though: using Cygwin Emacs with a non-cygwin program is bound to yield trouble (external non-cygwin programs will get confused about Emacs-supplied paths, or vice-versa (like here). Have you tried the native Emacs ? It should make all of these problems go away pretty nicely.

[cpitclaudel]

With the info branch merged on the fstar-mode side I think this is all set; we can discuss new issues in new threads :)