[isabelle-dev] HOL FAILED
Lawrence Paulson
lp15 at cam.ac.uk
Thu Oct 1 13:45:14 CEST 2009
I have just done a fetch and can no longer build Isabelle/HOL. I hope
somebody can fix this soon.
Larry
Building HOL ...
HOL FAILED
(see also /Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/log/HOL)
*** Warning: Pattern is not exhaustive. Found near
*** val ( [ isom_def], cdef_thy) = |>( |>( ...), ...(...)) (line 140
of "/Users/lp15/isabelle/Repos/src/HOL/Tools/record.ML")
*** structure IsTupleSupport :
*** sig
*** val add_istuple_type :
*** bstring * string list ->
*** Term.typ * Term.typ ->
*** Context.theory -> Term.term * Term.term * Context.theory
*** val dest_cons_tuple : Term.term -> Term.term * Term.term
*** val istuple_intros_tac : Context.theory -> int ->
Tactical.tactic
*** val mk_cons_tuple : Term.term * Term.term -> Term.term
*** val named_cterm_instantiate :
*** (string * Thm.cterm) list -> Thm.thm -> Thm.thm
*** end
*** Error: Mixed right and left associative operators of the same
precedence. (line 2124 of "/Users/lp15/isabelle/Repos/src/HOL/Tools/
record.ML")
*** Error: Mixed right and left associative operators of the same
precedence. (line 2128 of "/Users/lp15/isabelle/Repos/src/HOL/Tools/
record.ML")
*** Exception- Fail "Static errors (pass 1)" raised
*** At command "use" (line 459 of "/Users/lp15/isabelle/Repos/src/HOL/
Record.thy").
Exception- TOPLEVEL_ERROR raised
*** ML error
make: *** [/Users/lp15/.isabelle/heaps//polyml-5.2.1_x86-darwin/HOL]
Error 1
~/isabelle/Repos/src/HOL:
More information about the isabelle-dev
mailing list