HOL-Theorem-Prover/HOL

Fix intLib to avoid noisy output

Closed this issue · 1 comments

Following commit f6c3ef2, loading intLib produces a lot of output that should be suppressed and/or avoided (see below). Ideally there should not be calls to Meson when loading the library. The overloading/parsing warnings are a bit concerning as well.

> load "intLib";
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: inventing new type variable names: 'a, 'b>>
Meson search level: ...........
<<HOL message: inventing new type variable names: 'a>>
Meson search level: ..............................................
Meson search level: ........
Meson search level: ........
Meson search level: ...
Meson search level: 
Meson search level: ........
Meson search level: ........
Meson search level: ................................................................................................
Meson search level: ................
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: inventing new type variable names: 'a>>
Meson search level: ....

Should be fixed now.