Email Gateway (Aug 22 2022 at 21:15): Email Gateway (Aug 22 2022 at 21:15):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Christian,
(Replying on isabelle-users, because the dev mailing list is for discussions of the ongoing development. You report is about the official release.)
Thanks for your report. This is a rather hard crash. With my setup, I don't even need the explicit quickcheck invocation—Auto Quickcheck (which I have enabled) will lead to the same crash too. I don't know what quickcheck does internally that leads to this (I'll let the quickcheck experts answer and look into this), but a workaround is to add
code_lazy_type buggy_type
After the datatype declaration. You will also need to import HOL-Libarary.Code_Lazy to do so.
The command code_lazy_type will modify the code setup and is meant to avoid non-termination issues for code generation with codatatypes (into languages with strict evaluation). It seems also to help in the case of this non-recursive codatatype.
Cheers,
Dmitriy
Email Gateway (Aug 23 2022 at 08:11):From: Makarius <makarius@sketis.net>
This is a hard crash of the code produced by the Poly/ML compiler ---
quickcheck generates some ML source and lets Poly/ML evaluate it on the spot.
The problem first occurred in the transition from Poly/ML 5.6 to 5.7.1
(Isabelle changeset aefaaef29c58 from 26-Oct-2017). It has been there in
Isabelle2018 and Isabelle2019.
I will contact David Matthews, the master of Poly/ML, to take a look at it
(with a slightly more detailed example).
Makarius
Last updated: Apr 18 2024 at 01:05 UTC