[isabelle-dev] HOL FAILED
Lawrence Paulson wrote: I have just done a fetch and can no longer build Isabelle/HOL. confirmed for current tip: 0059238fe4bc Alex
[isabelle-dev] HOL FAILED
On Thu, 1 Oct 2009, Alexander Krauss wrote: Lawrence Paulson wrote: I have just done a fetch and can no longer build Isabelle/HOL. confirmed for current tip: 0059238fe4bc It should work again in e72347dd3e64. As Alex was pointing out, it makes only sense to speak about repository versions by giving official changeset ids. The repository version is not a defined thing, and can change every minute. Makarius
[isabelle-dev] Branch in isabelle repository
Hi all, I wonder whether the second branch in the repository is intentional. See http://isabelle.in.tum.de/repos/isabelle/graph/a0f38d8d633a Unfortunately, it means that my revised locales code is now hidden from tip :-( Clemens
[isabelle-dev] Branch in isabelle repository
Actually, having a closer look at the actual graph, this is a false alarm. The the visualisation on that web page is misleading if not wrong. Clemens Quoting Clemens Ballarin ballarin at in.tum.de: Hi all, I wonder whether the second branch in the repository is intentional. See http://isabelle.in.tum.de/repos/isabelle/graph/a0f38d8d633a Unfortunately, it means that my revised locales code is now hidden from tip :-( Clemens ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] HOL FAILED
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:
