[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

Re: RFS: proofgeneral



This is good news. I tried out proof general at one point, good to see
you working on it. I will try our your package when I find time.
mike

On Mon, Jan 9, 2012 at 10:54 PM, Hendrik Tews <tews@os.inf.tu-dresden.de> wrote:
> 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
>
>
> --
> To UNSUBSCRIBE, email to debian-mentors-REQUEST@lists.debian.org
> with a subject of "unsubscribe". Trouble? Contact listmaster@lists.debian.org
> Archive: [🔎] 20235.25094.153187.329551@blau.inf.tu-dresden.de">http://lists.debian.org/[🔎] 20235.25094.153187.329551@blau.inf.tu-dresden.de
>



-- 
James Michael DuPont
Member of Free Libre Open Source Software Kosova http://flossk.org


Reply to: