Switch to CI based on Jenkinsfile Dockerfile

Dockerfile

@@ -0,0 +1,34 @@
+FROM ubuntu:bionic
+
+ENV TZ=America/Chicago
+RUN    ln --symbolic --no-dereference --force /usr/share/zoneinfo/$TZ /etc/localtime \
+    && echo $TZ > /etc/timezone
+
+RUN    apt update                                                            \
+    && apt upgrade --yes                                                     \
+    && apt install --yes                                                     \
+        autoconf curl flex gcc libffi-dev libmpfr-dev libtool libz3-dev make \
+        maven opam openjdk-8-jdk pandoc pkg-config python3 python-pygments   \
+        python-recommonmark python-sphinx time zlib1g-dev z3
+
+RUN update-alternatives --set java /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java
+
+RUN curl -sSL https://get.haskellstack.org/ | sh
+
+ARG USER_ID=1000
+ARG GROUP_ID=1000
+RUN    groupadd --gid $GROUP_ID user                                        \
+    && useradd --create-home --uid $USER_ID --shell /bin/sh --gid user user
+
+USER $USER_ID:$GROUP_ID
+
+ADD .build/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev .build/k/k-distribution/src/main/scripts/bin/k-configure-opam-common /home/user/.tmp-opam/bin/
+ADD .build/k/k-distribution/src/main/scripts/lib/opam  /home/user/.tmp-opam/lib/opam/
+RUN    cd /home/user \
+    && ./.tmp-opam/bin/k-configure-opam-dev
+
+ENV LC_ALL=C.UTF-8
+ADD --chown=user:user .build/k/haskell-backend/src/main/native/haskell-backend/stack.yaml /home/user/.tmp-haskell/
+ADD --chown=user:user .build/k/haskell-backend/src/main/native/haskell-backend/kore/package.yaml /home/user/.tmp-haskell/kore/
+RUN    cd /home/user/.tmp-haskell \
+    && stack build --only-snapshot --test --bench --no-haddock-deps --haddock --library-profiling

Jenkinsfile

@@ -0,0 +1,59 @@
+pipeline {
+  agent {
+    dockerfile {
+      additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
+    }
+  }
+  stages {
+    stage("Init title") {
+      when { changeRequest() }
+      steps {
+        script {
+          currentBuild.displayName = "PR ${env.CHANGE_ID}: ${env.CHANGE_TITLE}"
+        }
+      }
+    }
+    stage('Dependencies') {
+      steps {
+        ansiColor('xterm') {
+          sh '''
+            make clean
+            make deps
+          '''
+        }
+      }
+    }
+    stage('Build') {
+      steps {
+        ansiColor('xterm') {
+          sh '''
+            make build -j4
+          '''
+        }
+      }
+    }
+    stage('Test') {
+      parallel {
+        stage('IMP') {
+          steps {
+            ansiColor('xterm') {
+              sh '''
+                make test-imp -j8
+              '''
+            }
+          }
+        }
+        stage('FUN') {
+          steps {
+            ansiColor('xterm') {
+              sh '''
+                echo "SKIPPING!!!"
+                # make test-fun -j8
+              '''
+            }
+          }
+        }
+      }
+    }
+  }
+}

Makefile

@@ -3,136 +3,146 @@
 
 build_dir:=.build
 defn_dir:=$(build_dir)/defn
-
 k_submodule:=$(build_dir)/k
-k_bin:=$(k_submodule)/k-distribution/target/release/k/bin
-kompile:=$(k_bin)/kompile
-krun:=$(k_bin)/krun
-
 pandoc_tangle_submodule:=$(build_dir)/pandoc-tangle
+k_bin:=$(k_submodule)/k-distribution/target/release/k/bin
 tangler:=$(pandoc_tangle_submodule)/tangle.lua
-LUA_PATH:=$(pandoc_tangle_submodule)/?.lua;;
-export LUA_PATH
-pandoc:=pandoc --from markdown --to markdown --lua-filter "$(tangler)"
 
-test_dir:=tests
-test_output:=.build/logs
+LUA_PATH=$(pandoc_tangle_submodule)/?.lua;;
+export LUA_PATH
 
-.PHONY: deps deps-k deps-ocaml deps-tangle \
-		defn  defn-imp  defn-imp-kcompile  defn-imp-krun  defn-fun  defn-fun-krun  defn-fun-kcompile \
-		build build-imp build-imp-kcompile build-imp-krun build-fun build-fun-krun build-fun-kcompile \
-		test test-imp test-fun
+.PHONY: all clean \
+        deps ocaml-deps haskell-deps \
+        defn defn-imp defn-imp-ocaml defn-imp-java defn-fun defn-fun-ocaml defn-fun-java \
+        build build-imp build-imp-ocaml build-imp-java build-fun build-fun-ocaml build-fun-java \
+        test test-imp test-fun
 
 all: build
 
 clean:
 	rm -rf $(build_dir)
+	git submodule update --init --recursive
 
-# Dependencies
-# ------------
+# Build Dependencies (K Submodule)
+# --------------------------------
 
-deps: deps-k deps-ocaml deps-tangle
-deps-k: $(k_submodule)/make.timestamp
-deps-tangle: $(pandoc_tangle_submodule)/make.timestamp
+deps: $(k_submodule)/make.timestamp $(pandoc_tangle_submodule)/make.timestamp ocaml-deps
 
 $(k_submodule)/make.timestamp:
-	git submodule update --init -- $(k_submodule)
-	cd $(k_submodule) \
-		&& mvn package -q -DskipTests
+	git submodule update --init --recursive
+	cd $(k_submodule) && mvn package -DskipTests -Dllvm.backend.skip
 	touch $(k_submodule)/make.timestamp
 
 $(pandoc_tangle_submodule)/make.timestamp:
 	git submodule update --init -- $(pandoc_tangle_submodule)
 	touch $(pandoc_tangle_submodule)/make.timestamp
 
-deps-ocaml:
-	opam init --quiet --no-setup
-	opam repository add k "$(k_submodule)/k-distribution/target/release/k/lib/opam" \
-	    || opam repository set-url k "$(k_submodule)/k-distribution/target/release/k/lib/opam"
-	opam update
-	opam switch 4.06.1+k
+ocaml-deps:
 	eval $$(opam config env) \
-	    opam install --yes mlgmp zarith uuidm ocaml-protoc rlp yojson hex ocp-ocamlres
+	    opam install --yes mlgmp zarith uuidm
+
+# Building Definition
+# -------------------
+
+imp_defn_dir:=$(defn_dir)/imp
+imp_krun_files:=imp.k
+imp_kcompile_files:=kat-imp.k kat.k imp.k
+
+imp_ocaml_dir:=$(imp_defn_dir)/ocaml
+imp_ocaml_defn:=$(patsubst %, $(imp_ocaml_dir)/%, $(imp_krun_files))
+imp_ocaml_kompiled:=$(imp_ocaml_dir)/imp-kompiled/interpreter
 
-# Build definition
-# ----------------
+imp_java_dir:=$(imp_defn_dir)/java
+imp_java_defn:=$(patsubst %, $(imp_java_dir)/%, $(imp_kcompile_files))
+imp_java_kompiled:=$(imp_java_dir)/kat-imp-kompiled/compiled.txt
 
-imp_dir=$(defn_dir)/imp
-imp_kcompile_files:=$(patsubst %, $(imp_dir)/kcompile/%, kat-imp.k kat.k imp.k)
-imp_krun_files:=$(patsubst %, $(imp_dir)/krun/%, imp.k)
+fun_defn_dir:=$(defn_dir)/fun
+fun_krun_files:=fun.k
+fun_kcompile_files:=kat-fun.k kat.k fun.k
 
-fun_dir=$(defn_dir)/fun
-fun_kcompile_files:=$(patsubst %, $(fun_dir)/kcompile/%, kat-fun.k kat.k fun.k)
-fun_krun_files:=$(patsubst %, $(fun_dir)/krun/%, fun.k)
+fun_ocaml_dir:=$(fun_defn_dir)/ocaml
+fun_ocaml_defn:=$(patsubst %, $(fun_ocaml_dir)/%, $(fun_krun_files))
+fun_ocaml_kompiled:=$(fun_ocaml_dir)/fun-kompiled/interpreter
+
+fun_java_dir:=$(fun_defn_dir)/java
+fun_java_defn:=$(patsubst %, $(fun_java_dir)/%, $(fun_kcompile_files))
+fun_java_kompiled:=$(fun_java_dir)/kat-fun-kompiled/compiled.txt
+
+# Tangle definition from *.md files
+
+krun_tangler:='.k,.krun'
+kcompile_tangler:='.k,.kcompile'
 
 defn: defn-imp defn-fun
+defn-imp: defn-imp-ocaml defn-imp-java
+defn-fun: defn-fun-ocaml defn-fun-java
 
-defn-imp: defn-imp-kcompile defn-imp-krun
-defn-imp-kcompile: $(imp_kcompile_files)
-defn-imp-krun:     $(imp_krun_files)
+defn-imp-ocaml: $(imp_ocaml_defn)
+defn-imp-java: $(imp_java_defn)
+defn-fun-ocaml: $(fun_ocaml_defn)
+defn-fun-java: $(fun_java_defn)
 
-$(imp_dir)/kcompile/%.k: %.md
-	@echo >&2 "==  tangle: $@"
+$(imp_ocaml_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+	@echo "==  tangle: $@"
 	mkdir -p $(dir $@)
-	$(pandoc) --metadata=code:'.k,.kcompile' $< > $@
+	pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(krun_tangler) $< > $@
 
-$(imp_dir)/krun/%.k: %.md
-	@echo >&2 "==  tangle: $@"
+$(imp_java_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+	@echo "==  tangle: $@"
 	mkdir -p $(dir $@)
-	$(pandoc) --metadata=code:'.k,.krun' $< > $@
+	pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(kcompile_tangler) $< > $@
 
-defn-fun: defn-fun-kcompile defn-fun-krun
-defn-fun-kcompile: $(fun_kcompile_files)
-defn-fun-krun:     $(fun_krun_files)
-
-$(fun_dir)/kcompile/%.k: %.md
-	@echo >&2 "==  tangle: $@"
+$(fun_ocaml_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+	@echo "==  tangle: $@"
 	mkdir -p $(dir $@)
-	$(pandoc) --metadata=code:'.k,.kcompile' $< > $@
+	pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(krun_tangler) $< > $@
 
-$(fun_dir)/krun/%.k: %.md
-	@echo >&2 "==  tangle: $@"
+$(fun_java_dir)/%.k: %.md $(pandoc_tangle_submodule)/make.timestamp
+	@echo "==  tangle: $@"
 	mkdir -p $(dir $@)
-	$(pandoc) --metadata=code:'.k,.krun' $< > $@
+	pandoc --from markdown --to markdown --lua-filter=$(tangler) --metadata=code:$(kcompile_tangler) $< > $@
 
-# Backends (for running and compiling)
+# Build definitions
 
 build: build-imp build-fun
+build-imp: build-imp-ocaml build-imp-java
+build-fun: build-fun-ocaml build-fun-java
 
-build-imp: build-imp-kcompile build-imp-krun
-build-imp-kcompile: $(imp_dir)/kcompile/kat-imp-kompiled/timestamp
-build-imp-krun:     $(imp_dir)/krun/imp-kompiled/interpreter
+build-imp-ocaml: $(imp_ocaml_kompiled)
+build-imp-java: $(imp_java_kompiled)
+build-fun-ocaml: $(fun_ocaml_kompiled)
+build-fun-java: $(fun_java_kompiled)
 
-$(imp_dir)/kcompile/kat-imp-kompiled/timestamp: $(imp_kcompile_files)
+$(imp_ocaml_kompiled): $(imp_ocaml_defn)
 	@echo "== kompile: $@"
-	$(kompile) --main-module IMP-ANALYSIS --backend java \
-				 --syntax-module IMP-ANALYSIS $< --directory $(imp_dir)/kcompile
+	eval $$(opam config env)                              \
+	    $(k_bin)/kompile -O3 --non-strict --backend ocaml \
+	    --directory $(imp_ocaml_dir) -I $(imp_ocaml_dir)  \
+	    --main-module IMP --syntax-module IMP $<
 
-$(imp_dir)/krun/imp-kompiled/interpreter: $(imp_krun_files)
+$(imp_java_kompiled): $(imp_java_defn)
 	@echo "== kompile: $@"
-	eval $$(opam config env) \
-		$(kompile) --main-module IMP --backend ocaml \
-					 --syntax-module IMP $< --directory $(imp_dir)/krun
+	$(k_bin)/kompile --backend java                                \
+	    --directory $(imp_java_dir) -I $(imp_java_dir)             \
+	    --main-module IMP-ANALYSIS --syntax-module IMP-ANALYSIS $<
 
-build-fun: build-fun-kcompile build-fun-krun
-build-fun-kcompile: $(fun_dir)/kcompile/kat-fun-kompiled/timestamp
-build-fun-krun:     $(fun_dir)/krun/fun-kompiled/interpreter
-
-$(fun_dir)/kcompile/kat-fun-kompiled/timestamp: $(fun_kcompile_files)
+$(fun_ocaml_kompiled): $(fun_ocaml_defn)
 	@echo "== kompile: $@"
-	eval $$(opam config env) \
-		$(kompile) --main-module FUN-ANALYSIS --backend java \
-				   --syntax-module FUN-UNTYPED-SYNTAX $< --directory $(fun_dir)/kcompile
+	eval $$(opam config env)                                     \
+	    $(k_bin)/kompile -O3 --non-strict --backend ocaml        \
+	    --directory $(fun_ocaml_dir) -I $(fun_ocaml_dir)         \
+	    --main-module FUN-UNTYPED --syntax-module FUN-UNTYPED $<
 
-$(fun_dir)/krun/fun-kompiled/interpreter: $(fun_krun_files)
+$(fun_java_kompiled): $(fun_java_defn)
 	@echo "== kompile: $@"
-	eval $$(opam config env) \
-		$(kompile) --main-module FUN-UNTYPED --backend ocaml \
-				   --syntax-module FUN-UNTYPED-SYNTAX $< --directory $(fun_dir)/krun
+	$(k_bin)/kompile --backend java                                \
+	    --directory $(fun_java_dir) -I $(fun_java_dir)             \
+	    --main-module FUN-ANALYSIS --syntax-module FUN-ANALYSIS $<
 
 # Testing
 # -------
 
+test_dir:=tests
 test_imp_files:=$(wildcard $(test_dir)/imp/*.strat)
 test_fun_files:=$(wildcard $(test_dir)/fun/*.strat)
 

fun.md

@@ -23,16 +23,6 @@ To make it more interesting and to highlight some of K's strengths, FUN includes
 -   Functions declared in `let`/`letrec` binders and declared anonymously can take multiple space-separated arguments.
     In addition, functions can be partially applied to arguments, allowing the function to be evaluated incrementally.
 
-    For example, the following is the reduction sequence of a partially applied anonymous function:
-
-    ```
-       (fun x y -> x) 3
-    => closure(.Map, x y -> x,           .Bindings, .List      ) 3
-    => closure(.Map,   y -> x, x = 3 and .Bindings, ListItem(3))
-    ```
-
-    with store location `L` pointing at the value `3`.
-
 -   Functions can be defined using pattern matching over the available data-types.
     For example, the program
 
@@ -46,6 +36,8 @@ To make it more interesting and to highlight some of K's strengths, FUN includes
     defines a function `max` that calculates the maximum element of a non-empty list, and the function
 
     ```
+    datatype ('a,'b) pair = Pair 'a 'b
+
     letrec ack = fun (Pair 0 n) -> n + 1
                  |   (Pair m 0) -> ack (Pair (m - 1) 1)
                  |   (Pair m n) -> ack (Pair (m - 1) (ack (Pair m (n - 1))))
@@ -104,14 +96,6 @@ Two special names `$x` and `$k` are used in the semantics for desugaring builtin
  // -------------------------------
 ```
 
-### Symbolic Integers
-
-```kcompile
-    syntax Int ::= "symbolicInt" [function]
- // ---------------------------------------
-    rule symbolicInt => ?V:Int
-```
-
 ### Values
 
 Expression constructs will be defined throughtout the syntax module.
@@ -439,11 +423,11 @@ Expressions
     rule <k> V1:Val == V2:Val => V1  ==K V2 ... </k>
     rule <k> V1:Val != V2:Val => V1 =/=K V2 ... </k>
 
-    rule <k>        ! T => notBool(T) ... </k>
-    rule <k> true  && E => E          ... </k>
-    rule <k> false && _ => false      ... </k>
-    rule <k> true  || _ => true       ... </k>
-    rule <k> false || E => E          ... </k>
+    rule <k>        ! T:Bool => notBool(T) ... </k>
+    rule <k> true  && E      => E          ... </k>
+    rule <k> false && _      => false      ... </k>
+    rule <k> true  || _      => true       ... </k>
+    rule <k> false || E      => E          ... </k>
 ```
 
 Lists must be handled carefully, because not every `ClosureVal` should be considered fully evaluated.
@@ -460,10 +444,10 @@ Lists must be handled carefully, because not every `ClosureVal` should be consid
     rule <k> E : ES => E ~> #consTail ES ... </k>
       requires notBool areFullyEvaluated(E : ES)
 
-    rule <k> V ~> #consTail ES => ES ~> #consHead V ... </k>
+    rule <k> V:Val ~> #consTail ES => ES ~> #consHead V ... </k>
       requires isFullyEvaluated(V)
 
-    rule <k> VS ~> #consHead V => V : VS ... </k>
+    rule <k> VS:Vals ~> #consHead V => V : VS ... </k>
       requires areFullyEvaluated(VS)
 ```