|
|
|---|
|
|
|
|---|
Frequently Asked Questions
| Q: | What is Eclipse? |
| A: | Eclipse is a highly modularized, extensible, free development environment for a variety of programming languages. See www.eclipse.org. Eclipse is written in Java and has an especially well developed development environment for Java. |
| Q: | Where do I learn about all this Eclipse lingo? |
| A: | See the Basic Tutorial section of the Workbench User Guide. |
| Q: | How do I tell what Java version Eclipse is running under, and if its 64bit? |
| A: | Inside Eclipse, go to Help | About Eclipse SDK and click "Installation Details". Under "Configuration" tab are the "eclipse.commands" property and the "java.runtime.*" properties, you will find the relevant information. You can also find out under "-arch" your machine architecture, for example, "X86_64" will indicate that you are running a 64bit Eclipse. "java.vm.name" will tell you if the Java being used is a 64bit JVM. |
| Q: | Where is Eclipse documentation? |
| A: | http://www.eclipse.org/documentation/main.html |
| Q: | Can I do a multi-user install of Eclipse? |
| A: | It is tricky to support a multi-user install of Eclipse. The key seems to be not running Eclipse at all in a way that would allow modification of the files in that eclipse installation. Once it has written some configuration stuff to the installation directory, it bombs if you can't write to that directory anymore. This is why I discourage this unless you're truly in an environment that's going to have many Eclipse users. As awkward as it sounds, just install Eclipse such that the user who will be running it can modify all of its files, and life will be easier. |
| Q: | What is ACL2? |
| A: | ACL2 is a programming language, logic, and theorem prover/checker based on Common Lisp. See the ACL2 home page for more information. |
| Q: | What is CAR? |
| A: | CAR is an abbreviation we sometimes use to refer to this
(print) book:
Computer-Aided Reasoning: An Approach.See J Moore's page about the book for description and affordable ordering information. |
| Q: | What is an ACL2 book? |
| A: | Basically, an ACL2 book is a bunch of ACL2 definitions (functions, theorems, proof rules, etc.) that can be easily imported into other ACL2 work. See ACL2::books for more information. |
| Q: | Can I use my own version of ACL2? i.e. Finding ACL2 on user's system: |
| A: |
This used to be a pain, but it's much simpler now. First, we have a preference in the Eclipse preferences (under ACL2s > ACL2) that allows one to specify the directory that contains your ACL2 image, whether it's "saved_acl2", "run_acl2", or "bin/acl2.exe" under that directory. If you don't specify that preference, we check to see if an "ACL2 Image" is installed in Eclipse, in which case we attempt to use that. Next we check the environment variable ACL2_HOME for the directory. Next the java property acl2.home. Then if none of those is fruitful, we just try executing "acl2" and see what happens. |
| Q: | Do I already have Java? What version? |
| A: | The simple answer is to type java -versionat your operating system's command prompt/terminal/shell. You might still have Java if the command is rejected. |
| Q: | Do I need the Java SDK or is the JRE fine? |
| A: | The SDK is only needed if you plan on ever doing any Java development. The (smaller) JRE should be opted if there is a choice. It is recommended to have separate eclipse installations (directories) for Java development and ACL2 development. |
| Q: | Can I use another version of Java? |
| A: | The ACL2s Eclipse plugin uses Java constructs from Java 11. You are likely to encounter problems if you use a Java runtime that is older than Java 11. We recommend the use of JRE 17 or 18. |
| Q: | Why won't ACL2s let me do <blah> in a session? |
| A: | In order for the plugin to follow what's going on in ACL2, we must impose some small limitations. One, for example, is that it will not let you break into raw Lisp. For those interested in this dangerous, low-level form of interaction, however, raw mode is supported (because it uses ACL2's reader). Another subtle limitation is that--aside from wormholes--ld will only let you read from *standard-oi* at ld level 1. The reason has to do with undoing and also ld-error-action. Another example is that good-bye and other exit commands are disabled to the user, to encourage use of the user interface operation "Stop session" instead. For more details, see How/what ACL2 functionality is modified for ACL2s in the ACL2s-implementation-notes. |
| Q: | Can I use ACL2s extensions to ACL2 in an Emacs development environment? |
| A: |
Yes! One can reproduce inside Emacs, the theorem proving environment ACL2 Sedan provides (sans GUI) in the various session modes. To use just the CCG analysis and Counterexample generation features individually, see the next question. You first need to identify where your ACL2 systems book directory is. You can do this by running (assoc :system (project-dir-alist (w state)))inside of an Eclipse ACL2s-mode session. The output of that command will start with
If you want finer control on what gets loaded, you can selectively copy and paste the forms in |
| Q: | Can I use CCG termination analysis and Counterexample generation in Emacs (ACL2 session)? |
| A: |
To enable CCG termination analysis, submit the following two commands in your emacs ACL2 session. (include-book "acl2s/ccg/ccg" :ttags ((:ccg)) :dir :system :load-compiled-file nil) (ld "acl2s/ccg/ccg-settings.lsp" :dir :system) To enable automated counterexample generation, submit the following two commands in your emacs ACL2 session. (include-book "acl2s/cgen/top" :dir :system :ttags :all) (acl2s-defaults :set testing-enabled T) |