ACL2 Developer's Workshop 2017:
Overview

This workshop will likely have three main components.

• (A) Overview of the organization of the ACL2 sources, presented by Matt and J. Relatively little detail will be covered; rather, the point will be to give high-level information sufficient to understand how to go about modifying the sources. For example, we might give a very brief tour of some of the many (89?) Essays in the sources:

      % grep '^; Essay on' *.lisp | wc -l
      93
      %
  

• (B) Examples of modifying ACL2 source code. Matt and/or J will take participants through the process of implementing changes to ACL2.


• (C) Challenge problems for participants to solve: perhaps an implementation of a new feature, an improvement to an existing feature, and/or a bug fix. Groups may typically consist of two or three people. Matt and J will provide assistance as requested.

Products of this workshop may include:

• A robust acl2-devel email list, as a way for budding ACL2 developers to collaborate on enhancements
• An improved development guide, based in part on materials presented in (A) and (B) and corresponding questions raised by attendees, and based in part on what we see is needed as people work through (C)

We will try to follow a schedule, but it can be changed to accommodate the needs of the participants. However, we will keep the discussion in scope, towards the goal of developing future ACL2 system developers.

We will make heavy use of Emacs.

Please see the preparations page for things to do in advance if you have time. Most critical:

Every participant should bring a laptop. Complementary wi-fi access will be available. Light snacks will be available during breaks, at least in the morning. Time and space will be reserved for lunches, which participants will generally purchase from the cafeteria downstairs.

The examples and exercises are in the tarball examples.tgz. The subdirectories for examples contain solutions. We will eventually provide solutions to the exercises as well.

Back to Developer's Workshop page