A tentative agenda, with notes, is below. They refer to the
examples extracted from
That extracts to an
examples/ directory and several
examples/ and the subdirectories all
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.
Back to Developer's Workshop page