[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.

Jasmin




More information about the isabelle-dev mailing list