Code Review

by Brown, Thursday, January 14, 2021, 16:28 (325 days ago)

Cezary Kaliszyk went through the Proofgold code recently and found a number of issues. In some cases fixing the issues led to significant speedup in the code (e.g., making use of tail recursion, chaning garbage collection settings, changing defaults on the database caching, reading int32/hashval byte by byte instead of bit by bit when possible, and other issues I don't recall offhand).

There were some other suggestions he gave that haven't been followed up on yet:

1. There are many places in the code where a try is paired with an arbtrary catch-all wildcard. This is at least bad style since in principle we should know what exceptions are possible at the given try. It is also a likely way to introduce real bugs since an exception intended to be caught somewhere else is caught "early". We should also make sure all exceptions are actually caught in order to avoid the process "silently exiting".

2. It's likely that some of the recursive functions can be rewritten to be tail recursive, making them significantly more efficient.

3. Currently there's no (or almost no?) signal handling, but obviously there should be.

There's more, but I can add them when they come to mind.

As for (1) I noticed there are some exceptions defined in the code that are never raised, so these could be deleted (unless I'm missing something):

blocktree: NoReq
ctre: MissingCTreeElt InsufficientInformation FoundHashval
mathdata: UnknownSigna UnknownTerm NotKnown NonNormalTerm TermLimit BetaLimit

We should probably identify where every exception might be raised and might be caught, and especially which exceptions can escape a function or pass through a function. I don't know a quick way of doing this and there are well over 1000 functions, so doing it by hand seems unrealistic.

As for (2) there are over 300 recursively defined functions, so it will take some time to look through them and determine if they can be made tail recursive. I'm not as motivated as I'd like to be to start going through them by hand.

Hope this helps.