Debian Bug report logs - #494491
RFP: isabelle -- Generic theorem proving environment

Package: wnpp; Maintainer for wnpp is wnpp@debian.org;

Reported by: Lionel Elie Mamane <lionel@mamane.lu>

Date: Sat, 9 Aug 2008 22:39:01 UTC

Severity: wishlist

Reply or subscribe to this bug.

Toggle useless messages

View this report as an mbox folder, status mbox, maintainer mbox


Report forwarded to debian-bugs-dist@lists.debian.org, debian-devel@lists.debian.org, brucker@member.fsf.org, <wnpp@debian.org>, Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org:
Bug#494491; Package wnpp. Full text and rfc822 format available.

Acknowledgement sent to Lionel Elie Mamane <lionel@mamane.lu>:
New Bug report received and forwarded. Copy sent to debian-devel@lists.debian.org, brucker@member.fsf.org, <wnpp@debian.org>, Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org. Full text and rfc822 format available.

Message #5 received at submit@bugs.debian.org (full text, mbox):

From: Lionel Elie Mamane <lionel@mamane.lu>
To: Debian Bug Tracking System <submit@bugs.debian.org>
Subject: ITP: isabelle -- Generic theorem proving environment
Date: Sun, 10 Aug 2008 00:37:34 +0200
Package: wnpp
Severity: wishlist
Owner: Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org

* Package name    : isabelle
  Version         : 2008
  Upstream Author : University of Cambridge (Larry Paulson), Technische Universitaet Muenchen (Tobias Nipkow, Makarius Wenzel)
* URL             : http://isabelle.in.tum.de/, http://www.cl.cam.ac.uk/research/hvg/Isabelle/
* License         : 3-clause BSD-like
                    (non-free documentation)
  Programming Lang: Standard ML
  Description     : Generic theorem proving environment

 Features a choice of several ready-to-use logics (Higher Order Logic,
 Higher Order Logic augmented with Scott's Logic for Computable
 Functions, First Order Logic, Zermello-Frankel, an extensional
 version of Martin-Löf Type Theory, Barendregt's Lambda Cube, a few
 sequent calculi (including modal and linear logics), ...) or
 defining your own logic / deductive system, a procedural and a
 declarative proof style, rich automation for classical reasoning,
 equational logic and algebra, LaTeX and X-Symbols notational support.
 .
 Isabelle can also be used as a generic framework for rapid
 prototyping of deductive systems.

-- System Information:
Debian Release: lenny/sid
  APT prefers unstable
  APT policy: (500, 'unstable'), (1, 'experimental')
Architecture: amd64 (x86_64)

Kernel: Linux 2.6.25-2-amd64 (SMP w/2 CPU cores)
Locale: LANG=fr_LU.UTF-8, LC_CTYPE=fr_LU.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/bash




Information forwarded to debian-bugs-dist@lists.debian.org, <wnpp@debian.org>, Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org:
Bug#494491; Package wnpp. Full text and rfc822 format available.

Acknowledgement sent to Loïc Fejoz <loic@fejoz.net>:
Extra info received and forwarded to list. Copy sent to <wnpp@debian.org>, Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org. Full text and rfc822 format available.

Message #10 received at 494491@bugs.debian.org (full text, mbox):

From: Loïc Fejoz <loic@fejoz.net>
To: Lionel Elie Mamane <lionel@mamane.lu>, 494491@bugs.debian.org
Subject: Re: Bug#494491: ITP: isabelle -- Generic theorem proving environment
Date: Mon, 11 Aug 2008 10:08:44 +0200
Good news !

Someone already have a repository:
deb http://kisogawa.inf.ethz.ch/isamorph/debian/ testing main

It may worth have a look at it...

PS : Same for PolyML (Bug#494488: ITP: polyml).

-- 
cheers,
Loïc Fejoz

Lionel Elie Mamane a écrit :
> Package: wnpp
> Severity: wishlist
> Owner: Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org
> 
> * Package name    : isabelle
>   Version         : 2008
>   Upstream Author : University of Cambridge (Larry Paulson), Technische Universitaet Muenchen (Tobias Nipkow, Makarius Wenzel)
> * URL             : http://isabelle.in.tum.de/, http://www.cl.cam.ac.uk/research/hvg/Isabelle/
> * License         : 3-clause BSD-like
>                     (non-free documentation)
>   Programming Lang: Standard ML
>   Description     : Generic theorem proving environment




Information forwarded to debian-bugs-dist@lists.debian.org, <wnpp@debian.org>, Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org:
Bug#494491; Package wnpp. Full text and rfc822 format available.

Acknowledgement sent to Lionel Elie Mamane <lionel@mamane.lu>:
Extra info received and forwarded to list. Copy sent to <wnpp@debian.org>, Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org. Full text and rfc822 format available.

Message #15 received at 494491@bugs.debian.org (full text, mbox):

From: Lionel Elie Mamane <lionel@mamane.lu>
To: Loïc Fejoz <loic@fejoz.net>
Cc: 494491@bugs.debian.org
Subject: Re: Bug#494491: ITP: isabelle -- Generic theorem proving environment
Date: Mon, 11 Aug 2008 12:33:42 +0200
On Mon, Aug 11, 2008 at 10:08:44AM +0200, Loïc Fejoz wrote:

> Someone already have a repository:
> deb http://kisogawa.inf.ethz.ch/isamorph/debian/ testing main

> It may worth have a look at it...

Actually, Achim also has a repository
http://www.brucker.ch/projects/debian/index.en.html. We are using
those as a starting point. Thank you for the pointer, though. These
packages are not quite ready for Debian, but we are working on it.

-- 
Lionel




Tags added: Request was from Lionel Elie Mamane <lionel@mamane.lu> to controlbugs.debian.org. (Mon, 11 Aug 2008 12:03:07 GMT) Full text and rfc822 format available.

Blocking bugs of 494491 added: 494488 Request was from Lionel Elie Mamane <lionel@mamane.lu> to control@bugs.debian.org. (Fri, 15 Aug 2008 21:27:30 GMT) Full text and rfc822 format available.

Reply sent to Lionel Elie Mamane <lionel@mamane.lu>:
You have taken responsibility. (Fri, 24 Jul 2009 11:12:07 GMT) Full text and rfc822 format available.

Notification sent to Lionel Elie Mamane <lionel@mamane.lu>:
Bug acknowledged by developer. (Fri, 24 Jul 2009 11:12:08 GMT) Full text and rfc822 format available.

Message #24 received at 494491-done@bugs.debian.org (full text, mbox):

From: Lionel Elie Mamane <lionel@mamane.lu>
To: 494491-done@bugs.debian.org
Subject: Not going to package Isabelle
Date: Fri, 24 Jul 2009 12:53:11 +0200
We have given up on packaging Isabelle, for various technical and
social reasons.

-- 
Lionel




Bug archived. Request was from Debbugs Internal Request <owner@bugs.debian.org> to internal_control@bugs.debian.org. (Sat, 22 Aug 2009 07:33:53 GMT) Full text and rfc822 format available.

Bug unarchived. Request was from Joachim Breitner <nomeata@debian.org> to control@bugs.debian.org. (Mon, 12 Apr 2010 21:09:10 GMT) Full text and rfc822 format available.

Did not alter fixed versions and reopened. Request was from Debbugs Internal Request <owner@bugs.debian.org> to internal_control@bugs.debian.org. (Mon, 12 Apr 2010 21:09:10 GMT) Full text and rfc822 format available.

Changed Bug title to 'RFP: isabelle -- Generic theorem proving environment' from 'ITP: isabelle -- Generic theorem proving environment' Request was from Joachim Breitner <nomeata@debian.org> to control@bugs.debian.org. (Mon, 12 Apr 2010 21:09:10 GMT) Full text and rfc822 format available.

Owner changed from Lionel Elie Mamane <lionel@mamane.lu>, brucker@member.fsf.org to Joachim Breitner <nomeata@debian.org>. Request was from Joachim Breitner <nomeata@debian.org> to control@bugs.debian.org. (Mon, 12 Apr 2010 21:09:11 GMT) Full text and rfc822 format available.

Information forwarded to debian-bugs-dist@lists.debian.org, wnpp@debian.org:
Bug#494491; Package wnpp. (Sat, 17 Jul 2010 20:24:02 GMT) Full text and rfc822 format available.

Acknowledgement sent to Joachim Breitner <nomeata@debian.org>:
Extra info received and forwarded to list. Copy sent to wnpp@debian.org. (Sat, 17 Jul 2010 20:24:02 GMT) Full text and rfc822 format available.

Message #39 received at 494491@bugs.debian.org (full text, mbox):

From: Joachim Breitner <nomeata@debian.org>
To: Lionel Elie Mamane <lmamane@debian.org>
Cc: 494491@bugs.debian.org
Subject: Isabelle packagin
Date: Sat, 17 Jul 2010 22:22:00 +0200
[Message part 1 (text/plain, inline)]
Hi Lionel,

> We have given up on packaging Isabelle, for various technical and
> social reasons.

I’m currently working a lot with Isabelle and obviously, I’m wondering
why it has not been packaged for Debian.

Could you elaborate what kind of technical and social issues came up?

Greetings,
Joachim

-- 
Joachim "nomeata" Breitner
Debian Developer
  nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C
  JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata
[signature.asc (application/pgp-signature, inline)]

Information forwarded to debian-bugs-dist@lists.debian.org, wnpp@debian.org, Joachim Breitner <nomeata@debian.org>:
Bug#494491; Package wnpp. (Sat, 17 Jul 2010 20:57:06 GMT) Full text and rfc822 format available.

Acknowledgement sent to "Achim D. Brucker" <brucker@member.fsf.org>:
Extra info received and forwarded to list. Copy sent to wnpp@debian.org, Joachim Breitner <nomeata@debian.org>. (Sat, 17 Jul 2010 20:57:06 GMT) Full text and rfc822 format available.

Message #44 received at 494491@bugs.debian.org (full text, mbox):

From: "Achim D. Brucker" <brucker@member.fsf.org>
To: Joachim Breitner <nomeata@debian.org>, 494491@bugs.debian.org
Cc: Lionel Elie Mamane <lmamane@debian.org>
Subject: Re: Bug#494491: Isabelle packagin
Date: Sat, 17 Jul 2010 22:45:12 +0200
[Message part 1 (text/plain, inline)]
Hi Joachim,

On Sat, Jul 17, 2010 at 10:22:00PM +0200, Joachim Breitner wrote:
> > We have given up on packaging Isabelle, for various technical and
> > social reasons.
> 
> I’m currently working a lot with Isabelle and obviously, I’m wondering
> why it has not been packaged for Debian.
> 
> Could you elaborate what kind of technical and social issues came up?

to make a long story short: the Isabelle developers strongly prefer to
have only one official Isabelle distribution and, thus, do not
encourage Isabelle distribution by others. Moreover, they prefer to
provide the whole "Isabelle suite" (i.e., Isabelle and all surrounding
tools (Poly/ML, Proof General, Scala, e, spass, jedit, etc) as one
integrated bundle.  Of course, this "bundling requirement" makes is
hard (if not impossible) to integrate properly into Debian.

Greetings, 
	   Achim
-- 
http://www.brucker.ch
[signature.asc (application/pgp-signature, inline)]

Removed annotation that Bug was owned by Joachim Breitner <nomeata@debian.org>. Request was from Bart Martens <bartm@debian.org> to control@bugs.debian.org. (Wed, 06 Jun 2012 00:39:25 GMT) Full text and rfc822 format available.

Send a report that this bug log contains spam.


Debian bug tracking system administrator <owner@bugs.debian.org>. Last modified: Sat Apr 19 07:53:21 2014; Machine Name: buxtehude.debian.org

Debian Bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.