If you use DariwinPorts on a Mac, here is a modified Portfile to fetch/compile/install the Proof General release candidate. However, it probably cannot be used until Trac issue #369 is dealt with. I have attached a (really ugly) patch to that ticket; if you apply the patch then the Portfile will work.
- a # $Id: Portfile 57375 2009-09-10 08:16:41Z ryandes...@macports.org $ PortSystem 1.0 name ProofGeneral version 4.0pre101004 categories math maintainers mww (tweaked by megacz) platforms darwin description An emacs mode for interactive prooving long_description The aim of Proof General is to provide powerful \ and configurable interfaces which help user-interaction \ with proof assistants. Proof General targets power users \ rather than novices, but is designed to be useful to \ both. Proof General leads to an environment for \ serious proof engineering of interactively-constructed \ proofs. homepage http://proofgeneral.inf.ed.ac.uk/ master_sites ${homepage}/releases/ extract.suffix .tgz checksums sha1 c930ee7e788c16afa869e156d519322321047065 use_configure no build { system "cd ${worksrcpath} && make clean" system "cd ${worksrcpath} && make" } destroot { xinstall -m 755 -d ${destroot}${prefix}/share file copy ${worksrcpath} ${destroot}${prefix}/share ln -s ${prefix}/share/ProofGeneral-${version} ${destroot}${prefix}/share/ProofGeneral ln -s ${prefix}/share/ProofGeneral-${version}/bin/proofgeneral ${destroot}${prefix}/bin/proofgeneral } post-install { ui_msg "\nTo use ProofGeneral with Emacs, add the following line to your ~/.emacs file:\n\ (load-file \"${prefix}/share/ProofGeneral/generic/proof-site.el\")\n" } livecheck.url http://proofgeneral.inf.ed.ac.uk/releases/?C=M\;O=D livecheck.type regex livecheck.regex ProofGeneral-(\[0-9.\]+).tgz _______________________________________________ ProofGeneral mailing list ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral