New Ticket     Wiki     Browse Source     Timeline     Roadmap     Ticket Reports     Search

Ticket #2443 (closed defect: fixed)

Opened 7 years ago

Last modified 7 years ago

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

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

Change History

Changed 7 years ago by dem5302@…

ProofGeneral Portfile

Changed 7 years ago by gwright@…

  • status changed from new to assigned

Changed 7 years ago by mww@…

  • status changed from assigned to new
  • owner changed from darwinports-bugs@… to jkh@…

assign to xemacs maintainer for review

Changed 7 years ago by jkh@…

  • status changed from new to closed
  • resolution set to fixed

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?

Changed 7 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 ;-)

Changed 7 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

Changed 7 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.