Emacs sends incomplete buffer to F* in case the comments are inlined in certain style (recent regression) about fstar-mode.el HOT 14 CLOSED

Thanks for the report; I'll investigate tonight if I have time.

from fstar-mode.el.

Hmm. I can't reproduce this. What version of Emacs are you using? I get the following in both 24.5 and 25.

QUERY [#push 1 0
module Test

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

from fstar-mode.el.

Hi Clement, I have GNU Emacs 24.5.1 (x86_64-unknown-cygwin), and I am using the fstar-mode.el from the git repo, i.e. I load it using load-file, and then I see this behavior.

from fstar-mode.el.

Hi @aseemr. Sorry for the delay; is the problem still happening? If so, I'll boot into Windows and investigate there. You use cygwin Emacs with a pre-built fstar, right?

from fstar-mode.el.

Hi Clement: yes, the problem still seems to be there. Others also observed it, and for now we have reverted to the version before this change. Yes, I have cygwin emacs, though it should be independent of F*, for example, even in the editor I see the whole buffer after a // comments all red. Would be great if you can take a look, thanks!

from fstar-mode.el.

from fstar-mode.el.

from fstar-mode.el.

Hi Clement: attaching two snapshots, as you can see in the first one the buffer passed to the F* process contains the code after the comment, whereas in the second one it does not. In the second case, the color of the buffer also becomes red once I refresh the buffer.

from fstar-mode.el.

In GNU Emacs 25.1.1 (x86_64-unknown-cygwin)
of 2016-09-18 built on desktop-new
Windowing system distributor 'Microsoft Corp.', version 10.0.14393
Configured using:
'configure
--srcdir=/home/kbrown/src/cygemacs/emacs-25.1-1.x86_64/src/emacs-25.1
--prefix=/usr --exec-prefix=/usr --localstatedir=/var --sysconfdir=/etc
--docdir=/usr/share/doc/emacs --htmldir=/usr/share/doc/emacs/html -C
--with-w32 'CFLAGS=-ggdb -O2 -pipe -Wimplicit-function-declaration
-fdebug-prefix-map=/home/kbrown/src/cygemacs/emacs-25.1-1.x86_64/build=/usr/src/debug/emacs-25.1-1
-fdebug-prefix-map=/home/kbrown/src/cygemacs/emacs-25.1-1.x86_64/src/emacs-25.1=/usr/src/debug/emacs-25.1-1'
CPPFLAGS= LDFLAGS='

Configured features:
XPM JPEG TIFF GIF PNG IMAGEMAGICK SOUND DBUS NOTIFY ACL GNUTLS LIBXML2
ZLIB TOOLKIT_SCROLL_BARS

Important settings:
value of $LANG: en_US.UTF-8
locale-coding-system: utf-8-unix

Major mode: Messages

Minor modes in effect:
diff-auto-refine-mode: t
tooltip-mode: t
global-eldoc-mode: t
electric-indent-mode: t
mouse-wheel-mode: t
tool-bar-mode: t
menu-bar-mode: t
file-name-shadow-mode: t
global-font-lock-mode: t
font-lock-mode: t
blink-cursor-mode: t
auto-composition-mode: t
auto-encryption-mode: t
auto-compression-mode: t
buffer-read-only: t
line-number-mode: t
transient-mark-mode: t

Recent messages:

let bar _ :nat =

#end #done-ok #done-nok
]
OUTPUT [C:\cygwin64\home\aseemr\FStar\bin..\ulib\prims.fst(690,0-690,39): (Error) Syntax error: Parsing.Parse_error(Also see: (6,1-6,1))

#done-nok

]
RESPONSE [nil] [C:\cygwin64\home\aseemr\FStar\bin..\ulib\prims.fst(690,0-690,39): (Error) Syntax error: Parsing.Parse_error(Also see: (6,1-6,1))]
previous-line: Beginning of buffer [4 times]

Load-path shadows:
None found.

Features:
(shadow sort mail-extr emacsbug message dired format-spec rfc822 mml
mml-sec password-cache epg gnus-util mm-decode mm-bodies mm-encode
mail-parse rfc2231 mailabbrev gmm-utils mailheader sendmail rfc2047
rfc2045 ietf-drums mm-util help-fns mail-prsvr mail-utils warnings
derived cl-seq cl-macs rx vc-git diff-mode easy-mmode fstar-mode edmacro
kmacro help-at-pt dash finder-inf package epg-config seq byte-opt gv
bytecomp byte-compile cl-extra help-mode easymenu cconv cl-loaddefs
pcase cl-lib time-date mule-util tooltip eldoc electric uniquify
ediff-hook vc-hooks lisp-float-type mwheel disp-table w32-win w32-vars
term/common-win tool-bar dnd fontset image regexp-opt fringe
tabulated-list newcomment elisp-mode lisp-mode prog-mode register page
menu-bar rfn-eshadow timer select scroll-bar mouse jit-lock font-lock
syntax facemenu font-core frame cl-generic cham georgian utf-8-lang
misc-lang vietnamese tibetan thai tai-viet lao korean japanese eucjp-ms
cp51932 hebrew greek romanian slovak czech european ethiopic indian
cyrillic chinese charscript case-table epa-hook jka-cmpr-hook help
simple abbrev minibuffer cl-preloaded nadvice loaddefs button faces
cus-face macroexp files text-properties overlay sha1 md5 base64 format
env code-pages mule custom widget hashtable-print-readable backquote
dbusbind gfilenotify w32 multi-tty make-network-process emacs)

Memory information:
((conses 16 173119 5422)
(symbols 48 25965 0)
(miscs 40 91 132)
(strings 32 40031 6531)
(string-bytes 1 995526)
(vectors 16 19294)
(vector-slots 8 524176 5858)
(floats 8 205 245)
(intervals 56 274 0)
(buffers 976 21))

from fstar-mode.el.

Above is the output of M-x report-emacs-bug. Thanks!

from fstar-mode.el.

Thanks, that's plenty of useful info. Please ping me by the end of the week if I haven't given signs of progress :)

from fstar-mode.el.

I tried reproducing this, but I really seem not to be able to. I wonder if the byte-compiler is messing up in some way. I installed your version of Emacs on cygwin with an empty .emacs did M-x package-install fstar-mode, configure fstar-executable, and ran through the example file, but everything seemed to work fine.

Could it be that something went wrong when installing the package? Can you try removing fstar-mode and re-installing it?

from fstar-mode.el.

hi @cpitclaudel, removing and re-installing worked, thanks! @nikswamy, @fournet, try this if you are still facing the issue.

from fstar-mode.el.

Thanks. No idea what caused this, but glad to hear it's resolved :)

from fstar-mode.el.