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

Bug#876533: marked as done (hol-light FTBFS with OCaml 4.05.0)

Your message dated Mon, 29 Jul 2019 11:07:54 +0000
with message-id <E1hs3VS-000Hwo-3I@fasolo.debian.org>
and subject line Bug#876533: fixed in hol-light 20190729-0.1
has caused the Debian Bug report #876533,
regarding hol-light FTBFS with OCaml 4.05.0
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.)


-- 
876533: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=876533
Debian Bug Tracking System
Contact owner@bugs.debian.org with problems
--- Begin Message --- 
Source: hol-light
Version: 20170109-2
Severity: serious

https://buildd.debian.org/status/package.php?p=hol-light&suite=sid

...
0..0..1..4..11..25..51..106..solved at 153
0..0..1..4..11..solved at 21
0..0..1..5..15..37..85..209..492..solved at 962
0..0..1..4..11..25..55..120..227..404..688..1152..1863..3160..solved at 4748
val CAUCHY_INDUCT : thm =
  |- !P. P 2 /\ (!n. P n ==> P (2 * n)) /\ (!n. P (n + 1) ==> P n)
         ==> (!n. P n)
1 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
3 basis elements and 0 critical pairs
3 basis elements and 3 critical pairs
4 basis elements and 5 critical pairs
4 basis elements and 4 critical pairs
4 basis elements and 3 critical pairs
5 basis elements and 0 critical pairs
0..0..1..2..5..solved at 10
0..0..1..solved at 4
0..0..1..2..5..solved at 10
0..0..1..2..4..solved at 9
0..0..1..solved at 4
0..0..1..2..4..6..8..11..14..17..solved at 27
val AGM : thm =
  |- !n a.
         1 <= n /\ (!i. 1 <= i /\ i <= n ==> &0 <= a i)
         ==> product (1..n) a <= (sum (1..n) a / &n) pow n
val it : unit = ()
# 
Error: This kind of expression is not allowed as right-hand side of `let rec'
Error in included file /<<PKGBUILDDIR>>/lists.ml

Error in Library/agm.ml, test failed
debian/rules:48: recipe for target 'override_dh_auto_test' failed
make[1]: *** [override_dh_auto_test] Error 1

--- End Message ---
--- Begin Message --- 
Source: hol-light
Source-Version: 20190729-0.1

We believe that the bug you reported is fixed in the latest version of
hol-light, which is due to be installed in the Debian FTP archive.

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 876533@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.

Debian distribution maintenance software
pp.
Gianfranco Costamagna <locutusofborg@debian.org> (supplier of updated hol-light 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@ftp-master.debian.org)


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

Format: 1.8
Date: Sat, 27 Jul 2019 10:19:28 +0200
Source: hol-light
Binary: hol-light
Architecture: source
Version: 20190729-0.1
Distribution: unstable
Urgency: medium
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Changed-By: Gianfranco Costamagna <locutusofborg@debian.org>
Description:
 hol-light  - HOL Light theorem prover
Closes: 876533 878615
Changes:
 hol-light (20190729-0.1) unstable; urgency=medium
 .
   * Non-maintainer upload
   * New upstream snapshot (Closes: #876533)
     - Patch for new ocaml and camlp5
     - tweak rules file to stop copy of the new ml file
       This is already done in upstream build system.
     - do not install .pc file in the system (Closes: #878615)
   * Update copyright file
   * Update copyright file http in https mode
Checksums-Sha1:
 368201127d3ee6734ba88d596c8d6662cccdd4b3 2051 hol-light_20190729-0.1.dsc
 78a00734637a1cb7312c4c3cf71f7efca559dee1 6959546 hol-light_20190729.orig.tar.gz
 b3d86f60a5d41c3a1c1a1c64b145977468247609 9576 hol-light_20190729-0.1.debian.tar.xz
 c5fa7efad994215cdaa35e9f153ab49731e86c5b 7330 hol-light_20190729-0.1_source.buildinfo
Checksums-Sha256:
 6f5541cd2e42e2c6897d49b87815ca6d788950b214ae9f7410d6197af4ddde68 2051 hol-light_20190729-0.1.dsc
 88cfcdd1430d963b9fc63960829e1a5f7c08df98ed92b3765cff51691dbfe75a 6959546 hol-light_20190729.orig.tar.gz
 882497a57fa3513d7b8878585cf4e9dedf97dfbb47532eef4ef8d04630ce27f7 9576 hol-light_20190729-0.1.debian.tar.xz
 930da06eef362c7dc5a55fbfdc38493213df9cebe55b5a19e423da1131f81718 7330 hol-light_20190729-0.1_source.buildinfo
Files:
 14cafd08250ae2ea98042418e3d08aef 2051 math extra hol-light_20190729-0.1.dsc
 9a8813a63d883e10c5b52c36b93ee9b0 6959546 math extra hol-light_20190729.orig.tar.gz
 305bbfda8b72464de992db2ca683414c 9576 math extra hol-light_20190729-0.1.debian.tar.xz
 3061e05f7ce23de96e18a442c187f571 7330 math extra hol-light_20190729-0.1_source.buildinfo

-----BEGIN PGP SIGNATURE-----

iQIzBAEBCAAdFiEEkpeKbhleSSGCX3/w808JdE6fXdkFAl0+0CwACgkQ808JdE6f
XdnfEA/8DQ+K3+zunygymZWI5EKmzccLvbHd+IQ5lSr/yhhXGD+eSq4uvDrKMJVS
uOWKKsul1dY2SNOiXfmkOIvLrIo2lkzVPELzhGiy2lNlnG6uxyvV0aaoKwOyUlP0
LUxAhM6xdXwMZ6ubvAGVISEodl/3hM48L4S1tYB6siQJDsjJrrXJ8NMSs9c7P3AP
DMG7DcAFjlGMA6NIVWqfOl+DH7Kgge1ZzzvjahPjAne2F+kMUbHo+CByH095cPKR
5xlo4NaYpa1ZhECZQT8wEn56fv6zaY9zDfp0v54+3c1EA03aWApNx8eXEHP0UsQs
q3d8B6ilqIYLxjN8hzZSvsmvu4Ki4sHBPawrOk9/UYTnFStL9IGxevSkL+UuhZDr
qnRXzDhlr7W9sCfYb644morkml4HrB389kFJ0ENQRs6jigng7f7oCcIlJylgonUH
HiWCzvR3gR7Z5lhCTpKboRYuqftdN9US8z8NyHVKOZv3//C+dV8jorqni/1gHdTg
gc7MEGPBnpzzvANSdP9hWx5X8VxCXTt61JmgqXGuYhEAOnvCAQkGryTUyoMIk63Z
/IvDLoklFAdzUheqEYo109DIp+e9LCPU7KGJaZFzAzFG7sTLboA3jhLlaZG6eFjh
dpQidoMfNcqObqbJEG1jCmTv694z/CVbMLJ3wX2was0qJxdcLVM=
=PHfZ
-----END PGP SIGNATURE-----

--- End Message ---
Reply to: