search

FStarLang / fstar-mode.el

Emacs support for F*
Apache License 2.0
67 stars 17 forks source link

Definition lookup works only once #97

Closed wintersteiger closed 5 years ago

wintersteiger commented 6 years ago

Example:

module Blah
let _ = FStar.UInt.lognot_lemma_1

Once F* is started (C-n), I can look up lognot_lemma_1 via M-., which opens FStar.UInt.fst and correctly puts me at the right place in the file. It's definition looks like so:

val lognot_lemma_1: #n:pos ->
  Lemma (requires True) (ensures (lognot #n (zero n) = ones n))
let lognot_lemma_1 #n = nth_lemma (lognot #n (zero n)) (ones n)

Once I'm there, I can not look up nth_lemma by pressing M-.; it just tells me to start a new F* process, thusly:

Please start F* to use this feature

This has never worked for me, through multiple versions of Windows, Ubuntu, F*, Emacs (both on Windows and Linux). The only thing that's unusual in my setup, but possibly at the core of the problem, is that I compile my own Emacs from the latest sources; it currently reports GNU Emacs 27.0.50 (build 1, x86_64-pc-linux-gnu) of 2018-07-18.