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

Bug#508468: marked as done (ITP: ssreflect -- small scale reflection extension for the Coq proof assistant)

Your message dated Mon, 31 Aug 2009 19:28:41 +0000
with message-id <E1MiCYT-0007k7-Rg@ries.debian.org>
and subject line Bug#508468: fixed in ssreflect 1.2+dfsg-1
has caused the Debian Bug report #508468,
regarding ITP: ssreflect -- small scale reflection extension for the Coq proof assistant
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.)


-- 
508468: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=508468
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Package: wnpp
Severity: wishlist
Owner: Stephane Glondu <steph@glondu.net>

* Package name    : ssreflect
  Version         : 1.1
  Upstream Author : Georges Gonthier (Microsoft Research - Inria Joint Centre)
* URL             : http://www.msr-inria.inria.fr/Projects/math-components
* License         : CeCILL-B
  Programming Lang: OCaml, Coq
  Description     : small scale reflection extension library for the Coq proof assistant

 The name Ssreflect stands for "small scale reflection", a style of
 proof that evolved from the computer-checked proof of the Four Colour
 Theorem and which leverages the higher-order nature of Coq's
 underlying logic to provide effective automation for many small,
 clerical proof steps. This is often accomplished by restating
 ("reflecting") problems in a more concrete form, hence the name. For
 example, in the Ssreflect library arithmetic comparison is not an
 abstract predicate, but a function computing a boolean.
 .
 The Ssreflect distribution comprises two parts:
 * A new tactic language, which promotes more structured, concise and
   robust proof scripts, and is in fact independent from the "reflection"
   proof style. It is implemented as a linkable extension to the Coq
   system. 
 * A set of Coq libraries that provide core "reflection-oriented"
   theories for basic combinatorics (roughly: arithmetic, lists, and
   finite sets). 

-- System Information:
Debian Release: lenny/sid
  APT prefers testing
  APT policy: (990, 'testing'), (500, 'unstable'), (1, 'experimental')
Architecture: i386 (i686)

--- End Message ---
--- Begin Message --- 
Source: ssreflect
Source-Version: 1.2+dfsg-1

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

libssreflect-coq_1.2+dfsg-1_all.deb
  to pool/main/s/ssreflect/libssreflect-coq_1.2+dfsg-1_all.deb
libssreflect-ocaml_1.2+dfsg-1_amd64.deb
  to pool/main/s/ssreflect/libssreflect-ocaml_1.2+dfsg-1_amd64.deb
ssreflect_1.2+dfsg-1.diff.gz
  to pool/main/s/ssreflect/ssreflect_1.2+dfsg-1.diff.gz
ssreflect_1.2+dfsg-1.dsc
  to pool/main/s/ssreflect/ssreflect_1.2+dfsg-1.dsc
ssreflect_1.2+dfsg.orig.tar.gz
  to pool/main/s/ssreflect/ssreflect_1.2+dfsg.orig.tar.gz



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 508468@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 ssreflect 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: Wed, 26 Aug 2009 23:41:27 +0200
Source: ssreflect
Binary: libssreflect-ocaml libssreflect-coq
Architecture: source amd64 all
Version: 1.2+dfsg-1
Distribution: unstable
Urgency: low
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Stéphane Glondu <glondu@debian.org>
Description: 
 libssreflect-coq - small scale reflection library for Coq (theories)
 libssreflect-ocaml - small scale reflection extension for Coq (plugin)
Closes: 508468
Changes: 
 ssreflect (1.2+dfsg-1) unstable; urgency=low
 .
   * Initial release (Closes: #508468)
Checksums-Sha1: 
 d35f093a88448d276478e3c6cc5fc56b1f4f6b3c 2064 ssreflect_1.2+dfsg-1.dsc
 2eb821b6d7660688f24b9158dbe3ee2ed2182282 332281 ssreflect_1.2+dfsg.orig.tar.gz
 7e13449f00091f24be910d949c0a048c7ff621af 12376 ssreflect_1.2+dfsg-1.diff.gz
 30957386bd6768d6de6666b8a107e1b4cf9e65e7 385188 libssreflect-ocaml_1.2+dfsg-1_amd64.deb
 c2b9669f3e62aef748b8247f3ffddd36cac9b784 3624536 libssreflect-coq_1.2+dfsg-1_all.deb
Checksums-Sha256: 
 d424a9cb3b1602ef9955ca4f8fb9c84f8350c5a7654316650f5e92d8fd4acc84 2064 ssreflect_1.2+dfsg-1.dsc
 be53184a5fffea4e055f616461f2adab660e1424c73d146b898ee35f0921cb94 332281 ssreflect_1.2+dfsg.orig.tar.gz
 c08d901ae960308b338754165163e26f35709b69d254693fff0ea93d0b2f2715 12376 ssreflect_1.2+dfsg-1.diff.gz
 85e2a8a31b8b7fee12d61dff0505f820c9f43d2f250b7e161ff21ac49678175c 385188 libssreflect-ocaml_1.2+dfsg-1_amd64.deb
 572f59e4f0b6b1c61a513b5cc723af2d08268b14d5bf133a1a2fa91b38acb1c6 3624536 libssreflect-coq_1.2+dfsg-1_all.deb
Files: 
 0d04121c6f8d0354ce239fcb76c02ef5 2064 math extra ssreflect_1.2+dfsg-1.dsc
 e0815fa981ea23087f7de90d9487e581 332281 math extra ssreflect_1.2+dfsg.orig.tar.gz
 37da3dda3147f72460fce28bd3f260c5 12376 math extra ssreflect_1.2+dfsg-1.diff.gz
 1938384ce17adfe4a8e92ef2f9354801 385188 math extra libssreflect-ocaml_1.2+dfsg-1_amd64.deb
 35ba32310d91f345f8ce534244d18865 3624536 math extra libssreflect-coq_1.2+dfsg-1_all.deb

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

iQIcBAEBCgAGBQJKla7oAAoJEHhT2k1JiBrTETEP/iBahPb0TRCRZCn8EJXU1xG3
zJeQysi16rmm/xl1ciYE8hcxe2PAYfOpQAodx4oLSpyNkxfCgT01L2BDxQP+WrdA
h1ULtVgjytyE8EaFvDjyEDs++WHIVBvUkRh7i7aRx53rtsL398IwrHSka+WoGe3j
+hu7/9OUeZYmx8xZ+LKZ32RE0XpzJ4kVgMfCZkORr1tTDW1l38kVjq0FulsppglH
yr16y+V+iq+Pp6lo7/7CVYfVK2/nCQy2nF906uRvzZXcyOYT4AX8dxiJD9a4V+UU
0Sxh2TP4hM6oyu9YMhGZpRdgtIOVw1hYDJvXZpC/mqXyIhWUBr203/050mzT9YWS
4CcxFVkw6qAH76wyatOzjfvbCyDvzcyIYNtufiKEE7U0NJw1kYmdR0BdHnf4Kaq0
YFz4w9BJ1QoDkQM2isZdfTXm5tEu2xCIoVmY/bEFzfzHHul0bxYKJiUzhQa60jMD
rWUwKzaISUPCm0mz9P5bWPgldxmp0XS5aPinzkwJsFEj/RWS1Y7w8zZddSw/jx1L
gPVwQ7bmEjZH7cjMzuf5aKiNOmpRIgJqDnmbIl5jvbRBcnZiRiD++lk4+/iKyFIy
rgFQe9ld+vbvFfKqHHHKef8w6oYX1JL8FfDo74AcP047c8QHle/7BsrNZ2Az6MMV
Qj35avH+nK92ZeBoDc2G
=dH2l
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: