You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 2518 Reporter: administrator Status: closed Resolution: fixed Priority: normal Severity: minor Category: ~DO NOT USE (was: OCaml general)
When I compile Coq 8.0 to object code (with ocamlopt) with OCaml 3.07+2 on an
amd64 machine (in 64bit mode), the resulting "coqtop.opt" fails to run at all:
It tries to allocate more than 128PiB of memory, which obviously fails:
lionelm@harif:/usr/src/coq/coq-8.0$ strace -f bin/coqtop.opt -boot -nois
-compile theories/Init/Notations
(...)
mmap(NULL, 144115188075860000, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS,
-1, 0) = -1 EINVAL (Invalid argument)
write(2, "Fatal error: out of memory.\n", 28Fatal error: out of memory.
) = 28
Other programs, like Coq 8.0beta, ocamlc.opt, ocamlopt.opt, small "hello world"
programs, ... run fine.
wget ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
tar xfz coq-8.0.tar.gz
cd coq-8.0
./configure -opt -local
make world
fails with out-of-memory
./bin/boqtop.opt -help
fails with out-of-memory
The diff between coq8.0 and coq8.0beta (to see what makes 8.0 fail, but not
8.0beta) can be generated from the tarballs or from CVS: Diff tags V8-0beta and
V8-0 on :pserver:anoncvs@coqcvs.inria.fr:/coq, module V7 (empty password).
The text was updated successfully, but these errors were encountered:
Original bug ID: 2518
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)
Bug description
Full_Name: Lionel Elie Mamane
Version: 3.07+2
OS: Debian GNU/Linux sid
Submission from: harif.cs.kun.nl (131.174.33.81)
When I compile Coq 8.0 to object code (with ocamlopt) with OCaml 3.07+2 on an
amd64 machine (in 64bit mode), the resulting "coqtop.opt" fails to run at all:
It tries to allocate more than 128PiB of memory, which obviously fails:
lionelm@harif:/usr/src/coq/coq-8.0$ strace -f bin/coqtop.opt -boot -nois
-compile theories/Init/Notations
(...)
mmap(NULL, 144115188075860000, PROT_READ|PROT_WRITE, MAP_PRIVATE|MAP_ANONYMOUS,
-1, 0) = -1 EINVAL (Invalid argument)
write(2, "Fatal error: out of memory.\n", 28Fatal error: out of memory.
) = 28
Other programs, like Coq 8.0beta, ocamlc.opt, ocamlopt.opt, small "hello world"
programs, ... run fine.
Coq8.0 works fine on 32bit machines.
The Coq devel team thinks it is an OCaml bug (which looks plausible), see
http://coq.inria.fr/bin/coq-bugs/open?id=661 .
Exact steps to reproduce:
wget ftp://ftp.inria.fr/INRIA/coq/V8.0/coq-8.0.tar.gz
tar xfz coq-8.0.tar.gz
cd coq-8.0
./configure -opt -local
make world
fails with out-of-memory
./bin/boqtop.opt -help
fails with out-of-memory
The diff between coq8.0 and coq8.0beta (to see what makes 8.0 fail, but not
8.0beta) can be generated from the tarballs or from CVS: Diff tags V8-0beta and
V8-0 on :pserver:anoncvs@coqcvs.inria.fr:/coq, module V7 (empty password).
The text was updated successfully, but these errors were encountered: