Software Design by Example in Python 20: A Package Manager

I had to learn almost as much to write Chapter 20: A Package Manager as I did to write the chapter on databases. Recursively enumerating all possible combinations of packages to find ones that were compatible with each other was relatively straightforward (by which I mean that someone taught me how to do it so long ago that it seems like I’ve always known). Using a theorem prover to do this more efficiently, on the other hand, was brand new. (I worked on a theorem prover for modal logics for my master’s degree, but it used a completely different approach and that was thirty-nine years ago.) I almost gave up on Z3 several times—its documenation is terrible—but then I stumbled across this talk by Andreas Zeller and things started to make sense. I don’t know if my exposition does the subject justice, but I’m grateful to have had an excuse to dive into it.

Terms defined: accumulator, backward-compatible, Boolean value, combinatorial explosion, cross product, model, patch, Recursive Enumeration pattern, scoring function, search space, semantic versioning.