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

2012-08-18 Thread Makarius
On Fri, 17 Aug 2012, Tobias Nipkow wrote: 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

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

2012-08-18 Thread Florian Haftmann
For the record: I did not know that Tjark had conversed with Florian privately before. This removes the main accusation on his http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was looking like he was seizing control of the draft started by Florian. The email reads (in

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

2012-08-18 Thread Makarius
On Sat, 18 Aug 2012, Florian Haftmann wrote: For the record: I did not know that Tjark had conversed with Florian privately before. This removes the main accusation on his http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was looking like he was seizing control of the draft

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

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

Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

2011-08-25 Thread Florian Haftmann
When I've seen the complete_boolean_algebra incident on the other thread my first impulse was to check how far the wiring of the class package wrt. the Isabelle document markup was. In principle the prover can provide useful clues in non-intrusive ways here, if done right. E.g. in

Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

2011-08-25 Thread Florian Haftmann
(BTW, in Scala ambiguity after additional imports is treated as an error, and causes the conflicting name entries to be canceled out.) I definitely like this! Florian -- Home: http://www.in.tum.de/~haftmann PGP available:

[isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

2011-08-22 Thread Brian Huffman
Hello everyone, Isabelle prints out warning messages whenever anyone declares a duplicate simp rule, intro rule, etc. It would be nice if Isabelle would print a similar warning whenever a definition reuses a name that is already in scope in the current context. For example, if a theory defines a

Re: [isabelle-dev] Feature request: print warning message when a definition shadows a previously-used name

2011-08-22 Thread Makarius
On Mon, 22 Aug 2011, Brian Huffman wrote: Isabelle prints out warning messages whenever anyone declares a duplicate simp rule, intro rule, etc. It would be nice if Isabelle would print a similar warning whenever a definition reuses a name that is already in scope in the current context. For

[isabelle-dev] Feature request

2010-12-07 Thread Thomas Sewell
Hello Isabelle developers. I was recently reminded of one of the things on my wish-list for Isabelle: a make -k mode in which the system continues for as long as possible and reports as many errors as possible, rather than halting after the first one. I think this would be generally useful to

Re: [isabelle-dev] Feature request

2010-12-07 Thread Makarius
On Tue, 7 Dec 2010, Thomas Sewell wrote: I was recently reminded of one of the things on my wish-list for Isabelle: a make -k mode in which the system continues for as long as possible and reports as many errors as possible, rather than halting after the first one. I think this would be