Some notes concerning the following recent changes:
082edd97ffe1 huffman
comment out dead code to avoid compiler warnings
6f28f96a09bf huffman
avoid 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.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
