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

Bug#538398: marked as done (coq: The description in README.Debian about proofgeneral is old.)



Your message dated Sat, 29 Aug 2009 16:35:10 +0000
with message-id <E1MhQtS-0004Q7-6d@ries.debian.org>
and subject line Bug#538398: fixed in coq 8.2.pl1+dfsg-3
has caused the Debian Bug report #538398,
regarding coq: The description in README.Debian about proofgeneral is old.
to be marked as done.

This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.

(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact owner@bugs.debian.org
immediately.)


-- 
538398: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=538398
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message ---
Package: coq
Version: 8.2.pl1+dfsg-2
Severity: minor

* A description of the incorrect behavior:

/usr/share/doc/coq/README.Debian says that there is no official Debian
package of Proof General yet.

>Coq frontends
>-------------
>For interactive use of coqtop, we suggest
>- either the Debian cle package
>- or the Proof-General (x)emacs mode, which unfortunately can not be
>distributed by Debian for copyright reasons. However, a Debian package
>might become available at proof general home page in the future
>(http://zermelo.dcs.ed.ac.uk/~proofgen)

But this information is old. The package proofgeneral-coq is available
now and coq recommends this package. Please update this section of
README.Debian.


* A suggested fix:

I found a diff in the net. See
https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/trunk/distrib/debian/README.Debian?root=coq&rev=3637&r1=2288&r2=3637


-- System Information:
Debian Release: squeeze/sid
  APT prefers unstable
  APT policy: (500, 'unstable')
Architecture: i386 (i686)


Versions of packages coq depends on:
ii  coq-theories              8.2.pl1+dfsg-2 proof assistant for higher-order l
ii  emacsen-common            1.4.19         Common facilities for all emacsen
ii  libc6                     2.9-21         GNU C Library: Shared libraries
ii  ocaml-base-nox [ocaml-bas 3.11.1-2       Runtime system for OCaml bytecode

Versions of packages coq recommends:
ii  coqide                    8.2.pl1+dfsg-2 proof assistant for higher-order l
ii  proofgeneral-coq          3.7-3          generic interface for proof assist

Versions of packages coq suggests:
ii  coq-doc                       8.1-3      documentation for Coq in html form
pn  libcoq-ocaml-dev              <none>     (no description available)
ii  ocaml-nox                     3.11.1-2   ML implementation with a class-bas
ii  proofgeneral-coq              3.7-3      generic interface for proof assist
ii  rlwrap [readline-editor]      0.30-1.1   readline feature command line wrap



--- End Message ---
--- Begin Message ---
Source: coq
Source-Version: 8.2.pl1+dfsg-3

We believe that the bug you reported is fixed in the latest version of
coq, which is due to be installed in the Debian FTP archive:

coq-theories_8.2.pl1+dfsg-3_all.deb
  to pool/main/c/coq/coq-theories_8.2.pl1+dfsg-3_all.deb
coq_8.2.pl1+dfsg-3.diff.gz
  to pool/main/c/coq/coq_8.2.pl1+dfsg-3.diff.gz
coq_8.2.pl1+dfsg-3.dsc
  to pool/main/c/coq/coq_8.2.pl1+dfsg-3.dsc
coq_8.2.pl1+dfsg-3_amd64.deb
  to pool/main/c/coq/coq_8.2.pl1+dfsg-3_amd64.deb
coqide_8.2.pl1+dfsg-3_amd64.deb
  to pool/main/c/coq/coqide_8.2.pl1+dfsg-3_amd64.deb
libcoq-ocaml-dev_8.2.pl1+dfsg-3_amd64.deb
  to pool/main/c/coq/libcoq-ocaml-dev_8.2.pl1+dfsg-3_amd64.deb



A summary of the changes between this version and the previous one is
attached.

Thank you for reporting the bug, which will now be closed.  If you
have further comments please address them to 538398@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Stéphane Glondu <glondu@debian.org> (supplier of updated coq package)

(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmaster@debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Format: 1.8
Date: Sat, 29 Aug 2009 16:58:45 +0200
Source: coq
Binary: coq coqide coq-theories libcoq-ocaml-dev
Architecture: source all amd64
Version: 8.2.pl1+dfsg-3
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Stéphane Glondu <glondu@debian.org>
Description: 
 coq        - proof assistant for higher-order logic (toplevel and compiler)
 coq-theories - proof assistant for higher-order logic (theories)
 coqide     - proof assistant for higher-order logic (gtk interface)
 libcoq-ocaml-dev - development libraries and tools for Coq
Closes: 538398
Changes: 
 coq (8.2.pl1+dfsg-3) unstable; urgency=low
 .
   * Update README.Debian (Closes: #538398)
   * Add 0001-Update-for-why-2.19.patch
   * debian/control:
     - update my e-mail address and remove DMUA
     - add why to Suggests
     - add quilt to Build-Depends
     - update Standards-Version to 3.8.3 (no changes)
   * Update README.source to reflect use of quilt
Checksums-Sha1: 
 ef1b0bdde9e7082f3357d7ef1df1cd11fa3da3fb 2241 coq_8.2.pl1+dfsg-3.dsc
 aa0ff3a8b48641abc06313d6882f6295287dbe09 15366 coq_8.2.pl1+dfsg-3.diff.gz
 7f451acff4d791ec380fd5e46baad7df8ea39973 18385280 coq-theories_8.2.pl1+dfsg-3_all.deb
 cfde5f650efd39e7d243dd84628ab036fedd18f5 15311654 coq_8.2.pl1+dfsg-3_amd64.deb
 6d1af285f21fe5d6a513a4d9a854c312ff46ab42 6538312 coqide_8.2.pl1+dfsg-3_amd64.deb
 c6ec229de2cfb357bf31db4b5e8ade52cac29330 6047962 libcoq-ocaml-dev_8.2.pl1+dfsg-3_amd64.deb
Checksums-Sha256: 
 334f0db990aff91d6f580198ec26df41e7c6fcb43293dcaefad2e50feb0022a1 2241 coq_8.2.pl1+dfsg-3.dsc
 955138b5d7c4184d74472937417422194b93b230081f603bb9231d72a10d36b6 15366 coq_8.2.pl1+dfsg-3.diff.gz
 7de64169eb5cf90956de151729d91c78f16d4f26c249ce13859f8a7f56d540c3 18385280 coq-theories_8.2.pl1+dfsg-3_all.deb
 5c7a75aa6a15458e105bff55aebfefd84d69a8741dffd05b466bab7f73a2912f 15311654 coq_8.2.pl1+dfsg-3_amd64.deb
 cedfa94f1ef103c4bea92f9d8cc118825ba1a656fa1d70a51ce6cb800e5c96d0 6538312 coqide_8.2.pl1+dfsg-3_amd64.deb
 f0903b0633e1657ffe020fa490de7a1171b1e34bf60bf11d673fe85ce69f4b5d 6047962 libcoq-ocaml-dev_8.2.pl1+dfsg-3_amd64.deb
Files: 
 1a49833777bf4b499fd58250aeebc881 2241 math optional coq_8.2.pl1+dfsg-3.dsc
 8667c0c9c1ef0ca6605b599064872808 15366 math optional coq_8.2.pl1+dfsg-3.diff.gz
 1d4285ba0f4d0c3501e85447f726d3cc 18385280 math optional coq-theories_8.2.pl1+dfsg-3_all.deb
 32ee6a98d5b7fffbf7d0ade395bcfa68 15311654 math optional coq_8.2.pl1+dfsg-3_amd64.deb
 bc00fd5eaeea99edc9ad6df677445def 6538312 math optional coqide_8.2.pl1+dfsg-3_amd64.deb
 dceb923a94a9a5bfb874fea273c26a68 6047962 ocaml optional libcoq-ocaml-dev_8.2.pl1+dfsg-3_amd64.deb

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)

iQIcBAEBCgAGBQJKmU0KAAoJEHhT2k1JiBrT+noP/2TRpENUl+7eZgO9drll3yfr
GYLZv3ZMjWW5lt640yp2R+CnJJV0GdKsepga96emi4vVBFUyI4E5Baz9fOI0EX9Z
xdB5AxbWusbhaerHyLsR3zcMNNRgc3Y3PcKnPcgGadortUL8hMRkHFy2mKN/ylQo
0tRiuJerkCgtG5DUAmdxBJG0E2iasUrYB4zkuCvQp1HVy980lYpehtR7p1SGdexi
25H1KLorWpCKWu0Ahe6ysxX7rXXyk2WDMOoE7iSiLbhJ4+RdTPXyuwhJnbaLY37H
9D2fWsbNtwgyzuOHH5vX0o2DigkzhDJjtng6M7gJBaWRz0VIBIT+PovDUo1HjrgG
m77FR6eL5d+toGnUhatOSN5Z2YsyhmgFcxNGlDCo4clU0uTNATpu1ZsWXQlr0wDa
4QoHfylyXgv38dmgF//IcKrds8KmYT/l5AG4uWwZhuNoq4kuvtrgjJQmFE+hE8Oy
m36p6SG8Gh51KFHIya3R714ICO8Cnbd9kKBxoQiVF0otsCx9xatvtiltXWyTvJkz
MQjtTHGUZaO4eChvLEZwWSA0Q+8xku4Gzcoil7UXLRLwn0uM5OEWyekqDPKBkAFY
ZfMMZ5gbYPIrr7XSXqaHZrqa/6Oh4RG+14HBhI/HX6nbrJagIWP6t36LLkD+dl1k
59McsykR8UqThOhxGK4X
=44Yr
-----END PGP SIGNATURE-----



--- End Message ---

Reply to: