Skip to content

ocamlbuild takes up to one minute to scan already done parts of Coq sources #4934

@vicuna

Description

@vicuna

Original bug ID: 4934
Reporter: letouzey
Status: closed (set by @gasche on 2016-02-16T00:23:34Z)
Resolution: suspended
Priority: normal
Severity: minor
Version: 3.11.1
Target version: later
Category: -for ocamlbuild use https://github.com/ocaml/ocamlbuild/issues
Tags: patch
Related to: #5754 #5756
Monitored by: @gasche mehdi @ygrek @glondu "Julien Signoles"

Bug description

Hi!

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

Best regards,
Pierre Letouzey

Instructions to reproduce:

  1. you'll need camlp5 installed
  2. get a copy of coq development archive
    svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk/
  3. ./configure -local -opt
  4. Launch a first build via ocamlbuild (./build is a small wrapper)
    ./build
  5. 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 #4922, unfortunately it doesn't help.
We're not recompiling too many files here, simply taking too much time
scanning cached things.

File attachments

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions