Introduction

Warning: This software is under development. It is riddled with bugs, lacks important features, and is not ready for public use!

Abettor is a framework for connecting external tools to ACL2.

The Abettor Server manages an ACL2 session. Clients communicate with the server through an XML based protocol. As a result, external tools can be written in practically any language, and can include complex graphical components.

The Abettor IDE is an integrated development environment based on this framework. This is a prototype, intended as a demonstration of the Abettor framework and as a glimpse at what might be possible when graphical capabilities are added to ACL2's interface.

Motivation and Purpose

The goal of Abettor is to increase the capabilities of ACL2's user interface. The text-based user interface is sometimes nice for expert users, but provides little guidance to an inexperienced user and is cumbersome even for experts for interactive tasks (such as the proof checker.)

The goal is not to eliminate text-based interaction with ACL2, but merely to augment it with graphical tools where appropriate.