RFS: proofgeneral
Dear mentors,
I am looking for a sponsor for my package "proofgeneral".
* Package name : proofgeneral
Version : 4.2~pre120104-1
Upstream Author : David Aspinall and others
* URL : http://proofgeneral.inf.ed.ac.uk/
* License : GPL 2
Section : science
It builds those binary packages:
proofgeneral - generic frontend for proof assistants
proofgeneral-doc - generic frontend for proof assistants - documentation
To access further information about this package, please visit the following URL:
http://mentors.debian.net/package/proofgeneral
Alternatively, one can download the package with dget using this command:
dget -x http://mentors.debian.net/debian/pool/main/p/proofgeneral/proofgeneral_4.2~pre120104-1.dsc
Ordinary Coq users and myself would be glad, if someone could
sponsor this package.
Some more information about the packaging:
The current proofgeneral package in Debian is orphaned. The
current Debian version is 3.7, which was released upstream in
July 2008. Meanwhile version 4.0 and 4.1 have been released.
I decided to package a prerelease of 4.2, because Coq 8.4 will
probably soon appear in testing and Proof General 4.2 contains
important changes for Coq 8.4 (namely support for proof-tree
displays).
I simplified the package structure. The orphaned package provides
a generic package, 3 proof assistant specific packages, and a doc
package. I believe there are at most 2 proof assistants that a
Debian package should support: Coq and PhoX. Apart from Isabelle/Hol
(isar), all the others are long obsolete. Isabelle/Hol is always
distributed with its own version of Proof General, so its better
not to interfere with that.
Because of all that my package proofgeneral replaces the orphaned
packages proofgeneral, proofgeneral-coq, proofgeneral-minlog and
proofgeneral-misc. I kept proofgeneral-doc separate, assuming
that most users will read the documentation on the Proof General
web site.
Known issues with my proofgeneral package:
- the Proof General splash screen misses the picture (still
investigating)
- proofgeneral-coq, proofgeneral-minlog and proofgeneral-misc are
not deleted when proofgeneral is upgraded.
Would Replaces: proofgeneral-coq, ... fix this?
Bye,
Hendrik
Reply to: