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 sta
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 Ger
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 welc
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 is
On Fri, 2012-08-17 at 21:57 +0200, Makarius wrote:
> Tjark has violated a bit too many rules of conduct in too short time,
> basically abusing his historic administrator privileges on the
> Isabelle repository.
In the past week, I made minor modifications to a two-week-old
maintenance script of F
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
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 hav
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
https://mailmanbroy.informatik.tu-mue
On Fri, 2012-08-17 at 15:15 +0200, Makarius wrote:
> If you need shortcuts, use existing shell alias or scripting facilities.
> You can even make your private Isabelle tools by augmenting ISABELLE_TOOLS
> and *not* pushing anything like that on the official repository.
Sure, but wouldn't the same
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
_
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
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.
Hi,
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.
In reality, ISABELLE_BUILD_OPTIONS are merely passed on to
isabelle.Build, which has its own idea of valid options.
I would suggest that "
> (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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/floria
> 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 Isa
I'm not sure that a warning is necessary. There were multiple factors in my
confusion.
One, clearly, was that type classes (like everything else) had always been
global, and I never expected them to be localised.
Two, I expected a type class such as complete_boolean_algebra to be canonical:
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 ex
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 c
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 gene
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
20 matches
Mail list logo
