Frequently Asked Questions

General

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 uname -a in your terminal, you have a 64bit OS, otherwise a 32 bit one. For other operating systems, please visit their respective FAQ pages: Windows.

Eclipse-related

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?
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.

ACL2-related

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.
Matt Kaufmann, Panagiotis Manolios, and J Strother Moore.
Kluwer Academic Publishers, June, 2000. (ISBN 0-7923-7744-3)
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 myeclipse/plugins/acl2_image.something/run_acl2 instead of the usual saved_acl2
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.

Java-related

Q: Do I already have Java? What version?
A: The simple answer is to type java -version at your operating system's command prompt/terminal/shell. You might still have Java if the command is rejected. See also How do I run Eclipse--with the right options? and Is there a difference between Java SDK 1.5.0 and 5.0? for more info.
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.

ACL2s-related

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.


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.

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.

  1. Open a shell in emacs, start the ACL2 session: my_eclipse/plugins/acl2_image.something/run_acl2
  2. In the ACL2 session, submit the following 3 commands:

    
     (add-include-book-dir :acl2s-modes "my_eclipse/plugins/acl2s_modes_something/") 
     (ld "acl2s-mode.lsp" :dir :acl2s-modes)
     (reset-prehistory t)
    

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 for the (include-book "ccg" ...) form, submit the rest of the events in acl2s-mode.lsp.

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)?
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)


Installation Issues

Q: I am having trouble installing/running ACL2s, what should I do?
A:
Case: Standard prepackaged installation
  • ACL2 appears to be stuck on starting (Anti-virus software is getting in the way): Do whatever is necessary to give eclipse/plugins/acl2_image*/run_acl2.exe appropriate privileges. In particular, if on Avast Anti-virus, go to settings and uncheck the DeepScreen feature.
  • OS mismatch: Make sure that the ACL2 Image you chose to install, matches the OS/Platform of your machine. e.g. If you are on a Windows64 OS, then Help->Installation Details should show ACL2 Image (Windows64/x86_64)
  • Uncommon Windows IssueIf in the .a2s session editor you find at the top (screen) the following lines:
        Can't allocate required TLS indexes.
        First available index value was 31
    This is an issue with Clozure Common Lisp. It appears that this happens when the Windows platform in question has many programs and updates installed. A possible workaround is to install from scratch a Windows or Linux OS on a VirtualBox and install ACL2s on it.
  • Old Linux distros On linux machines whose glibc version is older than 2.15 the current prepackaged tarball does not work. Please contact the ACL2s maintainer to provide you with a custom ACL2s build.

Case: Non-standard Installation:
  • MacOSX/Linux Permissions: If you installed eclipse on your Mac/Linux machine using a package manager that comes with the OS, then you will have trouble installing and starting ACL2s due to different permissions. Instead follow the eclipse download instructions as described above in the website, mainly: Download the Eclipse tar.gz and extract (without using sudo) the archive in your home directory (e.g. /home/johnd/tools/eclipse).
  • Cannot Start ACL2: If ACL2s was installed correctly, but when you start an ACL2 session, you get an error, then there can be other causes like:
    1. You only installed ACl2s plugin and not the ACL2 image and you forgot to specify the build path in Windows->Preferences->ACL2s->ACL2.
    2. You are using an older ACL2 version, again check the build path in Windows->Preferences->ACL2s->ACL2 and modify it to point to a newer version.
    3. You are using a workspace on network share path. Switch to a workspace on local path.
  • Java issues: Either Java is not installed (not in PATH) or you are using a version of JRE 1.7 that has a bug in its string library.