verifast-mode for Emacs

[arseniy.za...@dslab.org]

Hello,
Here is to promote a little undergoing of mine: the Emacs mode for VeriFast theory files.
The mode is very simple, it provides only syntax highlighting and indentation and a couple of useful ya-snippets, but that was already a great relief for me, comparing to the cc-mode.
Unfortunately, the mode currently supports only the pure VeriFast files (*.gh). There are ways to combine cc-mode with verifast-mode while editing the C files, but no one of them seems satisfactory.

Contributions are welcome!

8X------ sweet dreams below -------

I am aware of the VeriFast IDE, but unfortunately its editing capabilities are not nearly close to those of my favorite text editor.
I would love to extend verifast-mode to support all the features of vfide, but I do not have enough time these days.
The idea is simple: based on the comint-mode (https://www.emacswiki.org/emacs/ComintMode) make verifas-mode able to send lemmas one-by-one to verifast to check and show the unsound steps. We can add buffers for steps, assumptions, heap chunks, stack variables. It should be similar to the Proof General (https://proofgeneral.github.io/)
This would require extending the verifast terminal application to export context information, which should not be difficult, as vfide already does that.

The further step would include a context- and type- sensitive search over all the applicable lemmas, refactoring, support for automatic proof generation for simple lemmas.

[arseniy.za...@dslab.org]

Here is the link:
https://github.com/necto/verifast-mode

[Kiwamu Okabe]

On Fri, Mar 17, 2017 at 11:46 PM, <arseniy.za...@dslab.org> wrote:
> Here is to promote a little undergoing of mine: the Emacs mode for VeriFast
> theory files.

So great work!
I was dreaming some product like https://proofgeneral.github.io/ for VeriFast!
--
Kiwamu Okabe at METASEPI DESIGN