Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Huge memory allocation on amd64 #2518

Closed
vicuna opened this issue Apr 27, 2004 · 1 comment
Closed

Huge memory allocation on amd64 #2518

vicuna opened this issue Apr 27, 2004 · 1 comment
Labels

Comments

@vicuna
Copy link

vicuna commented Apr 27, 2004

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).

@vicuna
Copy link
Author

vicuna commented May 18, 2004

Comment author: administrator

Bad GC call in amd64.S:caml_alloc{1,2,3,N}. Fixed 2004-05-18 by XL.

@vicuna vicuna closed this as completed May 18, 2004
@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant