Vl-shell
An interactive VL command loop. Allows you to use the VL kit
as a normal copy of ACL2 with VL preloaded.
The vl shell enters a Lisp read-eval-print loop. From this
loop you can invoke lp to get into an ACL2 session where
much of VL is already loaded. This is an advanced feature that is mainly
intended for developers who are debugging and hacking on VL.
For usage information, you can run vl shell --help, or see *vl-shell-help*.
Subtopics
- Vl-shell-entry
- Implementation-level vl shell command.
- Vl-shell-top
- Top-level vl shell command.
- *vl-shell-help*
