Title:   The ACL2 logical world and navigating ACL2 source code
Speaker: Matt Kaufmann
Date:    October 28, 2009

Abstract:

The ACL2 source code contains about 250,000 lines (10.5 MB) and may
thus seem impenetrable at first glance.  In spite of this complexity,
ACL2 users are increasingly using source code routines, for example in
their own macros and clause processors.  Moreover, a new project is
underway to separate out a "trusted core", so that users can soundly
hack on interface code.  It is becoming important, therefore, to make
it easier for users to navigate the ACL2 sources.

This talk will take a step in that direction.  We will start by
discussing the ACL2 state and its logical world, which is a key
component of the ACL2 state.  Using an (undocumented) function,
walkabout, we will explore a sample ACL2 world.  We will also
illustrate the use of :props and getprop.

A main goal of this talk is to illustrate how I navigate the ACL2
source code.  I'm open to suggestions on which code to explore, but
here are a couple of ideas.  (1) I may explore the code for :UBT
(undoing) in a top-down manner, with a focus on the question of how
undoing installs a new enabled structure.  (2) I may explore the code
for DEFTHM in a top-down manner.  In both cases, I will mainly avoid
drilling into specifics except as requested and as time permits.

We have begun to write a style sheet, namely file
/projects/acl2/devel/style-sheet.txt.  It is in the very early stages
and we invite contributions.

The talk will likely include lots of interaction in an Emacs shell
buffer.  I intend to save a copy of that buffer on the web, at:

http://www.cs.utexas.edu/users/moore/acl2/2009.10-28-kaufmann/shell-log.txt