On 05/04/13 09:32, Makarius wrote:
> On Fri, 5 Apr 2013, David Greenaway wrote:
>> What practical things could such volunteers do that you would find
>> helpful?
>
> So how about maintaining Proof General, seriously, no-nonse?
As somebody who isn't a Proof General user, nor an Emacs user, nor has
On Fri, 5 Apr 2013, David Greenaway wrote:
What practical things could such volunteers do that you would find
helpful?
So how about maintaining Proof General, seriously, no-nonse?
And there are other unmaintained parts, such as WWW_Find. (Note that
several other people have worked there in
On 04/04/13 23:41, Makarius wrote:
> On Thu, 4 Apr 2013, Gerwin Klein wrote:
[...]
>> Again, I don't even disagree, it should get low priority and there are
>> good reasons for many of the traditional ways Isabelle development
>> happens. But the process clearly puts a lot of strain and time
>> co
On Thu, 4 Apr 2013, Christian Urban wrote:
Could the reason be that more often than wanted the answer to
emails on the Isabelle mailing lists is:
"person ?X, you have no business here"
"any changes to ?X are restricted to exactly one person"
you are on the wrong mailing list (isabelle vs i
On Thursday, April 4, 2013 at 12:42:42 (+0200), Makarius wrote:
> On Thu, 4 Apr 2013, Thomas Sewell wrote:
>
> > David's investigation explains a problem we had a few years ago where
> > some custom tactics of mine were killing my colleagues' ProofGeneral
> > sessions when they encountere
On Thu, 4 Apr 2013, Gerwin Klein wrote:
It was on these very mailing lists that it was proclaimed that PG is
dead and people shouldn't bother reporting problems, because there is
nobody there to maintain it. I'm not even disagreeing with it, I
certainly don't have the time to maintain PG/Isabe
On 04/04/2013, at 12:42 PM, Makarius wrote:
> On Thu, 4 Apr 2013, Thomas Sewell wrote:
>
>> David's investigation explains a problem we had a few years ago where some
>> custom tactics of mine were killing my colleagues' ProofGeneral sessions
>> when they encountered errors. The workaround at
On Thu, 4 Apr 2013, Thomas Sewell wrote:
David's investigation explains a problem we had a few years ago where
some custom tactics of mine were killing my colleagues' ProofGeneral
sessions when they encountered errors. The workaround at the time was to
remove all potentially useful debugging i
On Wed, 3 Apr 2013, Alexander Krauss wrote:
Thanks Alex, it always helps if someone else with substantial experience
explains things, so that I am not the lone voice in the desert. I let
your nice explanations stand as is.
The area of your issue (interaction with the underlying ML system) i
Just my two cents, but I'd like to see this problem fixed as well.
David's investigation explains a problem we had a few years ago where
some custom tactics of mine were killing my colleagues' ProofGeneral
sessions when they encountered errors. The workaround at the time was to
remove all pote
Hi Alexander,
Thanks for your helpful reply.
On 04/04/13 08:58, Alexander Krauss wrote:
> Hi David,
> On 04/03/2013 09:18 AM, David Greenaway wrote:
[...]
>> Does my 4 line patch violate the Isabelle style guidelines, or have
>> I missed something about the correct etiquette for submitting patch
Hi David,
On 04/03/2013 09:18 AM, David Greenaway wrote:
On 02/04/13 21:17, Makarius wrote:
before you send more patches, can you please go back to the very start
of the mail thread from last time, which contains a lot of hints how
things are done, including pointers to the documentation.
I a
Hi Makarius,
On 02/04/13 21:17, Makarius wrote:
> On Tue, 2 Apr 2013, David Greenaway wrote:
>
>> I would appreciate it if an Isabelle expert could review that patch
>> and, if acceptable, apply it to mainline. (This can be easily done
>> with "hg import ").
>
> before you send more patches, can
On Tue, 2 Apr 2013, David Greenaway wrote:
I would appreciate it if an Isabelle expert could review that patch and,
if acceptable, apply it to mainline. (This can be easily done with "hg
import ").
Dear David,
before you send more patches, can you please go back to the very start of
the mai
Hi all,
I have noticed that in c ertain circumstances both Isabelle/jEdit and
Isabelle/ProofGeneral will render certain constructs with a large number
of spaces in them.
The problem can be seen with the following testcase:
definition "test a b ≡ undefined"
notation (output) test ("test
15 matches
Mail list logo
