With changeset aa35c9454a95, HOL-Mutabelle compiles again.
Lukas
On 11/09/2011 06:16 PM, Makarius wrote:
In Isabelle/d17556b9a89b HOL-Mutabelle is broken:
HOL-Mutabelle FAILED
(see also
/Volumes/Macintosh_HD/Users/makarius/.isabelle//heaps/polyml-5.4.2_x86_64-darwin/log/HOL-Mutabelle)
*** int list -> term list option * Quickcheck.report option
*** Reason:
*** Can't unify string * Quickcheck_Common.compile_generator to
*** Proof.context ->
*** (term * term list) list ->
*** int list -> term list option * Quickcheck.report option
*** (Incompatible types)
*** Error (line 499 of "~~/src/HOL/Mutabelle/mutabelle.ML"):
*** Type error in function application.
*** Function:
*** Quickcheck_Common.test_term
*** Exhaustive_Generators.compile_generator_expr
*** ctxt'
*** : bool -> term * term list -> Quickcheck.result
*** Argument: (true, false) : bool * bool
*** Reason: Can't unify bool to bool * bool (Incompatible types)
***
*** At command "theory" (line 1 of
"~~/src/HOL/Mutabelle/MutabelleExtra.thy") Exception- TOPLEVEL_ERROR
raised
*** ML error
I have tried to repair this myself, but failed to understand the 3-4
changesets leading up to that problem -- just too many obscure
booleans floating around, and no proper explanations in the changelogs.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
