search

FStarLang / fstar-mode.el

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

Emacs sends incomplete buffer to F* in case the comments are inlined in certain style (recent regression) #43

Closed aseemr closed 7 years ago

aseemr commented 7 years ago

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
]
cpitclaudel commented 7 years ago

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

cpitclaudel commented 7 years ago

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
]
aseemr commented 7 years ago

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.

cpitclaudel commented 7 years ago

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?

aseemr commented 7 years ago

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!

cpitclaudel commented 7 years ago

Sure, I'd be happy to! Sorry to hear that things aren't working well. Can you include a screenshot, as well as the info produces by M-x report-emacs-bug, if possible?

aseemr commented 7 years ago

emacs_comments_1 emacs_comments_2

aseemr commented 7 years ago

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.

aseemr commented 7 years ago

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))

aseemr commented 7 years ago

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

cpitclaudel commented 7 years ago

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

cpitclaudel commented 7 years ago

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?

aseemr commented 7 years ago

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

cpitclaudel commented 7 years ago

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