[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