Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0004733OCamlOCaml generalpublic2009-02-27 11:412012-09-25 20:10
Reporterbacam 
Assigned Toxleroy 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionunable to reproduce 
PlatformOSOS Version
Product Version3.11.0 
Target VersionFixed in Version 
Summary0004733: Optimisation in bytecomp/simplif.ml leads to memory blowup in coq
DescriptionRecently 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!)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006352)
xleroy (administrator)
2011-12-17 11:01

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 PR#5205, PR#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?

(0006824)
xleroy (administrator)
2012-01-27 12:22

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

- Issue History
Date Modified Username Field Change
2009-02-27 11:41 bacam New Issue
2009-04-29 15:37 doligez Status new => assigned
2009-04-29 15:37 doligez Assigned To => xleroy
2011-12-17 11:01 xleroy Note Added: 0006352
2011-12-17 11:01 xleroy Status assigned => feedback
2012-01-27 12:22 xleroy Note Added: 0006824
2012-01-27 12:22 xleroy Status feedback => resolved
2012-01-27 12:22 xleroy Resolution open => unable to reproduce
2012-09-25 20:10 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker