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 these things).

- D.

ProofGeneral-devel mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to