Makefiles reference incorrect Make installation on Mac

[rahelFain]

When trying to build the everest package from the source I ran into an issue stemming from everest referencing the wrong version of make in my directory.

I say this because I encountered the following message:

Makefile:52: *** You seem to be using the OSX antiquated Make version. Hint: brew install make, then invoke gmake instead of make. Stop.

after running brew install make (and brew link make - to be safe) and updating my shell to ensure I had the new version of make (gmake) as my default:

$ make -v
GNU Make 4.2.1
Built for x86_64-apple-darwin17.7.0
Copyright (C) 1988-2016 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.



$ which make

/usr/bin/make

Upon looking more closely at the output from ./everest make I noticed that everest was overwriting my bash settings to reference the version installed by Xcode as shown in the line below:
/Library/Developer/CommandLineTools/usr/bin/make FSTAR_HOME=.. -f Makefile.verify verify-core

This is problematic because Apple refuses to install a newer version of Make on its machines and tools such as Homebrew store their installations in /usr/local/bin.

I've included the full output from running make as a reference.

$ ./everest make
# Switching to the everest directory ... now in /Users/rf/everest

exported FSTAR_HOME=/Users/rf/everest/FStar
exported OPENSSL_HOME=/Users/rf/everest/MLCrypto/openssl
exported KREMLIN_HOME=/Users/rf/everest/kremlin
exported VALE_HOME=/Users/rf/everest/vale
exported HACL_HOME=/Users/rf/everest/hacl-star
exported MLCRYPTO_HOME=/Users/rf/everest/MLCrypto
exported DYLD_LIBRARY_PATH=/Users/rf/everest/MLCrypto/openssl:
exported PATH=/Users/rf/FStar/bin:/Users/rf/everest/kremlin:/Users/rf/.opam/4.07.1/bin:/usr/local/opt/coreutils/libexec/gnubin:/Users/rf/everest/z3/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin
================================================================================
Rebuilding FStar
Running: build_fstar
echo 'open FStar_Util' > FStar_Version.ml
echo 'let dummy () = ();;' >> FStar_Version.ml
echo 'FStar_Options._version := "0.9.7.0-alpha1";;' >> FStar_Version.ml
echo 'FStar_Options._platform := "Darwin_x86_64";;' >> FStar_Version.ml
echo 'FStar_Options._compiler := "OCaml 4.07.1";;' >> FStar_Version.ml
# We deliberately use commitdate instead of date, so that rebuilds are no-ops
echo 'FStar_Options._date := "2019-11-20 10:43:51 -0300 ";;' >> FStar_Version.ml
echo 'FStar_Options._commit:= "5058d6ee7e88702618f269d1e1d2331082d52ae9";;' >> FStar_Version.ml
cd ../../ && ocamlbuild -cflag -g -I src/ocaml-output -I src/basic/ml -I src/parser/ml -I src/fstar/ml -I src/extraction/ml -I src/prettyprint/ml -I src/tactics/ml -I src/tests/ml -I ulib/ml -j 24 -build-dir src/ocaml-output/_build -use-ocamlfind main.native src/ocaml-output/FStar_Syntax_Syntax.inferred.mli
Finished, 362 targets (362 cached) in 00:00:02.
/Library/Developer/CommandLineTools/usr/bin/make FSTAR_HOME=.. -f Makefile.verify verify-core
make[1]: Nothing to be done for `verify-core'.
/Library/Developer/CommandLineTools/usr/bin/make -C .. install-fstarlib
cd ../ && OCAMLPATH="../../../bin/:" ocamlbuild -cflag -g -use-ocamlfind -build-dir ulib/ml/_build -I ulib/ml -I ulib/ml/extracted fstarlib.a fstarlib.cma fstarlib.cmxs fstarlib.cmxa
Finished, 387 targets (386 cached) in 00:00:01.
mkdir -p ../bin/fstarlib/
cp ml/_build/ulib/ml/*.cmi ml/_build/ulib/ml/*.cmx ml/_build/ulib/ml/extracted/*.cmi ml/_build/ulib/ml/extracted/*.cmx ml/_build/ulib/ml/fstarlib.a ml/_build/ulib/ml/fstarlib.cma ml/_build/ulib/ml/fstarlib.cmxs ml/_build/ulib/ml/fstarlib.cmxa ../bin/fstarlib/
sed "s/__FSTAR_VERSION__/$(cat ../version.txt)/" <ml/fstarlib-META >../bin/fstarlib//META
/Library/Developer/CommandLineTools/usr/bin/make -C .. install-fstar-tactics
cd ../ && OCAMLPATH="../../../bin/:" ocamlbuild -cflag -g -use-ocamlfind -build-dir ulib/tactics_ml/_build -I ulib/tactics_ml/ -I ulib/tactics_ml/extracted -I ulib/tactics_ml/fstarlib_leftovers fstartaclib.cma fstartaclib.cmxs fstartaclib.cmxa
Finished, 393 targets (392 cached) in 00:00:01.
mkdir -p ../bin/fstar-tactics-lib/
cp tactics_ml/_build/ulib/tactics_ml/*.cmi tactics_ml/_build/ulib/tactics_ml/*.cmx tactics_ml/_build/ulib/tactics_ml/fstarlib_leftovers/*.cmi tactics_ml/_build/ulib/tactics_ml/fstarlib_leftovers/*.cmx tactics_ml/_build/ulib/tactics_ml/extracted/*.cmi tactics_ml/_build/ulib/tactics_ml/extracted/*.cmx tactics_ml/_build/ulib/tactics_ml/fstartaclib.cma tactics_ml/_build/ulib/tactics_ml/fstartaclib.cmxs tactics_ml/_build/ulib/tactics_ml/fstartaclib.cmxa ../bin/fstar-tactics-lib/
================================================================================
Rebuilding kremlin
Running: build_kremlin
ocamlbuild -I src -I lib -I parser -I kremlib -use-menhir -use-ocamlfind -classic-display -menhir "menhir --infer --explain" Kremlin.native Tests.native
ln -sf Kremlin.native krml
/Library/Developer/CommandLineTools/usr/bin/make -C kremlib
/Library/Developer/CommandLineTools/usr/bin/make -C dist/generic -f Makefile.basic
make[2]: Nothing to be done for `all'.
/Library/Developer/CommandLineTools/usr/bin/make -C dist/uint128 -f Makefile.basic
make[2]: Nothing to be done for `all'.
/Library/Developer/CommandLineTools/usr/bin/make -C dist/minimal -f Makefile.basic
make[2]: Nothing to be done for `all'.
OCAMLPATH=":/Users/rf/everest/FStar/bin" ocamlbuild -I src -I lib -I parser -I kremlib -use-menhir -use-ocamlfind -classic-display -menhir "menhir --infer --explain" Ast.inferred.mli kremlib/C.cmx kremlib/TestLib.cmx kremlib/C.cmo kremlib/TestLib.cmo
/Library/Developer/CommandLineTools/usr/bin/make -C dist/generic -f Makefile.basic
make[1]: Nothing to be done for `all'.
/Library/Developer/CommandLineTools/usr/bin/make -C dist/uint128 -f Makefile.basic
make[1]: Nothing to be done for `all'.
/Library/Developer/CommandLineTools/usr/bin/make -C dist/minimal -f Makefile.basic
make[1]: Nothing to be done for `all'.
================================================================================



================================================================================
Rebuilding MLCrypto
Running: make -C MLCrypto
make: Nothing to be done for `all'.
================================================================================



================================================================================
Rebuilding hacl-star
Running: build_hacl
Makefile:52: *** You seem to be using the OSX antiquated Make version. Hint: brew install make, then invoke gmake instead of make.  Stop.
================================================================================
FAILURE: build failed for hacl-star

[s-zanella]

The everest script just prepends $(pwd)/FStar/bin:$(pwd)/kremlin to $PATH before calling make to build FStar.

A Makefile in FStar then calls make recursively using the MAKE variable (https://www.gnu.org/software/make/manual/html_node/MAKE-Variable.html#MAKE-Variable), which should match the original make that the script picked up. In your case, this appears to be /Library/Developer/CommandLineTools/usr/bin/make rather than /usr/bin/make.

What do you get when you run

PATH=/Users/rf/FStar/bin:/Users/rf/everest/kremlin:/Users/rf/.opam/4.07.1/bin:/usr/local/opt/coreutils/libexec/gnubin:/Users/rf/everest/z3/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin which make

You should get /usr/bin/make.

I don't think it would be an issue, but have you defined $MAKE in bash? E.g. what do you get when you run echo $MAKE?

[rahelFain]

I had tried aliasing via
alias make=/usr/local/bin/gmake
but had not had any success on that front.
After trying to set $MAKE in my .bash_profile, I saw the path change in the output. (So it was now referencing the correct make version via
export MAKE='/usr/local/bin/gmake'
).

My hunch as to why - Apple locks down the /usr/bin directory as part of its security settings. Even using sudo wouldn't work - I'd basically have to break the protection mechanisms in place to do this (which I am not willing to do).
So running /usr/bin/make -v returns:

GNU Make 3.81
Copyright (C) 2006  Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.

but running /usr/local/bin/gmake -v returns the newer installation.

/usr/local/bin/gmake -v
GNU Make 4.2.1
Built for x86_64-apple-darwin17.7.0
Copyright (C) 1988-2016 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.

That said, I am still getting the error on line 52 of hacl-star/Makefile noting that my make version is incorrect and don't know why.

[rahelFain]

After checking https://www.gnu.org/software/make/manual/make.html
it seems like $(MAKE_VERSION) was the culprit of the run failing.

"The built-in variable ‘MAKE_VERSION’ expands to the version number of the GNU make program"
I've set MAKE_VERSION to gmake's version.
This seems like a hack, but it works.

[rahelFain]

I am now running into an issue building the hacl-star portion when trying to run make.
Since I am still getting familiar with the project's components I cannot tell whether it is at all related to what I encountered earlier.

Is this related?
Alternately, is there any documentation I could reference to better understand the error messages?
I've included a trace below.

================================================================================
Rebuilding kremlin
Running: build_kremlin
ocamlbuild -I src -I lib -I parser -I kremlib -use-menhir -use-ocamlfind -classic-display -menhir "menhir --infer --explain" Kremlin.native Tests.native
ln -sf Kremlin.native krml
/usr/local/bin/gmake -C kremlib
gmake[1]: Entering directory '/Users/rf/everest/kremlin/kremlib'
/usr/local/bin/gmake -C dist/generic -f Makefile.basic
gmake[2]: Entering directory '/Users/rf/everest/kremlin/kremlib/dist/generic'
gmake[2]: Nothing to be done for 'all'.
gmake[2]: Leaving directory '/Users/rf/everest/kremlin/kremlib/dist/generic'
/usr/local/bin/gmake -C dist/uint128 -f Makefile.basic
gmake[2]: Entering directory '/Users/rf/everest/kremlin/kremlib/dist/uint128'
gmake[2]: Nothing to be done for 'all'.
gmake[2]: Leaving directory '/Users/rf/everest/kremlin/kremlib/dist/uint128'
/usr/local/bin/gmake -C dist/minimal -f Makefile.basic
gmake[2]: Entering directory '/Users/rf/everest/kremlin/kremlib/dist/minimal'
gmake[2]: Nothing to be done for 'all'.
gmake[2]: Leaving directory '/Users/rf/everest/kremlin/kremlib/dist/minimal'
gmake[1]: Leaving directory '/Users/rf/everest/kremlin/kremlib'
OCAMLPATH=":/Users/rf/everest/FStar/bin" ocamlbuild -I src -I lib -I parser -I kremlib -use-menhir -use-ocamlfind -classic-display -menhir "menhir --infer --explain" Ast.inferred.mli kremlib/C.cmx kremlib/TestLib.cmx kremlib/C.cmo kremlib/TestLib.cmo
/usr/local/bin/gmake -C dist/generic -f Makefile.basic
gmake[1]: Entering directory '/Users/rf/everest/kremlin/kremlib/dist/generic'
gmake[1]: Nothing to be done for 'all'.
gmake[1]: Leaving directory '/Users/rf/everest/kremlin/kremlib/dist/generic'
/usr/local/bin/gmake -C dist/uint128 -f Makefile.basic
gmake[1]: Entering directory '/Users/rf/everest/kremlin/kremlib/dist/uint128'
gmake[1]: Nothing to be done for 'all'.
gmake[1]: Leaving directory '/Users/rf/everest/kremlin/kremlib/dist/uint128'
/usr/local/bin/gmake -C dist/minimal -f Makefile.basic
gmake[1]: Entering directory '/Users/rf/everest/kremlin/kremlib/dist/minimal'
gmake[1]: Nothing to be done for 'all'.
gmake[1]: Leaving directory '/Users/rf/everest/kremlin/kremlib/dist/minimal'
================================================================================



================================================================================
Rebuilding MLCrypto
Running: make -C MLCrypto
make: Nothing to be done for `all'.
================================================================================



================================================================================
Rebuilding hacl-star
Running: build_hacl
tools/blast-staticconfig.sh default
/usr/local/bin/gmake all-staged
gmake[1]: Entering directory '/Users/rf/everest/hacl-star'
[STAGE1] Vale to F*
/usr/local/bin/gmake vale-fst
gmake[2]: Entering directory '/Users/rf/everest/hacl-star'
[FSTAR-DEPEND (make)], 0:16.31
[VALE-DEPEND], 0:04.50
[FSTAR-DEPEND (full)], 0:19.81
gmake[2]: Nothing to be done for 'vale-fst'.
gmake[2]: Leaving directory '/Users/rf/everest/hacl-star'
[STAGE2] Main target: all
FSTAR_DEPEND_FLAGS="--warn_error +285" /usr/local/bin/gmake all-unstaged
gmake[2]: Entering directory '/Users/rf/everest/hacl-star'
[FSTAR-DEPEND (make)], 0:14.85
[VALE-DEPEND], 0:04.33
[FSTAR-DEPEND (full)], 0:19.99
/Users/rf/everest/hacl-star/code/poly1305/Hacl.Poly1305.Field32xN.Lemmas.fst(1281,2-1281,8): (Error 19) assertion failed; Try with --query_stats to get more details (see also /Users/rf/everest/hacl-star/code/poly1305/Hacl.Poly1305.Field32xN.Lemmas.fst(1281,9-1281,57))
Verified module: Hacl.Poly1305.Field32xN.Lemmas
1 error was reported (see above)
<><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
Fatal error while running:  /Users/rf/everest/FStar/bin/fstar.exe --use_hints --use_hint_hashes --record_hints --odir obj --cache_checked_modules --include /Users/rf/everest/hacl-star/lib --include /Users/rf/everest/hacl-star/specs --include /Users/rf/everest/hacl-star/specs/lemmas --include /Users/rf/everest/hacl-star/specs/tests --include /Users/rf/everest/hacl-star/specs/drbg --include /Users/rf/everest/hacl-star/specs/frodo --include /Users/rf/everest/hacl-star/specs/frodo/params-64-cSHAKE --include /Users/rf/everest/hacl-star/code/hash --include /Users/rf/everest/hacl-star/code/hmac --include /Users/rf/everest/hacl-star/code/hkdf --include /Users/rf/everest/hacl-star/code/drbg --include /Users/rf/everest/hacl-star/code/sha3 --include /Users/rf/everest/hacl-star/code/poly1305 --include /Users/rf/everest/hacl-star/code/chacha20 --include /Users/rf/everest/hacl-star/code/chacha20poly1305 --include /Users/rf/everest/hacl-star/code/curve25519 --include /Users/rf/everest/hacl-star/code/tests --include /Users/rf/everest/hacl-star/code/ed25519 --include /Users/rf/everest/hacl-star/code/salsa20 --include /Users/rf/everest/hacl-star/code/nacl-box --include /Users/rf/everest/hacl-star/code/meta --include /Users/rf/everest/hacl-star/code/frodo --include /Users/rf/everest/hacl-star/code/frodo/params-64-cSHAKE --include /Users/rf/everest/hacl-star/vale/code/arch --include /Users/rf/everest/hacl-star/vale/code/arch/x64 --include /Users/rf/everest/hacl-star/vale/code/arch/x64/interop --include /Users/rf/everest/hacl-star/vale/code/crypto/aes --include /Users/rf/everest/hacl-star/vale/code/crypto/aes/x64 --include /Users/rf/everest/hacl-star/vale/code/crypto/bignum --include /Users/rf/everest/hacl-star/vale/code/crypto/ecc/curve25519 --include /Users/rf/everest/hacl-star/vale/code/crypto/poly1305 --include /Users/rf/everest/hacl-star/vale/code/crypto/poly1305/x64 --include /Users/rf/everest/hacl-star/vale/code/crypto/sha --include /Users/rf/everest/hacl-star/vale/code/lib/collections --include /Users/rf/everest/hacl-star/vale/code/lib/math --include /Users/rf/everest/hacl-star/vale/code/lib/util --include /Users/rf/everest/hacl-star/vale/code/lib/util/x64 --include /Users/rf/everest/hacl-star/vale/code/lib/util/x64/stdcalls --include /Users/rf/everest/hacl-star/vale/code/lib/transformers --include /Users/rf/everest/hacl-star/vale/code/test --include /Users/rf/everest/hacl-star/vale/code/thirdPartyPorts/Intel/aes/x64 --include /Users/rf/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/aes --include /Users/rf/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/poly1305/x64 --include /Users/rf/everest/hacl-star/vale/code/thirdPartyPorts/OpenSSL/sha --include /Users/rf/everest/hacl-star/vale/code/thirdPartyPorts/rfc7748/curve25519/x64 --include /Users/rf/everest/hacl-star/vale/code/thirdPartyPorts/SymCrypt/bignum --include /Users/rf/everest/hacl-star/vale/specs/crypto --include /Users/rf/everest/hacl-star/vale/specs/defs --include /Users/rf/everest/hacl-star/vale/specs/hardware --include /Users/rf/everest/hacl-star/vale/specs/interop --include /Users/rf/everest/hacl-star/vale/specs/math --include /Users/rf/everest/hacl-star/providers/evercrypt --include /Users/rf/everest/hacl-star/providers/evercrypt/fst --include /Users/rf/everest/hacl-star/providers/test --include /Users/rf/everest/hacl-star/providers/test/vectors --include /Users/rf/everest/hacl-star/providers/evercrypt/config/default --include /Users/rf/everest/hacl-star/secure_api/merkle_tree --include /Users/rf/everest/kremlin/runtime --include /Users/rf/everest/hacl-star/obj --include /Users/rf/everest/FStar/ulib/.cache --include /Users/rf/everest/kremlin/kremlib --cmi --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247-272' --cache_dir obj --trivial_pre_for_unannotated_effectful_fns false  /Users/rf/everest/hacl-star/code/poly1305/Hacl.Poly1305.Field32xN.Lemmas.fst  --hint_file hints/Hacl.Poly1305.Field32xN.Lemmas.fst.hints && touch -c obj/Hacl.Poly1305.Field32xN.Lemmas.fst.checked
Failed after: 1:46.36
Full log is in obj/Hacl.Poly1305.Field32xN.Lemmas.fst.checked.{out,err}, see excerpt below:
/Users/rf/everest/hacl-star/code/poly1305/Hacl.Poly1305.Field32xN.Lemmas.fst(1281,2-1281,8): (Error 19) assertion failed; Try with --query_stats to get more details (see also /Users/rf/everest/hacl-star/code/poly1305/Hacl.Poly1305.Field32xN.Lemmas.fst(1281,9-1281,57))
Verified module: Hacl.Poly1305.Field32xN.Lemmas
1 error was reported (see above)
<><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
gmake[2]: *** [Makefile:405: obj/Hacl.Poly1305.Field32xN.Lemmas.fst.checked] Error 1
gmake[2]: Leaving directory '/Users/rf/everest/hacl-star'
gmake[1]: *** [Makefile:114: all-staged] Error 2
gmake[1]: Leaving directory '/Users/rf/everest/hacl-star'
make: *** [all] Error 2
================================================================================
FAILURE: build failed for hacl-star

[msprotz]

Unfortunately, on OSX, hacl-star is known to unreliably build owing to OSX-specific Z3 behavior. We do not have OSX CI at the current time which makes these problems very hard to diagnose. If you are positive you have the right setup, including the right version of Z3, and the very latest version of everything (./everest pull) then the only option I would suggest is:

cd hacl-star
OTHERFLAGS="--admit_smt_queries true" gmake -j N

which will admit Z3 proof obligations for the sake of getting a successful build.

[rahelFain]

OK -
@msprotz Are the issues with hacl-star on OSX isolated to the initial build, or would I need to be prepared for persistent issues after building?

[beurdouche]

Unfortunately, on OSX, hacl-star is known to unreliably build owing to OSX-specific Z3 behavior. We do not have OSX CI at the current time which makes these problems very hard to diagnose. If you are positive you have the right setup, including the right version of Z3, and the very latest version of everything (./everest pull) then the only option I would suggest is:

cd hacl-star
OTHERFLAGS="--admit_smt_queries true" gmake -j N

which will admit Z3 proof obligations for the sake of getting a successful build.

We really need an "--admit_smt_queries_for_modules +A -B" syntax...

[rahelFain]

One last question - Is the OSX-specific behavior at all an issue with the Linux version?
Based on @beurdouche 's response, it sounds like I may need to consider using docker.

(I also assume I wouldn't be able to pull a docker image of the Windows distribution based on what I saw here.)

[s-zanella]

We have not observed inconsistent Z3 behavior between Linux and Windows as we did for Mac OS X.
This issue would need to be fixed upstream in Z3. In the meantime, if you are willing to admit the few proofs that fail during the initial build, it is unlikely this issue would block you when developing your own proofs.

Using a Docker Linux image would be a way of working around this issue on Mac OS X. We upload images built during CI to https://hub.docker.com/u/projecteverest (builds that failed have a -failed suffix).

You can only host Windows Docker containers on Windows, and the host and container Windows versions have to match.