|
|
|---|
|
|
|
|---|
A short ACL2s tutorial
Before starting this guide, follow the ACL2s-installation guide to install ACL2s on your system.
We will now guide you through the process of creating a new ACL2s/Lisp file, typing definitions into that file, opening up an associated ACL2 session, sending definitions to the session, querying the session, etc.
The first time you run Eclipse, it will prompt you for a "workspace" location. This is where Eclipse will save your configuration and layout and is the default location for your ACL2s projects and their associated files. Please choose a fresh workspace (e.g. /Users/yourname/acl2s-workspace) that is different from the workspace you use for Java or other eclipse projects.
If you get a welcome window, you can either click on "Hide" at the top-right corner of the screen or click on the "X" button to the right of the "Welcome" tab at the top of the screen.
To familiarize yourself with some Eclipse vocabulary and navigating the workbench, we recommend going through the Basic Tutorial section of the Workbench User Guide.
Create a project: Select File | New | Project... and select Project from the group General. Give a name to the project that will contain your ACL2 developments and click Finish.
Open the "ACL2 Development" perspective: Select
Window | Perspective | Open Perspective | Other... and then select ACL2 Development and then Open in the window that appears.
You could have instead clicked on the
Note that, on macOS, depending on where the workspace and project directories are located, you may get a popup asking you to give Eclipse access to one of your folders (typically Documents or Desktop). You should respond "Yes" if you're comfortable letting Eclipse access these folders (so it can access your workspace and project folders), or respond "No" and move your workspace somewhere that macOS does not require permission to access (see this Apple help page for more information).
Create a new Lisp file for getting the feel of Eclipse and our plugin. Select File | New | ACL2s/Lisp file. The "Directory" should already indicate the project you just created. If not, browse to the project you just created. Pick a file name like "test.lisp" or leave the default. Use "ACL2s" for the session mode and click Finish.
You can now type some ACL2 code in the editor. Type in this definition to get the feel of the auto-indenting, paren-matching, and syntax-based coloring:
; Computes the nth fibonacci number (maybe?) (definec fib (n :nat) :nat (match n ((:or 0 1) (+ (fib (1- n)) (fib (- n 2)))) (& 1)))
Upon creating the new file, an editor has now opened in the editor area of the workbench. Around the editor area are views, such as the Project Explorer view to the left and Outline view to the right. From their title areas, these can be dragged around, tiled, minimized, etc. You probably also noticed that (definec fib (n :nat) :nat showed up in the Outline view, which you can use to navigate the top-level forms of your file.
In the Project Explorer view, which is a tree view of projects and files, expand your project to reveal a few files:
Open test.lisp.a2s by double-clicking it in the
Project Explorer. Alternatively, hit Ctrl+Shift+o
(Mac:
Start a session for testing our code in test.lisp by
clicking the
ACL2 should start up, resulting in a .a2s file opening up and the "ACL2S >" prompt appearing after a few seconds.
Type an "immediate command" for ACL2, such as
(* 21 2)in the session editor (.a2s editor). Notice that the editor is read-only except for the part after the last prompt. Hitting Enter (Return) at the end of this editor will submit the typed form to ACL2. Actually, it will only submit syntactically valid commands to ACL2, so if one tries to trick it by hitting Enter after just
(* 21, the editor just goes to the next line.
Try submitting other types of input to ACL2.
(* 21 2)was classified by the plugin as "VALUE" input, because it's just computation that returns a value. Another example is a "QUERY" such as
:pe strip-cars, which prints out information about the current history or "world", in this case the definition of the function "strip-cars".
(definec successor (x :int) :int (1+ x))is an "EVENT" because it (potentially) changes the history. See ACL2s-command-classifications for more detail. For "EVENT" inputs, ACL2s pops up a dialog asking what to do about the fact that we did something logically relevant from the command line rather than from our source code. Read the dialog and for now choose "Insert".
Try submitting something with an error such as
(successor 1 2)This has an error because the arity of the successor function we just defined is 1. The red (maroon, I guess) output indicates the command was not successful. ACL2 is back in the state it was in before you submitted the form that caused the error.
Switch back to the .lisp editor where you will discover the
(definec successor (x :int) :int (1+ x))form we submitted in the session editor has been "inserted" above what we had typed previously! Also, that form is "above the line" and read-only. This is part of the intrinsic linkage between somename.lisp and somename.lisp.a2s: the forms "above the line" in the .lisp editor are those used to get the ACL2 session in the .lisp.a2s editor in its current state. To maintain this invariant, we have to do one of two things in the case of executing something history-relevant in the session editor: insert it at the line in the lisp editor or undo it. These are the options the "Relevant input at command line" dialog gave us. Note that "QUERY"s and "VALUE"s do not modify the history, so we don't need to insert those above the line.
Try moving the line past the definition we gave
for fib by pressing the "advance todo" button on the toolbar
(
The plugin models two "lines" in a .lisp file: the "completed line" and the "todo line". These "lines" are only visible as the boundary between regions with different highlighting. The "completed line" is at the last point of gray (or blue) highlighting. The "todo line" is at the last point of any highlighting: gray, blue or green.
Above the "completed line" is the (potentially empty) "completed region," which has forms that ACL2 has--get this--completed. Between the two lines are forms that we want ACL2 to work on completing (hence "todo"). This (potentially empty) region, the "todo region", has green highlighting. We can call the rest of the buffer the "working region", which is the freely editable part.
So what was the meaning of the flash of green highlighting? Clicking "advance todo" moved the "todo line" from between
(definec successor ...)and
(definec fib ...)to after
(definec fib ...). With at least one form in the "todo region", the session started processing the first (and only) one. If you look at the session output, you see that the attempt to admit our
Fix our
; Computes the nth fibonacci number (definec fib (n :nat) :nat (match n ((:or 0 1) 1) (& (+ (fib (1- n)) (fib (- n 2))))))Now clicking "advance todo" should result in the definition flashing green while it is in the todo region and turning gray after being accepted.