|Q:||Is my OS 32 bit or 64 bit?|
|A:||For Linux and MacOS, if you see "x86_64" or "amd64" in the
output of shell command |
|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 run Eclipse--with the right options?|
|A:||See the "Running Eclipse" section of the 3.5 Release Notes. To view details about how a currently-running Eclipse was invoked, go to Help | About Eclipse SDK and click "Configuration Details".|
|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?|
|Q:||Can I do a multi-user install of Eclipse?|
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
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 :DOC books and our guide to book development in ACL2s for more information.|
|Q:||Can I use the ACL2 image downloaded by Eclipse outside of Eclipse?|
|A:||Absolutely! From the ACL2 perspective, it has everything you would
have building ACL2 yourself. Use the following executable script
|Q:||Can I use my own version of ACL2? i.e. Finding ACL2 on user's system:|
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 |
|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:||Is there a difference between Java SDK 1.5.0 and 5.0?|
|A:||No. "5.0" is the version number adjusted for marketing-hype. See "Version 1.5.0 or 5.0?" on Sun's site. Similarily, there is no difference between Java version "6.0" and JDK/JRE 1.6.0 etc etc.|
|Q:||What is Netbeans?|
|A:||Netbeans is a Java development environment that feels much like Eclipse but is more Java-specific. You do not need it.|
|Q:||Can I use a version 1.* of Java?|
|A:||ACL2s Eclipse plugin uses 1.5 language constructs and APIs. You are likely to encounter problems if you use a Java runtime that is older than "5.0". Moreover due to a bug in JRE 1.7, ACL2s will not work with it. We recommend the use of JRE 1.6 or 1.8.|
|Q:||Why won't ACL2s let me do <blah> in a session?|
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.
|Q:||Can I use ACL2s extensions to ACL2 in an Emacs development environment?|
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.
Assuming you have ACL2s installed as an eclipse plugin in /Users/sarah/tools/eclipse, here are instructions on how to run an ACL2s mode session in Emacs. Name the above directory my_eclipse.
If you want more finer control on what gets loaded, you can selectively copy paste the forms in the acl2s-mode.lsp that
you need, in the emacs session. For example, say you want a session without trust tags, then except
To reproduce other sessions modes, follow the above, but replace acl2s-mode.lsp by the corresponding session mode file, e.g. acl2s-beginner.lsp
|Q:||Can I use CCG termination analysis and Counterexample generation in Emacs (ACL2 session)?|
To enable CCG termination analysis, submit the following two commands in your emacs ACL2 session.
To enable automated counterexample generation, submit the following two commands in your emacs ACL2 session.
|Q:||I am having trouble installing/running ACL2s, what should I do?|
Case: Standard prepackaged installation
Case: Non-standard Installation: