A tentative agenda, with notes, is below. They refer to the
examples extracted from examples.tgz.
That extracts to an examples/ directory and several
subdirectories; examples/ and the subdirectories all
have a README that serves as a starting point.
NOTE: Although we will try to keep to this schedule, so that there is
time for all of the prepared examples and exercises, it is not set in
stone. The lunch room (POB 6.102; see below) is reserved 12:30 to
2:00.
We expect that refreshments will be available during breaks in the
kitchen area just outside the meeting room.
Day 1 (Wednesday, May 24)
8:30 - 9:00
Mingle, chat
Matt plans to bring donuts and probably bagels and cream cheese,
and Warren plans to provide coffee (both regular and decaf).
There will also be instant hot drinks (cocoa, red date tea, ...).
9:00 - 10:00
Introduction [Matt]
- Welcome, emphasizing that the workshop is about training future ACL2
developers, though for a few years all enhancements will go through
Matt and J. We'll generally defer to offline discussion topics not
in direct support of that training goal, for example, how to
reorganize the source code or whether to change some algorithm or
interface.
- We'll probably email the ACL2 list, asking that requests for bug
fixes and enhancements be sent to the new acl2-devel list. (I'm the
moderator and will pass along the request from non-members if it
seems suitable.) J and I reserve the right to decide whether we'll
look at others' code -- feel free to "contract" with us before
embarking on designing or coding a fix or enhancement.
- We'll suggest that maybe participants keep a list of lessons learned
to discuss at the end of the day.
- We'll go briefly over this schedule and remind about overview.html.
- Limited expectations: the goal for only 2 days is some basic
background sufficient to learn more (and to learn how to learn more,
e.g., meta-x tags-apropos)
- Development can be a "gerbil" process -- e.g., sometimes we use
trace$ to get our heads around what's going on, and sometimes we
even ignore existing comments but other times we read them
carefully.
- Some development principles:
- Small examples help
- Minimal, incremental changes are often best (safest, most
efficient to implement, easiest to understand and maintain) -- we
like to wait for users to complain before doing more sweeping
changes
- We look for precedents.
- It has often seemed to us that it's best to be efficient rather
than curious -- it's a judgment call whether a candidate local fix
is sufficient or if a more global investigation is called for.
- Normally it's best to wait till the implementation is completed,
including testing if it's not a pretty trivial change, before
writing detailed user-level documentation. Occasionally it might
be good to sketch such documentation as an implementation guide.
- Some things that are critical and often more time-consuming than
writing the main code: writing :doc, comments, and error messages
- This isn't about how to program, though we might remark occasionally
on specifics when it seems helpful, for example, to avoid
code duplication or, if necessary, leave "keep in sync" comments.
- Please help each other on exercises ("social process"), and
later on any tasks via the acl2-devel email list.
- Ask questions -- perhaps the most important things to learn here in
order to begin to develop ACL2 system code are basics that we might
not think to discuss.
- Exercises to do during the workshop any time you have finished the
current exercise (or, after the workshop); or we could use these
as extra examples tomorrow:
+ examples/new-names/
+ examples/meta-fn-ctx-current-lit/
+ Add strip-cadrs.
+ Write a function to determine whether a symbol is a world global,
a state global, or neither.
10:00 - 10:30 [Matt]
Unusually trivial example to illustrate the development process:
- See examples/README
- See examples/intro/README
10:30 - 10:45
Break
10:45 - 12:15
Brief, incomplete overview of code and data structures [J], for
example:
- Terms, including lambdas
- World (maybe demo with walkabout)
- World globals and state globals
- Essays for learning more, e.g., Essay on Tag-Trees and
Essay on Enabling, Enabled Structures, and Theories
NOTE: If we finish early then we'll get a head start on the exercise
that starts after lunch. This might push back lunch just slightly.
12:15 - 1:30
Lunch: Purchase downstairs at O's, then gather at POB 6.102 (faculty
lounge in Peter O'Donnell Building, formerly known as "ACES").
1:30 - 2:30
Exercise: examples/extend-error-message
WARNING: You need to LOAD the patch file before you LD it!
NOTE: For this exercise, but only this exercise, we'd like everyone to
stay in the room and to ask questions out loud. We hope participants
(other than Matt and J) will answer, so as to encourage the social
process that we foresee taking place on the acl2-devel list. [J notes
that he and Bob had a very interactive social process during their
collaboration, and he and Matt often do now as well; so it's natural
to continue that even if the two of us get hit by a bus!]
2:30 - 3:00
Participant presentations on Exercise 1
- Solution
- Issues (and if possible, how they were addressed)
3:00 - 3:15 break
3:15 - 3:45 [Matt]
Example: examples/defabsstobj-events-2017-03/solution.txt
The point of this example is to illustrate how deep to dive. I didn't
try to understand why Sol's event is different from what defabsstobj
expected, and I didn't even try to understand how Sol figured out
which function to trace. I simply looked at the trace output and
realized that provable equality would suffice, so I wrote a suitable
function sufficient to solve problems like this. Not very deep!
I don't plan to discuss the code that I wrote; not enough time, and
it's "only" programming.
NOTE: Sometimes we prove correctness. I didn't do that here, though.
3:45 - 5:30
Exercise: examples/disable-compound-recognizers/README
This is similar to the one above (defabsstobj), in that the bug report
came with a very big hint and the rest is sort of routine.
[Note: This is a long time without a break, but of course anyone can
take a break at any time.]
5:30 - 6:00 [Matt, J]
Wrap-up; e.g., ask participants to enumerate lessons learned
Optional exercise for homework: examples/invariant-risk-2017-04/.
Matt might comment on how he used a thesaurus and spent perhaps 15
minutes coming up with a name for the new feature. (Finding good
names is important and sometimes challenging.)
NOTE: This would probably be way too hard without the hints provided
in the README.
------------------------------
Day 2 (Thursday, May 25)
8:30 - 9:00
Mingle, chat
Matt plans to bring donuts and probably bagels and cream cheese,
and Warren plans to provide coffee (both regular and decaf).
There will also be instant hot drinks (cocoa, red date tea, ...).
9:00 - 10:00
Discuss solution to optional exercise,
examples/invariant-risk-2017-04/
(ideally someone other than Matt or J).
Questions; miscellaneous relevant digressions
10:00 - 10:15
Break
10:15 - 11:45
Example; examples/stobj-let-2017-04/ [Matt]
This example should be a good step-by-step tutorial on something that
requires deeper knowledge about ACL2, though it's still relatively
routine. I wouldn't expect participants to be able to do this
themselves, but we want to show at least one example illustrating the
fact that not every ACL2 fix is possible simply by skillful hacking --
sometimes background knowledge is helpful. That knowledge comes over
time, typically by reading comments (user documentation, Essays, and
other Lisp comments). Tracing helps in getting one's head around the
problem.
11:45 - 12:15 [Matt]
Exercise introduction: examples/ruler-extenders/README
Emphasize the need to get the logic right.
12:15 - 1:30
Lunch: Purchase downstairs at O's, then gather at POB 6.102 (faculty
lounge in Peter O'Donnell Building, formerly known as "ACES").
1:30 - 3:00
Work on exercise, examples/ruler-extenders/README.
3:00 - 3:15
Break
3:15 - 4:00
Go over examples/ruler-extenders/ -- ideally, a participant will
present a solution.
4:00 - 4:15
Break
4:15 - 5:30 or 6:00
THEN: Wrap up. What did we learn?
If there is still time, we could discuss a bit about
examples/irrelevant-dcl/, which is a rather involved example (with
development thoughts recorded in
solutions/irrelevant-dcl/solution.txt). Depending on how things go,
we might start the exercise and let people continue working it over
time, communicating via acl2-devel.