From 3c5818f34339a8a3660d904000b207d1f63ae805 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Fri, 1 Apr 2016 16:16:27 -0400 Subject: Package Boogie library for experimental --- debian/changelog | 7 ++++ debian/compat | 1 + debian/control | 23 +++++++++++ debian/copyright | 91 ++++++++++++++++++++++++++++++++++++++++++++ debian/libboogie-cil.docs | 1 + debian/libboogie-cil.install | 1 + debian/rules | 9 +++++ debian/source/format | 1 + debian/watch | 4 ++ 9 files changed, 138 insertions(+) create mode 100644 debian/changelog create mode 100644 debian/compat create mode 100644 debian/control create mode 100644 debian/copyright create mode 100644 debian/libboogie-cil.docs create mode 100644 debian/libboogie-cil.install create mode 100755 debian/rules create mode 100644 debian/source/format create mode 100644 debian/watch diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 00000000..5da141aa --- /dev/null +++ b/debian/changelog @@ -0,0 +1,7 @@ +boogie (2.3.0.61016+dfsg+1.gbp64e8b3-1) experimental; urgency=medium + + ** SNAPSHOT build @64e8b33656140b87137d0662d9e6835e004d13c2 ** + + * Initial release. + + -- Benjamin Barenblat Fri, 01 Apr 2016 12:47:14 -0400 diff --git a/debian/compat b/debian/compat new file mode 100644 index 00000000..ec635144 --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +9 diff --git a/debian/control b/debian/control new file mode 100644 index 00000000..809936b5 --- /dev/null +++ b/debian/control @@ -0,0 +1,23 @@ +Source: boogie +Section: cli-mono +Priority: extra +Maintainer: Benjamin Barenblat +Build-Depends: + debhelper (>= 9), +Build-Depends-Indep: + cli-common-dev (>= 0.8), + mono-devel (>= 2.4.2.3), + mono-reference-assemblies-4.0, +Standards-Version: 3.9.7 +Homepage: http://research.microsoft.com/en-us/projects/boogie/ + +Package: libboogie-cil +Architecture: all +Depends: ${cli:Depends}, ${misc:Depends} +Description: verifiable programming language + Boogie is a compiler intermediate language with support for automatic invariant + checking using an SMT solver such as Z3. It supports program verification for + a variety of other, higher-level languages, including Spec\#, C, Dafny, and + Chalice. + . + This package contains the Boogie library. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 00000000..bfb67254 --- /dev/null +++ b/debian/copyright @@ -0,0 +1,91 @@ +Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: Boogie +Upstream-Contact: boogie-dev@imperial.ac.uk +Source: https://github.com/boogie-org/boogie +Copyright: 2003-2014 Microsoft +License: Ms-PL + +Files: * +Copyright: 2009-2015 Microsoft Corporation +License: Ms-PL + +Files: debian/* +Copyright: 2015-2016 Benjamin Barenblat +License: Apache-2.0 + +License: Apache-2.0 + Licensed under the Apache License, Version 2.0 (the "License"); you may not use + this file except in compliance with the License. You may obtain a copy of the + License at + . + http://www.apache.org/licenses/LICENSE-2.0 + . + Unless required by applicable law or agreed to in writing, software distributed + under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR + CONDITIONS OF ANY KIND, either express or implied. See the License for the + specific language governing permissions and limitations under the License. + . + On Debian systems, the complete text of the Apache License, Version 2.0, can be + found in "/usr/share/common-licenses/Apache-2.0". + +License: Ms-PL + 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. diff --git a/debian/libboogie-cil.docs b/debian/libboogie-cil.docs new file mode 100644 index 00000000..b43bf86b --- /dev/null +++ b/debian/libboogie-cil.docs @@ -0,0 +1 @@ +README.md diff --git a/debian/libboogie-cil.install b/debian/libboogie-cil.install new file mode 100644 index 00000000..77207bb6 --- /dev/null +++ b/debian/libboogie-cil.install @@ -0,0 +1 @@ +Binaries/*.dll /usr/lib/boogie diff --git a/debian/rules b/debian/rules new file mode 100755 index 00000000..03c5f4e3 --- /dev/null +++ b/debian/rules @@ -0,0 +1,9 @@ +#!/usr/bin/make -f +# -*- makefile -*- + +%: + dh $@ --with cli + +.PHONY: override_dh_auto_build +override_dh_auto_build: + xbuild Source/Boogie.sln diff --git a/debian/source/format b/debian/source/format new file mode 100644 index 00000000..163aaf8d --- /dev/null +++ b/debian/source/format @@ -0,0 +1 @@ +3.0 (quilt) diff --git a/debian/watch b/debian/watch new file mode 100644 index 00000000..6416e51b --- /dev/null +++ b/debian/watch @@ -0,0 +1,4 @@ +# Upstream does not cut releases at this point – only Git snapshots. +# Consequently, constructing a suitable watch file is impossible. +# +# -- Benjamin Barenblat Tue 11 Aug 2015 19:27:24 -0400 -- cgit v1.2.3