From e7e4c3c3035599c36a4c72c509c3de7dc6879eab Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Sat, 13 Jun 2020 22:24:55 +0000 Subject: [PATCH] Update Makefile for native Markdown support --- Makefile | 116 +++++++++++----------------- driver.md | 4 +- ewasm-test.md | 4 +- ewasm.md | 4 +- kewasm-lemmas.md | 3 +- tests/proofs/invoke-contract-spec.k | 2 +- 6 files changed, 54 insertions(+), 79 deletions(-) diff --git a/Makefile b/Makefile index 5d1d86c..43a3f9c 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ # Settings # -------- -deps_dir := deps -wasm_submodule := $(deps_dir)/wasm-semantics -eei_submodule := $(deps_dir)/eei-semantics -k_submodule := $(wasm_submodule)/deps/k +deps_dir := deps +KWASM_SUBMODULE := $(deps_dir)/wasm-semantics +eei_submodule := $(deps_dir)/eei-semantics +k_submodule := $(KWASM_SUBMODULE)/deps/k ifneq (,$(wildcard $(k_submodule)/k-distribution/target/release/k/bin/*)) K_RELEASE ?= $(abspath $(k_submodule)/k-distribution/target/release/k) @@ -15,17 +15,17 @@ K_BIN := $(K_RELEASE)/bin K_LIB := $(K_RELEASE)/lib/kframework export K_RELEASE -PATH:=$(K_BIN):$(abspath $(wasm_submodule)):$(PATH) +PATH:=$(K_BIN):$(abspath $(KWASM_SUBMODULE)):$(PATH) export PATH build_dir := .build -defn_dir := $(build_dir)/defn +DEFN_DIR := $(build_dir)/defn kompiled_dir_name := ewasm-test -wasm_make := make --directory $(wasm_submodule) DEFN_DIR=../../$(defn_dir) -eei_make := make --directory $(eei_submodule) DEFN_DIR=../../$(defn_dir) +KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE) +eei_make := make --directory $(eei_submodule) DEFN_DIR=../../$(DEFN_DIR) -pandoc_tangle_submodule := $(wasm_submodule)/deps/pandoc-tangle +pandoc_tangle_submodule := $(KWASM_SUBMODULE)/deps/pandoc-tangle tangler := $(pandoc_tangle_submodule)/tangle.lua LUA_PATH := $(pandoc_tangle_submodule)/?.lua;; export LUA_PATH @@ -34,7 +34,7 @@ export LUA_PATH deps haskell-deps \ defn defn-llvm defn-haskell \ definition-deps wasm-definitions eei-definitions \ - build build-llvm build-haskell \ + build \ test test-execution test-simple test-prove \ media presentations reports @@ -42,96 +42,72 @@ all: build clean: rm -rf $(build_dir) - rm -f $(wasm_submodule)/make.timestamp + rm -f $(KWASM_SUBMODULE)/make.timestamp rm -f $(eei_submodule)/make.timestamp git submodule update --init --recursive - $(MAKE) clean -C $(wasm_submodule) + $(MAKE) clean -C $(KWASM_SUBMODULE) $(MAKE) clean -C $(eei_submodule) # Build Dependencies (K Submodule) # -------------------------------- -wasm_files=test.k wasm.k wasm-text.k data.k kwasm-lemmas.k -wasm_source_files:=$(patsubst %, $(wasm_submodule)/%, $(patsubst %.k, %.md, $(wasm_files))) -eei_files:=eei.k -eei_source_files:=$(patsubst %, $(eei_submodule)/%, $(patsubst %.k, %.md, $(eei_files))) -ewasm_files:=ewasm-test.k driver.k ewasm.k kewasm-lemmas.k +wasm_files=test.md wasm.md wasm-text.md data.md kwasm-lemmas.md +wasm_source_files:=$(patsubst %, $(KWASM_SUBMODULE)/%, $(wasm_files)) +eei_files:=eei.md +eei_source_files:=$(patsubst %, $(eei_submodule)/%, $(eei_files)) +ewasm_files:=ewasm-test.md driver.md ewasm.md kewasm-lemmas.md +ewasm_source_files:=$(ewasm_files) all_k_files:=$(ewasm_files) $(wasm_files) $(eei_files) -deps: $(wasm_submodule)/make.timestamp $(eei_submodule)/make.timestamp definition-deps +llvm_dir:=$(DEFN_DIR)/llvm +llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files)) + +haskell_dir:=$(DEFN_DIR)/haskell +haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files)) -definition-deps: wasm-definitions eei-definitions +definition-deps: eei-definitions +deps: $(KWASM_SUBMODULE)/make.timestamp $(eei_submodule)/make.timestamp definition-deps wasm-definitions: - $(wasm_make) -B defn-llvm - $(wasm_make) -B defn-haskell + $(KWASM_MAKE) -B defn-llvm + $(KWASM_MAKE) -B defn-haskell eei-definitions: $(eei_source_files) $(eei_make) -B defn-llvm $(eei_make) -B defn-haskell -$(wasm_submodule)/make.timestamp: $(wasm_source_files) - git submodule update --init --recursive - $(wasm_make) deps - touch $(wasm_submodule)/make.timestamp +$(KWASM_SUBMODULE)/make.timestamp: $(wasm_source_files) + $(KWASM_MAKE) deps + touch $(KWASM_SUBMODULE)/make.timestamp $(eei_submodule)/make.timestamp: $(eei_source_files) - git submodule update --init --recursive touch $(eei_submodule)/make.timestamp # Building Definition # ------------------- -llvm_dir:=$(defn_dir)/llvm -llvm_defn:=$(patsubst %, $(llvm_dir)/%, $(all_k_files)) -llvm_kompiled:=$(llvm_dir)/ewasm-test-kompiled/interpreter - -haskell_dir:=$(defn_dir)/haskell -haskell_defn:=$(patsubst %, $(haskell_dir)/%, $(all_k_files)) -haskell_kompiled:=$(haskell_dir)/ewasm-test-kompiled/definition.kore - -main_module=EWASM-TEST -syntax_module=EWASM-TEST-SYNTAX - -# Tangle definition from *.md files - -defn: defn-llvm defn-haskell -defn-llvm: $(llvm_defn) -defn-haskell: $(haskell_defn) - -$(llvm_dir)/%.k: %.md $(tangler) - @echo "== tangle: $@" - mkdir -p $(dir $@) - pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@ - -$(haskell_dir)/%.k: %.md $(tangler) - @echo "== tangle: $@" - mkdir -p $(dir $@) - pandoc --from markdown --to $(tangler) --metadata=code:.k $< > $@ +MAIN_MODULE=EWASM-TEST +MAIN_SYNTAX_MODULE=EWASM-TEST-SYNTAX +MAIN_DEFN_FILE=ewasm-test # Build definitions KOMPILE_OPTS := build: build-llvm build-haskell -build-llvm: $(llvm_kompiled) -build-haskell: $(haskell_kompiled) - -$(llvm_kompiled): $(llvm_defn) - @echo "== kompile: $@" - kompile --backend llvm \ - --directory $(llvm_dir) -I $(llvm_dir) \ - --main-module $(main_module) \ - --syntax-module $(syntax_module) $< \ - $(KOMPILE_OPTS) - -$(haskell_kompiled): $(haskell_defn) - @echo "== kompile: $@" - kompile --backend haskell \ - --directory $(haskell_dir) -I $(haskell_dir) \ - --main-module $(main_module) \ - --syntax-module $(syntax_module) $< \ - $(KOMPILE_OPTS) + +build-%: + cp $(eei_source_files) $(ewasm_source_files) $(KWASM_SUBMODULE) + $(KWASM_MAKE) build-$* \ + DEFN_DIR=../../$(DEFN_DIR) \ + llvm_main_module=$(MAIN_MODULE) \ + llvm_syntax_module=$(MAIN_SYNTAX_MODULE) \ + llvm_main_file=$(MAIN_DEFN_FILE) \ + haskell_main_module=$(MAIN_MODULE) \ + haskell_syntax_module=$(MAIN_SYNTAX_MODULE) \ + haskell_main_file=$(MAIN_DEFN_FILE) \ + EXTRA_SOURCE_FILES="$(eei_files) $(ewasm_files)" \ + KOMPILE_OPTS="$(KOMPILE_OPTS)" # Testing # ------- diff --git a/driver.md b/driver.md index 966bfad..b3b4a7e 100644 --- a/driver.md +++ b/driver.md @@ -2,8 +2,8 @@ Ethereum Simulation =================== ```k -require "ewasm.k" -require "data.k" +require "ewasm.md" +require "data.md" module DRIVER-SYNTAX imports EWASM-SYNTAX diff --git a/ewasm-test.md b/ewasm-test.md index afb0f12..a724d2f 100644 --- a/ewasm-test.md +++ b/ewasm-test.md @@ -4,8 +4,8 @@ Testing We make use of the testing module for Wasm, which will let us make assertions about the Wasm runtime state. ```k -requires "test.k" // WASM-TEST -requires "driver.k" +requires "test.md" // WASM-TEST +requires "driver.md" module EWASM-TEST-SYNTAX imports WASM-TEST-SYNTAX diff --git a/ewasm.md b/ewasm.md index ba8dc5c..0a60c6a 100644 --- a/ewasm.md +++ b/ewasm.md @@ -2,8 +2,8 @@ Ewasm Specification ================= ```k -require "wasm.k" -require "eei.k" +require "wasm.md" +require "eei.md" module EWASM-SYNTAX imports WASM-TEXT-SYNTAX diff --git a/kewasm-lemmas.md b/kewasm-lemmas.md index b1fa300..89d0b1f 100644 --- a/kewasm-lemmas.md +++ b/kewasm-lemmas.md @@ -5,8 +5,7 @@ These lemmas aid in verifying Ewasm programs behavior. They are part of the *trusted* base, and so should be scrutinized carefully. ```k -requires "kwasm-lemmas.k" -requires "kewasm-lemmas.k" +requires "kwasm-lemmas.md" module KEWASM-LEMMAS imports EWASM-TEST diff --git a/tests/proofs/invoke-contract-spec.k b/tests/proofs/invoke-contract-spec.k index 472e012..1face3c 100644 --- a/tests/proofs/invoke-contract-spec.k +++ b/tests/proofs/invoke-contract-spec.k @@ -1,4 +1,4 @@ -requires "kewasm-lemmas.k" +requires "kewasm-lemmas.md" module INVOKE-CONTRACT-SPEC imports KEWASM-LEMMAS