[build] do not install javalib with `opam pin`

Summary:
Installing with `opam pin` risks upgrading a lot of package in the current
switch, which is very slow. It's also wasted work since we'll install back
their older versions afterwards with `opam lock`. Moreover, that second step
can now fail if javalib needs to be recompiled (which it seems it does),
because we delete the javalib sources after having pinned them.

Solution: 1. do not install javalib at `opam pin` time, and 2. do not remove its source tree after pinning.

Reviewed By: martinoluca

Differential Revision: D5764153

fbshipit-source-id: 9c9b1c7
master
Jules Villard 7 years ago committed by Facebook Github Bot
parent b2edf17b21
commit 6ab174f0c3

1
.gitignore vendored

@ -18,6 +18,7 @@
/_build_logs /_build_logs
/infer/tests/codetoanalyze/java/*/codetoanalyze /infer/tests/codetoanalyze/java/*/codetoanalyze
/dependencies/infer-deps-* /dependencies/infer-deps-*
/dependencies/javalib/javalib-2.3.3/
_build_infer _build_infer
*.exp.test* *.exp.test*
*.test.dot *.test.dot

@ -176,9 +176,7 @@ install_patched_javalib() {
tar xvf "$javalib_dir"/javalib-2.3.3.tar.bz2 -C "$javalib_dir" tar xvf "$javalib_dir"/javalib-2.3.3.tar.bz2 -C "$javalib_dir"
# apply the patch # apply the patch
patch -d "$unzipped_javalib_dir"/src < "$javalib_dir"/allow_empty_method.patch patch -d "$unzipped_javalib_dir"/src < "$javalib_dir"/allow_empty_method.patch
opam pin add javalib "$unzipped_javalib_dir" opam pin add --no-action javalib "$unzipped_javalib_dir"
# clean up unzipped source
rm -rf "$unzipped_javalib_dir"
} }
install_locked_deps() { install_locked_deps() {

Loading…
Cancel
Save