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.

Computer-Aided Reasoning: An Approach.
Matt Kaufmann, Panagiotis Manolios, and J Strother Moore.
Kluwer Academic Publishers, June, 2000. (ISBN 0-7923-7744-3)

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.

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.

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

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)

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.
• 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.
  4. Certain exectuable scripts e.g. run_acl2, dx86cl64, wx86cl64.exe etc in your acl2_image* plugin do not have executable permissions.
• Java issues: We recommend JRE version 1.8 (also known as Java 8.0). 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.