Arch/Ubuntu Linux packaging (#398)

* package/PKGBUILD: add packaging file for arch

* INSTALL: add installation instructions for packaging KEVM

* Jenkinsfile: add Deploy stage for building/uploading packages

* .gitignore: update ignored files

* package/debian: packaging setup for ubuntu 18.04

* package/Dockerfile.{arch,ubuntu-bionic}: dockerfiles for building the Arch/Ubuntu packages

* package/{debian,PKGBUILD}: set DESTDIR and INSTALL_PREFIX manually

* Jenkinsfile: only run build/test steps on PRs

* Jenkinsfile: add slack notification on deploy failure

* .gitignore: update ignored dirs

.gitignore

@@ -1,2 +1,6 @@
 /.build/*
 /rustc-*
+/pkg
+/src
+/package/pkg
+/package/src

INSTALL.md

@@ -0,0 +1,67 @@
+Installing Release Builds
+=========================
+
+These instructions explain how to download, install, and build the KEVM packages.
+Current supported systems are:
+
+-   Arch Linux
+-   Ubuntu Bionic (18.04)
+
+Downloading Packages
+--------------------
+
+We release our packages on GitHub, visit the [Releases](https://github.com/kframework/evm-semantics/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 ./kevm_X.Y.Z_amd64_ID.deb
+```
+
+### Arch
+
+Install the package with (`X.Y.Z-V` is version number):
+
+```sh
+sudo pacman -U ./kevm-git-X.Y.Z-V-x86_64.pkg.tar.xz
+```
+
+Building Packages
+-----------------
+
+Make sure to bump the version numbers in the following places:
+
+-   `RELEASE_ID` in `Jenkinsfile`,
+-   `pkgver` in `package/PKGBUILD`, and
+-   version number in `package/debian/changelog`.
+
+If these numbers do not agree, then building the release will not work.
+
+### Ubuntu/Debian
+
+Build the package in by running:
+
+```sh
+cp -r package/debian ./
+dpkg-buildpackage --no-sign
+```
+
+This will throw an error for any build dependencies you're missing, install them with `sudo apt install ...`.
+The `kevm_X.Y.Z_amd64_ID.deb` package will be placed one directory up from the repository root.
+
+### Arch
+
+Build the package with:
+
+```sh
+cd package
+makepkg -s
+```
+
+This will put `kevm-git-X.Y.Z-V-x86_64.pkg.tar.xz` in the current directory.

Jenkinsfile

@@ -1,10 +1,5 @@
 pipeline {
-  agent {
-    dockerfile {
-      additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
-      args '-m 60g'
-    }
-  }
+  agent none
   options {
     ansiColor('xterm')
   }
@@ -17,117 +12,213 @@ pipeline {
         }
       }
     }
-    stage('Dependencies') {
-      steps {
-        sh '''
-          make all-deps -B
-          make split-tests -B
-        '''
-      }
-    }
-    stage('Build') {
-      steps {
-        sh '''
-          make build build-llvm build-haskell build-node -j4 -B
-        '''
+    stage('Build and Test') {
+      when { changeRequest() }
+      agent {
+        dockerfile {
+          additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
+          args '-m 60g'
+        }
       }
-    }
-    stage('Test Execution') {
-      failFast true
-      parallel {
-        stage('Conformance (OCaml)') {
+      stages {
+        stage('Dependencies') {
           steps {
             sh '''
-              nprocs=$(nproc)
-              [ "$nprocs" -gt '16' ] && nprocs='16'
-              make test-conformance -j"$nprocs" TEST_CONCRETE_BACKEND=ocaml
+              make all-deps -B
+              make split-tests -B
             '''
           }
         }
-        stage('Conformance (LLVM)') {
+        stage('Build') {
           steps {
             sh '''
-              nprocs=$(nproc)
-              [ "$nprocs" -gt '16' ] && nprocs='16'
-              make test-conformance -j"$nprocs" TEST_CONCRETE_BACKEND=llvm
+              make build build-llvm build-haskell build-node -j4 -B
             '''
           }
         }
-      }
-    }
-    stage('Test Proofs (Java)') {
-      options {
-        lock("proofs-${env.NODE_NAME}")
-      }
-      steps {
-        sh '''
-          nprocs=$(nproc)
-          [ "$nprocs" -gt '6' ] && nprocs='6'
-          make test-proof -j"$nprocs"
-        '''
-      }
-    }
-    stage('Test Interactive') {
-      failFast true
-      parallel {
-        stage('OCaml krun') {
-          steps {
-            sh '''
-              make test-interactive-run TEST_CONCRETE_BACKEND=ocaml
-            '''
+        stage('Test Execution') {
+          failFast true
+          parallel {
+            stage('Conformance (OCaml)') {
+              steps {
+                sh '''
+                  nprocs=$(nproc)
+                  [ "$nprocs" -gt '16' ] && nprocs='16'
+                  make test-conformance -j"$nprocs" TEST_CONCRETE_BACKEND=ocaml
+                '''
+              }
+            }
+            stage('Conformance (LLVM)') {
+              steps {
+                sh '''
+                  nprocs=$(nproc)
+                  [ "$nprocs" -gt '16' ] && nprocs='16'
+                  make test-conformance -j"$nprocs" TEST_CONCRETE_BACKEND=llvm
+                '''
+              }
+            }
           }
         }
-        stage('LLVM krun') {
-          steps {
-            sh '''
-              make test-interactive-run TEST_CONCRETE_BACKEND=llvm
-            '''
+        stage('Test Proofs (Java)') {
+          options {
+            lock("proofs-${env.NODE_NAME}")
           }
-        }
-        stage('Java krun') {
           steps {
             sh '''
-              make test-interactive-run TEST_CONCRETE_BACKEND=java
+              nprocs=$(nproc)
+              [ "$nprocs" -gt '6' ] && nprocs='6'
+              make test-proof -j"$nprocs"
             '''
           }
         }
-        stage('Haskell krun') {
-          steps {
-            sh '''
-              make test-interactive-run TEST_CONCRETE_BACKEND=haskell
-            '''
+        stage('Test Interactive') {
+          failFast true
+          parallel {
+            stage('OCaml krun') {
+              steps {
+                sh '''
+                  make test-interactive-run TEST_CONCRETE_BACKEND=ocaml
+                '''
+              }
+            }
+            stage('LLVM krun') {
+              steps {
+                sh '''
+                  make test-interactive-run TEST_CONCRETE_BACKEND=llvm
+                '''
+              }
+            }
+            stage('Java krun') {
+              steps {
+                sh '''
+                  make test-interactive-run TEST_CONCRETE_BACKEND=java
+                '''
+              }
+            }
+            stage('Haskell krun') {
+              steps {
+                sh '''
+                  make test-interactive-run TEST_CONCRETE_BACKEND=haskell
+                '''
+              }
+            }
+            stage('OCaml kast') {
+              steps {
+                sh '''
+                  make test-parse TEST_CONCRETE_BACKEND=ocaml
+                '''
+              }
+            }
+            stage('Failing tests') {
+              steps {
+                sh '''
+                  make test-failure TEST_CONCRETE_BACKEND=ocaml
+                  make test-failure TEST_CONCRETE_BACKEND=llvm
+                '''
+              }
+            }
+            stage('Java KLab') {
+              steps {
+                sh '''
+                  make test-klab-prove TEST_SYMBOLIC_BACKEND=java
+                '''
+              }
+            }
+            stage('KEVM help') {
+              steps {
+                sh '''
+                  ./kevm help
+                '''
+              }
+            }
           }
         }
-        stage('OCaml kast') {
-          steps {
-            sh '''
-              make test-parse TEST_CONCRETE_BACKEND=ocaml
-            '''
-          }
+      }
+    }
+    stage('Deploy') {
+      when {
+        not { changeRequest() }
+        branch 'master'
+        beforeAgent true
+      }
+      agent { label 'docker' }
+      options { skipDefaultCheckout() }
+      environment {
+        GITHUB_TOKEN = credentials('rv-jenkins')
+        RELEASE_ID   = '1.0.0'
+      }
+      stages {
+        stage('Checkout SCM') {
+          steps { dir("kevm-${env.RELEASE_ID}") { checkout scm } }
         }
-        stage('Failing tests') {
+        stage('Build Ubuntu Package') {
+          agent {
+            dockerfile {
+              dir "kevm-${env.RELEASE_ID}/package"
+              filename 'Dockerfile.ubuntu-bionic'
+              reuseNode true
+            }
+          }
           steps {
-            sh '''
-              make test-failure TEST_CONCRETE_BACKEND=ocaml
-              make test-failure TEST_CONCRETE_BACKEND=llvm
-            '''
+            dir("kevm-${env.RELEASE_ID}") {
+              sh '''
+                sudo apt update && sudo apt upgrade --yes
+                cp -r package/debian ./
+                dpkg-buildpackage --no-sign
+              '''
+            }
+            stash name: 'bionic', includes: "kevm_${env.RELEASE_ID}_amd64.deb"
           }
         }
-        stage('Java KLab') {
+        stage('Build Arch Package') {
+          agent {
+            dockerfile {
+              dir "kevm-${env.RELEASE_ID}/package"
+              filename 'Dockerfile.arch'
+              additionalBuildArgs '--build-arg USER_ID=$(id -u) --build-arg GROUP_ID=$(id -g)'
+              reuseNode true
+            }
+          }
           steps {
-            sh '''
-              make test-klab-prove TEST_SYMBOLIC_BACKEND=java
-            '''
+            dir("kevm-${env.RELEASE_ID}") {
+              sh '''
+                sudo pacman -Syu
+                cd package
+                makepkg --noconfirm --syncdeps
+              '''
+            }
+            stash name: 'arch', includes: "kevm-${env.RELEASE_ID}/package/kevm-git-${env.RELEASE_ID}-1-x86_64.pkg.tar.xz"
           }
         }
-        stage('KEVM help') {
+        stage('Upload Packages') {
+          agent {
+            dockerfile {
+              dir 'package'
+              filename 'Dockerfile.arch'
+              reuseNode true
+            }
+          }
           steps {
+            unstash 'bionic'
+            unstash 'arch'
             sh '''
-              ./kevm help
+              git_commit=$(cd kevm-$RELEASE_ID && git rev-parse --short HEAD)
+              hub release create                                                                                            \
+                  --attach "kevm_${RELEASE_ID}_amd64.deb#Ubuntu Bionic (18.04) Package"                                     \
+                  --attach "kevm-${RELEASE_ID}/package/kevm-git-${RELEASE_ID}-1-x86_64.pkg.tar.xz#Arch Package"             \
+                  --message "$(echo -e "KEVM Release $RELEASE_ID - $git_commit\n\n" ; cat kevm-${RELEASE_ID}/INSTALL.md ;)" \
+                  --commitish $(git rev-parse HEAD) "v$RELEASE_ID-$git_commit"
             '''
           }
         }
       }
+      post {
+        failure {
+          slackSend color: '#cb2431'                                   \
+                  , channel: '#kevm'                                   \
+                  , message: "KEVM Packaging Failed: ${env.BUILD_URL}"
+        }
+      }
     }
   }
 }

package/Dockerfile.arch

@@ -0,0 +1,13 @@
+FROM archlinux/base
+
+RUN    pacman -Syu --noconfirm \
+    && pacman -S   --noconfirm git hub sudo
+
+ADD https://github.com/kframework/k/releases/download/nightly-89361d7c8/kframework-5.0.0-1-x86_64.pkg.tar.xz kframework_5.0.0-1_x86_64.pkg.tar.xz
+RUN pacman --noconfirm -U ./kframework_5.0.0-1_x86_64.pkg.tar.xz
+
+ARG USER_ID=1000
+ARG GROUP_ID=1000
+RUN    groupadd -g $GROUP_ID user                                                \
+    && useradd --create-home --uid $USER_ID --shell /bin/sh --gid $GROUP_ID user \
+    && echo "user ALL=(ALL) NOPASSWD:ALL" >> /etc/sudoers