Makefile refactors for global install and new sysroot (#801)

* Makefile: make explicit variable LOCAL_LIB * Makefile: remove unused variables INSTALL_PREFIX and INSTALL_DIR * Makefile: set K_RELEASE based on where K is * Makefile: remove git submodule updates * Makefile: remove redundant K_RELEASE setting * Makefile: remove split-tests target * Jenkinsfile: remove split-tests stage * Makefile: formatting * Makefile: factor out STANDALONE_KOMPILE_OPTS * Makefile: formatting * Makefile: remove duplicate -I $(llvm_dir) * Makefile, README: remove LIBFF_CC and LIBFF_CXX * Makefile: set K_RELEASE with abspath for cmake * cmake/client/CMakeLists: allow for global install of K too * Makefile: organize * Makefile: depend directly on files in submodules * kevm: same logic for setting K_RELEASE * Makefile: remove PKG_CONFIG_PATH variable * Makefile: correct depending on K Jar * README: update instructions * Makefile: add include/kllvm to STANDALONE_KOMPILE_OPTS * Jenkinsfile: increase parallelism of build step * Makefile: full path to K_LIB
runtimeverification · May 27, 2020 · fac5ebb · fac5ebb
1 parent 9b9b4e6
commit fac5ebb
Show file tree

Hide file tree

Showing 5 changed files with 82 additions and 122 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -24,13 +24,8 @@ pipeline {
         }
       }
       stages {
-        stage('Dependencies') {
-          parallel {
-            stage('K')     { steps { sh 'make deps RELEASE=true' } }
-            stage('Tests') { steps { sh 'make split-tests -j3'   } }
-          }
-        }
-        stage('Build') { steps { sh 'make build -j4' } }
+        stage('K Dependencies') { steps { sh 'make deps  RELEASE=true'     } }
+        stage('Build')          { steps { sh 'make build RELEASE=true -j6' } }
         stage('Test Execution') {
           failFast true
           options { timeout(time: 20, unit: 'MINUTES') }

diff --git a/Makefile b/Makefile
@@ -1,38 +1,37 @@
 # Settings
 # --------
 
+DEPS_DIR      := deps
 BUILD_DIR     := .build
 SUBDEFN_DIR   := .
 DEFN_BASE_DIR := $(BUILD_DIR)/defn
 DEFN_DIR      := $(DEFN_BASE_DIR)/$(SUBDEFN_DIR)
 BUILD_LOCAL   := $(abspath $(BUILD_DIR)/local)
+LOCAL_LIB     := $(BUILD_LOCAL)/lib
 
-LIBRARY_PATH       := $(BUILD_LOCAL)/lib
+K_SUBMODULE := $(DEPS_DIR)/k
+ifneq (,$(wildcard $(K_SUBMODULE)/k-distribution/target/release/k/bin/*))
+    K_RELEASE ?= $(abspath $(K_SUBMODULE)/k-distribution/target/release/k)
+else
+    K_RELEASE ?= $(dir $(shell which kompile))..
+endif
+K_BIN := $(K_RELEASE)/bin
+K_LIB := $(K_RELEASE)/lib/kframework
+export K_RELEASE
+
+LIBRARY_PATH       := $(LOCAL_LIB)
 C_INCLUDE_PATH     += :$(BUILD_LOCAL)/include
 CPLUS_INCLUDE_PATH += :$(BUILD_LOCAL)/include
-PKG_CONFIG_PATH    := $(LIBRARY_PATH)/pkgconfig
+PATH               := $(K_BIN):$(PATH)
 
 export LIBRARY_PATH
 export C_INCLUDE_PATH
 export CPLUS_INCLUDE_PATH
-export PKG_CONFIG_PATH
-
-INSTALL_PREFIX := /usr/local
-INSTALL_DIR    ?= $(DESTDIR)$(INSTALL_PREFIX)/bin
+export PATH
 
-DEPS_DIR         := deps
-K_SUBMODULE      := $(abspath $(DEPS_DIR)/k)
 PLUGIN_SUBMODULE := $(abspath $(DEPS_DIR)/plugin)
 export PLUGIN_SUBMODULE
 
-K_RELEASE ?= $(K_SUBMODULE)/k-distribution/target/release/k
-K_BIN     := $(K_RELEASE)/bin
-K_LIB     := $(K_RELEASE)/lib
-export K_RELEASE
-
-PATH := $(K_BIN):$(PATH)
-export PATH
-
 # need relative path for `pandoc` on MacOS
 PANDOC_TANGLE_SUBMODULE := $(DEPS_DIR)/pandoc-tangle
 TANGLER                 := $(PANDOC_TANGLE_SUBMODULE)/tangle.lua
@@ -44,7 +43,6 @@ export LUA_PATH
         deps all-deps llvm-deps haskell-deps repo-deps k-deps plugin-deps libsecp256k1 libff                                     \
         build build-java build-specs build-haskell build-llvm build-web3                                                         \
         defn java-defn specs-defn web3-defn haskell-defn llvm-defn                                                               \
-        split-tests                                                                                                              \
         test test-all test-conformance test-rest-conformance test-all-conformance test-slow-conformance test-failing-conformance \
         test-vm test-rest-vm test-all-vm test-bchain test-rest-bchain test-all-bchain                                            \
         test-web3 test-all-web3 test-failing-web3                                                                                \
@@ -56,7 +54,7 @@ export LUA_PATH
         media media-pdf metropolis-theme
 .SECONDARY:
 
-all: build split-tests
+all: build
 
 clean:
 	rm -rf $(DEFN_BASE_DIR)
@@ -68,84 +66,63 @@ distclean:
 # Non-K Dependencies
 # ------------------
 
-libsecp256k1_out := $(LIBRARY_PATH)/pkgconfig/libsecp256k1.pc
-libff_out        := $(LIBRARY_PATH)/libff.a
+libsecp256k1_out := $(LOCAL_LIB)/pkgconfig/libsecp256k1.pc
+libff_out        := $(LOCAL_LIB)/libff.a
 
 libsecp256k1: $(libsecp256k1_out)
 libff:        $(libff_out)
 
-$(DEPS_DIR)/secp256k1/autogen.sh:
-	git submodule update --init --recursive -- $(DEPS_DIR)/secp256k1
-
 $(libsecp256k1_out): $(DEPS_DIR)/secp256k1/autogen.sh
-	cd $(DEPS_DIR)/secp256k1/ \
-	    && ./autogen.sh \
+	cd $(DEPS_DIR)/secp256k1/                                             \
+	    && ./autogen.sh                                                   \
 	    && ./configure --enable-module-recovery --prefix="$(BUILD_LOCAL)" \
-	    && $(MAKE) \
+	    && $(MAKE)                                                        \
 	    && $(MAKE) install
 
 UNAME_S := $(shell uname -s)
 
 ifeq ($(UNAME_S),Linux)
-  LIBFF_CMAKE_FLAGS=
-  LINK_PROCPS=-lprocps
+    LIBFF_CMAKE_FLAGS=
 else
-  LIBFF_CMAKE_FLAGS=-DWITH_PROCPS=OFF
-  LINK_PROCPS=
+    LIBFF_CMAKE_FLAGS=-DWITH_PROCPS=OFF
 endif
 
-LIBFF_CC  := clang-8
-LIBFF_CXX := clang++-8
-
-$(DEPS_DIR)/libff/CMakeLists.txt:
-	git submodule update --init --recursive -- $(DEPS_DIR)/libff
-
 $(libff_out): $(DEPS_DIR)/libff/CMakeLists.txt
 	@mkdir -p $(DEPS_DIR)/libff/build
-	cd $(DEPS_DIR)/libff/build \
-	    && CC=$(LIBFF_CC) CXX=$(LIBFF_CXX) cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$(BUILD_LOCAL) $(LIBFF_CMAKE_FLAGS) \
-	    && make -s -j4 \
+	cd $(DEPS_DIR)/libff/build                                                                            \
+	    && cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=$(BUILD_LOCAL) $(LIBFF_CMAKE_FLAGS) \
+	    && make -s -j4                                                                                    \
 	    && make install
 
 # K Dependencies
 # --------------
 
+K_JAR := $(K_SUBMODULE)/k-distribution/target/release/k/lib/java/kernel-1.0-SNAPSHOT.jar
+
 deps: repo-deps
 repo-deps: tangle-deps k-deps plugin-deps
-k-deps: $(K_SUBMODULE)/make.timestamp
+k-deps: $(K_JAR)
 tangle-deps: $(TANGLER)
-plugin-deps: $(PLUGIN_SUBMODULE)/make.timestamp
+plugin-deps: $(PLUGIN_SUBMODULE)/client-c/main.cpp
 
 ifneq ($(RELEASE),)
-K_BUILD_TYPE         := FastBuild
-SEMANTICS_BUILD_TYPE := Release
-KOMPILE_OPTS         += -O3
+    K_BUILD_TYPE         := FastBuild
+    SEMANTICS_BUILD_TYPE := Release
+    KOMPILE_OPTS         += -O3
 else
-K_BUILD_TYPE         := FastBuild
-SEMANTICS_BUILD_TYPE := Debug
+    K_BUILD_TYPE         := FastBuild
+    SEMANTICS_BUILD_TYPE := Debug
 endif
 
-$(K_SUBMODULE)/make.timestamp:
-	git submodule update --init --recursive -- $(K_SUBMODULE)
-	cd $(K_SUBMODULE) && mvn package -DskipTests -U -Dproject.build.type=${K_BUILD_TYPE}
-	touch $(K_SUBMODULE)/make.timestamp
-
-$(TANGLER):
-	git submodule update --init -- $(PANDOC_TANGLE_SUBMODULE)
-
-$(PLUGIN_SUBMODULE)/make.timestamp:
-	git submodule update --init --recursive -- $(PLUGIN_SUBMODULE)
-	touch $(PLUGIN_SUBMODULE)/make.timestamp
+$(K_JAR):
+	cd $(K_SUBMODULE) && mvn package -DskipTests -U -Dproject.build.type=$(K_BUILD_TYPE)
 
 # Building
 # --------
 
-build-web3: MAIN_DEFN_FILE = web3
-build-web3: MAIN_MODULE    = WEB3
-build-web3: SYNTAX_MODULE  = WEB3
 MAIN_MODULE    := ETHEREUM-SIMULATION
 SYNTAX_MODULE  := $(MAIN_MODULE)
-export MAIN_DEFN_FILE := driver
+MAIN_DEFN_FILE := driver
 
 k_files       := driver.k data.k network.k evm.k evm-types.k json.k krypto.k edsl.k web3.k asm.k state-loader.k serialization.k evm-imp-specs.k
 EXTRA_K_FILES += $(MAIN_DEFN_FILE).k
@@ -172,6 +149,12 @@ haskell_kompiled := $(haskell_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
 llvm_kompiled    := $(llvm_dir)/$(MAIN_DEFN_FILE)-kompiled/interpreter
 
 web3_kore := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
+$(web3_kompiled): MAIN_DEFN_FILE := web3
+$(web3_kompiled): MAIN_MODULE    := WEB3
+$(web3_kompiled): SYNTAX_MODULE  := WEB3
+$(web3_kompiled): web3_kore      := $(web3_dir)/$(MAIN_DEFN_FILE)-kompiled/definition.kore
+
+export MAIN_DEFN_FILE
 
 # Tangle definition from *.md files
 
@@ -215,15 +198,15 @@ build-web3:    $(web3_kompiled)
 build-haskell: $(haskell_kompiled)
 build-llvm:    $(llvm_kompiled)
 
-# Java Backend
+# Java
 
 $(java_kompiled): $(java_files)
 	kompile --debug --main-module $(MAIN_MODULE) --backend java              \
 	        --syntax-module $(SYNTAX_MODULE) $(java_dir)/$(MAIN_DEFN_FILE).k \
 	        --directory $(java_dir) -I $(java_dir)                           \
 	        $(KOMPILE_OPTS)
 
-# Imperative Specs Backend
+# Imperative Specs
 
 $(specs_kompiled): MAIN_DEFN_FILE=evm-imp-specs
 $(specs_kompiled): MAIN_MODULE=EVM-IMP-SPECS
@@ -235,15 +218,15 @@ $(specs_kompiled): $(specs_files)
 	        --directory $(specs_dir) -I $(specs_dir) \
 	        $(KOMPILE_OPTS)
 
-# Haskell Backend
+# Haskell
 
 $(haskell_kompiled): $(haskell_files)
 	kompile --debug --main-module $(MAIN_MODULE) --backend haskell --hook-namespaces KRYPTO \
 	        --syntax-module $(SYNTAX_MODULE) $(haskell_dir)/$(MAIN_DEFN_FILE).k             \
 	        --directory $(haskell_dir) -I $(haskell_dir)                                    \
 	        $(KOMPILE_OPTS)
 
-# Web3 Backend
+# Web3
 
 $(web3_kore): $(web3_files)
 	kompile --debug --main-module $(MAIN_MODULE) --backend llvm              \
@@ -255,21 +238,26 @@ $(web3_kore): $(web3_files)
 
 $(web3_kompiled): $(web3_kore) $(libff_out)
 	@mkdir -p $(web3_dir)/build
-	cd $(web3_dir)/build && cmake $(CURDIR)/cmake/client -DCMAKE_BUILD_TYPE=${SEMANTICS_BUILD_TYPE} -DCMAKE_INSTALL_PREFIX=${INSTALL_PREFIX} && $(MAKE)
+	cd $(web3_dir)/build && cmake $(CURDIR)/cmake/client -DCMAKE_BUILD_TYPE=$(SEMANTICS_BUILD_TYPE) && $(MAKE)
+
+# Standalone
 
-# LLVM Backend
+STANDALONE_KOMPILE_OPTS := -L$(LOCAL_LIB) -I$(K_RELEASE)/include/kllvm \
+                           $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp     \
+                           $(PLUGIN_SUBMODULE)/plugin-c/blake2.cpp     \
+                           -g -std=c++14 -lff -lcryptopp -lsecp256k1
+
+ifeq ($(UNAME_S),Linux)
+    STANDALONE_KOMPILE_OPTS += -lprocps
+endif
 
 $(llvm_kompiled): $(llvm_files) $(libff_out)
 	kompile --debug --main-module $(MAIN_MODULE) --backend llvm                                  \
 	        --syntax-module $(SYNTAX_MODULE) $(llvm_dir)/$(MAIN_DEFN_FILE).k                     \
-	        --directory $(llvm_dir) -I $(llvm_dir) -I $(llvm_dir)                                \
+	        --directory $(llvm_dir) -I $(llvm_dir)                                               \
 	        --hook-namespaces KRYPTO                                                             \
 	        $(KOMPILE_OPTS)                                                                      \
-	        -ccopt $(PLUGIN_SUBMODULE)/plugin-c/crypto.cpp                                       \
-	        -ccopt $(PLUGIN_SUBMODULE)/plugin-c/blake2.cpp                                       \
-	        -ccopt -g -ccopt -std=c++14                                                          \
-	        -ccopt -L$(LIBRARY_PATH)                                                             \
-	        -ccopt -lff -ccopt -lcryptopp -ccopt -lsecp256k1 $(addprefix -ccopt ,$(LINK_PROCPS))
+	        $(addprefix -ccopt ,$(STANDALONE_KOMPILE_OPTS))
 
 # Installing
 # ----------
@@ -303,12 +291,6 @@ KPROVE_OPTIONS :=
 test-all: test-all-conformance test-prove test-interactive test-parse
 test: test-conformance test-prove test-interactive test-parse
 
-split-tests: tests/ethereum-tests/make.timestamp
-
-tests/%/make.timestamp:
-	git submodule update --init -- tests/$*
-	touch $@
-
 # Generic Test Harnesses
 
 tests/ethereum-tests/VMTests/%: KEVM_MODE=VMTESTS
@@ -499,5 +481,4 @@ media-pdf: $(patsubst %, media/%.pdf, $(media_pdfs))
 metropolis-theme: $(BUILD_DIR)/media/metropolis/beamerthememetropolis.sty
 
 $(BUILD_DIR)/media/metropolis/beamerthememetropolis.sty:
-	git submodule update --init -- $(dir $@)
 	cd $(dir $@) && $(MAKE)
diff --git a/README.md b/README.md
@@ -107,39 +107,21 @@ export PATH=$HOME/.local/bin:$PATH
 
 ### Build K Dependency
 
-Get the submodules:
+The `Makefile` and `kevm` will work with either a (i) globally installed K, or (ii) the submodule built K.
+If you want to use the submodule, follow these instructions, then get the submodules and build the repository dependencies:
 
 ```sh
-git submodule update --init --recursive
-```
-
-And finally build the repository specific dependencies:
-
-```sh
-make RELEASE=1 deps
-```
-If you are a developer, you probably should omit `RELEASE` from the above commands unless you are testing performance, as the build is somewhat slower.
-
-On Arch, instead do:
-
-```sh
-make LIBFF_CC=clang LIBFF_CXX=clang++ RELEASE=1 deps
+git submodule update --init --recursive -- deps/k
+make deps
 ```
 
 ### Building
 
-Finally, you can install repository specific dependencies and build the semantics:
-
-```sh
-make build RELEASE=1
-```
-
-You can also build specific backends as so:
+Finally, you can build the semantics (after getting the plugin and tangle submodule dependencies):
 
 ```sh
-make build-haskell
-make build-llvm RELEASE=1
-make build-java
+git submodule update --init --recursive -- deps/plugin deps/pandoc-tangle
+make build
 ```
 
 Example Usage

diff --git a/cmake/client/CMakeLists.txt b/cmake/client/CMakeLists.txt
@@ -1,6 +1,7 @@
 cmake_minimum_required (VERSION 3.4)
 
 list(APPEND CMAKE_MODULE_PATH "$ENV{K_RELEASE}/cmake")
+list(APPEND CMAKE_MODULE_PATH "$ENV{K_RELEASE}/lib/cmake/kframework")
 include(LLVMKompilePrelude)
 project (KevmClient CXX)
 
@@ -22,6 +23,7 @@ endif()
 target_include_directories(kevm-client
 	PUBLIC $ENV{PLUGIN_SUBMODULE}/plugin-c
 	PUBLIC $ENV{PLUGIN_SUBMODULE}/deps/cpp-httplib
+	PUBLIC $ENV{K_RELEASE}/include/kllvm
 	PUBLIC ${CMAKE_SOURCE_DIR}/..)
 target_compile_options(kevm-client
 	PUBLIC $ENV{LLVM_KOMPILE_OPTS}

diff --git a/kevm b/kevm
@@ -3,11 +3,21 @@
 set -euo pipefail
 shopt -s extglob
 
+notif() { echo "== $@" >&2 ; }
+fatal() { echo "[FATAL] $@" ; exit 1 ; }
+
 kevm_dir="${KEVM_DIR:-.}"
 build_dir="$kevm_dir/.build"
 defn_dir="${KEVM_DEFN_DIR:-$build_dir/defn}"
 lib_dir="$build_dir/local/lib"
 k_release_dir="${K_RELEASE:-$kevm_dir/deps/k/k-distribution/target/release/k}"
+if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then
+    if which kompile &> /dev/null; then
+        k_release_dir="$(dirname $(which kompile))/.."
+    else
+        fatal "Cannot find K Installation!"
+    fi
+fi
 
 export PATH="${defn_dir}/web3/build:$k_release_dir/lib/native/linux:$k_release_dir/lib/native/linux64:$k_release_dir/bin/:$PATH"
 export LD_LIBRARY_PATH="$k_release_dir/lib/native/linux64:$lib_dir:${LD_LIBRARY_PATH:-}"
@@ -20,16 +30,6 @@ KLAB_OUT="${KLAB_OUT:-$build_dir/klab}"
 KLAB_NODE_STACK_SIZE="${KLAB_NODE_STACK_SIZE:-30000}"
 export KLAB_OUT
 
-# Utilities
-# ---------
-
-notif() { echo "== $@" >&2 ; }
-fatal() { echo "[FATAL] $@" ; exit 1 ; }
-
-pretty_diff() {
-    git --no-pager diff --no-index --ignore-all-space "$@"
-}
-
 # Runners
 # -------