Re: [isabelle-dev] http://isabelle.in.tum.de/testboard/

2012-08-17 Thread Tobias Nipkow
Thanks for fixing it. Unfortunately I cannot push to it anymore, it asks me for a password. Tobias Am 16/08/2012 22:40, schrieb Alexander Krauss: Quoting Makarius makar...@sketis.net: The end of Python vomiting has this: class 'mpatch.mpatchError': patch cannot be decoded args =

[isabelle-dev] the “algebra proof method

2012-08-17 Thread Lawrence Paulson
As far as I am aware, we provide no documentation on the “algebra proof method. My impression is that this method will prove anything that it can convert to the form p1 = 0 == … == pn = 0 == p = 0 where p1, …, pn, p are polynomials, possibly in multiple variables, over a suitable

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Makarius
On Fri, 17 Aug 2012, Tjark Weber wrote: I had expected that ISABELLE_BUILD_OPTIONS would allow me to specify default options for the isabelle build tool, for instance -v for verbose output. None of the regular tools ever had such a feature, for usedir it was merely a historical accident.

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Tobias Nipkow
Am 17/08/2012 15:15, schrieb Makarius: I count this as trolling on this mailing list. We all have our pet peeves. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Makarius
On Fri, 17 Aug 2012, Tobias Nipkow wrote: Am 17/08/2012 15:15, schrieb Makarius: I count this as trolling on this mailing list. We all have our pet peeves. Tjark can express that somewhere privately, not here on this mailing list. Makarius

[isabelle-dev] PLATFORMS

2012-08-17 Thread Makarius
Isabelle/10584ca5785f has an updated version of Admin/PLATFORMS. Executive summary: * Mac OS Mountain Lion is now supported (macbroy30) * Mac OS Leopard has been discontinued * old 32 bit Mac hardware is no longer usable (lack of Java 7) * explicit ISABELLE_PLATFORM32 helps to make

[isabelle-dev] isabelle components

2012-08-17 Thread Makarius
Various changes leading up to Isabelle/ae7429d66b1e attempt to disentangle the component situation on the Isabelle repository, as opposed to regular releases. See the end of README_REPOSITORY and the system manual on Add-on components and the isabelle components tool. Short version: *

Re: [isabelle-dev] PLATFORMS

2012-08-17 Thread Clemens Ballarin
Any chance of still working on Leopard if I neither use jEdit nor any of the external provers? Clemens Quoting Makarius makar...@sketis.net: Isabelle/10584ca5785f has an updated version of Admin/PLATFORMS. Executive summary: * Mac OS Mountain Lion is now supported (macbroy30) * Mac

Re: [isabelle-dev] PLATFORMS

2012-08-17 Thread Makarius
On Fri, 17 Aug 2012, Clemens Ballarin wrote: Any chance of still working on Leopard if I neither use jEdit nor any of the external provers? Basically no. I also need to ugrade my own MacBook Pro after so many years of Leopard. Makarius

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Makarius
Tjark, you have no business here. If you want to propose changes to the Isabelle repository, you can send them the via email as hg changeset. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Christian Urban
On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the isabelle-users and isabelle-dev lists. After all, we like to

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Makarius
On Fri, 17 Aug 2012, Christian Urban wrote: On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the isabelle-users and

Re: [isabelle-dev] Feature Request for ISABELLE_BUILD_OPTIONS: Support isabelle build Options

2012-08-17 Thread Tobias Nipkow
Am 17/08/2012 21:51, schrieb Christian Urban: On Friday, August 17, 2012 at 21:18:35 (+0200), Makarius wrote: Tjark, you have no business here. I assume something got here lost in translation. Otherwise, we should all make reasonable effort to welcome everybody on both, the