summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2016-04-01 16:16:27 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2016-04-01 16:16:27 -0400
commit3c5818f34339a8a3660d904000b207d1f63ae805 (patch)
tree636859571747ad89a71b4dfacf830d40d409eda2
parent64e8b33656140b87137d0662d9e6835e004d13c2 (diff)
Package Boogie library for experimental
-rw-r--r--debian/changelog7
-rw-r--r--debian/compat1
-rw-r--r--debian/control23
-rw-r--r--debian/copyright91
-rw-r--r--debian/libboogie-cil.docs1
-rw-r--r--debian/libboogie-cil.install1
-rwxr-xr-xdebian/rules9
-rw-r--r--debian/source/format1
-rw-r--r--debian/watch4
9 files changed, 138 insertions, 0 deletions
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 <bbaren@mit.edu> 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 <bbaren@mit.edu>
+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 <bbaren@mit.edu>
+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 <bbaren@mit.edu> Tue 11 Aug 2015 19:27:24 -0400