#67 Default Build Generates Various Warnings

[Tjark Weber]

Building HOL4 generates a number (25, to be precise) of warnings on my machine. These are related to the parsing of numerals (22), overloading resolution (1), and EmitML's type info (2):

<<HOL warning: parse_term.term_parser:
0 treated specially and allowed - no other numerals permitted>>
<<HOL warning: Preterm.remove_overloading: many overloaded symbols in term: overloading resolution might take a long time.>>
<<HOL warning: EmitML.datatype_silent_defs: No info in the TypeBase for "int">>

In my opinion, a warning (in contrast to a message) should alert the user to a potential problem. So if there is a potential problem with the calls that generate these warnings, the code should be fixed; if there isn't, the warnings should be disabled explicitly.

In any case, a default build of HOL4 in my humble opinion should not produce any warnings if everything goes according to plan.