Re: [PG-devel] Reboot: Release of PG 4.2
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 anything left to do before you can do make release? Maybe I or somebody else could help? (My Coq project is now so large that the sequential blocking compilation really sucks. I would really like to start now with rewriting the compilation with parallel background jobs.) 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] Reboot: Release of PG 4.2
Hendrik Tews t...@os.inf.tu-dresden.de writes: - support for braces and bullets This requires more work than I thought. I have to postpone this to October. Given that only few people use braces/bullets (because they are new) and even fewer use Prooftree, it doesn't make sense to delay the release of Proof General because of this issue. The problem is that with braces and bullets Coq exhibits a state where the old current goal has been finished but it has not yet switched to the next goal. Without braces and bullets you never see such a state and therefore all prooftree code assumes that such a state is not visible. 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] Reboot: Release of PG 4.2
(add-hook 'proof-activate-scripting-hook '(lambda () (when As mentioned recently, the above (lambda ...) s-expressions is not data but is a function, so don't quote it with '. Stefan PS: As Elisp slowly moves to lexical scoping, the difference between the two is becoming more important, hence my renewed battle against such quoting. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
