Re: [isabelle] Isabelle2014-RC0 available for testing



Two small things that might be worth looking at:

- on my laptop, Isabelle 2014-RC0/jedit comes up with non-retina fonts, whereas 2013-2 does (different java version I guess)

- on the Mac, by default the Isabelle app is not associated with .thy files (which is fine). If you do associate it manually, and either “open file.thy” on the command line, or double click a .thy file in Finder, Isabelle/jedit comes up, but loads Scratch.thy. This was already the case in 2013-2, I just forgot about it again. There is probably just some command line argument that needs to be passed to isabelle jedit in the Mac application magic.

Cheers,
Gerwin


On 5 Jul 2014, at 8:04 pm, Makarius <makarius at sketis.net> wrote:

> Dear Isabelle users,
>
> the coming Isabelle2014 release is anticipated for August 2014.  As an early semi-official release candidate for general testing there is now Isabelle2014-RC0 available from here:
>
>  http://isabelle.in.tum.de/website-Isabelle2014-RC0
>
> This is an opportunity to look how things will presumably be in the release, and to report problems, either on the isabelle-users mailing list or via private mail.
>
> The very same version will be used at the Isabelle tutorial at VSL 2014 in Vienna next week: http://vsl2014.at/isabelle
>
>
> The Vienna Summer of Logic is the largest convention of Logicians of known human history (i.e. the last 15000 years) on this planet. Many of the protagonists of this mailing list will be there.  I am myself attending the ITP week with two adjacent workshop days: 13..18-Jul-2014.
>
> If there are any particular problems with the increasingly interactive Isabelle computer-game, which is the Prover IDE, I would be happy to sort this out personally.  (Including the canonical question about remaining uses of Proof General.)
>
>
> After the conference -- more than 2 weeks from now -- there will be the normal Isabelle2014-RC1, with more formal testing, reporting, polishing, until final lift-off in August, when most Frenchmen are on vacation.
>
>
>       Makarius
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.