Vince, I tried your new `ignore' idea with your previous `get' idea, and I
think it works but doesn't suppress error messages. That is, it works fine if
I replace my definition of `is_thm' in RichterHilbertAxiomGeometry/readable.m,
with your
let is_thm s =
try ignore (exec_thm s); true
with _ -> false;;
But let's try to use your old `get' ideas:
let get = Obj.magic o Toploop.getvalue;;
let is_thm s =
try ignore ((get s):thm); true
with _ -> false;;
readable.ml still runs, but the output is littered with warnings. If I
evaluate this
let AXIOM_OF_CHOICE = theorem `;
∀P. (∀x. ∃y. P x y) ⇒ ∃f. ∀x. P x (f x)
proof
intro_TAC ∀P, H1;
exists_TAC λx. @y. P x y;
fol H1;
qed;
`;;
I get the output
>> Fatal error: H1 unbound at toplevel
>> Fatal error: H1 unbound at toplevel
Warning: inventing type variables
0..0..1..solved at 4
val AXIOM_OF_CHOICE : thm = |- !P. (!x. ?y. P x y) ==> (?f. !x. P x (f x))
#
So we're still proving the theorem, but we get this error message. We can ask
where the error message comes from, and I'm not sure, but look at this output:
is_thm "EVEN_MULT";;
val it : bool = true
is_thm "EVEN_mult";;
>> Fatal error: EVEN_mult unbound at toplevel
val it : bool = false
The output is correct, but before, I didn't get the error message.
> 1) Can you pretty-print error messages in HOL Light?
Not to my knowledge.
I believe miz3/miz3.ml does so, and there are many functions defined there
starting with print:
print_to_string1
print_boxed
print_step
print_qsteps
There's some interesting looking code there, e.g.
let output s m n = sbuff := (!sbuff)^(String.sub s m n) and flush() = () in
--
Best,
Bill
------------------------------------------------------------------------------
This SF.net email is sponsored by Windows:
Build for Windows Store.
http://p.sf.net/sfu/windows-dev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
