[PPL-devel] Ocaml docs being built even though interface is not enabled

[Michael Tautschnig]

Hi!

> Michael Tautschnig wrote:
> [...]
>> Sorry, there still is an issue here: make user-configured is indeed fine and
>> that stuff is handled nicely in the Makefile, but running make install (in the
>> top-level directory, actually) is troublesome. This causes builds of all the
>> other documents as well, disregarding all the configure stuff. Could you fix
>> that? It might be an option to make the install: target a no-op as well, just as
>> all: is!?
>>
>> Thanks,
>> Michael
>
> I am not sure I am understanding the issue.
> Does the problem shows up when you are acting as a "final user"
> or as a "packager" of the PPL ?
>
Well, isn't the difference mostly in the prefix where things get installed?

> I am asking because yesterday I tried installing the PPL as a final  
> user: I downloaded the latest snapshot, I configured it with all foreign  
> language interfaces _disabled_ (and after having _uninstalled_ ocamldoc,  
> just to be sure) and everything went fine. That is, the manuals that  
> need to be installed by `make install' are already built and distributed  
> in the PPL .tar.gz.
>
> Can you please provide us with the exact sequence of commands leading to  
> the problem?
>

Not exact, but sufficiently close I think:

make distclean
./configure
make
make -C doc user-configured
make install

From what you're telling I believe the problem to be in the make distclean step.
I guess it deletes any pre-built docs as well. Well, not a guess only, just
confirmed in my build here.

So, what should we conclude with? There's two options here IMHO:

- Have make distclean not delete any pre-built documentation. Consequently, make
  dist should then actually build the documents to ensure that make dist always
  ends up with the same tar ball.
- In our debian package, we could first move the pre-built docs to a safe
  location, and put them in place after make distclean.

What would you consider the preferred way?

Best,
Michael