diff --git a/.gitignore b/.gitignore index 6d9eaef4c..51177fc04 100644 --- a/.gitignore +++ b/.gitignore @@ -18,7 +18,7 @@ /_build_logs /infer/_build /infer/tests/codetoanalyze/java/*/codetoanalyze -/infer-deps-* +/dependencies/infer-deps-* _build_infer *.exp.test* *.test.dot diff --git a/build-infer.sh b/build-infer.sh index fe6c9404f..8a143fc49 100755 --- a/build-infer.sh +++ b/build-infer.sh @@ -12,7 +12,8 @@ set -e SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" -INFER_ROOT="$SCRIPT_DIR/../" +INFER_ROOT="$SCRIPT_DIR" +INFER_DEPS_DIR="$INFER_ROOT/dependencies/infer-deps" PLATFORM="$(uname)" NCPU="$(getconf _NPROCESSORS_ONLN 2>/dev/null || echo 1)" OCAML_VERSION="4.02.3" @@ -101,6 +102,8 @@ YES= if [ "$INTERACTIVE" = "no" ]; then YES=--yes fi +# --yes by default for opam commands +export OPAMYES=1 check_installed () { local cmd=$1 @@ -121,20 +124,27 @@ add_opam_git_pin () { PIN_HASH=$3 if [ "$(opam show -f pinned "$PACKAGE_NAME")" != "git ($PIN_HASH)" ]; then - opam pin add --yes --no-action "$PACKAGE_NAME" "$REPO_URL" + opam pin add --no-action "$PACKAGE_NAME" "$REPO_URL" fi } +# Install and record the infer dependencies in opam. The main trick is to install the +# $INFER_DEPS_DIR directory instead of the much larger infer repository. That directory contains +# just enough to pretend it installs infer. install_opam_deps () { - # trick to avoid rsync'inc the whole directory to opam since we are only interested in - # installing the dependencies - INFER_DEPS_DIR=$(mktemp -d infer-deps-XXXX) - cp opam "$INFER_DEPS_DIR" + # remove previous infer-deps pin, which might have conflicting dependencies + opam pin remove infer-deps --no-action + INFER_TMP_DEPS_DIR=$(mktemp -d "$INFER_ROOT"/dependencies/infer-deps-XXXX) + INFER_TMP_PACKAGE_NAME="$(basename "$INFER_TMP_DEPS_DIR")" + cp -a "$INFER_DEPS_DIR"/* "$INFER_TMP_DEPS_DIR" # give unique name to the package to force opam to recheck the dependencies are all installed - opam pin add --yes --no-action "$INFER_DEPS_DIR" "$INFER_DEPS_DIR" - opam install -j $NCPU --yes --deps-only "$INFER_DEPS_DIR" - opam pin remove "$INFER_DEPS_DIR" - rm -fr "$INFER_DEPS_DIR" + opam pin add --no-action "$INFER_TMP_PACKAGE_NAME" "$INFER_TMP_DEPS_DIR" + opam install -j $NCPU --deps-only "$INFER_TMP_PACKAGE_NAME" + opam pin remove "$INFER_TMP_PACKAGE_NAME" + rm -fr "$INFER_TMP_DEPS_DIR" + # pin infer so that opam doesn't violate its package constraints when the user does + # "opam upgrade" + opam pin add infer-deps "$INFER_DEPS_DIR" } echo "initializing opam... " diff --git a/dependencies/infer-deps/Makefile b/dependencies/infer-deps/Makefile new file mode 100644 index 000000000..a0c433dd4 --- /dev/null +++ b/dependencies/infer-deps/Makefile @@ -0,0 +1,12 @@ +# Copyright (c) 2017 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +# This file exists to make opam happy, it should not do anything useful besides that. + +.PHONY: install uninstall +install uninstall: + @: diff --git a/dependencies/infer-deps/autogen.sh b/dependencies/infer-deps/autogen.sh new file mode 100755 index 000000000..b82344e5b --- /dev/null +++ b/dependencies/infer-deps/autogen.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +# Copyright (c) 2017 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +# This file exists just to make opam happy, it should not do anything useful besides that. diff --git a/dependencies/infer-deps/configure b/dependencies/infer-deps/configure new file mode 100755 index 000000000..b82344e5b --- /dev/null +++ b/dependencies/infer-deps/configure @@ -0,0 +1,10 @@ +#!/bin/bash + +# Copyright (c) 2017 - present Facebook, Inc. +# All rights reserved. +# +# This source code is licensed under the BSD style license found in the +# LICENSE file in the root directory of this source tree. An additional grant +# of patent rights can be found in the PATENTS file in the same directory. + +# This file exists just to make opam happy, it should not do anything useful besides that. diff --git a/dependencies/infer-deps/opam b/dependencies/infer-deps/opam new file mode 120000 index 000000000..9d9c75a75 --- /dev/null +++ b/dependencies/infer-deps/opam @@ -0,0 +1 @@ +../../opam \ No newline at end of file