boogie-org / boogie-friends Goto Github PK
View Code? Open in Web Editor NEWTools for interacting with Boogie
Tools for interacting with Boogie
Example - http://rise4fun.com/Dafny/Ute6
When a error is related to parent module of a refinement, Dafny will output error lines as "X.dfy[Y]: ...",
and current error pattern will interpret the filename as "X.dfy[Y]".
Here is my local fix in .emacs, it also contains a workaround attempt of #8.
(setq old-parse-errors (symbol-function 'inferior-dafny-parse-errors))
;; a workaround for removing [module-name] and dealing with external file locations
(defun inferior-dafny-parse-errors (errors)
(mapc (lambda (e)
(let ((fname (flycheck-error-filename e)))
(if (eq fname nil)
(setq fname buffer-file-name)
(if (string-match
(rx (group (* (not (in "[]")))) (* anything))
fname)
(setq fname (match-string 1 fname)))
(if (not (string-equal fname buffer-file-name))
(let ((old-fname (flycheck-error-filename e))
(old-msg (flycheck-error-message e))
(old-col (flycheck-error-column e))
(old-line (flycheck-error-line e)))
(setf (flycheck-error-message e)
(concat (format "%s(%d:%d)-"
(file-name-nondirectory fname)
old-line
old-col
)
old-msg
"(" old-fname ")"))
(setf (flycheck-error-column e) nil)
;; since line is required ...
(setf (flycheck-error-line e) 1)
(setq fname buffer-file-name))))
(setf (flycheck-error-filename e) fname)
))
(funcall old-parse-errors errors)))
Thanks for creating this excellent mode!
I am interested in trying the inferior-dafny backend to take advantage of Dafny's caching. But when I enable it, nothing happens. I turned on (inferior-dafny-toggle-debug)
and can see that the client is sending messages, but it looks like the server never responds. In fact, while inferior-dafny-live-p
returns non-nil, I can find no evidence outside of Emacs that the server is actually running (eg, ps aux | grep -i dafny
finds nothing).
I am running OS X and had to patch flycheck-def-executable-var
to point to a shell script that runs DafnyServer.exe
under mono, similar to the script that runs Dafny.exe
. Before I did this, I still got no error message, despite the fact that the executable file it was looking for did not exist.
I am looking for help getting more information about exactly what inferior-dafny is trying to do and why it's not starting the server properly.
datatype foo = Foo |
Bar
lemma hello() {}
dafny-mode
seems to not realise that the datatype declaration has completed and wants to indent everything following that extra level. Any ideas?
Howdy Boogie-friends,
I really appreciate y'all, and I can live with what I have working and be very grateful for at least the syntax highlighting and other features. But fly-check and compiling internally would be nice...
The problem: Both flycheck and compiling are complaining about discovering .NET Core:
Suspicious state from syntax checker dafny: Flycheck checker dafny returned 1, but its output contained no errors: Error: Dafny requires .NET Core to run on non-Windows systems.
Try installing a more recent version of dafny, and please open a bug report if the issue persists in the latest release. Thanks!
Suspicious state from syntax checker dafny: Flycheck checker dafny returned 1, but its output contained no errors: Error: Dafny requires .NET Core to run on non-Windows systems.
Try installing a more recent version of dafny, and please open a bug report if the issue persists in the latest release. Thanks!
Below is a screen shot that best summarizes my state:
Left Top :: .emacs
setup doing everything to find .NET Core and setting up boogie-friends to succeed.
Left Mid-Top :: Flycheck verification showing dafny working
Left Mid-Bot :: Error messages from flycheck and compilation
Left Bottom :: test.dfy
buffer
Right Top :: execution of dafny test.dfy
successful. FYI, I am on Dafny 3.2.0.30713
Right bottom :: execution of quicktest.sh
from my dafny source.
I can even compile and test my team's current projects, as long as I am not in emacs.
I will keep track of #23 to see if that resolution de-dupes this. It does not seem likely...
I will say I was confused by the installation directions for Mac OS:
From the README.md/Setup/Automatic/Step 3:
On GNU/Linux or MacOS, use the path to the dafny and dafny-server wrapper scripts for the first two.
Are you sure it is the first two? I had imagined it would be flycheck-dafny-executable
and flycheck-inferior-dafny-executable
.
That won't solve my problem, but being explicit in the README may prevent other's confusion.
Happy to support in any way. Tony
The emacs mode for Dafny visualizes Dafny's forall
keyword in two different ways. For forall
expressions (that is, universal quantifications), it visualizes the keyword as an ∀. For forall
statements it (mostly) visualizes the keyword as itself (forall
). Which one to choose is, I believe, determined by a simple syntactic scan of some things that follow the forall
keyword. Here is one case where that simple scan makes the wrong determination, which I think can easily be improved.
When the ensures
clause happens on the subsequent line, all is good:
forall x: int | true
ensures Ǝ y :: x == y
{
}
But when the first line contains a ::
(even if there's an ensures
in between), then the forall
turns into a ∀:
∀ x: int | true ensures Ǝ y :: x == y {
}
It would seem that the syntactic scan could look for an ensures
. If it finds an ensures
before it finds a ::
, then the preceding forall
is probably a forall
statement.
Thanks for dafny-mode and friends. By accident, I discovered that if I add:
(setq dafny-prover-custom-args '("/printTooltips"))
... to my .emacs
, then I get handy tooltips for selected triggers and decreases clauses. Perhaps consider documenting this feature in the README?
When I write a sequence of case statements, my expectation is that Tab
to re-indent dafny code would line up all case
occurrences vertically with the same number of space characters from the left of each line. However, each case
is lined up with the statements inside of the case
above:
method Baz(x:int) returns (y:int)
{
if {
case x == 0 =>
y := 0;
case 0 < x =>
y := y + 1;
case x < 0 =>
y := y - 1;
}
}
Suppose I create two files, A.dfy
and B.dfy
, as follows:
A.dfy
:
predicate Problem() {
1 == false
}
B.dfy
:
include "A.dfy"
lemma UhOh()
ensures false
{
}
When viewing A.dfy
, the type error in the body of Problem
is correctly identified. However, when viewing B.dfy
, no error is reported (the Flycheck status in the modeline indicates no errors, and there are no errors to be jumped to via Flycheck keybindings). Commenting the include
statement causes the unprovable lemma to be correctly identified.
In general, this problem is: when there is a syntax or type error in an included file (i.e. A.dfy
), verification of the including module (i.e. B.dfy
) appears to succeed. A verification error in the included file will not cause this effect, and this effect will not mask the reporting of syntax or type errors in the including file—only verification errors are masked by this problem.
It's unclear to me whether the fix to this bug lies with Dafny or with the Emacs mode; paging @RustanLeino for further discussion of this.
The automatic formatting that dafny-mode performs does not produce nice results in calc
statements. In fact, I find the automatic formatting is working against me, and I constantly have to correct what it's doing. I'd love to see this improved.
Repro:
Start with
lemma L() {
calc {
}
}
Then, inside the braces that follow the calc
statement, type the following lines in order:
A(x);
==
B(x);
C(x);
== // here is a comment
D(x);
== { MyFavoriteLemma(x, y); }
E(x);
{ AnotherLemma(x, y); }
F(x);
<
100;
This produces:
lemma L() {
calc {
A(x);
==
B(x);
C(x);
== // here is a comment
D(x);
== { MyFavoriteLemma(x, y); }
E(x);
{ AnotherLemma(x, y); }
F(x);
<
100;
}
}
but I wish it would instead produce:
lemma L() {
calc {
A(x);
==
B(x);
C(x);
== // here is a comment
D(x);
== { MyFavoriteLemma(x, y); }
E(x);
{ AnotherLemma(x, y); }
F(x);
<
100;
}
}
When there is an error in the file, adding a line of whitespace above the error causes the flycheck highlighting to incorrectly "move up" (or to incorrectly "stay put", depending on your prospective).
For example, consider the following file.
method Foo() returns (j: int)
ensures j > 0
{}
When inferior-dafny
checks this file, flycheck places an error on the open curly brace and a warning on the greater-than symbol. Now go to the top of the file and add a few newlines. Note that flycheck is now highlighting empty whitespace.
This can be very confusing if you don't realize the highlighting is wrong!
I am wondering if it would be possible to have flycheck autodetect that the current buffer is a Dafny or Boogie test, and to use the flags in the // RUN:
comment at the top of the file instead of the otherwise configured flags.
This would solve the issue of flycheck reporting spurious errors when editing a test due to using different flags than the ones the test expects.
Perhaps the easiest way to implement this is just to look for such comments in any files and use them as flags.
Since this behavior could be surprising, it might be best if it was guarded by a customizable variable.
I'm planning to prototype it for my own use, but was curious to see whether others would fine it helpful.
I've found the following quite handy in my .emacs file to enable M-x compile to parse Dafny and Boogie error messages and warnings, and give me a clickable link directly to the offending source location. I don't know if this fits in the agenda for this package, so feel free to incorporate it or not, as you like.
(require 'compile)
(push
'(boogieErr
"^\\([a-zA-Z0-9_][^($]+\\)(\\([0-9]+\\),\\([0-9]+\\)): \\(Error\\|Verification of .* timed out\\).*$"
1 2 3) compilation-error-regexp-alist-alist)
(push
'(boogieInfo
"^\\([a-zA-Z0-9_][^($]+\\)(\\([0-9]+\\),\\([0-9]+\\)): \\(Warning:\\|Related location\\|Timed out on\\).*$"
1 2 3 0 nil) compilation-error-regexp-alist-alist)
(push 'boogieErr compilation-error-regexp-alist)
(push 'boogieInfo compilation-error-regexp-alist)
When the buffer is opened the temporary file for flycheck to verify is annoying, especially when you want to do stuff with git. Would it be better to move them to more convenient temporary file provided by mktemp
or so?
Hi. I'm trying to set up dafny for Emacs but i'm getting the message
Could not start checker for Dafny: '~/Programs/dafny/' not found. Please fix 'flycheck-dafny-executable'.
I've tried changing the path to '~/Programs/dafny/Dafny.exe' and that doesn't work either, just in case you were wondering.
How do i fix this?
Symptom
In the following, ↓
denotes the cursor position and ▯
denotes a space.
Example 1: If I have
procedure foo () {↓
then typing }
results in
procedure foo () {}↓▯
Example 2: If I have
procedure foo () {
↓
then typing }
results in
procedure foo () {
}↓▯▯▯▯▯▯▯▯▯
Cause
In contrast to Dafny mode (which has dafny-indent-keep-position
), Boogie mode does not set a custom indent-line-function
. I don't know to which function it actually points to in Boogie mode, but it causes the above behavior in boogie-friends-self-insert-and-indent
.
Possible Solutions
}
from boogie-friends.el
into dafny-mode.el
.dafny-indent
/dafny-indent-keep-position
in Boogie mode. I can't say I understand the code, but in a quick experiment just using these functions in Boogie mode seemed to behave reasonable.Any advice?
I'm working on a large project, with lots of included files and lots of moving parts. When I'm working on a single lemma, I often find I'm more productive by running Dafny on the command line with a suitable /proc: parameter to restrict verification to just the lemma I'm working on, rather than using the flycheck mode. It would be really nice if there was an equivalent to /proc in the Emacs mode, so I could say "just verify this lemma as I work on it, and ignore everything else".
BTW, I guess in theory that DafnyServer's caching should obviate the need for this, but it doesn't because:
Only verification errors are reported when using the Dafny server backend. Syntax, type checking and symbol resolution errors aren't shown. When the default backend is used instead, all errors are reported.
Could that be related to the fact that Dafny server returns I'm using Dafny 1.9.7.[SUCCESS]
when these errors occur?
And thanks for this useful mode!
I have a nasty lemma that times out without reporting any specific failures; command-line Dafny gives:
Verifying Impl$$_module.__default.lemma__ARM__L1PTE__Validity ...
[62.239 s, 67 proof obligations] timed out
pagedb.i.dfy(227,6): Verification of 'Impl$$_module.__default.lemma__ARM__L1PTE__Validity' timed out after 60 seconds
However, when I open this file in Emacs, I don't see any red squigglies, and the status bar shows only "(Dafny ... FlyC)" as if there were no errors.
This is my file:
function fib(n: int): int {
if n in {0,1}
then 1
else fib(n-1) + fib(n-2)
}
Running dafny
on it produces the following error:
$ dafny /compile\:0 /nologo /home/sohum/tmp/1fib.dfy
/home/sohum/tmp/1fib.dfy(4,9): Error: decreases expression must be bounded below by 0
/home/sohum/tmp/1fib.dfy(1,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon7_Else
(0,0): anon8_Else
Dafny program verifier finished with 0 verified, 1 error
Compilation exited abnormally with code 3 at Tue Sep 27 14:45:48
dafny-mode however crashes on it and reports no errors, showing this stack trace:
Debugger entered--Lisp error: (wrong-type-argument arrayp nil)
replace-regexp-in-string("/home/sohum/tmp/flycheck_1fib\\.dfy" "/home/sohum/tmp/1fib.dfy" nil fixed-case literal)
flycheck-fix-error-filename([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil] ("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/")
#[257 "\302�\300\301#\207" [("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/" flycheck-fix-error-filename] 5 "\n\n(fn E)"]([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil])
seq-map(#[257 "\302�\300\301#\207" [("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/" flycheck-fix-error-filename] 5 "\n\n(fn E)"] ([cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 9 "decreases n" tooltip nil] [cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 4 9 "decreases expression must be bounded below by 0" error nil] [cl-struct-flycheck-error #<buffer 1fib.dfy> dafny "/home/sohum/tmp/1fib.dfy" 1 13 nil warning nil]))
flycheck-finish-checker-process(dafny 3 ("/home/sohum/tmp/flycheck_1fib.dfy") "/home/sohum/tmp/flycheck_1fib.dfy(1,9): Info: decreases n\n/home/sohum/tmp/flycheck_1fib.dfy(4,9): Error: decreases expression must be bounded below by 0\n/home/sohum/tmp/flycheck_1fib.dfy(1,13): Related location\nExecution trace:\n (0,0): anon0\n (0,0): anon7_Else\n (0,0): anon8_Else\n\nDafny program verifier finished with 0 verified, 1 error\n" #[128 "\301\302\300�#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/")
#[0 "\304\300!\211\305=\203��\302\306!\202)�\211\307=\203(�\310\311\300\312\"\313\300!\301\314\300!\302\303&�\202)�\315\207" [#<process flycheck-dafny> ("/home/sohum/tmp/flycheck_1fib.dfy") #[128 "\301\302\300�#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/" process-status signal interrupted exit flycheck-finish-checker-process process-get flycheck-checker process-exit-status flycheck-get-output nil] 8 "\n\n(fn)"]()
funcall(#[0 "\304\300!\211\305=\203��\302\306!\202)�\211\307=\203(�\310\311\300\312\"\313\300!\301\314\300!\302\303&�\202)�\315\207" [#<process flycheck-dafny> ("/home/sohum/tmp/flycheck_1fib.dfy") #[128 "\301\302\300�#\207" [[cl-struct-flycheck-syntax-check #<buffer 1fib.dfy> dafny #<process flycheck-dafny> "/home/sohum/tmp/"] apply flycheck-report-buffer-checker-status] 5 "\n\n(fn &rest ARGS)"] "/home/sohum/tmp/" process-status signal interrupted exit flycheck-finish-checker-process process-get flycheck-checker process-exit-status flycheck-get-output nil] 8 "\n\n(fn)"])
flycheck-handle-signal(#<process flycheck-dafny> "exited abnormally with code 3\n")
It looks like the structure returned as the warning doesn't include the (flycheck-error-message)
.
Hello, I got some problem when using the dafny flycheck. I built my dafny-mode in emacs according to README. But when I open a .dfy file I got message like this
But when I checked my dafny flycheck by M-x flycheck-verify-setup
, it shows that the Dafny.exe can be found
When I type C-c C-c I got the message like this, it tells me that Dafny.exe can not be found.
And every time I save a .dfy file, the message same as the first picture comes again
mono has been installed in my computer, and I can verify the code in terminal. But how can I do it in emacs?
I don't know what was omitted in my operations.
Appreciate your help ! ! !
Sometimes, Boogie will report errors without providing location information. (This could be due to the error having no true source-level location, for example.) In that case, the flycheck error patterns simply fail to match the error, which can lead to believing a file verifies, when in fact it does not.
Consider a that has two files A.dfy
and B.dfy
. A
contains library declarations, which B
uses via the include
directive.
// A.dfy
method foo(x: int)
requires x > 0
requires x % 2 == 0
{
}
// B.dfy
include "A.dfy"
method bar()
{
foo(0);
}
Then flycheck will report that a precondition of foo
is violated, but it won't tell you which one. This gets annoying when there are many preconditions, and I am reduced to copy-pasting the contents of A
into B
or to running dafny on the command line.
Would it be possible to get this information into flycheck, preferably including the ability to jump to the precondition, just like when the caller and callee are in the same file?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.