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

[build] Ensure make world builds all targets present in make install #14233

Merged
merged 1 commit into from May 4, 2021

Conversation

ejgallego
Copy link
Member

It is important to ensure a phase separation of make world and make install as this last one may be called using sudo in some contexts
and thus create build objects under the root user, which leads to
disaster usually.

In order to fix that quickly, we just extend the world target to be
comprehensive.

Note that dune upstream enforced this by forbidding dune install to
build anything, but there is a bit more convenient as the
foo.install file depends on all the objects to installed already by
construction.

We should follow a similar path in our make wrappers, but that would
require a bit of rewrite / design, with given the status of the code
may not be a bad idea as it has gotten to a point where cleanup would
be nice.

Fixes #14228 , keeping #14232 open as to try to improve install
locations a little bit for 8.14, tho the issue is subtle.

@ejgallego ejgallego requested a review from a team May 1, 2021 23:54
@ejgallego
Copy link
Member Author

cc @JasonGross this gives you the workaround to the problem, just add temporarily the 2 / missing .install targets and make install won't do rebuild anymore

@Zimmi48
Copy link
Member

Zimmi48 commented May 2, 2021

@gares The async build failed with a segfault. There might be info to extract.

Makefile.install Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 added kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. part: build The build system. labels May 3, 2021
@Zimmi48 Zimmi48 added this to the 8.14+rc1 milestone May 3, 2021
It is important to ensure a phase separation of `make world` and `make
install` as this last one may be called using `sudo` in some contexts
and thus create build objects under the root user, which leads to
disaster usually.

In order to fix that quickly, we just extend the `world` target to be
comprehensive.

Note that dune upstream enforced this by forbidding `dune install` to
build anything, but there is a bit more convenient as the
`foo.install` file depends on all the objects to installed already by
construction.

We should follow a similar path in our make wrappers, but that would
require a bit of rewrite / design, with given the status of the code
may not be a bad idea as it has gotten to a point where cleanup would
be nice.

Fixes coq#14228 , keeping coq#14232 open as to try to improve install
locations a little bit for 8.14, tho the issue is subtle.
@Zimmi48 Zimmi48 self-assigned this May 4, 2021
@Zimmi48
Copy link
Member

Zimmi48 commented May 4, 2021

I'll merge this PR later today.

@Zimmi48
Copy link
Member

Zimmi48 commented May 4, 2021

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 4421d93 into coq:master May 4, 2021
@ejgallego ejgallego deleted the build+install_tweaks branch May 4, 2021 17:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. part: build The build system.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

global make install is broken both with and without sudo on MacOS, and should be tested on Coq's CI
2 participants