Use Vale in Emacs!
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
python3on your path, and to set the
vale-interact-pathto point to
(setq-default vale-interact-path "/PATH/TO/interact.py")
To be able to quickly jump around between procedures, make sure to have
etagson your path.
Alternate setup using
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
(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))
||Use Vale interactively|
||Create a TAGS file for quickly jumping between procedures|
||Switch to corresponding generated
||Jump to definition of procedure under the cursor|
||Jump to definition of procedure under the cursor (in another window)|
||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.