Alpha-testers wanted for interactive support

[cpitclaudel]

Hi all,

I've just pushed extremely experimental support for interactive editing in fstar-mode.el. I think it could use quite a bit of alpha-testing at this point, but a first sanity check would be great to begin with.

Pulling the latest release should give you the relevant code (you'll need to M-x package-install flycheck first, though), and the interactive mode is enabled by default (accordingly, flycheck is currently disabled by default).

Unlike atom, Emacs uses a succession of two empty lines as a block delimiter (I couldn't remember what comment string was used in Atom). The keybindings are inspired from Proof-General. That is, C-c C-n processes the next block, C-c C-u retracts the last block, and C-c C-RET processes or retracts up to the current point.

I expect that some number of synchronization issues and small errors will pop up, but on my machine at least this is already quite useful for navigating around. Please help me test it :)

Explicitly CC-ing @nikswamy and @catalin-hritcu, as I'm not sure whether issues in this repo trigger automatic notifications.

Still TODO for me:

• [x] Make overlays read-only
• [x] Make error markers squiggly
• [x] Auto-retract up to editing point?
• [x] Fix overlay colors for light backgrounds
• [x] Kill process buffer when parent buffer is closed
• [x] Fix single-line comments
• [ ] Figure out the special comments that Atom uses to delimit sections (ask @aseemr maybe?)

Cheers, Clément.

[cpitclaudel]

Obligatory screenshot:

[catalin-hritcu]

This seems great. I will gladly test but I didn't manage to get it started at all. C-c C-n and C-c C-ret don't seem to do anything. Screenshot attached.

Edit: and one more

[catalin-hritcu]

Nevermind, it was a local error. Managed to make it work, just that the grey bar got stuck with a "user-error: Nothing to process!" message:

[cpitclaudel]

Thanks for trying this out!

Indeed, the error above was relative to outdated packages in your config :)

Could you post a copy of a (not too big) file that displays the issue that you're seeing? The debug output looks very strange.

Cheers, Clément.

[cpitclaudel]

Interestingly, I can't really seem to reproduce this issue with that particular file. The contents of the whole *Messages* buffer could be helpful too.

[mwhicks1]

I've tried this out, too, but I'm not sure what's supposed to happen. Seems to not work.

I have fstar-mode.el installed, latest version, and I have the most recent Fstar from git, compiled with ocaml. In my .emacs file I have added the line:

(require 'fstar-mode "/Users/mwhicks/research/projects/fstar.el/fstar-mode.el")

I picked the example FStar/examples/circuitcompiler/wires.fst as an example, and that works with my normal fstar configuration:

% fstar wires.fst Verifying module: Wires All verification conditions discharged successfully

With the emacs mode, this file is nicely formatted (though very slow).

Now, when I hit C-c, C-Ret to try to process any lines in the file, it highlights those lines but doesn't seem to do anything. It generates the Message

Processing queue QUERY [#push module Wires

(* TODO: ranges are wire bundles and that usually correspond to values; take advantage of that correspondence somehow? ) type wrange = p:(nat \ nat){snd p >= fst p}

let wirezero:nat = 0 let wireone:nat = 1

let g_init = 1 (* initial counter ) val alloc_wrange: g:nat -> sz:nat{sz > 0} -> Tot(g':nat{g' = g+sz} \ wrange) let alloc_wrange g sz = g+sz, (g+1,g+sz)

(* TODO: We convert to lists here so we can fold. But it might be better to write iterator functions over ranges directly? *) val rangetolist: p:wrange -> Tot (list nat) (decreases(snd p - fst p)) let rec rangetolist (i,j) = if j = i then [i] else i::(rangetolist (i+1,j))

end #done-ok #done-nok

]

But then nothing happens aside from highlighting in purple. Subsequent uses of C-c, C-Ret highlight in gray, and nothing else happens.

So perhaps my "config" is messed up. Help would be appreciated.

-Mike

PS. When I attempt to add the line following line to my .emacs it fails with "Attempt to set a constant symbol: nil"

(set-default flycheck-fstar-executable "/Users/mwhicks/research/projects/FStar/bin/fstar.exe")

On Sun, Sep 6, 2015 at 10:35 AM, Clément Pit--Claudel < notifications@github.com> wrote:

Interestingly, I can't really seem to reproduce this issue with that particular file. The contents of the whole Messages buffer could be helpful too.

— Reply to this email directly or view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/3#issuecomment-138090010 .

[cpitclaudel]

Thanks Catalin and mwhicks1 for the help. I can reproduce parts of this, but only if I run Emacs with -q (no local configuration). This is rather strange.

I'll keep you updated.

[cpitclaudel]

Hi all,

I've fixed an issue where not setting flycheck-fstar-executable manually would prevent the process from starting. @catalin-hritcu, does this solve your problem?

@mwhicks1, are you using a recent build of fstar? Can you try with the updated code?

Thanks again for the help with this!

[catalin-hritcu]

Things are better for me. The file I'm using for testing is this: https://github.com/FStarLang/FStar/blob/master/examples/metatheory/stlc_strong_db_parsubst.fst One of the things that were strange before but work now are the line breaks in the Message window.

Even with the newest version I still get an error:

Identifier not found: [excluded_middle]

that doesn't occur if running fstar.exe on this file from the command line:

[hritcu@detained pub]$ fstar.exe examples/metatheory/stlc_strong_db_parsubst.fst
Verifying module: FStar.Constructive
Verifying module: FStar.Classical
Verifying module: FStar.FunctionalExtensionality
Verifying module: StlcStrongDbParSubst
All verification conditions discharged successfully
[hritcu@detained pub]$ 

Could it be a build-config problem?

And here is the message log: https://gist.github.com/catalin-hritcu/04346ba911df9dda2a94

[cpitclaudel]

Ah, awesome! So the interactive stuff is working :)) Yes, I would bet on a build-config issue. At the moment, Emacs does not make any attempt at parsing the build-config section, so it just calls fstar.exe --in. I could change this and do the parsing from Emacs, but do we really want this? Wouldn't it be best if F* did the parsing itself?

[catalin-hritcu]

Ah, it's that one :) Agreed, it should be F* to parse the build-config, not the editor modes. Filed an F* issue on this: https://github.com/FStarLang/FStar/issues/346

[jkzinzindohoue]

It works out of the box for me on Windows. I need to set up manually flycheck-fstar-executable on Ubuntu, after which it also works.

I will make further reports on this thread if I encounter issues. Thanks !

[jkzinzindohoue]

@mwhicks1 adding a tick : (set-default 'flycheck-fstar-executable "~/fstar/FStar/bin/fstar.exe") makes it working for me.

[cpitclaudel]

@jkzinzindohoue Thanks for trying this out! By the way, (set-default 'flycheck-fstar-executable "~/fstar/FStar/bin/fstar.exe") is equivalent to (setq-default flycheck-fstar-executable "~/fstar/FStar/bin/fstar.exe"), as the latter is a macro that automatically quotes its argument.

[beurdouche]

Hey ! Thanks for this =) Here are some comments :

• It worked out of the box =) once I understood I needed to install dash and flycheck before the fstar mode. (I am running OSX and both can be installed using homebrew).
• I have trouble running C-c C-RET from an emacs that runs inside the OSX terminal. This does not work for me as it is interpreted as C-c RET all the time. It is not the case if I run emacs with GUI. (It might be specific to OSX, I am not sure..) =s
• If i saw correctly "Queue is empty" is the message when the previous block typechecked sucessfully. Maybe this could simply be changed to "OK" ?

Cheers ! =) B.

[cpitclaudel]

@beurdouche Great news! Glad to see it works.

The dependencies thing is only a problem with this beta; I'll upload this package to MELPA once it's a bit more stable. The following snippet would have pulled these dependencies as well, but it's much better if beta-testers can get it from source; thanks for taking the time!

(let ((url "https://raw.githubusercontent.com/FStarLang/fstar.el/master/fstar-mode.el"))
  (with-current-buffer (url-retrieve-synchronously url)
    (package-install-from-buffer)))

I clarified the initial post, too: thanks for pointing this out.

C-c C-RET not working in a terminal is expected, though annoying (RET is already C-m there). If you're a user of Proof-General, what do you use to process the file up to a certain point when writing Coq scripts? (@jasongross might be able to help here; Jason, do you remap proof-goto-point when you use Coq in emacs from the terminal?)

Finally, the messages: At the moment they are just horribly verbose (the full input and output is printed for every query). I was expecting more bugs, so I thought it good to enable them always. Once we converge to something more stable, I'll flip the switch and quiet most of them.

By the way, you might want to try a graphical Emacs :) prettify-symbols-mode is a neat feature.

Cheers and thanks again for the debugging help!

[JasonGross]

I map C-c RET so I can ignore the fact that C-RET shows up as RET. I think this onlso shows up in emacs under ssh for me, but I almost never use terminal emacs not under ssh, so I'm not sure.

[cpitclaudel]

Awesome, thanks Jason. Maybe I'll make that the default here too.

[cpitclaudel]

By the way @catalin-hritcu and @nikswamy, is it reasonable to consider a sequence of two empty lines to be a good breaking point? I think it feels much nicer if, when processing a large buffer, checkpoints are inserted automatically (otherwise an error on line 100 makes you rewind all the way to the top). I don't remember what checkpoints atom uses (special comments?); I think it would be nice to have a notion of automatic checkpoints though.

I've pushed code that makes C-u C-c C-RET ignore infered breaking points and send everything as one query.

[nikswamy]

How about this: relative to the current cursor, the nearest succeeding sequence of two or more empty or space-only lines, ending either in EOF or in a line with a non-space character in column zero; or, EOF if no such lines exist.

-Nik

Sent from my Windows Phone

---

From: Clément Pit--Claudelmailto:notifications@github.com Sent: ‎9/‎6/‎2015 17:23 To: FStarLang/fstar-mode.elmailto:fstar-mode.el@noreply.github.com Cc: nikswamymailto:nswamy@live.com Subject: Re: [fstar-mode.el] Alpha-testers wanted for interactive support (#3)

By the way @catalin-hritcu and @nikswamy, is it reasonable to consider a sequence of two empty lines to be a good breaking point? I think it feels much nicer if, when processing a large buffer, checkpoints are inserted automatically (otherwise an error on line 100 makes you rewind all the way to the top). I don't remember what checkpoints atom uses (special comments?); I think it would be nice to have a notion of automatic checkpoints though.

I've pushed code that makes C-u C-c C-RET ignore infered breaking points and send everything as one query.

---

Reply to this email directly or view it on GitHub: https://github.com/FStarLang/fstar-mode.el/issues/3#issuecomment-138139856

[fournet]

Installed it too, thanks! Some minor issues/comments

1. my fonts still miss symbols (on Windows 10, after installing fonts suggested by JK). It would be good to recommend fonts in the readme, and more generally to document which packages need to be installed too: dash, tuareg, ...
2. how to add fontification for C-style // comments ? how to substitute symbol in comments too?
3. Working on miTLS, a project with many fstar directories and files, the long command-line options passed to fstar are generated by a Makefile. How to automatically pass those options in interactive mode? Maybe calling make to set up an FSTAR_OPTION environment variable? So far "make json" generates a global config file (atom-fstar-build.js) but I'd prefer to be less atom-specific.
4. Re: breakpoints, why not just stopping at every line with a non-space character in column zero? As long as editing automatically retracts verification, this would be the most convenient for me.

[cpitclaudel]

@nikswamy This seems like a reasonable choice, and I think it's pretty close to what I have at the moment :) Anyhow, if we at some point implement an interface for IDEs to query F* for a parse tree, then that could come with appropriate checkpoint locations.

[cpitclaudel]

@fournet Thanks for trying this out!

1. my fonts still miss symbols (on Windows 10, after installing fonts suggested by JK). It would be good to recommend fonts in the readme, and more generally to document which packages need to be installed too: dash, tuareg, ...

I've updated the README to list good fonts. What particular characters do you have issue with? tuareg is not a dependency; installing flycheck will pull dash. There's a snippet in the README that will install this repo as a package, pulling the dependencies automatically.

1. how to add fontification for C-style // comments ? how to substitute symbol in comments too?

Thanks for spotting the comments issue (it's fixed now!). Substituting symbols in comments is tricky; it might involve more hackery than I want to invest :)

1. Working on miTLS, a project with many fstar directories and files, the long command-line options passed to fstar are generated by a Makefile. How to automatically pass those options in interactive mode? Maybe calling make to set up an FSTAR_OPTION environment variable? So far "make json" generates a global config file (atom-fstar-build.js) but I'd prefer to be less atom-specific.

Isn't that what build-config comments are for? I could implement support for parsing atom-fstar-build.js, but I'm not sure how good an idea that is.

1. Re: breakpoints, why not just stopping at every line with a non-space character in column zero? As long as editing automatically retracts verification, this would be the most convenient for me.

Editing doesn't retract verification at the moment; I'll probably implement that later. Single line breaks do not work well because of cases like the following:

val f: int -> int
val g: int -> int

let rec f x =
  if x > 0 then g x else 0

and g x =
  if x > 0 then f (x - 1) else 0

Thanks for all the feedback!

[fournet]

Re 1.packages: I had to install a few by hand before it worked (probably because my .emacs was not using melpa).

Re 1.fonts, I had problems e.g. with <==>.

Re 3: Parsing in emacs (or atom) is a bad idea --- what I need is a convenient way to pass any additional arguments (as a string) as fstar is invoked.

Re 4: I'd rather not force programmers to skip multiples line because of one editor. I'd refine the condition on breakpoints to "non-empty column-0 line and non-and". Or just let fstar report breakpoint locations --- the more robust solution suggested by Nikhil.

[cpitclaudel]

@fournet

1.packages: Indeed, probably 1.fonts: Do you still have problems after installing one of the recommended fonts? 3: Do build-config comments not work for that? 4: I think I was the one who suggested this, actually :) I don't know F* well enough to have a good grasp on what the right break point is, and special-casing and feels brittle. Feel free to experiment by changing the fstar-subp-block-sep regular expression.

[cpitclaudel]

@fournet: I implemented automatic retracting; your feedback is welcome :)

[cpitclaudel]

@mwhicks1: You mentioned performance problems; could you give me more details? I have no problems with this particular file :/ Is it only when you first open the file? Or is it still slow if you close it an re-open it?

[fournet]

Re: fonts, I get a rectangle for (at least) <==> with DejaVu Sans Mono and Arial Unicode. Segoe UI Symbol seems fine, but I need a fixed-width font for code.

Re: build-config embedded in files, this is a source of conflicts on projects with concurrent editing. We already have Makefile to pick the right command-line arguments depending on the local config and the task at hand, and we don't want to duplicate it. Ideally emacs would ask make nicely for the arguments to use, e.g. by running "make foo.fst.interactive". Alternatively, I need e.g. an emacs buffer-local variable to customize those arguments.

Thanks again, -Cédric

[jkzinzindohoue]

For some reason, after installing all the fonts listed in the README on Windows (more likely after installing Cambria Math), the prettification works for all fonts now on my machine.

Auto retracting works, although not if the build-config is modified (I guess because it is seen as comments ?). It seems that it is not loading the build config though, I cannot open FStar.Seq.fst for instance, while running in the command line works fine.

[cpitclaudel]

@fournet The font issue is surprising (but then again, font selection in Emacs on windows is a source of many surprises). Here are a bunch of things to try:

• Set the actual main font to one of the suggested monospace fonts (from the options / set default font menu)
• Use the snippet provided in the README page: I use elisp (set-fontset-font t 'unicode (font-spec :name "Consolas") nil 'append) (set-fontset-font t 'unicode (font-spec :name "Symbola") nil 'append)
• Reboot ?

Regarding arguments: I've added a new setting:

fstar-subp-prover-args is a variable defined in ‘fstar-mode.el’.
Its value is nil

Documentation:
Used for computing arguments to pass to F* in interactive mode.

If set to a string, that string is considered to be a single
argument to pass to F*. If set to a list of strings, each element
of the list is passed to F*. If set to a function, that function
is called in the current buffer without arguments, and expected
to produce a string or a list of strings.

Some examples:

- (setq fstar-subp-prover-args "--ab") results in F* being
called as 'fstar.exe --in --ab'.

- (setq fstar-subp-prover-args '("--ab" "--cd")) results in
F* being called as 'fstar.exe --in --ab --cd'.

- (setq fstar-subp-prover-args (lambda () '("--ab" "--cd")))
results in F* being called as 'fstar.exe --in --ab --cd'.

To debug unexpected behaviours with this variable, try
evaluating (fstar-subp-get-prover-args).

It should work fine as a buffer-local variable, too. In your case, maybe the following snippet could help (I wrote it quickly, so there might be small problems in it)?

(defun my-fstar-compute-prover-args-using-make ()
  "Construct arguments to pass to F* by calling make."
  (with-demoted-errors "Error when constructing arg string: %S"
    (let* ((fname (file-name-nondirectory buffer-file-name))
           (target (concat fname ".interactive"))
           (argstr (car (process-lines "make" "--quiet" target))))
      (split-string argstr))))

(setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)

[cpitclaudel]

@jkzinzindohoue You're right, changing the build-config should actually kill the F* subprocess; thanks for pointing that out! I've fixed it.

Build-config comments are not used by the interactive Emacs mode at the moment. Atom parses them, but I really believe F* should be doing that, not the IDE. See https://github.com/FStarLang/FStar/issues/346 for more info (I hope this gets implemented soon :)

[mwhicks1]

Seems better with the most recent version, and my other problems are gone too. Thanks! --Mike

On Mon, Sep 7, 2015 at 1:41 PM, Clément Pit--Claudel < notifications@github.com> wrote:

@mwhicks1 https://github.com/mwhicks1: You mentioned performance problems; could you give me more details? I have no problems with this particular file :/ Is it only when you first open the file? Or is it still slow if you close it an re-open it?

— Reply to this email directly or view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/3#issuecomment-138347324 .

[cpitclaudel]

@mwhicks1 Great, thanks!

[fournet]

Thanks for adding support for custom arguments!

• I got it to work only when explicitly passing a list; otherwise the string is (probably) passed quoted, e.g. with "--verify_module TLS TLS.fst" fstar complain there is literally not such file name.
• In particular, using (setq fstar-subp-prover-args (lambda () (shell-command-to-string "cd ..; make tls.in"))), I get back the correct argument string but could not pass it to fstar.
• By the way, how do I refer to the current .fst/.fsti buffer name in that lambda? For concreteness, here are the arguments I am currently using:

(setq fstar-subp-prover-args
`("--trace_error" "--max_fuel" "4" "--initial_fuel" "0" "--max_ifuel" "2" "--initial_ifuel" "1" "--z3timeout" "100" "../../../FStar/lib/ext.fst" "../../../FStar/lib/classical.fst" "../../../FStar/lib/set.fsi" "../../../FStar/lib/heap.fst" "../../../FStar/lib/map.fsi" "../../../FStar/lib/listTot.fst" "../../../FStar/lib/hyperHeap.fsi" "../../../FStar/lib/stHyperHeap.fst" "../../../FStar/lib/allHyperHeap.fst" "../../../FStar/lib/char.fsi" "../../../FStar/lib/string.fst" "../../../FStar/lib/list.fst" "../../../FStar/lib/listproperties.fst" "../../../FStar/lib/seq.fsi" "../../../FStar/lib/seqproperties.fst" "../../../FStar/lib/int64.fst" "../../../FStar/contrib/Platform/fst/Bytes.fst" "../../../FStar/contrib/Platform/fst/Date.fst" "../../../FStar/contrib/Platform/fst/Error.fst" "../../../FStar/contrib/Platform/fst/Tcp.fst" "../../../FStar/contrib/CoreCrypto/fst/CoreCrypto.fst" "../../../FStar/contrib/CoreCrypto/fst/DHDB.fst" "--admit_fsi" "FStar.Set" "--admit_fsi" "FStar.Map" "--admit_fsi" "FStar.HyperHeap" "--admit_fsi" "FStar.Seq" "--admit_fsi" "FStar.Char" "--admit_fsi" "FStar.SeqProperties" "--admit_fsi" "SessionDB" "--admit_fsi" "UntrustedCert" "--admit_fsi" "DHDB" "--admit_fsi" "CoreCrypto" "--admit_fsi" "Cert" "--admit_fsi" "Handshake" "--admit_fsi" "StatefulLHAE" "TLSError.fst" "Nonce.p.fst" "TLSConstants.fst" "RSAKey.fst" "DHGroup.p.fst" "ECGroup.fst" "CommonDH.fst" "PMS.p.fst" "HASH.fst" "HMAC.fst" "Sig.p.fst" "UntrustedCert.fsti" "Cert.fsti" "TLSInfo.fst" "Range.p.fst" "DataStream.fst" "Alert.fst" "Content.fst" "StatefulPlain.fst" "LHAEPlain.fst" "StatefulLHAE.fsti" "Handshake.fsti" "Record.fst" "--verify_module" "TLS"))

[cpitclaudel]

Hi Cédric,

Indeed, single strings are considered to be a single argument (If set to a string, that string is considered to be a single argument to pass to F*.). I've added one more warning to the docs; feel free to suggest further improvements :)

The example lisp code that I gave in the previous post should do all that you mentioned and more; it shows how to use buffer-file-name to get the buffer's file name, and split-string to create a list of arguments.

If changing the Makefile slightly is possible, returning one argument per line in and just using process-lines would work nicely, too:

(defun my-fstar-compute-prover-args-using-make ()
  "Construct arguments to pass to F* by calling make."
  (with-demoted-errors "Error when constructing arg string: %S"
    (let* ((fname (file-name-nondirectory buffer-file-name))
           (target (concat fname ".interactive"))
           (args (process-lines "make" "--quiet" target)))
      args)))

(setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)

[s-zanella]

Hi Clément,

I got the error below when installing the mode both on Windows with Emacs 24.5.1 and Mac OS X with Emacs 24.4:

Compiling file ****/.emacs.d/elpa/fstar-mode-0.1/fstar-mode.el at Tue Sep 8 18:06:47 2015 fstar-mode.el:938:1:Error: Unknown upattern `(quote pg)'

It works if I replace the quotes in 'pg and 'atom with backquotes in the problematic pcase expression.

It would be nice to document in the README file the minimum Emacs version required (is it 24.0?), and that one needs to enable installation of MELPA packages for the automated setup to work.

Thanks a lot for the effort you put into writing this mode!

Cheers, --Santiago

On Tue, Sep 8, 2015 at 2:56 PM, Clément Pit--Claudel < notifications@github.com> wrote:

Hi Cédric,

Indeed, single strings are considered to be a single argument (If set to a string, that string is considered to be a single argument to pass to F*.). I've added one more warning to the docs; feel free to suggest further improvements :)

The example lisp code that I gave in the previous post should do all that you mentioned and more; it shows how to use buffer-file-name to get the buffer's file name, and split-string to create a list of arguments.

If changing the Makefile slightly is possible, returning one argument per line in and just using process-lines would work nicely, too:

(defun my-fstar-compute-prover-args-using-make () "Construct arguments to pass to F* by calling make." (with-demoted-errors "Error when constructing arg string: %S" (let* ((fname (file-name-nondirectory buffer-file-name)) (target (concat fname ".interactive")) (args (process-lines "make" "--quiet" target))) args)))

(setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)

— Reply to this email directly or view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/3#issuecomment-138567603 .

[cpitclaudel]

Hi Santiago,

Thanks for the feedback! I documented the requirement of Emacs 24.3 or later. Emacs 24.0 (24.1, actually) came out in 2012, so I took the liberty to require something a bit more recent :) I also fixed the pattern issue (looks like it's a new feature in 25), thanks!

Does the snippet in the README not install dependencies as well for you? It seems to work for me.

Cheers, Clément.

[s-zanella]

Thanks for the fixes Clément.

The snippet in the README didn't install all dependencies for me. flycheck and dash are only in the MELPA repository, so I had to add it in my init file:

(require 'package) (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/")) ... (package-initialize)

On Tue, Sep 8, 2015 at 7:27 PM, Clément Pit--Claudel < notifications@github.com> wrote:

Hi Santiago,

Thanks for the feedback! I documented the requirement of Emacs 24.3 or later. Emacs 24.0 (24.1, actually) came out in 2012, so I took the liberty to require something a bit more recent :) I also fixed the pattern issue (looks like it's a new feature in 25), thanks!

Does the snippet in the README not install dependencies as well for you? It seems to work for me.

Cheers, Clément.

— Reply to this email directly or view it on GitHub https://github.com/FStarLang/fstar-mode.el/issues/3#issuecomment-138660639 .

[cpitclaudel]

Ah, of course! I keep forgetting about that. I updated the README. There's plenty of cool stuff on MELPA, by the way; flycheck is an obvious candidate, but multiple-cursors, company, smex(in addition to ido-mode), yasnippet and wgrep are all awesome as well.

[cpitclaudel]

Hi all,

This wouldn't be a proper alpa release if I didn't decide to randomly rename variables :/ In this case I've renamed flycheck-fstar-executable to fstar-executable. This is part of removing the dependency on flycheck; support is still provided for it, but it's not mandatory any more, as the interactive support seems to be getting a bit more stable.

I've aliased each variable into the other, so this shouldn't really break anything, but changing the setting in your .emacs would still be a good idea.

Cheers, Clément.

[aseemr]

@cpitclaudel , a couple of questions/comments, none are critical so please feel free to address at leisure :).

1. For F* interfaces (files ending with .fsi or .fsti), the editor needs to pass --fsi flag (in addition to --in) when starting the F* process. Without that interactive verification of .fsi does not work (try lib/ordset.fsi for example).
2. If the verification fails, I can see the error in emacs command line, but as soon as I move the cursor the error disappears from there. How can I see the error message(s) again, is Message window the only option ? Perhaps it's worth adding to README. There is nothing about navigating error messages there.
3. When I installed the mode, the command for installing dependencies (via eval-buffer, in the Setup section of the README) did not work for me. I got an error saying "dash-2.11 not available" or something. But I was able to install it manually. I have emacs version 24.5 and I had the (require packge ...) lines as first lines in .emacs.

[cpitclaudel]

Hey @aseemr:

I've fixed 1, thanks. Can you check? Re 2: the point will jump to the first error, and it should be underlined in red. Pressing C-h . there will display the error again. So will hovering with your mouse. I'm still thinking about how to integrate best an error list. Using the Flycheck backend does all this, of course, but it doesn't take advantage of the interactivity. I'll welcome suggestions :) Re 3: I don't think this will be an issue any more when we're on MELPA, which is probably in a few hours :)

[aseemr]

1 works now, thanks.

[cpitclaudel]

Exciting news: I've submitted the new F* mode for inclusion in MELPA, and it was accepted. This means that it should now be much easier to install it, and there should be no more dependency issues. Thanks to autoloads, you also don't need to (require 'fstar-mode) anymore, which should improve Emacs' load times.

I've updated the README accordingly; let me know if you run into issues.

[cpitclaudel]

I think this can be closed :)