Adds support for editing Vale (Verified Assembly Language for Everest) files, and interacting with the prover.
Vale Mode requires Emacs 25 or newer.
It is distributed through MELPA.
-
Add the following to your init file (usually
.emacs
) if it is not already there:(require 'package) (add-to-list 'package-archives '("melpa" . "http://melpa.org/packages/") t) (package-initialize)
-
Restart Emacs, then run M-x package-refresh-contents and M-x package-install RET vale-mode RET. Future updates can be downloaded using M-x list-packages U x y.
-
To be able to use the interactive portions of Vale, make sure to have
python3
on your path, and to set thevale-interact-path
to point tointeract.py
from vale.(setq-default vale-interact-path "/PATH/TO/interact.py")
-
To be able to quickly jump around between procedures, make sure to have
etags
on your path.
use-package
makes your init file configuration extremely tidy, and also makes it easy to ensure that all the packages you want are automatically installed when on a new machine.
Use the following code in your init file to ensure that you've got use-package
(after the (package-initialize)
):
(eval-when-compile
(or (require 'use-package nil t)
(progn
(package-refresh-contents)
(package-install 'use-package)
(message "On a new system. Just installed use-package!"))))
Now, you can install vale-mode
simply by using the following declaration in your init file:
(use-package vale-mode
:ensure t
:custom
(vale-interact-path "/PATH/TO/interact.py")
:mode ("\\.vaf\\'" . vale-mode))
Key | Action |
---|---|
C-c C-c |
Use Vale interactively |
C-c C-t |
Create a TAGS file for quickly jumping between procedures |
C-c C-a |
Switch to corresponding generated .fst file. Repeat with the .fst to jump to the .fsti . |
C-. |
Jump to definition of procedure under the cursor |
C-' |
Jump to definition of procedure under the cursor (in another window) |
C-, |
Pop back to previous location |
Copyright 2019 Jay Bosamiya
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.