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 compilation feature? 
For me it works perfectly and I would make it default (and delete
serial compilation before the 4.4 release).

I have some comments about recent commits:

- the project file feature should IMHO be mentioned in the user
  manual

- similarly for the coq/faq: wouldn't it be better to integrate
  this in the user manual and have then a "coq faq" link on the
  web page?

- similarly for ML4PG: it certainly deserves a separate
  subsection in the user manual


About Hol Light support: I posted a hint about it on hol-info but
got no reaction. It seems that no Hol Light user is interested in
having Proof General support. I therefore expect it to stay
forever in the current unfinished state. 

   2013/7/4 David Aspinall <david.aspin...@ed.ac.uk>

   > 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

A better tracker would certainly be nice. Otherwise I don't care
much.

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to