Re: [isabelle] provers used by sledgehammer



On Fri, 20 Jul 2012, Jasmin Christian Blanchette wrote:

Am 20.07.2012 um 17:50 schrieb Jasmin Blanchette:

My personal preference would be for somebody who will be around in Chair 21 for the next 2 or 3 years at least. But if none of the people meeting this criterion (and the maintenance criterion) step forward, I'd be willing to step in at least for the next year and do the minimal amount of work needed to keep it running on our three main platforms with the latest Isabelle.

Larry wrote off-list that he would be willing to help with occasional Emacs Lisp programming.

Both of us are fervent adepts of Aquamacs. One of the first things we'd like to do is make that the default on the Mac again. Some issues were mentioned on the list but don't seem to affect me (with PG 3.7.1.1) or Larry (with PG 4.0?). Do you remember anything specific from the top of your head?

OK, so Jasmin and Larry will take care of it in the near future, until some more Proof General adherents will join eventually. Some people could also share their experience with old versions of PG and old versions of Emacs on the Isabelle community wiki.

Jasmin and Larry, you should also get in touch with David Aspinall, concerning recent PG repository versions. There has been quite some activity recently, and last time I've checked it did not work on stock Linux distributions with slightly old Emcas 23 anymore. (This is not surprising, it has happenend routinely over the years.)


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.