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

Optimisation in bytecomp/simplif.ml leads to memory blowup in coq #4733

Closed
vicuna opened this issue Feb 27, 2009 · 2 comments
Closed

Optimisation in bytecomp/simplif.ml leads to memory blowup in coq #4733

vicuna opened this issue Feb 27, 2009 · 2 comments
Assignees
Labels

Comments

@vicuna
Copy link

vicuna commented Feb 27, 2009

Original bug ID: 4733
Reporter: bacam
Assigned to: @xavierleroy
Status: closed (set by @xavierleroy on 2012-09-25T18:10:24Z)
Resolution: unable to duplicate
Priority: normal
Severity: minor
Version: 3.11.0
Category: ~DO NOT USE (was: OCaml general)
Monitored by: @glondu

Bug description

Recently I discovered that a particularly demanding file in our coq development (due to the way in which we use coq's module system) compiled in under 1.5GB using the native code version build with -g, but exceeded the maximum 32bit process size (~3GB) using the native code version without -g.

I've tracked this down by trail and error to the optimisation of Llet(Alias, v, l1, l2) in bytecomp/simplif.ml when v only appears once. However I'm not sure exactly which part of the coq source triggers the problem, or if it can be easily solved. (Or if it's even reasonable to blame it on ocamlopt!)

@vicuna
Copy link
Author

vicuna commented Dec 17, 2011

Comment author: @xavierleroy

Another PR that has been dormant for too long, sorry about that.

bytecomp/simplif.ml was significantly revised this summer to fix issues that may or may not be related (see #5205, #5288). So my questions are:

  • Is this still a problem? especially with the svn trunk version of OCaml?
  • If so, could we get a repro case?

@vicuna
Copy link
Author

vicuna commented Jan 27, 2012

Comment author: @xavierleroy

Unable to reproduce. I move to close this PR unless new information is added.

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

2 participants