Hello Adam
Many thanks for the feedback and suggestions. Would you be so kind as to lodge
tickets on our trac for these?
http://proofgeneral.inf.ed.ac.uk/trac
Both issues sound like faults, in fact. Please explain exactly which version
of PG you are using.
Thanks
- David
On 29 Jul 2010,
Dear PG users and developers,
With help from a few special people over the past few months, we have
ironed out many issues with the CVS version of Proof General and I think
it is good enough to make into an official release --- the first in over
two years.
In the hope of nipping the last few prob
On 15/12/10 14:33, Makarius wrote:
On Fri, 10 Dec 2010, Michael Chan wrote:
Is there a way to disable the display of messages that are annotated
with proof-shell-eager-annotation-start and
proof-shell-eager-annotation-end? I believe these are so called
'urgent messages'.
Can you explain which
> > Yes: on that note, I have been meaning to ask on the Isabelle devel list
> > if we can remove the "[Successful|Failed] attempt to solve goal by ..."
> > message from having the urgent message classification.
>
> This is an ancient workaround to get some output to the user in a proof
> stat
Unfortunately this sort of thing is a real struggle for Emacs,
especially XEmacs (try typing "yes" in a shell buffer of an XEmacs you
don't care about...). Suggest you turn off decoration and if you're
using XEmacs, switch.
- D.
On 17/12/10 13:59, Michael Chan wrote:
Just to add that I can
://proofgeneral.inf.ed.ac.uk/trac/
Best wishes,
- David
David Aspinall, email: david.aspin...@ed.ac.uk
LFCS, School of Informatics, URL: http://homepages.inf.ed.ac.uk/da
University of Edinburgh
___
ProofGeneral mailing list
Dear PG users and developers,
Hopefully many of you will know the CICM conference and have seen the CFP:
http://www.cicm-conference.org/2013/cicm.php?event=&menu=cfp
I'm the track chair for MKM (Mathematical Knowledge Management) this
year, I'm keen to see plenty of submissions for our track
Dear All,
I'm looking for industrial users of Proof General who have used it in
the last five years. Industrial means people who have used theorem
provers for applications outside of academia. Commercial research would
count so long as the use is not in theorem proving related research.
Are
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Forwarded Message
Subject:Using Proof-General with the HoTT Modification to Coq
Date: Wed, 22 Apr 2015 17:38:17 -0700
From: Casey Coleman
Hello,
I am
well as the usual Github mechanisms, there are some links to Zulip
chats there where PG developers and users can discuss.
Thanks to list members still here for their contributions over the years!
Best wishes,
- David
--
Prof. David Aspinall, Email: david.aspin...@ed.ac.uk
LFCS
To: David Aspinall
Thank you David!
Let me give some direct pointers as a follow-up of your e-mail:
Two communication channels are indeed preferred to get in touch with PG
devs/users: Zulip and GitHub.
So feel free to do one or both of the following actions if you're
interested
11 matches
Mail list logo
