[Pkg-ocaml-maint-commits] [hol-light] branch master updated (a5735d4 -> db54cd8)

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a change to branch master
in repository hol-light.

  from  a5735d4   Update watch file
   new  991870c   Imported Upstream version 20170109
   new  0d4515f   Merge tag 'upstream/20170109'
   new  db54cd8   update packaging for new upstream version

The 3 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails.  The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.


Summary of changes:
 100/bernoulli.ml   | 2 +-
 100/cayley_hamilton.ml | 7 +-
 100/circle.ml  | 2 -
 100/constructible.ml   |12 +-
 100/e_is_transcendental.ml | 4 +-
 100/fourier.ml |  1317 +-
 100/heron.ml   | 2 +-
 100/independence.ml|   148 +-
 100/liouville.ml   | 2 +-
 100/minkowski.ml   | 3 +-
 100/piseries.ml| 2 +-
 100/pnt.ml | 9 +-
 100/polyhedron.ml  | 4 +-
 100/ptolemy.ml |18 +-
 100/ramsey.ml  |12 +-
 100/reciprocity.ml | 2 +-
 100/sqrt.ml|42 +
 Arithmetic/definability.ml | 2 +-
 Boyer_Moore/clausal_form.ml| 4 +-
 Boyer_Moore/definitions.ml |12 +-
 Boyer_Moore/environment.ml | 6 +-
 Boyer_Moore/equalities.ml  |12 +-
 Boyer_Moore/generalize.ml  |46 +-
 Boyer_Moore/induction.ml   | 2 +-
 Boyer_Moore/irrelevance.ml | 2 +-
 Boyer_Moore/rewrite_rules.ml   | 4 +-
 Boyer_Moore/support.ml | 4 +-
 Boyer_Moore/terms_and_clauses.ml   | 5 +-
 Boyer_Moore/waterfall.ml   |16 +-
 CHANGES|  2579 +-
 Complex/complex_grobner.ml |24 +-
 Complex/complexnumbers.ml  |10 +-
 Complex/quelim.ml  | 4 +-
 Examples/brunn_minkowski.ml|43 +-
 Examples/cooper.ml |32 +-
 Examples/dickson.ml|85 +
 Examples/division_algebras.ml  |   575 +
 Examples/dlo.ml| 6 +-
 Examples/gcdrecurrence.ml  |   230 +
 Examples/harmonicsum.ml|   123 +
 Examples/hol88.ml  |12 +-
 Examples/holby.ml  |24 +-
 Examples/inverse_bug_puzzle_tac.ml | 2 +-
 Examples/kb.ml |22 +-
 Examples/lucas_lehmer.ml   |   412 +
 Examples/misiurewicz.ml|  1296 +
 Examples/mizar.ml  |   122 +-
 Examples/prog.ml   |52 +-
 Examples/prover9.ml|25 +-
 Examples/solovay.ml| 2 +-
 Examples/sos.ml|44 +-
 Examples/update_database.ml| 8 +-
 Formal_ineqs/README.txt| 8 +
 Formal_ineqs/arith/arith_cache.hl  |   212 +
 Formal_ineqs/arith/arith_num.hl|  1448 +
 Formal_ineqs/arith/eval_interval.hl|   278 +
 Formal_ineqs/arith/float.hl|  3889 ++
 Formal_ineqs/arith/float_atn.hl|   582 +
 Formal_ineqs/arith/float_theory.hl |87 +
 Formal_ineqs/arith/interval_arith.hl   |59 +
 Formal_ineqs/arith/more_float.hl   |   491 +
 Formal_ineqs/arith/nat.hl  |   102 +
 Formal_ineqs/arith/num_exp_theory.hl   |   251 +
 Formal_ineqs/arith_options.hl  |25 +
 Formal_ineqs/docs/FormalVerifier.pdf   |   Bin 0 -> 223139 bytes
 Formal_ineqs/docs/FormalVerifier.tex   |   419 +
 Formal_ineqs/examples.hl   |74 +
 Formal_ineqs/examples_flyspeck.hl  |   326 +
 Formal_ineqs/examples_poly.hl  |   141 +
 Formal_ineqs/informal/informal_arith.hl

[Pkg-ocaml-maint-commits] [hol-light] 02/03: Merge tag 'upstream/20170109'

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a commit to branch master
in repository hol-light.

commit 0d4515f9ce415a6b6a904e64243abd3a462d
Merge: a5735d4 991870c
Author: Hendrik Tews 
Date:   Mon Jan 9 20:52:16 2017 +0100

Merge tag 'upstream/20170109'

Upstream version 20170109

 100/bernoulli.ml   | 2 +-
 100/cayley_hamilton.ml | 7 +-
 100/circle.ml  | 2 -
 100/constructible.ml   |12 +-
 100/e_is_transcendental.ml | 4 +-
 100/fourier.ml |  1317 +-
 100/heron.ml   | 2 +-
 100/independence.ml|   148 +-
 100/liouville.ml   | 2 +-
 100/minkowski.ml   | 3 +-
 100/piseries.ml| 2 +-
 100/pnt.ml | 9 +-
 100/polyhedron.ml  | 4 +-
 100/ptolemy.ml |18 +-
 100/ramsey.ml  |12 +-
 100/reciprocity.ml | 2 +-
 100/sqrt.ml|42 +
 Arithmetic/definability.ml | 2 +-
 Boyer_Moore/clausal_form.ml| 4 +-
 Boyer_Moore/definitions.ml |12 +-
 Boyer_Moore/environment.ml | 6 +-
 Boyer_Moore/equalities.ml  |12 +-
 Boyer_Moore/generalize.ml  |46 +-
 Boyer_Moore/induction.ml   | 2 +-
 Boyer_Moore/irrelevance.ml | 2 +-
 Boyer_Moore/rewrite_rules.ml   | 4 +-
 Boyer_Moore/support.ml | 4 +-
 Boyer_Moore/terms_and_clauses.ml   | 5 +-
 Boyer_Moore/waterfall.ml   |16 +-
 CHANGES|  2579 +-
 Complex/complex_grobner.ml |24 +-
 Complex/complexnumbers.ml  |10 +-
 Complex/quelim.ml  | 4 +-
 Examples/brunn_minkowski.ml|43 +-
 Examples/cooper.ml |32 +-
 Examples/dickson.ml|85 +
 Examples/division_algebras.ml  |   575 +
 Examples/dlo.ml| 6 +-
 Examples/gcdrecurrence.ml  |   230 +
 Examples/harmonicsum.ml|   123 +
 Examples/hol88.ml  |12 +-
 Examples/holby.ml  |24 +-
 Examples/inverse_bug_puzzle_tac.ml | 2 +-
 Examples/kb.ml |22 +-
 Examples/lucas_lehmer.ml   |   412 +
 Examples/misiurewicz.ml|  1296 +
 Examples/mizar.ml  |   122 +-
 Examples/prog.ml   |52 +-
 Examples/prover9.ml|25 +-
 Examples/solovay.ml| 2 +-
 Examples/sos.ml|44 +-
 Examples/update_database.ml| 8 +-
 Formal_ineqs/README.txt| 8 +
 Formal_ineqs/arith/arith_cache.hl  |   212 +
 Formal_ineqs/arith/arith_num.hl|  1448 +
 Formal_ineqs/arith/eval_interval.hl|   278 +
 Formal_ineqs/arith/float.hl|  3889 ++
 Formal_ineqs/arith/float_atn.hl|   582 +
 Formal_ineqs/arith/float_theory.hl |87 +
 Formal_ineqs/arith/interval_arith.hl   |59 +
 Formal_ineqs/arith/more_float.hl   |   491 +
 Formal_ineqs/arith/nat.hl  |   102 +
 Formal_ineqs/arith/num_exp_theory.hl   |   251 +
 Formal_ineqs/arith_options.hl  |25 +
 Formal_ineqs/docs/FormalVerifier.pdf   |   Bin 0 -> 223139 bytes
 Formal_ineqs/docs/FormalVerifier.tex   |   419 +
 Formal_ineqs/examples.hl   |74 +
 Formal_ineqs/examples_flyspeck.hl  |   326 +
 Formal_ineqs/examples_poly.hl  |   141 +
 Formal_ineqs/informal/informal_arith.hl|   805 +
 Formal_ineqs/informal/informal_eval_interval.hl|   275 +
 Formal_ineqs/informal/informal_m_taylor.hl |   403 +
 Formal_ineqs/informal/informal_m_verifier.hl   |   302 +
 .../jordan/parse_ext_override_interface.hl

[Pkg-ocaml-maint-commits] [hol-light] 03/03: update packaging for new upstream version

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a commit to branch master
in repository hol-light.

commit db54cd89ee1b59337e9583b6a327a8d94bae2abc
Author: Hendrik Tews 
Date:   Mon Jan 9 23:32:00 2017 +0100

update packaging for new upstream version
---
 debian/README.Debian| 51 --
 debian/changelog| 23 +++
 debian/control  |  6 +-
 debian/copyright| 91 -
 debian/hol-light-source.exclude |  5 +-
 debian/patches/cd-holtest-parallel.patch| 13 
 debian/patches/holtest-no-proof-recording.patch |  2 +-
 debian/patches/series   |  1 +
 debian/rules|  5 +-
 9 files changed, 169 insertions(+), 28 deletions(-)

diff --git a/debian/README.Debian b/debian/README.Debian
index 331d58c..94317aa 100644
--- a/debian/README.Debian
+++ b/debian/README.Debian
@@ -12,7 +12,7 @@ For information on how to use HOL Light, please visit the HOL 
Light
 website at http://www.cl.cam.ac.uk/~jrh13/hol-light/
 
 HOL Light runs inside an OCaml toplevel. On every session start, the
-logical core and all auxilary theorems are loaded as sources into the
+logical core and all auxiliary theorems are loaded as sources into the
 OCaml toplevel. On modern hardware this takes about 90 seconds.
 
 HOL Light can use several external tools. Prover9, CSDP, PARI/GP and
@@ -61,27 +61,40 @@ installing security updates.
 Hol Light test suite
 
 
-The HOL Light test suite is in /usr/share/hol-light/holtest. You
-should install the packages prover9, coinor-csdp, pari-gp and
-libocamlgraph-ocaml-dev before running it. The test suite will run for
-the best part of a day. To check success you have to search for
-"Error", "Not_found" and "not found" in the output, for example by
-doing
+The HOL Light test suite is in /usr/share/hol-light/holtest and in
+/usr/share/hol-light/holtest_parallel. Both scripts run the same
+tests, the latter one uses ``make -j $(getconf _NPROCESSORS_ONLN)'' to
+run the tests in parallel on all available cores. When I last tried,
+the tests run for about 70 CPU hours (10 hours on 8 cores for the
+parallel version).
+
+You should install the packages prover9, coinor-csdp, pari-gp and
+libocamlgraph-ocaml-dev before running the tests. The sequential
+version produces the output on standard output, which you should
+capture with something like
 
-/usr/share/hol-light/holtest 2>&1 | tee holtest.log | egrep -i 
'###|error|not.found' 
+/usr/share/hol-light/holtest 2>&1 | tee holtest.log
+
+The parallel version eventually produces the file
+/tmp/hollog_/holtest.log containing all the output.
+To check success you have to search for
+"Error", "Not_found" and "not found" in the output, for example by
+using
 
-With this command you can watch all HOL Light messages flying by with
-"tail -f holtest.log". 
+egrep -i 'error|not.found'
 
-On Debian the test suite will produce one error 
-"Error: skip Minisat/make.ml...", because the Minisat examples cannot
-be run without zChaff, which is not available in Debian. Further,
-there are a number of false positives, because a number of values and
-exceptions contain "error" in their name.
+On Debian, the test suite will produce the error "Error: skip
+Minisat/make.ml...", because the Minisat examples cannot be run
+without zChaff, which is not available in Debian. Additionally, the
+tests Mizarlight/make.ml, miz3/make.ml and QBF/make.ml will fail as
+they do for the upstream version. On architecture i386 (and probably
+other 32 bit architectures as well), the test 100/pnt.ml fails because
+it runs out of memory.
 
-Note that some tests pass successfully even if the functionality is
-not available. For instance, "QBF/make.ml" is loaded successfully,
-regardless of whether squolem2 is installed or not.
+Note that the above grep command produces quite a few false positives,
+because a number of values and exceptions contain "error" in their
+name. Note also, that some tests pass successfully even if the
+functionality is not available.
 
 
- -- Hendrik Tews , Fri, 17 May 2013 13:54:06 +0200
+ -- Hendrik Tews , Mon,  9 Jan 2017 23:30:42 +0100
diff --git a/debian/changelog b/debian/changelog
index 52aa11a..1d6b415 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,26 @@
+hol-light (20170109-1) unstable; urgency=low
+
+  [ Mehdi Dogguy ]
+  * Update watch file
+
+  [ Hendrik Tews ]
+  * Imported Upstream version 20170109
+with git hash f468686c09996f77ccfa98c30ba98f8db2c8cfd9
+  * update copyright, patches, README.Debian
+  * standards-version 3.9.8; update Vcs fields
+  * disable building the Mizarlight syntax extension (fails upstream with
+OCaml 4.02 - already reported to John Harrison)
+  *

[Pkg-ocaml-maint-commits] [hol-light] branch pristine-tar updated (862c915 -> c2552f0)

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a change to branch pristine-tar
in repository hol-light.

  from  862c915   pristine-tar data for hol-light_20131026.orig.tar.bz2
   new  c2552f0   pristine-tar data for hol-light_20170109.orig.tar.gz

The 1 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails.  The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.


Summary of changes:
 hol-light_20170109.orig.tar.gz.delta | Bin 0 -> 36362 bytes
 hol-light_20170109.orig.tar.gz.id|   1 +
 2 files changed, 1 insertion(+)
 create mode 100644 hol-light_20170109.orig.tar.gz.delta
 create mode 100644 hol-light_20170109.orig.tar.gz.id

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git

___
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

[Pkg-ocaml-maint-commits] [hol-light] branch upstream updated (fc867d4 -> 991870c)

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a change to branch upstream
in repository hol-light.

  from  fc867d4   Imported Upstream version 20131026
   new  991870c   Imported Upstream version 20170109

The 1 revisions listed above as "new" are entirely new to this
repository and will be described in separate emails.  The revisions
listed as "adds" were already present in the repository and have only
been added to this reference.


Summary of changes:
 100/bernoulli.ml   | 2 +-
 100/cayley_hamilton.ml | 7 +-
 100/circle.ml  | 2 -
 100/constructible.ml   |12 +-
 100/e_is_transcendental.ml | 4 +-
 100/fourier.ml |  1317 +-
 100/heron.ml   | 2 +-
 100/independence.ml|   148 +-
 100/liouville.ml   | 2 +-
 100/minkowski.ml   | 3 +-
 100/piseries.ml| 2 +-
 100/pnt.ml | 9 +-
 100/polyhedron.ml  | 4 +-
 100/ptolemy.ml |18 +-
 100/ramsey.ml  |12 +-
 100/reciprocity.ml | 2 +-
 100/sqrt.ml|42 +
 Arithmetic/definability.ml | 2 +-
 Boyer_Moore/clausal_form.ml| 4 +-
 Boyer_Moore/definitions.ml |12 +-
 Boyer_Moore/environment.ml | 6 +-
 Boyer_Moore/equalities.ml  |12 +-
 Boyer_Moore/generalize.ml  |46 +-
 Boyer_Moore/induction.ml   | 2 +-
 Boyer_Moore/irrelevance.ml | 2 +-
 Boyer_Moore/rewrite_rules.ml   | 4 +-
 Boyer_Moore/support.ml | 4 +-
 Boyer_Moore/terms_and_clauses.ml   | 5 +-
 Boyer_Moore/waterfall.ml   |16 +-
 CHANGES|  2579 +-
 Complex/complex_grobner.ml |24 +-
 Complex/complexnumbers.ml  |10 +-
 Complex/quelim.ml  | 4 +-
 Examples/brunn_minkowski.ml|43 +-
 Examples/cooper.ml |32 +-
 Examples/dickson.ml|85 +
 Examples/division_algebras.ml  |   575 +
 Examples/dlo.ml| 6 +-
 Examples/gcdrecurrence.ml  |   230 +
 Examples/harmonicsum.ml|   123 +
 Examples/hol88.ml  |12 +-
 Examples/holby.ml  |24 +-
 Examples/inverse_bug_puzzle_tac.ml | 2 +-
 Examples/kb.ml |22 +-
 Examples/lucas_lehmer.ml   |   412 +
 Examples/misiurewicz.ml|  1296 +
 Examples/mizar.ml  |   122 +-
 Examples/prog.ml   |52 +-
 Examples/prover9.ml|25 +-
 Examples/solovay.ml| 2 +-
 Examples/sos.ml|44 +-
 Examples/update_database.ml| 8 +-
 Formal_ineqs/README.txt| 8 +
 Formal_ineqs/arith/arith_cache.hl  |   212 +
 Formal_ineqs/arith/arith_num.hl|  1448 +
 Formal_ineqs/arith/eval_interval.hl|   278 +
 Formal_ineqs/arith/float.hl|  3889 ++
 Formal_ineqs/arith/float_atn.hl|   582 +
 Formal_ineqs/arith/float_theory.hl |87 +
 Formal_ineqs/arith/interval_arith.hl   |59 +
 Formal_ineqs/arith/more_float.hl   |   491 +
 Formal_ineqs/arith/nat.hl  |   102 +
 Formal_ineqs/arith/num_exp_theory.hl   |   251 +
 Formal_ineqs/arith_options.hl  |25 +
 Formal_ineqs/docs/FormalVerifier.pdf   |   Bin 0 -> 223139 bytes
 Formal_ineqs/docs/FormalVerifier.tex   |   419 +
 Formal_ineqs/examples.hl   |74 +
 Formal_ineqs/examples_flyspeck.hl  |   326 +
 Formal_ineqs/examples_poly.hl  |   141 +
 Formal_ineqs/informal/informal_arith.hl|   805 +
 Formal_ineqs/informal/informal_eval_interval.hl|   275 +

[Pkg-ocaml-maint-commits] [hol-light] annotated tag upstream/20170109 created (now 3eb0ea7)

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a change to annotated tag upstream/20170109
in repository hol-light.

at  3eb0ea7   (tag)
   tagging  991870cb311cf1da0bf42e9f383eec43c66be2fc (commit)
  replaces  upstream/20131026
 tagged by  Hendrik Tews
on  Mon Jan 9 20:52:16 2017 +0100

- Log -
Upstream version 20170109

Hendrik Tews (1):
  Imported Upstream version 20170109

---

No new revisions were added by this update.

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git

___
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

[Pkg-ocaml-maint-commits] [hol-light] 01/01: pristine-tar data for hol-light_20170109.orig.tar.gz

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a commit to branch pristine-tar
in repository hol-light.

commit c2552f005a9bea6fead729c4dce8473274267995
Author: Hendrik Tews 
Date:   Mon Jan 9 20:52:16 2017 +0100

pristine-tar data for hol-light_20170109.orig.tar.gz
---
 hol-light_20170109.orig.tar.gz.delta | Bin 0 -> 36362 bytes
 hol-light_20170109.orig.tar.gz.id|   1 +
 2 files changed, 1 insertion(+)

diff --git a/hol-light_20170109.orig.tar.gz.delta 
b/hol-light_20170109.orig.tar.gz.delta
new file mode 100644
index 000..a9a9cd9
Binary files /dev/null and b/hol-light_20170109.orig.tar.gz.delta differ
diff --git a/hol-light_20170109.orig.tar.gz.id 
b/hol-light_20170109.orig.tar.gz.id
new file mode 100644
index 000..a9fc4c4
--- /dev/null
+++ b/hol-light_20170109.orig.tar.gz.id
@@ -0,0 +1 @@
+cad327b0538c7a5cf65652ad42ba62cc986fc3ce

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git

___
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits

[Pkg-ocaml-maint-commits] [hol-light] annotated tag debian/20170109-1 created (now 2017bc9)

2017-01-12 Thread Hendrik Tews 
This is an automated email from the git hooks/post-receive script.

hendrik-guest pushed a change to annotated tag debian/20170109-1
in repository hol-light.

at  2017bc9   (tag)
   tagging  db54cd89ee1b59337e9583b6a327a8d94bae2abc (commit)
  replaces  debian/20131026-1
 tagged by  Hendrik Tews
on  Thu Jan 12 09:10:17 2017 +0100

- Log -
hol-light Debian release 20170109-1
-BEGIN PGP SIGNATURE-
Version: GnuPG v1

iQIcBAABCgAGBQJYdznpAAoJEOxoV33tyu5oztUQAIn98IiaMpsQIFvFfYUBSG3K
Q8ViHODm19RGtotGnDfYTxnfHuv5sPZX8UvWi1ifzURzQ9F/R6u3GGDyXBcxrbDY
Xitzlo999hX+1QmoOSv5biroAq0v0PWbwx6vM/J0DKJkz8F96ELRZcupPVVLDNTC
UXkEwMbllQCU2jBMge4We0hEfHAKzjpwkFeVeOhvE7nTGyE6DlNPu5VHK2d0ARHf
BNTtAh/iCVlJkXNVozWX7lzJwHO4F80ektvsRWUJBsX6JXlXUu1n1rJLhh+97jDJ
YjOWiPFLWISG0oVWbdtbYMJs3p9zJSOCjWdAclWAF9BZtjMuKWkX3fBZVlnfgMuh
IOkJEn7TPOJdxsVHXcc3Rrl9/FT3QmiNd2Mvse5ZfyFHK4NT2tuJkPr+J2gKMPds
NI9yc6bfuRj1l+oNFQMQjLkh93wqI2J1bjjHYf6kYFVPOE0CBFHDWp6Mu9kQQXjj
GzubQ6bMNk3ZM5F7nmd3/yQS0P40g0avAZ4MQQQFYUzwEdD1+vzuLewvEbGxB+we
2W2ipl14g8X2aDBMHCa8zbAgdf44K2VGK9utOkwe9u/hbfwqUTX1GUxJ+f9ywhlx
ps8Jg5DrJfhjqWvOZmXTA9Q8/ZZ48xL9MPf0BB086I0gFbCDcJnfkc7EbZByjF8k
r4QPZblLP6+5JXH3FbyZ
=VhLs
-END PGP SIGNATURE-

Hendrik Tews (3):
  Imported Upstream version 20170109
  Merge tag 'upstream/20170109'
  update packaging for new upstream version

Mehdi Dogguy (1):
  Update watch file

---

No new revisions were added by this update.

-- 
Alioth's /usr/local/bin/git-commit-notice on 
/srv/git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git

___
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits