|Anonymous | Login | Signup for a new account||2014-03-08 02:48 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0004934||OCaml||OCamlbuild (the tool)||public||2009-12-08 17:01||2014-01-21 14:01|
|Target Version||4.01.1+dev||Fixed in Version|
|Summary||0004934: ocamlbuild takes up to one minute to scan already done parts of Coq sources|
I'm investigating the use of ocamlbuild for building Coq. I'd be glad to completely get rid of nasty Makefile stuff, but currently, two major issues prevent a complete switch to ocamlbuild. One is the lack of proper parallel compilation (see a forthcoming bug report). Another is that the delay needed by ocamlbuild to scan already built parts (> 1min here) prohibits using it
for interactive development (edit a file, recompile, and so on). I've already had private discussions on this topic, without clear solutions, so I turn this into a proper bug report, for the records.
Disclaimer: I clearly do not claim my myocamlbuild.ml file to be perfect, so
this inefficiency can be caused by the way it is written. Any hints are welcome...
Instructions to reproduce:
0) you'll need camlp5 installed
1) get a copy of coq development archive
svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk/ [^]
2) ./configure -local -opt
3) Launch a first build via ocamlbuild (./build is a small wrapper)
4) Launch ./build again
Here, the first build says:
Finished, 2716 targets (0 cached) in 00:13:10.
While the second says:
Finished, 2716 targets (2716 cached) in 00:01:07.
With old-style make, the second run of make says instantly that nothing is to be done.
NB: I've tried the patch for bug 0004922, unfortunately it doesn't help.
We're not recompiling too many files here, simply taking too much time
scanning cached things.
|Attached Files|| 0001-cache-expand_module.patch [^] (1,010 bytes) 2011-05-17 16:41 [Show Content]
0002-disable-logging-in-Solver.self.patch [^] (2,413 bytes) 2011-05-17 16:42 [Show Content]
0003-specialize-List.union.patch [^] (3,220 bytes) 2011-05-17 16:42 [Show Content]
0004-specialize-hashtbl-for-Resource.Cache.patch [^] (861 bytes) 2011-05-17 16:42 [Show Content]
Here are some observations.
Ocaml_utils.expand_module is pure and called too often (and generates lots of garbage) with same arguments - simple memoisation reduces the number of invocations by the factor of 100 (for coq sources) and cuts running time by 30 sec (out of 2 minutes).
Solver.self calls dprintf which doesn't print anything at default logging level, but still incurs too much overhead, commenting it out cuts another 40 seconds. (One day I hope to have type-safe camlp4 printf which doesn't parse format string at runtime..)
Another offender is generic compare_val called from various places - specializing My_std.List.union and Hashtbl in Resource.Cache casts away 8 more seconds.
Contrary to my expectation using Set(String) instead of list to detect circular deps in Solver.self didn't give speedup..
All in all - 42 seconds vs 2+ minutes. Quick'n'dirty patches attached.
BTW better names for anonymous functions and better debug-symbol info would be greatly appreciated for debugging such issues
|Why not apply at least the first patch?|
|Ygrek, your patch is being considered for an inclusion - at least the first one, however it looks we have general scalability problems with ocamlbuild, and until we will know what we can do to improve it in general case, I will postpone applying it. I don't believe scanning the tree should take that long. What we can also do is to spawn several processes scanning the tree - but this will be the last thing we we will do, however.|
|As for the logging - we could functorize the implementation, and replace the logging functions with a dummy ones if the user requested logging. I'll look into that.|
|I raised PR#5756 for this chunk of work.|
|Ygrek, for your patch 0000004: I think what we want to do is to get rid of lists all together, and replace them with something better (e.g: Set). Nevertheless it highlights some obvious optimisations we could do.|
I agree that there are speed problems at different levels, and not doing unnecessary work is the best optimisation anyway :)
I doubt it is possible to fix logging with functorizing.. Maybe better wrap it oldschool way with : `if loglevel X then ...`
|2009-12-08 17:01||letouzey||New Issue|
|2011-05-02 12:38||doligez||Status||new => acknowledged|
|2011-05-17 16:41||ygrek||File Added: 0001-cache-expand_module.patch|
|2011-05-17 16:42||ygrek||File Added: 0002-disable-logging-in-Solver.self.patch|
|2011-05-17 16:42||ygrek||File Added: 0003-specialize-List.union.patch|
|2011-05-17 16:42||ygrek||File Added: 0004-specialize-hashtbl-for-Resource.Cache.patch|
|2011-05-17 16:43||ygrek||Note Added: 0005902|
|2011-06-06 13:02||xclerc||Status||acknowledged => assigned|
|2011-06-06 13:02||xclerc||Assigned To||=> xclerc|
|2012-02-02 15:17||protz||Category||OCamlbuild => OCamlbuild (the tool)|
|2012-05-22 11:26||ygrek||Note Added: 0007447|
|2012-07-06 16:33||doligez||Target Version||=> 4.01.0+dev|
|2012-07-06 16:33||doligez||Description Updated||View Revisions|
|2012-07-31 13:36||doligez||Target Version||4.01.0+dev => 4.00.1+dev|
|2012-09-03 02:08||meyer||Relationship added||related to 0005754|
|2012-09-04 01:53||meyer||Note Added: 0008012|
|2012-09-04 02:04||meyer||Note Added: 0008013|
|2012-09-04 02:11||meyer||Relationship added||related to 0005756|
|2012-09-04 02:12||meyer||Note Added: 0008014|
|2012-09-04 02:17||meyer||Note Added: 0008015|
|2012-09-04 10:33||ygrek||Note Added: 0008017|
|2012-09-06 19:20||frisch||Target Version||4.00.1+dev => 4.00.2+dev|
|2013-01-20 01:01||meyer||Assigned To||xclerc => meyer|
|2013-06-16 18:33||gasche||Target Version||4.00.2+dev => 4.02.0+dev|
|2013-06-16 21:25||gasche||Severity||major => minor|
|2013-07-12 18:15||doligez||Target Version||4.02.0+dev => 4.01.1+dev|
|2013-09-04 21:06||doligez||Tag Attached: patch|
|2014-01-21 14:01||doligez||Assigned To||meyer =>|
|Copyright © 2000 - 2011 MantisBT Group|