Re: [PG-devel] non-fatal warnings for make compile
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 variable `coq-project-filename' (Hendrik, I think this is yours?) - David On 22/05/13 21:40, Hendrik Tews wrote: Hi, I spend some time to find a fix for tickets #458. The problem is that special-display-regexps is obsolete in 24.3, while its replacement, display-buffer-alist was only introduced in 24.1 and not fully functional before 24.3. Writing compatible code for emacs 23 and 24 without obsolete warning therefore requires explicit version checks. I therefore suggest that we change to display-buffer-alist when we drop support for Emacs 23. To fix #458, warnings should be non-fatal when users compile Proof General for their local emacs. I just committed the necessary changes in the Makefile. For developers, there is now the new target 'check' that retains the old behavior, i.e., stopping compilation on every byte-compilation warning. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] non-fatal warnings for make compile
2013/7/4 David Aspinall david.aspin...@ed.ac.uk 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.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] non-fatal warnings for make compile
David Aspinall david.aspin...@ed.ac.uk 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 compilation errors are not an issue. They are rare and if one is reported on this list it is fixed immediately. I have nevertheless two suggestions: - we could have a nightly compilation and spam pg-devel when errors occur - we could add -include LocalMakefile to Makefile and have a LocalMakefile that makes ``check'' the default compilation target and omit LocalMakefile from the distribution. If you think these compilation errors are an issue, I volunteer to implement one or both suggestions. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] non-fatal warnings for make compile
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://travis-ci.org/ which appears to offer a free build server for OS projects hosted on Github. Don't know quite how they finance the cycles (but building PG shouldn't take many). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] non-fatal warnings for make compile
Fixed. There was also a problem with m4pg, also fixed at coq.el:2204. P. 2013/7/4 Pierre Courtieu pierre.court...@cnam.fr 2013/7/4 David Aspinall david.aspin...@ed.ac.uk 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.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] non-fatal warnings for make compile
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 http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
