fstarlang / fstar-mode.el Goto Github PK

module Test

open Heap

type content =
| Link: ref content -> content
| Root: content

val repr: content -> content
let rec repr x =
  match x with
  | Link r ->
    repr !r
  | Root ->
    root

With the fstar-mode: identifier not found: ref
With the fstar batch compiler: identifier not found: root (that's the right error).

Hey ! =)

It seems that some error messages are not propagated from F* to emacs in interactive mode using a build-config.

• If there is no build-config, errors get printed in emacs. This is ok.
  
• If there is a correct build-config, no problem either. This is ok.
  
• If there is an incorrect build-config and the type-checking fails, F* returns an error message, but it does not appear in Emacs.
  (The text is briefly highlighted as usual and of course doesn't stay violet as it failed to verify the block but no error message...)
  

Hi @cpitclaudel.

I just installed the fstar-mode 20160701.309 package through melpa on Emacs 25.0.95.1 but M-x fstar-mode gives me the following error: byte-code: Symbol’s function definition is void: seq-do

I think it might be related to my flycheck (20160622.952) and/or my seq (2.3-builtin) packages but I am not sure exactly what happens... Do you have any clue about this ?

Thanks a lot ! ;) Ben

(I just installed on my mac the --devel version of emacs with Homebrew because the stable version had some updating bugs)

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:

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

Cheers,
Clément.

Any chance we could render things like x_0, y_1 etc. with subscripts?

It's missing

The two symbols are really close to each other visually. Is there any way you could make ∨ bold to distinguish it from the variable v? Or perhaps in a different color.

Thanks!

Jonathan

(** Some extra helper functions for lists. *)

module ListSet

open FStar.List

let _ = "foo"

(** [lsubset la lb] is true if and only if all the elements from [la]
    are also in [lb]. *)
val lsubset: #a:Type -> list a -> list a -> Tot bool
let rec lsubset la lb =
match la with
| [] -> true
| h :: tl ->  ((mem h lb) && (lsubset tl lb))

Hit C-c C-n. Get "Unexpected pattern at the top-level".

Fix it by removing the "let _ = foo" line. Hit C-c C-n. Get "Identifier not found: [mem].".

Kill the sub-process. Hit C-c C-n again. Everything works fine.

Forked off #56, partly implemented as FStarLang/FStar#940 ; ideally agda-style case splits, but as a first step just destructing on a type name would be nice (cc @kyoDralliam)

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.

• Jump to definition in other window
• Pick the reduction rules to apply in "compute"
• Jump to dependencies of current file
• Simple form of "destruct" that just inserts a single match
• Jump to the "alternate" location of an error
• List of option values

As mentioned in the title, if a file starts with // then the interactive mode commands C-c C-RET and C-c C-n simply show a seq: Beginning of buffer error in the Messages buffer, but don't do any actual checking.

I've tried to debug this even though I don't know much about Emacs or Lisp, and as far as I could tell (using Emacs' debugger) the error seems to come from this line of code:

More specifically, it seems that the error gets thrown by the comment-search-forward function, if I'm not mistaken (that's how I figured the error had something to do with comments).

This might be a design decision, but I find that opening a (new) split buffer to display error messages is a bit intrusive.
Type checking the following code in interactive-mode, it opens a new buffer to display the error instead of displaying it at the bottom of the existing buffer.

module Test

open FStar.Seq

type x = na

I turn on auto-fill so that my comments wrap after a while. However, in the fstar-mode, every time auto-fill wraps into a new line, I get:

(* foo ... long line
  (* ⬚

Where ⬚ is the position of the cursor. Notice 1) the extra indentation and 2) the undesired (*.

Desired behavior: either

(* foo ... long line
 * ⬚

or

(* foo ... long line
   ⬚

Thanks,

Jonathan

Forked from #50. It would be nice to be able to kill Z3 from Emacs, or more generally to interrupt the current calculation. Questions:

• Is there a small example of code that takes Z3 a long time that I could use for testing?
• Could F* process a ^C signal and kill Z3 on its own?

protz@Joprotze-Z420:~/Code/misc $ fstar scratch.fs
scratch.fs: Expected a module

(just do a file that contains type t = T)

Hi @nikswamy and @aseemr,

I'm having trouble making sense of this (on master):

$ printf "#push 1 0\nmodule Test\n  le\n#end #done-ok #done-nok" | /build/FStar/bin/fstar.exe --in
<input>(2,3-2,5): (Error) Syntax error (System.Exception: parse error
  …
#done-nok

$ printf "#push 1 0\nmodule Test\n  let\n#end #done-ok #done-nok" | /build/FStar/bin/fstar.exe --in
<input>(3,1-3,1): (Error) Syntax error (System.Exception: parse error
  …
#done-nok

The first one seems to suggest that columns count from 0, but then the second one refers to a non-existent line, and a non-existent position on that line :/

Similarly, in Aseem's example:

module Simple

type t = nat

val foo: x:t -> Pure t (requires True) (ensures (fun y -> y = x))
let foo x = x + 1

Processing the val foo: x:t -> Pure t (requires True) (ensures (fun y -> y = x)) part in #lax mode causes the line number of the error produced when processing the next line in regular mode to be off (it reports 3 instead of 5)

I did a list-packages, chose fstar-mode, and clicked on Install. I got the messages below. Is this expected? Or, should I fix my emacs configuration in some way?

Compiling file c:/Users/nswamy/.emacs.d/elpa/fstar-mode-20151023.753/fstar-mode-pkg.el at Wed Oct 28 07:58:21 2015
Entering directory `c:/Users/nswamy/.emacs.d/elpa/fstar-mode-20151023.753/'

Compiling file c:/Users/nswamy/.emacs.d/elpa/fstar-mode-20151023.753/fstar-mode.el at Wed Oct 28 07:58:21 2015
fstar-mode.el:99:17:Warning: reference to free variable `flycheck-checkers'
fstar-mode.el:99:17:Warning: assignment to free variable `flycheck-checkers'

In fstar-setup-interactive:
fstar-mode.el:1132:19:Warning: reference to free variable
    `flycheck-disabled-checkers'
fstar-mode.el:1132:19:Warning: assignment to free variable
    `flycheck-disabled-checkers'

In end of data:
fstar-mode.el:1214:1:Warning: the following functions are not known to be defined:
    flycheck-define-command-checker,
    flycheck-increment-error-columns, flycheck-mode

Hi Clement,

You may have shown me how to do this in person ... but I've forgotten.

Is there a way to force emacs to choose a certain font for rendering particular symbols. For example, I'd like the forall symbol to come from Symbola but the lambda to come from Consolas.

The only thing I am able to do is to set the fonts in some order so that it picks, say, Consolas first, if the symbol exists there, and uses Symbola otherwise. But, this is not specific to the particular characters I care about.

Please answer at your leisure.

Enjoying this emacs mode a lot!

Thanks,
Nik

I needed to switch to using the above variant of emacs to get things working with Cygwin.

Unfortunately, I'm having trouble getting fstar-mode.el to work well with it.

After checking in an initial block of code (which successfully turns blue), giving the next block to just hangs (remains pink indefinitely).

Here's a transcript from the Messages buffer ... is there a way to get it to print more debugging info?

Started F* interactive with arguments ("--in")
Processing queue
QUERY [#push
module Test
let f = "hello"
#end #done-ok #done-nok
]
OUTPUT [
#done-ok
]
RESPONSE [t] []
Queue is empty (processed)
Processing queue
QUERY [#push

let g = "world"
#end #done-ok #done-nok
]

|| and && are Boolean connectives; \/ and /\ are propositional connectives. Conflating them in the rendering is perhaps a bit confusing.

When reporting an error (in a newly opened split buffer, but this is probably a separate issue), fstar-mode includes the name of the most recently open'd module like this:
Example code, which causes an error due to the missing 't' at the end of "nat":

module Test

open FStar.Seq

type x = na

/home/kk/repositories/everest/FStar/ulib/FStar.Seq.Properties.fst(716,0-723,49): (Error) Identifier not found: [na](Also see: (5,9-5,11))] (FIXME)

Without opening FStar.Seq, the error is just

F*: subprocess exited.

(without openeing a split buffer). While running fstar.exe Test.fst from the command line just outputs:

./Test.fst(5,9-5,11) : (Error) Identifier not found: [na]

in both cases
Or maybe this is due to a configuration error on my part?

Hello, I have a strange error when trying to interactively type-check some files :
Name "FStar.All.ML" not found

This does not happen when I use FStar directly...

Any ideas ?

Would be great to have a command to kill all running F* processes.

I currently have to search through all my buffers killing F* in each one each time I want to rebuild the F* binary.

Hi all,

Based on @nikswamy's experiments I looked at adding completion support to fstar-mode.el. I cobbled together a rough prototype at https://github.com/FStarLang/fstar-mode.el/tree/company , with corresponding F* patches at https://github.com/cpitclaudel/FStar/tree/clement_info

Here's how it looks:

The basic idea is that fstar-mode send a search term, and F* responds with a list of candidates. Then, while displaying search terms, fstar-mode queries the underlying F* process to get type information. If you feel adventurous, you can test it by checking out and compiling the branches linked above :) (you'll need to M-x package-install company on the Emacs side)

Remaining issues:

• Results aren't sorted
• Completion only returns definitions, not modules (what else would be relevant?)
• Completion only returns fully qualified names, instead of using the shortest name in scope (e.g. "Som" should complete to "Some", not "Prims.Some" — but "Pr.So" should complete to "Prims.Some")
• The implementation of the #info-fqn query is horrendous (it doesn't have to be: I just didn't know which function to call to resolve a fully-qualified name)
• I haven't measured performance. What's a typical number of symbols in scope in F* (does it run in the thousands, or tens of thousands, or...)?
• Company's completion popups flicker
• The #info request doesn't work on non-fully-qualified names

Can a more experienced F* hacker help with the issues above? Thanks!

It would be nice to have automatic line breaks happening in comments when the line grows too long. From what I could find on that subject, it is already implemented in modes for other languages. Not sure if this is feasible to do, but I think this would be a useful feature.

Trying this out ... looks great!

However, it seems I don't have all the Unicode symbols available for rendering this properly on my machine. For example, the rendering of nat as a bb N doesn't show up for me (I just get a box).

What are the recommended Unicode settings for using this mode?

Thanks!

I'm getting Identifier not found errors for mutually defined functions in the emacs mode (only):

To reproduce this take any mutual fixpoint let rec ... and ... (for instance examples/bug-reports/bug442.fst), feed the val declarations to F*, but not the let rec. Then feed the let rec. There might be more circumstances / steps to reproduce this, but I manage very often without even trying too hard :)

I often make syntax errors. I get F*: subprocess exited on the command line, and go to the Messages buffer to know where to look at:

[F* raw output] Interactive mode; ignoring --verify_module{"kind":"protocol-info","version":1,"features":["autocomplete","describe-protocol","exit","lookup","lookup/documentation","pop","push"]}
[F* error] C:/cygwin64/home/fournet/everest/mitls-fstar/src/tls/Handshake.fst(310,18-310,18): (Error) Syntax error: Parsing.Parse_error
[F* error] 1 error was reported (see above)
F*: subprocess exited.
Mark set [2 times]

Displaying the detailed error within my fstar buffer would be very convenient.

Hi Clement,

Many of us use cygwin emacs with a native windows F* using OCaml.

It turns out that in this configuration, fstar-mode.el is unable to parse the version of F*. It complains with

version-to-list: Invalid version syntax: '0.9.3.1-beta^M'

Notice the suspicious trailing ^M.

Could this be handled within fstar-mode.el, perhaps getting it to trim the string before parsing it?

Thanks,
Nik

Hi Clement,
thanks a lot for this Emacs mode, it's my favourite :)

Emacs for Mac recently got support for font ligatures, and there are cool fonts like Fira and Hasklig that offer substitutions for character combinations that look better than their single character counterparts.
It would be great to disable character substitution for those specific cases, would that be possible to configure through some Emacs settings?

Hi all,

company-coq got subscript highlighting a few months after fstar-mode got it, and in hindsight I feel that it works a bit better there. Unlike fstar-mode (which requires an underscore), company-coq highlights all numbers at the end of variable names as subscripts. Concretely, that means that you can write x1 instead of x_1 to get x₁.

Quick statistics suggest that fstar-mode's _<number> syntax isn't used very often in F* code in the wild, while identifiers with a number at the end are pretty common (see table below). And in fact, when the _<number> syntax is used, it isn't always obvious that a subscript was actually desired (e.g. lemma_intro_modifies_0, division_definition_lemma_1, lognot_lemma_1). In the entire ulib/ directory, I could find only four examples of short variable names using the _<number> syntax: s_1, s_2, qj_1, and qj_2. The only other cases that I could find where _ are used for subscripting are the int_8, int_16 etc. types.

How would we feel about changing F* mode to highlight x1 as x₁? To prevent confusion, this would mean ceasing to highlight x_1 as x₁ (otherwise it wouldn't be possible to distinguish x1 an x_1). Of course, it'd remain easy to turn off subscripts highlighting entirely, and it would also be relatively easy to locally hide the _, if desired.

[File name]                            [x1]     [x_1]
FStar.All.fst                          3        0
FStar.Array.fst                        136      0
FStar.Axiomatic.Array.fst              41       0
FStar.BitVector.fst                    0        8
FStar.Buffer.Quantifiers.fst           50       10
FStar.Buffer.fst                       1739     376
FStar.Bytes.fst                        0        0
FStar.Classical.fst                    0        5
FStar.Constructive.fst                 19       0
FStar.Crypto.fst                       3        0
FStar.DependentMap.fst                 144      0
FStar.ErasedLogic.fst                  8        0
FStar.Fin.fst                          22       0
FStar.FunctionalExtensionality.fst     0        0
FStar.Ghost.fst                        12       0
FStar.Heap.fst                         80       0
FStar.HyperHeap.fst                    147      0
FStar.HyperStack.fst                   187      6
FStar.IndefiniteDescription.fst        0        0
FStar.Int.Cast.fst                     249      0
FStar.Int.fst                          19       0
FStar.Int128.fst                       12       0
FStar.Int16.fst                        12       0
FStar.Int31.fst                        12       0
FStar.Int32.fst                        12       0
FStar.Int63.fst                        12       0
FStar.Int64.fst                        12       0
FStar.Int8.fst                         12       0
FStar.Integers.fst                     3        22
FStar.List.Tot.Base.fst                109      0
FStar.List.Tot.Properties.fst          435      0
FStar.List.Tot.fst                     0        0
FStar.List.fst                         164      0
FStar.MRef.fst                         37       0
FStar.Map.fst                          108      0
FStar.MarkovsPrinciple.fst             0        0
FStar.Math.Lemmas.fst                  117      52
FStar.Math.Lib.fst                     9        3
FStar.Monotonic.RRef.fst               38       0
FStar.Monotonic.Seq.fst                255      63
FStar.Mul.fst                          0        0
FStar.OrdMap.fst                       81       0
FStar.OrdMapProps.fst                  0        0
FStar.OrdSet.fst                       278      0
FStar.OrdSetProps.fst                  31       0
FStar.PredicateExtensionality.fst      12       0
FStar.PropositionalExtensionality.fst  6        0
FStar.Reader.fst                       30       0
FStar.Relational.Comp.fst              169      0
FStar.Relational.Relational.fst        54       0
FStar.Relational.State.fst             4        0
FStar.ST.fst                           19       0
FStar.Seq.Base.fst                     153      0
FStar.Seq.Properties.fst               535      4
FStar.Seq.fst                          0        0
FStar.Set.fst                          102      0
FStar.Squash.fst                       0        0
FStar.SquashEffect.fst                 0        0
FStar.SquashProperties.fst             37       0
FStar.StrongExcludedMiddle.fst         0        0
FStar.Struct.fst                       1253     84
FStar.StructNG.fst                     1269     71
FStar.TSet.fst                         88       0
FStar.Tcp.fst                          0        0
FStar.TwoLevelHeap.fst                 35       0
FStar.UInt.fst                         289      61
FStar.UInt128.fst                      14       0
FStar.UInt16.fst                       14       0
FStar.UInt31.fst                       14       0
FStar.UInt32.fst                       14       0
FStar.UInt63.fst                       14       0
FStar.UInt64.fst                       14       0
FStar.UInt8.fst                        14       0
FStar.Universe.fst                     5        0
FStar.Util.fst                         0        0
FStar.WellFounded.fst                  5        0
prims.fst                              104      1

I have the blank square issue, but I'm using the recommended font (DejaVu Sans). Which fonts have the "cons" symbol? Is it possible to disable this symbol only?

Thanks,

Jonathan

If I do C-c C-RET in the middle of a toplevel definition, I get a Parsing.Parse_error, then it's impossible to recover from it, I have to kill the subprocess and make sure I only ever hit C-c C-RET while I'm right after a toplevel definition.

It seems that there is some magic convention about double-newlines? If so, it would be good to specify it on the README.md page.

Thanks,

Jonathan

These are comments, so 7c16a9c strips them, but they should be an exception.

I'm trying to install fstar-mode.el from source rather than from melpa.

It fails while trying to evaluate (require dash)

I've tried to M-x package-install dash, but melpa doesn't seem to know about it.

Any suggestions?

Hi Clement, I'm trying to understand the coloring rule for identifiers. In the snippet below, the three top-level identifiers all have different colors. What does it signify? Thanks!

Hi Clement @cpitclaudel ! Just decided to fill some nits in the syntax highlighting that I find annoying. If you have time at some point could you have a look ? Clearly this is not an emergency... ;) Thanks a lot ! B.

The characters (// seems to be interpreted by fstar-mode as a comment initiator which cannot be terminated (It displays everything until the end of buffer as commented).

I'd like to have a third possible outcome, that says "please display this error message, then kill the fstar process". Would it be hard to implement?

(Granted, I could rework the F* code to be able to do this without a third message, but it's a lot of work and #done-kill seems like a useful feature to have.)

Thanks,

Jonathan

I'm getting started with FStar at the CUFP tutorial and attempting to use this emacs mode results in the following message when I load a .fst file: File mode specification error: (void-function fstar-setup-prettify).

I installed the mode by using:

git clone https://github.com/FStarLang/fstar-mode.el ~/.emacs.d/site-lisp/fstar-mode
echo "(require 'fstar-mode ]"~/.emacs.d/site-lisp/fstar-mode/fstar-mode.el\")" >> ~/.emacs

Lines commented by // are not coloured in red =)

Sometimes when I push a new chunk of code for which verification succeeds, and saving the buffer immediately after, the state reverts to the previous checkpoint (reverting the chunk that just verified).

Sorry if this is hard to reproduce.
I can't say exactly what triggers this but I hit this quite often in a session.
Mostly, I want to know if I'm the only one seeing this behavior or if it is something that other users experienced.

I'm wondering whether it would be possible to tag an fstar-mode.el release corresponding to the new F* release we did yesterday, so that people who want to use the binary package have some chance to also use a working version of the interactive mode. This would increase the value of our releases and thus motivate us to release some more :)

Just a heads up that F* now has experimental support for transitive dependencies via build-config. Editor support for this would of course be nice, if you have some more time to spare :)
FStarLang/FStar#272 (comment)

Hi Clement, in the following code, using C-c C-RET at the end of the buffer sends an incomplete buffer to F* (pasting the command sent at the end). This was working a few days back, so I suspect this could be a regression from the last commit. Thanks!

module Test

type t =
  | C: nat
       -> nat //a constructor
       -> t
  | D: nat -> t // another constructor

QUERY [#push 1 0
module Test

type t =
  | C: nat
       -> nat                
           
                                      
#end #done-ok #done-nok
]

Would save a few keystrokes.

It's annoying that C-c C-n stops at (*

module M
(*


*)
val u : unit

If I'm working on file A which depends on file B and I make a change in B I then

1. kill the subprocess in file A in order to reload file B
2. get a message F*: subprocess exited. until I fix any outstanding syntax errors and save them

Is step 1 the appropriate way to deal with this situation?

As a feature request, once I have started stepping into a file, syntax errors/what is saved is no longer a problem, it would be great if it were the same initially.