Migrate build to kdist (#605)

* Remove `kbuild.toml` * Move K source files into Python package * Add `kdist` plugin * Set Version: 0.1.27 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Apr 12, 2024 · 76d796d · 76d796d
1 parent 424b1ba
commit 76d796d
Show file tree

Hide file tree

Showing 23 changed files with 146 additions and 153 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -39,7 +39,7 @@ jobs:
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
-        with:    
+        with:
           submodules: recursive
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
@@ -53,7 +53,7 @@ jobs:
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
-        with:    
+        with:
           submodules: recursive
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
@@ -67,23 +67,24 @@ jobs:
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
-        with:    
+        with:
           submodules: recursive
       - name: Login to Docker Hub
         uses: docker/login-action@v3
         with:
           username: rvdockerhub
-          password: ${{ secrets.DOCKERHUB_PASSWORD }} 
+          password: ${{ secrets.DOCKERHUB_PASSWORD }}
 
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kwasm-ci-integration-${{ github.sha }}
-      - name: 'Build LLVM Backend and pykwasm'
-        run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} make -j2 build-llvm
+      - name: 'Build pykwasm'
+        run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} poetry -C pykwasm install
+      - name: 'Build LLVM definition'
+        run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.llvm
       - name: 'Build and run integration tests'
-        run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} make -C pykwasm cov-integration \
-                 TEST_ARGS='--llvm-dir ../.build/defn/llvm/test-kompiled'
+        run: docker exec -u user kwasm-ci-integration-${GITHUB_SHA} make -C pykwasm cov-integration
       - name: 'Tear down Docker'
         if: always()
         run: |
@@ -105,13 +106,15 @@ jobs:
         with:
           username: rvdockerhub
           password: ${{ secrets.DOCKERHUB_PASSWORD }}
-        
+
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kwasm-ci-parse-${{ github.sha }}
-      - name: 'Build LLVM Backend and pykwasm'
-        run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make -j2 build-llvm RELEASE=true
+      - name: 'Build pykwasm'
+        run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} poetry -C pykwasm install
+      - name: 'Build LLVM definition'
+        run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.llvm
       - name: 'Conformance parse'
         run: docker exec -u user kwasm-ci-parse-${GITHUB_SHA} make test-conformance-parse
       - name: 'Tear down Docker'
@@ -129,23 +132,25 @@ jobs:
         uses: actions/checkout@v3
         with:
           submodules: recursive
- 
+
       - name: Login to Docker Hub
         uses: docker/login-action@v3
         with:
           username: rvdockerhub
           password: ${{ secrets.DOCKERHUB_PASSWORD }}
-   
+
       - name: 'Set up Docker'
         uses: ./.github/actions/with-docker
         with:
           container-name: kwasm-ci-conformance-${{ github.sha }}
-      - name: 'Build LLVM Backend'
-        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 build-llvm RELEASE=true
+      - name: 'Build pykwasm'
+        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} poetry -C pykwasm install
+      - name: 'Build LLVM definition'
+        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.llvm
       - name: 'Simple tests'
-        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 TEST_CONCRETE_BACKEND=llvm test-simple
+        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 test-simple
       - name: 'Conformance run'
-        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 TEST_CONCRETE_BACKEND=llvm test-conformance-supported
+        run: docker exec -u user kwasm-ci-conformance-${GITHUB_SHA} make -j2 test-conformance-supported
       - name: 'Tear down Docker'
         if: always()
         run: |
@@ -165,8 +170,10 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kwasm-ci-prove-${{ github.sha }}
-      - name: 'Build Haskell Backend'
-        run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} make -j2 build-haskell build-wrc20
+      - name: 'Build pykwasm'
+        run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm install
+      - name: 'Build Haskell definitions'
+        run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} poetry -C pykwasm run kdist -v build wasm-semantics.{kwasm-lemmas,wrc20} -j2
       - name: 'Prove'
         run: docker exec -u user kwasm-ci-prove-${GITHUB_SHA} make -j6 test-prove
       - name: 'Tear down Docker'

diff --git a/Makefile b/Makefile
@@ -1,109 +1,29 @@
-# Settings
-# --------
-
-BUILD_DIR := .build
-DEFN_DIR  := $(BUILD_DIR)/defn
-K_INCLUDE_DIR ?= $(CURDIR)
-
 .PHONY: all                                                                \
-        build build-llvm build-haskell build-wrc20                         \
         test test-execution test-simple test-prove                         \
         test-conformance test-conformance-parse test-conformance-supported \
         media presentations reports
 
+
 all: build
 
+
 # Building Definition
 # -------------------
 
-KOMPILE_OPTS         :=
-LLVM_KOMPILE_OPTS    :=
-HASKELL_KOMPILE_OPTS :=
-
-tangle_selector := k
-
-SOURCE_FILES       := data         \
-                      kwasm-lemmas \
-                      numeric      \
-                      test         \
-                      wasm         \
-                      wasm-text    \
-                      wrc20
-EXTRA_SOURCE_FILES :=
-ALL_SOURCE_FILES   := $(patsubst %, %.md, $(SOURCE_FILES)) $(EXTRA_SOURCE_FILES)
-
-build: build-llvm build-haskell build-wrc20
-
-ifneq (,$(RELEASE))
-    KOMPILE_OPTS += -O2 --gen-glr-bison-parser
-else
-    KOMPILE_OPTS += --debug
-endif
-
-ifeq (,$(RELEASE))
-    LLVM_KOMPILE_OPTS += -g
-endif
-
-KOMPILE_LLVM := kompile --backend llvm --md-selector "$(tangle_selector)" \
-                $(KOMPILE_OPTS)                                           \
-                $(addprefix -ccopt ,$(LLVM_KOMPILE_OPTS))
-
-KOMPILE_HASKELL := kompile --backend haskell --md-selector "$(tangle_selector)" \
-                   $(KOMPILE_OPTS)                                              \
-                   $(HASKELL_KOMPILE_OPTS)                                      \
-                   --warnings-to-errors
-
-### LLVM
-
-llvm_files         := $(ALL_SOURCE_FILES)
-llvm_main_module   := WASM-TEST
-llvm_syntax_module := $(llvm_main_module)-SYNTAX
-llvm_main_file     := test
-llvm_dir           := $(DEFN_DIR)/llvm/$(llvm_main_file)-kompiled
-llvm_kompiled      := $(llvm_dir)/interpreter
-
-build-llvm: $(llvm_kompiled)
-
-$(llvm_kompiled): $(llvm_files)
-	$(KOMPILE_LLVM) $(llvm_main_file).md      \
-	    --output-definition $(llvm_dir) -I $(K_INCLUDE_DIR)  \
-	    --main-module $(llvm_main_module)     \
-	    --syntax-module $(llvm_syntax_module) \
-	    --emit-json
-
-### Haskell
-
-haskell_files         := $(ALL_SOURCE_FILES)
-haskell_main_module   := KWASM-LEMMAS
-haskell_syntax_module := WASM-TEXT-SYNTAX
-haskell_main_file     := kwasm-lemmas
-haskell_dir           := $(DEFN_DIR)/haskell/$(haskell_main_file)-kompiled
-haskell_kompiled      := $(haskell_dir)/definition.kore
-
-build-haskell: $(haskell_kompiled)
-
-$(haskell_kompiled): $(haskell_files)
-	$(KOMPILE_HASKELL) $(haskell_main_file).md   \
-	    --output-definition $(haskell_dir) -I $(K_INCLUDE_DIR)  \
-	    --main-module $(haskell_main_module)     \
-	    --syntax-module $(haskell_syntax_module)
-
-### WRC-20 Verification
-
-wrc20_files         := $(haskell_files) wrc20.md
-wrc20_main_module   := WRC20-LEMMAS
-wrc20_syntax_module := WASM-TEXT-SYNTAX
-wrc20_main_file     := wrc20
-wrc20_dir           := $(DEFN_DIR)/haskell/$(wrc20_main_file)-kompiled
-wrc20_kompiled      := $(wrc20_dir)/definition.kore
-
-build-wrc20: $(wrc20_kompiled)
-
-$(wrc20_kompiled): $(wrc20_files)
-	$(KOMPILE_HASKELL) $(wrc20_main_file).md   \
-	    --output-definition $(wrc20_dir) -I $(K_INCLUDE_DIR)  \
-	    --main-module $(wrc20_main_module)     \
-	    --syntax-module $(wrc20_syntax_module)
+POETRY := poetry -C pykwasm
+
+.PHONY: pykwasm
+pykwasm:
+	$(POETRY) install
+
+.PHONY: build
+build: pykwasm
+	$(POETRY) run kdist -v build -j3
+
+.PHONY: clean
+clean: pykwasm
+	$(POETRY) run kdist clean
+
 
 # Testing
 # -------
@@ -114,31 +34,33 @@ CHECK := git --no-pager diff --no-index --ignore-all-space -R
 TEST_CONCRETE_BACKEND := llvm
 TEST_SYMBOLIC_BACKEND := haskell
 
+SOURCE_DIR := pykwasm/src/pykwasm/kdist
+
 test: test-execution test-prove
 
 # Generic Test Harnesses
 
-tests/%.run: tests/% $(llvm_kompiled)
+tests/%.run: tests/%
 	$(TEST) run --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	$(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/success-$(TEST_CONCRETE_BACKEND).out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 
-tests/%.run-term: tests/% $(llvm_kompiled)
+tests/%.run-term: tests/%
 	$(TEST) run --backend $(TEST_CONCRETE_BACKEND) $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	grep --after-context=2 "<instrs>" tests/$*.$(TEST_CONCRETE_BACKEND)-out > tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
 	$(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out-term tests/success-k.out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
 	rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
 
-tests/%.parse: tests/% $(llvm_kompiled)
+tests/%.parse: tests/%
 	$(TEST) kast --backend $(TEST_CONCRETE_BACKEND) $< kast > $@-out
 	rm -rf $@-out
 
-tests/%.prove: tests/% $(haskell_kompiled)
-	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< $(haskell_main_file)
+tests/%.prove: tests/%
+	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< kwasm-lemmas -I $(SOURCE_DIR)
 
-tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k $(wrc20_kompiled)
-	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< $(wrc20_main_file)
+tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k
+	$(TEST) prove --backend $(TEST_SYMBOLIC_BACKEND) $< wrc20 -I $(SOURCE_DIR)
 
 ### Execution Tests
 
@@ -169,8 +91,10 @@ proof_tests:=$(wildcard tests/proofs/*-spec.k)
 
 test-prove: $(proof_tests:=.prove)
 
+
 # Analysis
 # --------
+
 json_build := $(haskell_dir)/parsed.json
 
 $(json_build):
@@ -179,6 +103,7 @@ $(json_build):
 graph-imports: $(json_build)
 	kpyk $(haskell_dir) graph-imports
 
+
 # Presentation
 # ------------
 

diff --git a/kbuild.toml b/kbuild.toml
diff --git a/kwasm b/kwasm
@@ -8,7 +8,8 @@ fatal() { echo "[FATAL] $@" ; exit 1 ; }
 
 kwasm_dir="${KWASM_DIR:-$(dirname $0)}"
 build_dir="$kwasm_dir/.build"
-defn_dir="${KWASM_DEFN_DIR:-$build_dir/defn}"
+kdist_dir="$(poetry -C pykwasm run -- kdist which)"
+defn_dir="${KWASM_DEFN_DIR:-$kdist_dir}/wasm-semantics"
 lib_dir="$build_dir/local/lib"
 k_release_dir="${K_RELEASE:-$kwasm_dir/deps/k/k-distribution/target/release/k}"
 if [[ ! -f "${k_release_dir}/bin/kompile" ]]; then
@@ -45,21 +46,16 @@ preprocess() {
 # -------
 
 run_krun() {
-    local additional_run_args
-
-    additional_run_args=()
-    ! $bug_report || additional_run_args+=(--haskell-backend-command "kore-exec --bug-report $bug_report_name")
-
     preprocess
-    krun --definition "$backend_dir/test-kompiled" "$run_file" "${additional_run_args[@]}" "$@"
+    krun --definition "$defn_dir/llvm" "$run_file" "$@"
 }
 
 run_kast() {
     local output_mode
 
     preprocess
     output_mode="${1:-kast}" ; shift
-    kast --definition "$backend_dir/test-kompiled" "$run_file" --output "$output_mode" "$@"
+    kast --definition "$defn_dir/llvm" "$run_file" --output "$output_mode" "$@"
 }
 
 run_prove() {
@@ -71,7 +67,7 @@ run_prove() {
     ! $repl       || additional_proof_args+=(--debugger)
     ! $bug_report || additional_proof_args+=(--haskell-backend-command "kore-exec --bug-report $bug_report_name")
 
-    kprove --definition "$backend_dir/$def_module-kompiled" -I "$kwasm_dir" "$run_file" "${additional_proof_args[@]}" "$@"
+    kprove --definition "$defn_dir/$def_module" -I "$kwasm_dir" "$run_file" "${additional_proof_args[@]}" "$@"
 }
 
 # Main
@@ -146,8 +142,6 @@ set -- "${args[@]}"
 ! $repl       || [[ "$backend" == "haskell" ]] || fatal "--repl option only available for Haskell backend."
 ! $bug_report || [[ "$backend" == "haskell" ]] || fatal "--bug-report option only available for Haskell backend."
 
-backend_dir="$defn_dir/$backend"
-
 # get the run file
 [[ ! -z ${1:-} ]] || usage_fatal "Must supply a file to run on."
 run_file="$1" ; shift

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.26
+0.1.27
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -4,12 +4,15 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.26"
+version = "0.1.27"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
 
+[tool.poetry.plugins.kdist]
+wasm-semantics = "pykwasm.kdist.plugin"
+
 [tool.poetry.dependencies]
 python = "^3.10"
 cytoolz = "^0.12.1"

diff --git a/pykwasm/src/pykwasm/kdist/__init__.py b/pykwasm/src/pykwasm/kdist/__init__.py
diff --git a/auxil.md → pykwasm/src/pykwasm/kdist/auxil.md b/auxil.md → pykwasm/src/pykwasm/kdist/auxil.md
diff --git a/data.md → pykwasm/src/pykwasm/kdist/data.md b/data.md → pykwasm/src/pykwasm/kdist/data.md
diff --git a/data/int-type.k → pykwasm/src/pykwasm/kdist/data/int-type.k b/data/int-type.k → pykwasm/src/pykwasm/kdist/data/int-type.k
diff --git a/data/list-int.k → pykwasm/src/pykwasm/kdist/data/list-int.k b/data/list-int.k → pykwasm/src/pykwasm/kdist/data/list-int.k
diff --git a/data/list-ref.k → pykwasm/src/pykwasm/kdist/data/list-ref.k b/data/list-ref.k → pykwasm/src/pykwasm/kdist/data/list-ref.k
diff --git a/data/map-int-to-int.k → ...m/src/pykwasm/kdist/data/map-int-to-int.k b/data/map-int-to-int.k → ...m/src/pykwasm/kdist/data/map-int-to-int.k
diff --git a/data/sparse-bytes.k → ...asm/src/pykwasm/kdist/data/sparse-bytes.k b/data/sparse-bytes.k → ...asm/src/pykwasm/kdist/data/sparse-bytes.k
diff --git a/data/tools.k → pykwasm/src/pykwasm/kdist/data/tools.k b/data/tools.k → pykwasm/src/pykwasm/kdist/data/tools.k
diff --git a/kwasm-lemmas.md → pykwasm/src/pykwasm/kdist/kwasm-lemmas.md b/kwasm-lemmas.md → pykwasm/src/pykwasm/kdist/kwasm-lemmas.md
diff --git a/numeric.md → pykwasm/src/pykwasm/kdist/numeric.md b/numeric.md → pykwasm/src/pykwasm/kdist/numeric.md