[isabelle-dev] Dead code smells
makarius at sketis.net
Wed Aug 24 17:56:58 CEST 2011
Some notes concerning the following recent changes:
comment out dead code to avoid compiler warnings
A priori, warnings are really just warnings, not errors.
When Poly/ML acquired this very useful warning for unused identifiers, I
did go through all my code and cross-checked if I agree with the compiler.
There were typically one of the following cases:
(1) There is genuine unused stuff that is better removed altogether.
(Maybe 90% of the time.)
(2) Certain unused arguments indicate a deeper problem in the code -- it
requires some care and understanding how things work exactly to amend this.
Removing the offending identifiers merely makes things worse,
because semantic unclarities are swept under the carpet.
(May happens a few % of the time.)
(3) Small named arguments that actually improved readability and
uniformity. (Up to 10% of the time.)
Here is a trivial example from src/Pure/library.ML:
fun fst (x, y) = x;
fun snd (x, y) = y;
Replacing everything by "_" blindly is not really progress in code quality.
I have occasionally tried to clean up things like positivstellensatz.ML
myself, but failed to do it right without substantial involvement.
(Without the latter the preferred style of the original author takes
precedence, even if it happens to be suboptimal.)
Dead code really starts smelling quickly and should not be introduced at
all. Either it is left in and statically checked, or removed from the
text. (The history is 100% persistent so interested parties can retrieve
old material any time.)
More information about the isabelle-dev