#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)
Change History (7)
Changed 20 years ago by dem5302@…
comment:1 Changed 20 years ago by gwright@…
| Status: | new → assigned |
|---|
comment:2 Changed 20 years ago by mww@…
| Owner: | changed from darwinports-bugs@… to jkh@… |
|---|---|
| Status: | assigned → new |
assign to xemacs maintainer for review
comment:3 Changed 20 years ago by jkh@…
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
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.
ProofGeneral Portfile