Re: [PG-devel] non-fatal warnings for make compile

2013-07-04 Thread David Aspinall
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 var

[PG-devel] Move to Github

2013-07-04 Thread David Aspinall
Dear PG Devs, Some time ago I mooted moving from our clunky University-hosted CVS+trac to Github. I think it would allow people to more easily make modifications and propose small patches. And it looks as if the Github issue tracking system is now reasonable enough to use that we can move t

Re: [PG-devel] Move to Github

2013-07-04 Thread Pierre Courtieu
No objection! Pierre 2013/7/4 David Aspinall > Dear PG Devs, > > Some time ago I mooted moving from our clunky University-hosted CVS+trac > to Github. I think it would allow people to more easily make modifications > and propose small patches. And it looks as if the Github issue tracking > sy

Re: [PG-devel] non-fatal warnings for make compile

2013-07-04 Thread Pierre Courtieu
2013/7/4 David Aspinall > introduce No it is mine. Sorry I will look at it. this is my recent attempt at reading coq project files as described in coq documentation. P. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists

Re: [PG-devel] non-fatal warnings for make compile

2013-07-04 Thread Hendrik Tews
David Aspinall writes: This fix was helpful but unfortunately means that developers are more likely to introduce bugs unless they run make clean; make check I agree. But even before the change we had now and then compilation errors in the repository. >From my point of view the com

Re: [PG-devel] non-fatal warnings for make compile

2013-07-04 Thread David Aspinall
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 https://tr

Re: [PG-devel] non-fatal warnings for make compile

2013-07-04 Thread Pierre Courtieu
Fixed. There was also a problem with m4pg, also fixed at coq.el:2204. P. 2013/7/4 Pierre Courtieu > > 2013/7/4 David Aspinall > >> introduce > > > > No it is mine. Sorry I will look at it. this is my recent attempt at > reading coq project files as described in coq documentation. > > P. >

Re: [PG-devel] Move to Github

2013-07-04 Thread Hendrik Tews
Hi, I am happy to see Pierre you back on this list and back committing to Proof General. Regarding the 4.3 release: There are some indentation bugs in the tracker. Pierre, could you spend some time for them? I intend to fix #467 and have a look at #460. Does anybody else use the new parallel c

Re: [PG-devel] Move to Github

2013-07-04 Thread Hendrik Tews
Hendrik Tews writes: Regarding the 4.3 release: ... I have another issue that I would like to see resolved in 4.3: The feature name conflict with Coq, see http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2012/000241.html Both Proof General and Coq install coq.el (and some other files