diff --git a/.gitignore b/.gitignore
index b3ed51d21b2..f1e1ae3e43a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,4 +22,7 @@ junit-reports
 target/
 kore/doc
 __pycache__
-rustc-*-src
+/rustc-*
+/.cargo
+/.rustup
+/pkg
diff --git a/Dockerfile.debian b/Dockerfile.debian
index 3f65e2ea6ff..7e356976355 100644
--- a/Dockerfile.debian
+++ b/Dockerfile.debian
@@ -4,10 +4,10 @@ ARG BASE_IMAGE
 
 RUN if [ "$BASE_IMAGE" = "debian:stretch" ]; then echo "Enabling backports..."; echo "deb http://ftp.debian.org/debian stretch-backports main" > /etc/apt/sources.list.d/stretch-backports.list; fi
 RUN apt-get update && \
-    apt-get install -y git debhelper maven openjdk-8-jdk cmake libboost-test-dev libyaml-dev libjemalloc-dev flex bison clang-8 llvm-8-tools lld-8 zlib1g-dev libgmp-dev libmpfr-dev gcc z3 libz3-dev opam pkg-config curl python3
+    apt-get install -y git debhelper maven openjdk-8-jdk cmake libboost-test-dev libyaml-dev libjemalloc-dev flex bison clang-8 llvm-8-tools lld-8 zlib1g-dev libgmp-dev libmpfr-dev gcc z3 libz3-dev opam pkg-config curl python3 haskell-stack
 RUN update-alternatives --set java /usr/lib/jvm/java-8-openjdk-amd64/jre/bin/java
 ENV JAVA_HOME=/usr/lib/jvm/java-8-openjdk-amd64/
-RUN curl -sSL https://get.haskellstack.org/ | sh      
+RUN curl -sSL https://get.haskellstack.org/ | sh -s - -f
 
 ARG USER_ID=1000
 ARG GROUP_ID=1000
diff --git a/INSTALL.md b/INSTALL.md
new file mode 100644
index 00000000000..c8977312596
--- /dev/null
+++ b/INSTALL.md
@@ -0,0 +1,78 @@
+Installing Release Builds
+=========================
+
+These instructions explain how to download, install, and build the K packages.
+Current supported systems are:
+
+-   Arch Linux
+-   Ubuntu Bionic (18.04)
+-   Ubuntu Xenial (16.04)
+-   Debian Stretch
+
+Downloading Packages
+--------------------
+
+We release our packages on GitHub, visit the [Releases](https://github.com/kframework/k/releases) page to see available versions.
+Releases are generated as often as possible from the `master` branch of the repository.
+
+Installing Packages
+-------------------
+
+### Ubuntu/Debian
+
+Install the package with (`X.Y.Z` is version number, `ID` is platform identifier):
+
+```sh
+sudo apt install ./kframework_X.Y.Z_amd64_ID.deb
+```
+
+On Debian Stretch, you also must first enable stretch-backports by running:
+
+```sh
+sudo echo "deb http://ftp.debian.org/debian stretch-backports main" > /etc/apt/sources.list.d/stretch-backports.list
+sudo apt-get update.
+```
+
+### Arch
+
+Install the package with (`X.Y.Z-V` is version number):
+
+```sh
+sudo pacman -U ./kframework-git-X.Y.Z-V-x86_64.pkg.tar.xz
+```
+
+### Windows
+
+On Windows, start by installing Windows Subsystem for Linux with Ubuntu (or an Ubuntu VM), after which you can install like Ubuntu.
+K requires gcc and other Linux libraries to run, and building on native Windows, Cygwin, or MINGW is not supported
+
+### Other
+
+If your OS is not supported, you can download and extract the "Platform-Independent K binary", and follow the instructions in INSTALL.md within the target directory.
+Note however that this will not support the Haskell or LLVM Backends.
+
+Building Packages
+-----------------
+
+Update `stack` with `sudo stack upgrade` or `curl -sSL https://get.haskellstack.org/ | sh -s - -f` to make sure you have the newest version (> 2.0).
+
+### Ubuntu/Debian
+
+Build the package in by running:
+
+```sh
+dpkg-buildpackage --no-sign
+```
+
+This will throw an error for any build dependencies you're missing, install them with `sudo apt install ...`.
+The `kframework_X.Y.Z_amd64_ID.deb` package will be placed one directory up from the repository root.
+
+### Arch
+
+Build the package with:
+
+```sh
+makepkg -s
+```
+
+This will put `kframework-git-X.Y.Z-V-x86_64.pkg.tar.xz` in the current directory.
diff --git a/PKGBUILD b/PKGBUILD
index 277092333e7..f1ecd6edd2c 100644
--- a/PKGBUILD
+++ b/PKGBUILD
@@ -1,15 +1,15 @@
 # Maintainer: Dwight Guth <dwight.guth@runtimeverification.com>
-pkgname=kframework
+pkgname=kframework-git
 pkgver=5.0.0
 pkgrel=1
 epoch=
-pkgdesc="K framework toolchain. Includes K Framework compiler for K language definitions, and K interpreter and prover for programs written in languages defined in K."
+pkgdesc='K framework toolchain. Includes K Framework compiler for K language definitions, and K interpreter and prover for programs written in languages defined in K.'
 arch=('x86_64')
-url="https://github.com/kframework/k"
+url='https://github.com/kframework/k'
 license=('custom')
 groups=()
 depends=('java-runtime' 'flex' 'gcc' 'gmp' 'mpfr' 'z3' 'clang' 'libyaml' 'jemalloc' 'opam' 'gawk' 'make' 'diffutils' 'patch' 'tar' 'grep' 'llvm' 'lld')
-makedepends=('maven' 'jdk-openjdk' 'cmake' 'boost' 'zlib')
+makedepends=('maven' 'jdk8-openjdk' 'cmake' 'boost' 'zlib' 'stack' 'pkg-config' 'bison' 'python' 'fakeroot')
 checkdepends=()
 optdepends=()
 provides=()
@@ -17,28 +17,27 @@ conflicts=()
 replaces=()
 backup=()
 options=(!strip)
-install=kframework.install
+install=kframework-git.install
 changelog=
-source=()
+source=('git+https://github.com/kframework/k#branch=master')
 noextract=()
-md5sums=()
+md5sums=('SKIP')
 validpgpkeys=()
 
 prepare() {
-	true
+    cd "$srcdir/k"
+    git submodule update --init --recursive
+    ./llvm-backend/src/main/native/llvm-backend/install-rust
 }
 
 build() {
-	cd ..
-	mvn package -DskipTests
-}
-
-check() {
-	true
+    export PATH="${CARGO_HOME:-$HOME/.cargo}/bin:$PATH"
+    cd "$srcdir/k"
+    mvn package -DskipTests
 }
 
 package() {
-	cd ..
-	DESTDIR="$pkgdir/usr/" src/main/scripts/package
-	install -Dm644 LICENSE.md "$pkgdir/usr/share/licenses/$pkgname/LICENSE"
+    cd "$srcdir/k"
+    DESTDIR="$pkgdir/usr/" src/main/scripts/package
+    install -Dm644 LICENSE.md "$pkgdir/usr/share/licenses/$pkgname/LICENSE"
 }
diff --git a/debian/control b/debian/control
index c9282cdf7d5..ed5522e5f57 100644
--- a/debian/control
+++ b/debian/control
@@ -2,7 +2,7 @@ Source: kframework
 Section: devel
 Priority: optional
 Maintainer: Dwight Guth <dwight.guth@runtimeverification.com>
-Build-Depends: debhelper (>=9), maven, openjdk-8-jdk, cmake, libboost-test-dev, libyaml-dev, libjemalloc-dev, flex, bison, clang-8, zlib1g-dev, libgmp-dev, libmpfr-dev
+Build-Depends: debhelper (>=9), maven, openjdk-8-jdk, cmake, libboost-test-dev, libyaml-dev, libjemalloc-dev, flex, bison, clang-8, zlib1g-dev, libgmp-dev, libmpfr-dev, pkg-config, llvm-8-tools, haskell-stack
 Standards-Version: 3.9.6
 Homepage: https://github.com/kframework/k
 
diff --git a/debian/rules b/debian/rules
index 3dd32eeadb9..c2cc0f01c19 100755
--- a/debian/rules
+++ b/debian/rules
@@ -13,11 +13,15 @@
 # package maintainers to append LDFLAGS
 #export DEB_LDFLAGS_MAINT_APPEND = -Wl,--as-needed
 
+CARGO_HOME?=$(HOME)/.cargo
+export CARGO_HOME
 
 %:
-	dh $@ 
+	dh $@
 
 override_dh_auto_build:
+	git submodule update --init --recursive
+	./llvm-backend/src/main/native/llvm-backend/install-rust
 	mvn package -DskipTests
 
 override_dh_auto_install:
diff --git a/kframework.install b/kframework-git.install
similarity index 100%
rename from kframework.install
rename to kframework-git.install