Opened 20 years ago

Closed 20 years ago

Last modified 20 years ago

#2443 closed defect (fixed)

NEW: ProofGeneral-3.5

Reported by: dem5302@… Owned by: jkh@…
Priority: Normal Milestone:
Component: ports Version: 1.0
Keywords: Cc:
Port:

Description

A new portfile for the Proof General xemacs mode

Attachments (1)

Portfile (1.2 KB) - added by dem5302@… 20 years ago.
ProofGeneral Portfile

Download all attachments as: .zip

Change History (7)

Changed 20 years ago by dem5302@…

Attachment: Portfile added

ProofGeneral Portfile

comment:1 Changed 20 years ago by gwright@…

Status: newassigned

comment:2 Changed 20 years ago by mww@…

Owner: changed from darwinports-bugs@… to jkh@…
Status: assignednew

assign to xemacs maintainer for review

comment:3 Changed 20 years ago by jkh@…

Resolution: fixed
Status: newclosed

Committed, with some cleanup. Not exactly sure how to use it, however. /opt/local/bin/proofgeneral doesn't appear to work - is there some secret?

comment:4 Changed 20 years ago by gwright@…

Um, this is already in math/. Perhaps the bug was never closed out?

Greg, your friendly vizier of darwinports theorem provers ;-)

comment:5 Changed 20 years ago by gwright@…

ProofGeneral really want a dependency on _either_ coq or isabelle, since it's not much use without an underlying theorem prover.

/gw

comment:6 Changed 20 years ago by jkh@…

Whoops. Duplicate port deleted and the optimizations merged over to the math/ version.

Note: See TracTickets for help on using tickets.