---

Ⅰ. 插件描述

a vim plugin for Dafny, a verified programming language.

Ⅱ. 基本信息

创建日期：  2015-04-24 使用用户：  7 Github星：  10 插件作者：  Lilith Stephenson

Ⅲ. 安装方法

使用Vundle管理器安装

在你的.vimrc下添加:

Plugin 'mlr-msft/vim-loves-dafny'

… 然后在Vim中运行以下命令:

:source %
:PluginInstall

对于Vundle版本 < 0.10.2，请用上面的Bundle替换Plugin。

使用NeoBundle管理器安装

在你的.vimrc下添加:

NeoBundle 'mlr-msft/vim-loves-dafny'

… 然后在Vim中运行以下命令:

:source %
:NeoBundleInstall

使用VimPlug管理器安装

在你的.vimrc下添加:

Plug 'mlr-msft/vim-loves-dafny'

… 然后在Vim中运行以下命令:

:source %
:PlugInstall

使用Pathogen管理器安装

在终端中运行以下命令:

cd ~/.vim/bundle
git clone https://github.com/mlr-msft/vim-loves-dafny

Ⅳ. 文档说明

vim ❤ dafny

vim-loves-dafny is a Vim plugin for
Dafny, a
C#-like
language with support for formal verification.

Features

• .dfy file detection.
• Syntax highlighting.
• Syntastic integration

Installation

You can use your favorite
pathogen-compatible plugin manager to
install vim-loves-dafny.

If you're using vim-plug, for example,
follow the following steps:

1. Edit your .vimrc and add a Plug declaration for vim-loves-dafny.

   call plug#begin()
   " ...
   Plug 'mlr-msft/vim-loves-dafny', {'for': 'dafny'}
   " ...
   call plug#end()

2. Restart Vim
3. :PlugInstall to install the plugin.

Configuration

Customizing the Dafny command arguments

You can ask Syntastic to pass
custom arguments to Dafny. For example, you can add the following to your
vimrc:

let g:syntastic_dafny_dafny_args = '-allowGlobals'

Passive Syntastic Checks

Non-trivial Dafny programs may take significantly more time to verify than a
compiler would take to compile a single source file-- particularly if you are
using include directives in your Dafny source. Unfortunately, Vim, being
single-threaded, will freeze while Dafny is verifying your sources. We strongly
recommend that you set Syntastic up to check your Dafny sources passively
(on-demand) for this reason.

Add the following to your .vimrc to set this up:

" (optional) set your leader key (the default is <\>)
let mapleader=","
" Tell Syntastic to:
" - check files on save.
" - but only check Dafny files when requested.
let g:syntastic_mode_map = {
        \ "mode": "active",
        \ "passive_filetypes": ["dafny"] }
" (optional) map "save and check current file" to <leader>c
noremap <Leader>c :w<CR>:SyntasticCheck<CR>

Now, you can use :SyntasticCheck or, if you elected to do so, ,c to check
your dafny file.

License

vim-loves-dafny is distributed under the Microsoft Public License, which same
license that Dafny itself uses. See
LICENSE for
more details.

Planned Improvements

• more vibrant syntax highlighting.