|
|
|---|
|
|
|
|---|
ACL2 Sedan interface
Many successful ACL2 users run in an shell under Emacs; see emacs. However, those not familiar with Emacs may prefer to start with an Eclipse-based interface initially developed by Peter Dillinger and Pete Manolios called the ACL2 Sedan or ``ACL2s''.
ACL2 sessions in the ACL2 Sedan can utilize non-standard extensions and enhancements, especially geared toward new users, termination reasoning, and attaching rich user interfaces. These extensions are generally available as certifiable ACL2 books. (Some code originating from this project has been migrated to the ACL2 community books, but only after it was quite stable.) Thanks to Peter Dillinger, Pete Manolios, Daron Vroon, and Harsh Raju Chamarthi for their work on the ACL2 Sedan and for making their books available to ACL2 users.