On Thu, 28 Apr 2011, David Aspinall wrote:
I am keen to use a more modern distributed system but it probably means
choosing an external provider rather than trying to get the University
to provide yet another semi-supported tool that works at the beginning
and then rusts. Sourceforge is the
commercial hosting platform that looks quite shiny is
http://www.fogcreek.com/kiln/
This is definitely moving far away from what hardcore GNU people would
like ...
Makarius
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http
made a little experiment with Coq 8.4 beta as PIDE
backend. See also
https://bitbucket.org/makarius/coq-clone/src/4b806b6e1757/README.PIDE
https://bitbucket.org/makarius/isabelle-coq/src at rev 07c7fc8ba7bd
Both taken together gives you a proof of concept: Isabelle/PIDE/jEdit as
front-end
in the
background, and the editor merely asks for small parts in some kind of
display protocol. The latter notion is by David Aspinall from PGIP,
more than 10 years ago.
Makarius
___
ProofGeneral-devel mailing list
ProofGeneral-devel
On Tue, 21 Apr 2015, Andreas Röhler wrote:
for the sake of a very, very interesting project as Isabelle certainly
looks like, also having done fairly enough mistakes by myself, please
permit to outline what's wrong here IMHO:
first, there is no need to support Emacs actively by any core
e 1990s and no longer relevant.
Isabelle has moved away from PG in 2011, and Isabelle2014 (August 2014)
is the last version that can in principle use PG. Afterwards, all
remains of the TTY loop have been dismantled: Isabelle operates directly
on multiple
eaded JVM,
even though the JVM is a bit ugly.
BTW, I complained about the "master / slave" terminology of the new Coq
protocol when Enrico introduced that in 2012/2013, not for P.C. reasons
but for technological ones. In PIDE, the front-end and back-end are
anybody
wants to join pg-devel for further discussion, although I wouldn't
expect much from it.
Makarius
signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists
On 16/06/16 00:07, Clément Pit--Claudel wrote:
> On 2016-06-15 17:51, Makarius wrote:
>> Concerning the "new" prover APIs of Coq and Isabelle in general: I was
>> in contact with Enrico Tassi when he introduced this for Coq -- it was
>> part of our Paral-ITP p
