(See the ACL2s home page/documentation for general information)
The computer labs here have Eclipse with ACL2s installed. It should be located in the start menu under Department Applications | CCIS Applications | Development Tools | Eclipse | eclipse. Running Eclipse for the first time, you will be prompted for a workspace location. We recommend "Z:\Workspace", because this is in your personal drive that is backed up by the college.
Assuming you are familiar enough with ACL2s (begin with the tutorial if you are not), you will need to change one setting in order to successfully start a session in ACL2s. In Eclipse, go to Window | Preferences.... On the left side, expand the ACL2s category and select the ACL2 preference page. Under "ACL2 bulid path" type "N:\arch-windows\acl2-3.3", like so:
Now you should be able to start a session successfully, without any message about .cert files being fixed and without recertifying the system books.
Note: At the moment, our Windows build of ACL2 does not support interruption properly. This means that stopping a run-away proof attempt or long-running execution will kill your session. Fortunately, by starting a new session, everything that was previously completed is automatically loaded. We are working to address this issue.