Thanks for followup, Hendrik.
I'd like to push the button on this soon, so I think we should stop
adding new features/hacks to the CVS head for a while...
How about Hol light? Would you release 4.2 with the current
partial hol light support enabled? Or would you put hol-light
into comments in generic/proof-site.el?
I think it's best to disable it for now, have just done so. There is
some more effort available to work on this again after Oct (Hendrik,
I'll talk to you about this separately).
I would suggest that we agree on some schedule. For instance:
- we stop adding new features now
- permit 2 weeks for further bug fixes
- have another prerelease on 18 September
- release 4.2 on 25 September
That's a good suggestion. Unfortunately I have very little bandwidth
personally this month: to help smooth things out effectively I'd like to
fix/extend the automatic tests and add proper regression tests for fixed
bugs (Coq parsing is the most thorny).
I'd like to support Emacs 24 properly although there are API updates
which are tricky to support in two versions --- esp when the rightly
increasingly rigorous byte compiler tries to compile code for old
versions and barfs.
In addition to Davids list we should fix the conflict between
proof-electric-terminator and coq-colon-self-insert, that I
reported yesterday on this list.
I would like to fix some proof-tree problems before the release:
- Proof appears as command in the proof tree
- support for braces and bullets
Sounds good (if you want to add to Trac we can know when you've done
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.