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:
1
As 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
Undoing those Add LoadPath commands with Remove LoadPath commands
would be rather difficult. If one adds a directory which is
already in the LoadPath, coq reorders the LoadPath, a subsequent
remove will not yield the starting state.
In that case I'm not sure how you can achieve what you need,
For getting correct multiple file scripting for coq I would first
try to restart coqtop on every new scripting buffer. What would
be the best way to achieve this? Put proof-shell-exit into
proof-deactivate-scripting-hook?
I suppose but this does seem pretty crude, there is some cost to
This is, however, not the expected simplification. I decided for
this simple change, because it keeps the functionality of other
proof assistants without that I have to touch their code.
This sounds wise, and what Pierre originally suggested, although if I've
followed it seems as if that's
Thinking again on this:
This optimisation becomes desirable because we have the situation with the
implementation that the control over ancestor files is fine-grained (i.e.
during scripting the file rather than at the start by parsing imports which
the included files behaviour assumed). I
I'd recommend Savannah (either as a GNU or a non-GNU project).
interesting idea, good choice of VC systems there, not just bzr
Which reminds me: it would be nice to include PG into the GNU ELPA (a
package archive from which Elisp packages can be installed conveniently
via package.el). If
I would not expect a paragraph that starts with modern end with
Sourceforge. They added some half-harted support for Mercurial,
Bazaar, Git some years ago, and people rightly complained that it was
too late and too little.
There are several reasons to suggest sf. One is the provision of
As Emacs maintainer I recommend package maintainers to setup their
foo-site.el such that it is (mostly if not completely) auto-generated
by something like update-directory-autoloads.
In such a situation a simple
;;;###autoload
(add-to-list 'completion-ignored-extensions .vo)
in
BTW, http://proofgeneral.inf.ed.ac.uk/download still shows RC4.
Oops, committing web page failed -- will fix tomorrow, thanks for note.
+(if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t))
OK, this is likely to be contentious for Emacs experts who prefer the toolbar
off and
Dear PG-dev'ers,
This morning I made the release of PG 4.1, almost a year after 4.0.
I plan to announce a little bit more widely later this week, please let
me know asap if there are any hiccups.
Meanwhile, a big Thank-You to all on this list who have contributed
improvements and bug
On 09/08/12 11:11, Lionel Elie Mamane wrote:
That's why (back when it was available), I preferred to use the
coq-interface protocol rather than the coqtop -emacs protocol,
which has chunking multiple commands cleanly. I haven't looked at it
recently, but it seems to be the PCoq interface
Hi Hendrik
Thanks for the nudge --- no blockers I don't think, except extreme
overwork, 8-). I'll try to push the button soon, just need a spare
hour to run checks and update all the pieces. Apologies for the delay.
- David
On 17/10/12 15:25, Hendrik Tews wrote:
Hi,
David, is there
Hi Hendrik,
I am missing the documentation comment for
pg-finish-tracing-display. What is it used for?
I've just added it:
Handle the end of possibly voluminous tracing-style output.
If the output update was slowed down, show it now
Tracing output is defined with a regexp, it isn't used
I just came across proof-shell-pre-interrupt-hook. I can't find
any location where this hook is run. Am I missing something?
Likely obsolete but let me check some old versions:
http://proofgeneral.inf.ed.ac.uk/trac/ticket/457
--
The University of Edinburgh is a charitable body, registered
Hello Hendrik
Quick thoughts: this sounds like a pretty fundamental problem and
surprising if we hadn't come across it before. Do you definitely see
this in the ordinary running code, not just when using the debugger?
Maybe prooftree input is different case to prover input.
If we need to
Hendrik,
Thanks a lot for tackling this, I looked at it a while ago and saw it
was going to be a nuisance to fix...
- David.
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
This fix was helpful but unfortunately means that developers are more
likely to introduce bugs unless they run
make clean; make check
before committing. E.g., I have just tried to make a pre-release but I
now get the error
In toplevel form:
coq/coq.el:1040:67:Error: reference to free
On 04/07/13 12:21, Hendrik Tews wrote:
If you think these compilation errors are an issue, I volunteer
to implement one or both suggestions.
Thanks indeed! I think an automatic build would definitely be nice to
have if you have inclination/interest. Recently I found about Travis
On 11/07/2013 08:00, Hendrik Tews wrote:
Pierre Courtieu pierre.court...@cnam.fr writes:
- similarly for the coq/faq: wouldn't it be better to integrate
this in the user manual and have then a coq faq link on the
web page?
I don't understand this one. Do you mean in
Hi Erik,
> If you are thinking of adding a GitHub repo dedicated to the webpages
> sources, maybe it would be convenient to host the webpages themselves
> at GitHub too? Because according to https://pages.github.com/ and
> https://help.github.com/categories/github-pages-basics/ it would
> suffice
in emacs, it seems I can only work on one at a
time using Proof General, and there's only one proof-shell mode window
active.
-- Paul
On Fri, May 6, 2016 at 3:15 PM, David Aspinall <david.aspin...@ed.ac.uk> wrote:
I did something like this once to support PGIP, which was a sort of
pre-cursor o
ogramme Committee **
Serge Autexier, DFKI Bremen, Germany (Co-Chair)
Pedro Quaresma, U Coimbra, Portugal (Co-Chair)
David Aspinall, University of Edinburgh, Scotland
Chris Benzmüller, FU Berlin, Germany & Stanford, USA
Yves Bertot, INRIA Sophia-Antipolis, France
Gudmund Grov, Heriott-Watt Uni
I did something like this once to support PGIP, which was a sort of
pre-cursor of PIDE based on exchanging XML messages. You can find the
source in the CVS repo PG Kit repo (Kit/src/pgemacs). But it probably
isn't useful: it's about 10 years old and the case we wanted to allow
was input coming
As 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:
1
26 matches
Mail list logo
