[isabelle-dev] Isabelle release test website
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Wed May 2 14:02:20 CEST 2012
Am 02.05.2012 um 13:55 schrieb Makarius:
> On Thu, 26 Apr 2012, Christian Sternagel wrote:
>> I was just curious what "mirabelle" actually is/does, which I still don't know.
> I don't know how (or if) it is tested.
The "HOL-Mirabelle" session ensures that the ML code compiles. This already catches 98% of what can go wrong.
The script itself isn't tested, but I use it frequently, almost weekly, and I never had problems with it before.
More information about the isabelle-dev