Update boogie PKGBUILD

4 files changed, 100 insertions, 0 deletions

diff --git a/.SRCINFO b/.SRCINFO
new file mode 100644
index 000000000000..256968d23f22
--- /dev/null
+++ b/.SRCINFO
@@ -0,0 +1,21 @@
+pkgbase = boogie-git
+	pkgdesc = Boogie is an Intermediate Verification Language (IVL) for describing proof obligations to be discharged by a reasoning engine, typically an SMT solver
+	pkgver = 0.r4273.bad6c01
+	pkgrel = 1
+	url = http://boogie.codeplex.com
+	arch = any
+	license = custom: Ms-Pl
+	makedepends = mercurial
+	makedepends = wget
+	depends = z3-git
+	depends = mono
+	provides = boogie
+	conflicts = boogie
+	source = boogie-git::git+https://github.com/boogie-org/boogie.git
+	source = execute_boogie.sh
+	source = license.txt
+	md5sums = SKIP
+	md5sums = 3c484f49455c24eb8984461b9d78d45f
+	md5sums = ab2e2e62d9befcc932895745749d4a54
+
+pkgname = boogie-git
diff --git a/PKGBUILD b/PKGBUILD
new file mode 100644
index 000000000000..2b56b08337be
--- /dev/null
+++ b/PKGBUILD
@@ -0,0 +1,46 @@
+# Maintainer: Florian Hahn <flo@fhahn.com>
+
+pkgname=boogie-git
+pkgdesc='Boogie is an Intermediate Verification Language (IVL) for describing proof obligations to be discharged by a 
+reasoning engine, typically an SMT solver'
+license=('custom: Ms-Pl')
+pkgver=0.r4273.bad6c01
+pkgrel=1
+depends=('z3-git' 'mono')
+makedepends=('mercurial' 'wget')
+conflicts=('boogie')
+provides=('boogie')
+arch=('any')
+url=('http://boogie.codeplex.com')
+source=("$pkgname"::'git+https://github.com/boogie-org/boogie.git'
+        execute_boogie.sh
+        license.txt)
+md5sums=('SKIP'
+         '3c484f49455c24eb8984461b9d78d45f'
+         'ab2e2e62d9befcc932895745749d4a54')
+
+
+pkgver() {
+    cd "$pkgname"
+    printf "0.r%s.%s" "$(git rev-list --count HEAD)" "$(git rev-parse --short HEAD)"
+}
+
+build() {
+    cd "${srcdir}/${pkgname}/"
+    wget https://nuget.org/nuget.exe
+    mono ./nuget.exe restore Source/Boogie.sln
+    xbuild Source/Boogie.sln
+}
+
+package() {
+    install -Dm755 execute_boogie.sh "${pkgdir}/usr/bin/boogie"
+    install -Dm644 license.txt "${pkgdir}/usr/share/licenses/boogie/LICENSE"
+    cd "${srcdir}/${pkgname}/Binaries"
+
+    # install dll and exe files
+    for dll in $(ls *.dll *.exe)
+    do
+        install -Dm644 "$dll" "${pkgdir}/usr/lib/boogie/$dll"
+    done
+    ln -s /usr/bin/z3 "${pkgdir}/usr/lib/boogie/z3.exe"
+}
diff --git a/execute_boogie.sh b/execute_boogie.sh
new file mode 100644
index 000000000000..d490257be1ad
--- /dev/null
+++ b/execute_boogie.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+mono /usr/lib/boogie/Boogie.exe $@
diff --git a/license.txt b/license.txt
new file mode 100644
index 000000000000..e12bbfb0abab
--- /dev/null
+++ b/license.txt
@@ -0,0 +1,31 @@
+Microsoft Public License (Ms-PL)
+
+This license governs use of the accompanying software. If you use the software, you accept this license. If you do not accept the license, do not use the software.
+
+1. Definitions
+
+The terms "reproduce," "reproduction," "derivative works," and "distribution" have the same meaning here as under U.S. copyright law.
+
+A "contribution" is the original software, or any additions or changes to the software.
+
+A "contributor" is any person that distributes its contribution under this license.
+
+"Licensed patents" are a contributor's patent claims that read directly on its contribution.
+
+2. Grant of Rights
+
+(A) Copyright Grant- Subject to the terms of this license, including the license conditions and limitations in section 3, each contributor grants you a non-exclusive, worldwide, royalty-free copyright license to reproduce its contribution, prepare derivative works of its contribution, and distribute its contribution or any derivative works that you create.
+
+(B) Patent Grant- Subject to the terms of this license, including the license conditions and limitations in section 3, each contributor grants you a non-exclusive, worldwide, royalty-free license under its licensed patents to make, have made, use, sell, offer for sale, import, and/or otherwise dispose of its contribution in the software or derivative works of the contribution in the software.
+
+3. Conditions and Limitations
+
+(A) No Trademark License- This license does not grant you rights to use any contributors' name, logo, or trademarks.
+
+(B) If you bring a patent claim against any contributor over patents that you claim are infringed by the software, your patent license from such contributor to the software ends automatically.
+
+(C) If you distribute any portion of the software, you must retain all copyright, patent, trademark, and attribution notices that are present in the software.
+
+(D) If you distribute any portion of the software in source code form, you may do so only under this license by including a complete copy of this license with your distribution. If you distribute any portion of the software in compiled or object code form, you may only do so under a license that complies with this license.
+
+(E) The software is licensed "as-is." You bear the risk of using it. The contributors give no express warranties, guarantees or conditions. You may have additional consumer rights under your local laws which this license cannot change. To the extent permitted under your local laws, the contributors exclude the implied warranties of merchantability, fitness for a particular purpose and non-infringement.