Package: hol-light
Version: 20170109-1
Severity: normal
Dear Maintainer,
*** Reporter, please consider answering these questions, where appropriate ***
* What led up to the situation?
$ cd /usr/share/hol-light/Formal_ineqs
$ hol-light
...hol-light starts up and presents prompt #...
# needs "verifier/m_verifier_main.hl";;
... Formal_ineqs systems loads, this ends after 1 hour with these lines:
val BERNSTEIN_WEIERSTRASS : thm =
|- !f e.
f real_continuous_on real_interval [&0,&1] /\ &0 < e
==> (?N. !n x.
N <= n /\ x IN real_interval [&0,&1]
==> abs
(f x -
sum (0..n) (\k. f (&k / &n) * bernstein n
k x)) <
e)
Warning:
inventing type variables
0..0..3..solved
at 6
0..0..2..7..18..33..75..132..245..473..921..1493..2790..4343..solved at 7055
0..0..solved at 2
0..0..0..2..5..solved at 10
0..0..0..2..5..solved at 10
Signal -7
* What exactly did you do (or not do) that was effective (or
ineffective)?
* What was the outcome of this action?
* What outcome did you expect instead?
*** End of the template - remove these template lines ***
-- System Information:
Debian Release: 9.4
APT prefers stable-updates
APT policy: (500, 'stable-updates'), (500, 'stable')
Architecture: amd64 (x86_64)
Kernel: Linux 4.9.87-linuxkit-aufs (SMP w/4 CPU cores)
Locale: LANG=C, LC_CTYPE=C (charmap=ANSI_X3.4-1968), LANGUAGE=C
(charmap=ANSI_X3.4-1968)
Shell: /bin/sh linked to /bin/dash
Init: unable to detect
Versions of packages hol-light depends on:
ii camlp5 [camlp5-ixut4] 6.16-1
ii ocaml-nox [ocaml-nox-4.02.3] 4.02.3-9
hol-light recommends no packages.
Versions of packages hol-light suggests:
pn coinor-csdp <none>
pn dmtcp <none>
ii ledit [readline-editor] 2.03-5
pn libocamlgraph-ocaml-dev <none>
pn maxima <none>
pn pari-gp <none>
pn prover9 <none>
-- no debconf information
