From 19a85de4b442ec8fe91ef091d17e21ede67a6755 Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 5 Sep 2015 14:32:48 -0400 Subject: Start packaging Dwarf Fortress --- debian/.gitignore | 7 + debian/bin/dwarf-fortress | 55 +++ debian/changelog | 5 + debian/compat | 1 + debian/control | 32 ++ debian/control~ | 94 +++++ debian/copyright | 106 +++++ debian/copyright~ | 50 +++ debian/docs | 5 + debian/dwarf-fortress.6 | 55 +++ debian/dwarf-fortress.6~ | 903 +++++++++++++++++++++++++++++++++++++++++ debian/dwarf-fortress.links | 2 + debian/dwarf-fortress.manpages | 1 + debian/install | 8 + debian/menu | 2 + debian/rules | 31 ++ debian/source/format | 1 + debian/watch | 2 + 18 files changed, 1360 insertions(+) create mode 100644 debian/.gitignore create mode 100644 debian/bin/dwarf-fortress create mode 100644 debian/changelog create mode 100644 debian/compat create mode 100644 debian/control create mode 100644 debian/control~ create mode 100644 debian/copyright create mode 100644 debian/copyright~ create mode 100644 debian/docs create mode 100644 debian/dwarf-fortress.6 create mode 100644 debian/dwarf-fortress.6~ create mode 100644 debian/dwarf-fortress.links create mode 100644 debian/dwarf-fortress.manpages create mode 100644 debian/install create mode 100644 debian/menu create mode 100755 debian/rules create mode 100644 debian/source/format create mode 100644 debian/watch diff --git a/debian/.gitignore b/debian/.gitignore new file mode 100644 index 0000000..5ad5207 --- /dev/null +++ b/debian/.gitignore @@ -0,0 +1,7 @@ +# -*- conf -*- + +# Editor backup files +*~ +\#* +.\#* +.*.swp diff --git a/debian/bin/dwarf-fortress b/debian/bin/dwarf-fortress new file mode 100644 index 0000000..2afbcfa --- /dev/null +++ b/debian/bin/dwarf-fortress @@ -0,0 +1,55 @@ +#!/bin/bash -eu +# +# Debian Dwarf Fortress launcher +# © 2012 Beren Minor +# © 2015 Benjamin Barenblat +# +# This program is free software; you can redistribute it and/or modify it under +# the terms of the GNU General Public License as published by the Free Software +# Foundation; either version 3 of the License, or (at your option) any later +# version. +# +# This program is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +# FOR A PARTICULAR PURPOSE. See the GNU General Public License for more +# details. +# +# You should have received a copy of the GNU General Public License along with +# this program. If not, see +# +# On Debian systems, the complete text of the GNU General Public License version +# 3 can be found in "/usr/share/common-licenses/GPL-3". +# +# +# This script adapts Dwarf Fortress to run out of tree by staging its files into +# a temporary directory, symlinking in the user’s save files, and launching. + +# User configuration: This environment variable controls where user saves and +# movies will be stored. It defaults to ~/.local/share/dwarf-fortress. +declare -r DWARF_FORTRESS_DATA_HOME="${DWARF_FORTRESS_DATA_HOME:-${XDG_DATA_HOME:-$HOME/.local/share}/dwarf-fortress}" + + +declare -r DF="/usr/lib/games/dwarf-fortress" + +# Create a directory to stage Dwarf Fortress in. +declare -r TMP="$(mktemp --directory --tmpdir dwarf-fortress.XXXXXXXXXX)" +trap "rm -rf \"$TMP\"" EXIT + +# Stage the game files. +cp -r --dereference --symbolic-link "$DF"/* "$TMP" + +# Actually copy the data/index file, because Dwarf Fortress gets unhappy if it’s +# a symlink. +rm "$TMP"/data/index +cp -r --dereference --reflink=auto "$DF"/data/index "$TMP"/data + +# Link in the user’s save and movies files. +mkdir -p "$DWARF_FORTRESS_DATA_HOME"/movies +mkdir -p "$DWARF_FORTRESS_DATA_HOME"/save +ln -s "$DWARF_FORTRESS_DATA_HOME"/movies "$TMP"/data +ln -s "$DWARF_FORTRESS_DATA_HOME"/save "$TMP"/data + +# Start Dwarf Fortress! +echo "User data is $DWARF_FORTRESS_DATA_HOME" +echo "wd is $TMP" +"$TMP"/df "$@" diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 0000000..0559658 --- /dev/null +++ b/debian/changelog @@ -0,0 +1,5 @@ +dwarf-fortress (0.40.24-1) UNRELEASED; urgency=low + + * Initial release (Closes: #588377) + + -- Benjamin Barenblat Sat, 05 Sep 2015 09:37:23 -0400 diff --git a/debian/compat b/debian/compat new file mode 100644 index 0000000..ec63514 --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +9 diff --git a/debian/control b/debian/control new file mode 100644 index 0000000..a8d16a3 --- /dev/null +++ b/debian/control @@ -0,0 +1,32 @@ +Source: dwarf-fortress +Section: non-free/games +Priority: optional +Maintainer: Benjamin Barenblat +Build-Depends: + debhelper (>= 9), + libgl1-mesa-glx | libgl1, + libglu1-mesa | libglu1, + libgtk2.0-0, + libsdl1.2debian, + libsdl-image1.2, + libsdl-ttf2.0-0 +Standards-Version: 3.9.6 +Homepage: http://www.bay12games.com/dwarves/ +Vcs-Git: git://benjamin.barenblat.name/debian-dwarf-fortress.git +Vcs-Browser: https://benjamin.barenblat.name/gitweb/?p=debian-dwarf-fortress.git;a=summary + +Package: dwarf-fortress +Architecture: i386 +Depends: ${shlibs:Depends}, ${misc:Depends} +Description: control a band of dwarves as they establish a new outpost + Slaves to Armok: God of Blood Chapter II: Dwarf Fortress is an absurdly + detailed indie roguelike which takes place in a massive, procedurally + generated, open world. Take command of a band of dwarves, guiding them as they + mine, farm, and defend a new home, or become an adventurer and seek your + fortune. + . + World detail cannot be underestimated. History, NPC behaviors, terrain, + weather, mineral deposits, and much more are generated anew by Dwarf Fortress’s + engine before the game begins and rendered in excruciating detail using an + extended ASCII character set drawn with OpenGL. New features are added all the + time. diff --git a/debian/control~ b/debian/control~ new file mode 100644 index 0000000..7226a7d --- /dev/null +++ b/debian/control~ @@ -0,0 +1,94 @@ +Source: dwarf-fortress +Section: non-free/games +Priority: optional +Maintainer: Benjamin Barenblat +Build-Depends: + debhelper (>= 9) +Standards-Version: 3.9.6 +Homepage: http://www.bay12games.com/dwarves/ +Vcs-Git: git://benjamin.barenblat.name/debian-dwarf-fortress.git +Vcs-Browser: https://benjamin.barenblat.name/gitweb/?p=debian-dwarf-fortress.git;a=summary + +Package: dwarf-fortress +Architecture: i386 +Depends: ${shlibs:Depends}, ${misc:Depends} +Description: control a band of dwarves as they establish a new outpost + Slaves to Armok: God of Blood Chapter II: Dwarf Fortress is an absurdly + detailed indie roguelike in which players control a dwarven outpost or an + adventurer in a randomly generated, persistent world. + . + Although Dwarf Fortress is still in a work in progress, many features have + already been implemented. + . + • The world is randomly generated with distinct civilizations spanning + centuries of detailed history, hundreds of towns, caves and regions with + various wildlife. + . + • The world persists as long as you like, over many games, recording + historical events and tracking changes. + . + • Command your dwarves as they search for wealth in the mountain. + ◦ Craft treasures and furniture from many materials and improve these + objects with precious metals, jewels and more. + ◦ Defend yourself against attacks from hostile civilizations, the + wilderness, the depths, the dead and creatures of the night. + ◦ Trade for all manner of exotic goods with your neighbors. + ◦ Establish a barony and support the nobility as they make demands of + your populace. + ◦ Keep your dwarves happy and read their thoughts as they work and relax. + ◦ Z coordinate allows you to dig out fortresses with multiple levels. + Build towers or conquer the underworld. + ◦ Build floodgates to divert water for farming or to drown your + adversaries … and don’t forget the magma! + ◦ Surgery, sutures, splints, crutches and more: care for your wounded + dwarves instead of leaving them to fend for themselves. + ◦ Retire your fortress, then unretire it after spending time playing + other roles in the world. + ◦ Honey, wax, pottery, windmills, waterwheels, soap, plaster, wool, eggs, + dyes, cheese, glass, animal training, and much, much more … + . + • Play an adventurer and explore, quest for glory or seek vengeance. + ◦ Meet adversaries from previous games. + ◦ Recruit people to come with you on your journey. + ◦ Explore without cumbersome plot restrictions – thriving capitals, + villages, catacombs, labyrinths, bandit camps, caves and more! + ◦ Seamlessly wander the world or travel more rapidly on the region map + and in underground tunnels. + ◦ Travel by day and search for a place to shelter as night falls. + ◦ Listen to rumors and help out town and civilization leaders. + ◦ Earn a reputation as a hero, friend, soldier, enemy, thug, etc. with + the various civilizations in the world. + ◦ Retire and meet your old characters. Bring them along on an adventure + with a new character or reactivate them and play directly. + ◦ Z coordinate allows you to move between twisting underground caverns + and scale structures, fighting adversaries above and below. Climb, jump + and sprint! + ◦ Stealth system with vision arcs which also respects vegetation density + and other factors. + ◦ Use signs like shoe impressions and animal tracks to hunt and avoid + danger. + ◦ Steal a mummy’s treasure or learn the secrets of life and death at a + necromancer’s tower. + ◦ Visit your retired fortresses and ask your dwarves to join you on + adventures. + . + • The combat model uses skills, body parts, individual tissues, material + properties, aimed attacks, wrestling, one-time opportunities, charging and + dodging between squares, bleeding, pain, nausea, various poison effects and + much more. Attacks and other movements extend over several instants, + allowing you to deliberately catch enemy blows or plan your counter-attack. + . + • Hundreds of animals and other monsters, including many that are randomly + generated for each world. + . + • Multi-tile climbable trees and many, many kinds of plants. Fruit, flowers + and falling leaves. + . + • A dynamic weather model tracks wind, humidity and air masses to create + fronts, clouds, rain storms and blizzards. + . + • Over two hundred rock and mineral types are incorporated into the world, + placed in their proper geological environments. + . + • Extended ASCII character set rendered in 16 colors (including black) as + well as 8 background colors (including black). diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 0000000..3ab0f6d --- /dev/null +++ b/debian/copyright @@ -0,0 +1,106 @@ +Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: Dwarf Fortress +Upstream-Contact: Tarn Adams +Source: http://www.bay12games.com/dwarves/ +Disclaimer: + This package is not part of the Debian distribution. It is provided in + the non-free archive area as a convenience to Debian users. + . + The contents of this package cannot be distributed as part of the Debian + distribution because no source code is provided and the package license + permits only non-commercial, unmodified distribution. +Copyright: 2002-2015 Tarn Adams +License: Dwarf-Fortress + +Files: * +Copyright: 2002-2015 Tarn Adams +License: Dwarf-Fortress + +Files: data/art/font.ttf +Copyright: Copyright (c) 2003 by Bitstream, Inc. All Rights Reserved. + Bitstream Vera is a trademark of Bitstream, Inc. + DejaVu changes are in public domain. +License: DejaVu + +Files: debian/* +Copyright: 2011-2012 Beren Minor + 2015 Benjamin Barenblat +License: GPL-3+ + +Files: sdl/sdl*license.txt +Copyright: 1991, 1999 Free Software Foundation, Inc. +License: FSF-LGPL + +License: DejaVu + Permission is hereby granted, free of charge, to any person obtaining a copy + of the fonts accompanying this license ("Fonts") and associated + documentation files (the "Font Software"), to reproduce and distribute the + Font Software, including without limitation the rights to use, copy, merge, + publish, distribute, and/or sell copies of the Font Software, and to permit + persons to whom the Font Software is furnished to do so, subject to the + following conditions: + . + The above copyright and trademark notices and this permission notice shall + be included in all copies of one or more of the Font Software typefaces. + . + The Font Software may be modified, altered, or added to, and in particular + the designs of glyphs or characters in the Fonts may be modified and + additional glyphs or characters may be added to the Fonts, only if the fonts + are renamed to names not containing either the words "Bitstream" or the word + "Vera". + . + This License becomes null and void to the extent applicable to Fonts or Font + Software that has been modified and is distributed under the "Bitstream + Vera" names. + . + The Font Software may be sold as part of a larger software package but no + copy of one or more of the Font Software typefaces may be sold by itself. + . + THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS + OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT OF COPYRIGHT, PATENT, + TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL BITSTREAM OR THE GNOME + FOUNDATION BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, INCLUDING + ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL DAMAGES, + WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF + THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM OTHER DEALINGS IN THE + FONT SOFTWARE. + . + Except as contained in this notice, the names of Gnome, the Gnome + Foundation, and Bitstream Inc., shall not be used in advertising or + otherwise to promote the sale, use or other dealings in this Font Software + without prior written authorization from the Gnome Foundation or Bitstream + Inc., respectively. For further information, contact: fonts at gnome dot + org. + +License: Dwarf-Fortress + All rights are retained by Tarn Adams, save the following: you may redistribute + the binary and accompanying files, unmodified, provided you do so free of + charge. If you'd like to distribute a modified version of the game or portion + of the archive and are worried about copyright infringement, please contact + Tarn Adams at toadyone@bay12games.com. + . + This software is still in development, and this means that there are going to + be problems, including serious problems that, however unlikely, might damage + your system or the information stored on it. Please be aware of this before + playing + +License: FSF-LGPL + Everyone is permitted to copy and distribute verbatim copies of this license + document, but changing it is not allowed. + +License: GPL-3+ + This package is free software; you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free Software + Foundation; either version 3 of the License, or (at your option) any later + version. + . + This package is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU General Public License for more details. + . + You should have received a copy of the GNU General Public License along with + this program. If not, see + . + On Debian systems, the complete text of the GNU General Public License + version 3 can be found in "/usr/share/common-licenses/GPL-3". diff --git a/debian/copyright~ b/debian/copyright~ new file mode 100644 index 0000000..1635523 --- /dev/null +++ b/debian/copyright~ @@ -0,0 +1,50 @@ +Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: Dwarf Fortress +Upstream-Contact: Tarn Adams +Source: http://www.bay12games.com/dwarves/ +Disclaimer: + This package is not part of the Debian distribution. It is provided in + the non-free archive area as a convenience to Debian users. + . + The contents of this package cannot be distributed as part of the Debian + distribution because no source code is provided and the package license + permits only non-commercial, unmodified distribution. +Copyright: 2002-2015 Tarn Adams +License: Dwarf-Fortress + +Files: * +Copyright: 2002-2015 Tarn Adams +License: Dwarf-Fortress + +Files: debian/* +Copyright: 2011-2012 Beren Minor + 2015 Benjamin Barenblat +License: GPL-3+ + +License: Dwarf-Fortress + All rights are retained by Tarn Adams, save the following: you may redistribute + the binary and accompanying files, unmodified, provided you do so free of + charge. If you'd like to distribute a modified version of the game or portion + of the archive and are worried about copyright infringement, please contact + Tarn Adams at toadyone@bay12games.com. + . + This software is still in development, and this means that there are going to + be problems, including serious problems that, however unlikely, might damage + your system or the information stored on it. Please be aware of this before + playing + +License: GPL-3+ + This package is free software; you can redistribute it and/or modify it under + the terms of the GNU General Public License as published by the Free Software + Foundation; either version 3 of the License, or (at your option) any later + version. + . + This package is distributed in the hope that it will be useful, but WITHOUT ANY + WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A + PARTICULAR PURPOSE. See the GNU General Public License for more details. + . + You should have received a copy of the GNU General Public License along with + this program. If not, see + . + On Debian systems, the complete text of the GNU General Public License + version 3 can be found in "/usr/share/common-licenses/GPL-3". diff --git a/debian/docs b/debian/docs new file mode 100644 index 0000000..b73748a --- /dev/null +++ b/debian/docs @@ -0,0 +1,5 @@ +command*line.txt +file*changes.txt +README.linux +readme.txt +release*notes.txt diff --git a/debian/dwarf-fortress.6 b/debian/dwarf-fortress.6 new file mode 100644 index 0000000..2861992 --- /dev/null +++ b/debian/dwarf-fortress.6 @@ -0,0 +1,55 @@ +.\" © 2013, 2015 Benjamin Barenblat +.\" +.\" 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, W.TPOUT +.\" WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +.\" License for the specific language governing permissions and limitations +.\" under the License. +.pc +.TH DWARF-FORTRESS 6 "2015-01-07" "0.40.24" "Dwarf Fortress" +.SH NAME +dwarf-fortress \- control a band of dwarves as they establish an outpost +.SH SYNOPSIS +.B dwarf-fortress [\| -gen +.I id-number seed world-gen-param-title +\|] +.SH DESCRIPTION +.I Slaves to Armok: God of Blood Chapter II: Dwarf Fortress +is an absurdly detailed indie roguelike which takes place in a massive, procedurally generated, open world. +Take command of a band of dwarves, guiding them as they mine, farm, and defend a new home, or become an adventurer and seek your fortune. +.PP +World detail in +.I Dwarf Fortress +cannot be underestimated. +History, NPC behaviors, terrain, weather, mineral deposits, and much more are generated anew by Dwarf Fortress's engine before the game begins and rendered in excruciating detail using an extended ASCII character set drawn with OpenGL. +New features are added all the time. +.SH OPTIONS +.B dwarf-fortress +is an interactive program, and most players will run it without arguments. +However, advanced users can batch-generate worlds using the +.B -gen +option, specifying a world ID number, an engine seed (or +.I RANDOM +to use a random seed), and parameters to the generation engine. +.SH ENVIRONMENT +.B dwarf-fortress +looks for user saves and movies in the directory described by +.BR DWARF_FORTRESS_DATA_HOME . +This defaults to +.BR $XDG_DATA_HOME/dwarf-fortress . +As +.I Dwarf Fortress +is alpha software, you are strongly encouraged to back up this directory. +.SH COPYRIGHT +.I Dwarf Fortress +is copyright \(co 2002-2015 Tarn Adams. +All rights are reserved, except redistribution of the game binary and accompanying files, unmodified, free of charge, is permitted. +If you'd like to distribute a modified version of the game or portion of the archive, please contact Tarn Adams at . +.PP +This manual page is copyright \(co 2013, 2015 Benjamin Barenblat and licensed under the Apache License, Version 2.0. diff --git a/debian/dwarf-fortress.6~ b/debian/dwarf-fortress.6~ new file mode 100644 index 0000000..056dccc --- /dev/null +++ b/debian/dwarf-fortress.6~ @@ -0,0 +1,903 @@ +.\" © 2013, 2015 Benjamin Barenblat +.\" +.\" 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, W.TPOUT +.\" WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the +.\" License for the specific language governing permissions and limitations +.\" under the License. +.pc +.TH dafny 1 "2015-05-11" "1.9.5" Dafny +.SH NAME +dafny \- compiler for the Dafny programming language +.SH SYNOPSIS +.B dafny +.RI [\| options \|] +.IR file.dfy \ .\|.\|.\& +.SH DESCRIPTION +.B dafny +is a compiler for Microsoft Research's Dafny programming language, an imperative language with built-in specification constructs. +The integrated static analyzer can verify functional correctness as part of the compilation process. +.SH OPTIONS +.B dafny +accepts a number of different types of options. +.SS "File macros" +A number of +.B dafny +options accept a +.I file +argument, which may contain the following macros: +.TP +.B @FILE@ +Expands to the last filename specified on the command line. +.TP +.B @PREFIX@ +Expands to the concatenation of strings given by +.B /logPrefix +options. +.TP +.B @TIME@ +Expands to the current time. +.SS "General options" +.TP +.BI /env: n +Control printing of command-line arguments. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Suppress printing of command-line arguments. +.TP +.B 1 +(default) Print command-line arguments during BPL print and prover log. +.TP +.B 2 +Print command-line arguments during BPL print and prover log, and also to standard output. +.RE +.TP +.B /noLogo +Suppress printing of the version number and copyright message. +.TP +.B /wait +Wait for a carriage return from the keyboard before exiting. +.TP +.BI /xml: file +Also produce output in XML format to +.IR file . +.SS "Dafny options" +Multiple +.B .dfy +files supplied on the command line are concatenated into one Dafny program. +.TP +.B /allowGlobals +Allow the implicit class +.B \%_default +to contain fields, instance functions, and instance methods. +These class members are declared at module scope, outside of explicit classes. +This command-line option is provided to simplify a a transition from the behavior in the language prior to version 1.9.3, from which point onward all functions and methods declared at the module scope are implicitly static and field declarations are not allowed at the module scope. +.TP +.BI /autoReqPrint: file +Print requirements automatically generated by autoReq to the specified file. +.TP +.BI /compile: n +Enable or disable compilation. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Do not compile. +.TP +.B 1 +(default) Compile Dafny to CLI assembly. +The output file name shares the base name of the last .dfy file on the command line. +If the program has a Main method, the output will have the extension +.BR .exe ; +otherwise, it will be a +.BR .dll . +.RE +.TP +.B /dafnycc +Disable features not supported by DafnyCC. +.TP +.BI /dafnyVerify: n +Control how far compilation proceeds. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Stop after typechecking. +.TP +.B 1 +Typecheck, verify, and compile. +.RE +.TP +.BI /dprelude: file +Choose Dafny prelude file. +.TP +.BI /dprint: file +Print Dafny program to the specified file after parsing. +Specify +.B \%/dprint:\- +to print to standard output. +.TP +.BI /induction: n +Control when Dafny performs induction. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Never do induction, not even when attributes request it. +.TP +.B 1 +Apply induction only when attributes request it. +.TP +.B 2 +Apply induction as requested by attributes and also for heuristically chosen quantifiers. +.TP +.B 3 +(default) Apply induction as requested by attributes, for heuristically chosen quantifiers, and for ghost methods. +.RE +.TP +.BI /inductionHeuristic: n +Control how discriminating the induction heuristic is. +.B \%/inductionHeuristic:0 +is the least discriminating (that is, it leans toward applying induction most often); increasing +.I n +up to\ 6, the default, increases +.BR dafny 's +reluctance to apply induction. +.TP +.B /noAutoReq +Ignore autoReq attributes. +.TP +.BI /noCheating: n +Control how strict +.B dafny +is about unproven constructs. Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Allow +.B assume +statements and free invariants. +.TP +.B 1 +Treat all assumptions as assertions, and drop free. +.RE +.TP +.B /noIncludes +Ignore +.B include +directives. +.TP +.B /noNLarith +Reduce Z3's knowledge of nonlinear arithmetic (multiplication and division). +This results in more manual work but also tends to produce more predictable behavior. +.TP +.BI /printMode: mode +Control printing. +Accepted values for\ \fImode\fP are: +.RS +.TP +.B Everything +(default) Print everything. +.TP +.B NoIncludes +Disable printing of +.B \%"{:verify false} +methods incorporated via the include mechanism, as well as datatypes and fields included from other files. +.TP +.B NoGhost +Like +.BR NoIncludes , +but also disable printing of functions ghost methods, and proof statements in implementation methods. +.RE +.TP +.BI /rprint: file +Print Dafny program to the specified file after resolving it. +Specify +.B \%/rprint:\- +to print to standard output. +.TP +.BI /spillTargetCode: n +Control whether or not +.B dafny +emits intermediate C# code. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Don't save intermediate C# code. +.TP +.B 1 +Save intermediate C# code as a +.B .cs +file. +.RE +.SS "Boogie options" +Multiple .bpl files supplied on the command line are concatenated into one Boogie program. +.TP +.BI /enhancedErrorMessages: n +Control printing of enhanced error messages. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Do not print enhanced error messages. +.TP +.B 1 +Print Z3 error model enhanced error messages. +.RE +.TP +.BI /loopUnroll: n +Unroll loops, following up to +.I n +back edges (and then some). +.TP +.BI /mv: file +Save the model in BVD format to the specified file. +.TP +.B /noResolve +Parse only. +.TP +.B /noTypecheck +Parse and resolve only. +.TP +.B /overlookTypeErrors +Skip any implementation with resolution or type checking errors. +.TP +.BI /pretty: n +Control pretty-printing of Boogie code. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Print each Boogie statement on one line. +.TP +.B 1 +(default) Pretty-print with some line breaks. +This is slower but easier to read. +.RE +.TP +.BI /print: file +Print Boogie program to the specified file after parsing it. +Specify +.B \%/print:\- +to print to standard output. +.TP +.BI /printCFG: prefix +Print the control flow graph of each implementation in +.BR dot (1) +format to files named +.IR prefix . procedurename .dot. +.TP +.B /printDesugared +With +.BR /print , +desugar calls. +.TP +.BI /printModel: n +Control printing of Z3's error model. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Do not print Z3's error model. +.TP +.B 1 +Print Z3's error model. +.TP +.B 2 +Print Z3's error model and reverse mappings. +.TP +.B 3 +Print Z3's error model in a more human-readable way. +.RE +.TP +.B /printUnstructured +With +.BR /print , +desugar all structured statements. +.TP +.B /printWithUniqueIds +Print augmented information that uniquely identifies variables. +.TP +.BI /proc: p +Limit which procedures to check. +.TP +.B /soundLoopUnrolling +Enable sound loop unrolling. +.TP +.B /useBaseNameForFileName +When parsing, use the base name of the file for tokens instead of the path supplied on the command line. +.SS "Inference options" +.TP +.B /checkInfer +Instrument inferred invariants as asserts to be checked by the theorem prover. +.TP +.B /contractInfer +Perform procedure contract inference. +.TP +\fB/infer\fP[:\fIdomains\/\fP] +Use abstract interpretation to infer invariants. +.I domains +may be any of the following: +.RS +.TP +.B c +constant propagation +.TP +.B d +dynamic type +.TP +.B i +intervals +.TP +.B j +stronger intervals (cannot be combined with other domains) +.TP +.B n +nullness +.TP +.B p +polyhedra for linear inequalities +.TP +.B t +trivial bottom/top lattice (cannot be combined with other domains) +.RE +.IP "" +You may also specify the following options as pseudo-domains: +.RS +.TP +.B s +debug statistics +.TP +.BR 0 .\|.\|.\| 9 +number of iterations before applying a widen (default: 0) +.RE +.IP "" +The default is +.BR /infer:i . +With +.B /infer +(and no +.IR domains ), +all domains will be used. +.TP +.BI /instrumentInfer: flag +Control when inferred invariants are instrumented. +Accepted values +for\ \fIflag\fP are: +.RS +.TP +.B h +(default) Instrument inferred invariants only at the beginning of loop headers. +.TP +.B e +Instrument inferred invariants at the beginning and end of every block. +This mode is intended for use in debugging abstract domains. +.RE +.TP +.B /noinfer +Turn off the default inference, and override any previous +.B /infer +flags. +.TP +.B /printInstrumented +Print Boogie program after it has been instrumented with invariants. +.SS "Debugging and tracing options" +.TP +\fB/break\fP +Launch and break into the debugger. +.TP +\fB/log\fP[:\fImethod\/\fP] +Print debug output during translation. +.TP +\fB/trace\fP +Blurt out various debug trace information. Implies +.BR /tracePOs . +.TP +.B /tracePOs +Output information about the number of proof obligations. +.TP +.B /traceTimes +Output timing information at certain points in the pipeline. +.SS "Verification condition generation options" +.TP +.B /alwaysAssumeFreeLoopInvariants +Include free loop invariants as assumptions in checking contexts. +Usually, a free loop invariant (or assume statement in that position) is ignored in checking contexts (like other free things). +.TP +.B /causalImplies +Translate Boogie's +.B A\ ==>\ B +into prover's +.BR "A\ ==>\ A\ &&\ B" . +.TP +.BI /coalesceBlocks: n +Control when to coalesce blocks. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Do not coalesce blocks. +.TP +.B 1 +(default) Coalesce blocks. +.RE +.TP +.BI /fixedPointEngine: engine +Use the specified fixed point engine for inference. +.TP +.BI /inferLeastForUnsat: prefix +Infer the least number of constants (whose names are prefixed by +.IR prefix ) +that need to be set to true for the program to be correct. +Implies +.BR /stratifiedInline:1 . +.TP +.BI /inline: strategy +Use the specified inlining strategy for procedures with the +.B :inline +attribute. +Accepted strategies are +.BR none , +.B assume +(the default), +.BR assert , +and +.BR spec . +.TP +.B /lazyInline:1 +Use the lazy inlining algorithm. +.TP +.BI /liveVariableAnalysis: n +Control when and how to perform live variable analysis. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Do not perform live variable analysis. +.TP +.B 1 +(default) Perform live variable analysis. +.TP +.B 2 +Perform interprocedural live variable analysis. +.RE +.TP +.B /monomorphize +Do not abstract map types in the encoding. +This is an experimental feature which will not do the right thing if the program uses polymorphism. +.TP +.B /noVerify +Skip verification condition generation and invocation of the theorem prover. +.TP +.B /printInlined +Print the implementation after inlining calls to procedures with the +.B :inline +attribute. +.TP +.BI /recursionBound: n +Set the recursion bound for stratified inlining to +.IR n . +By default, +.I n +is 500. +.TP +.B /reflectAdd +In the verification condition, generate an auxiliary symbol, elsewhere defined to be +.BR + , +instead of +.BR + . +.TP +.BI /removeEmptyBlocks: n +Control whether to remove empty blocks during verification condition generation. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Do not remove empty blocks. +.TP +.B 1 +(default) Remove empty blocks. +.RE +.TP +.B /smoke +Run the soundness smoke test: try to stick +.B assert false; +in some places in the BPL and see if we can still prove it. +.TP +.BI /smokeTimeout: n +Set the timeout, in seconds, for a single theorem prover invocation during the smoke test. +By default, +.I n +is 10. +.TP +.B /stratifiedInline:1 +Use the stratified inlining algorithm. +.TP +.BI /subsumption: n +Control when subsumption is applied to asserted conditions. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Never apply subsumption. +.TP +.B 1 +Do not apply subsumption for quantifiers. +.TP +.B 2 +(default) Always apply subsumption. +.RE +.TP +.B /traceVerify +Print debug output during verification condition generation. +.TP +.BI /typeEncoding: method +Control how to encode types when sending the verification condition to the the theorem prover. +Allowed methods are: +.RS +.TP +.B a +arguments +.TP +.B m +monomorphic +.TP +.B n +none (unsound) +.TP +.B p +(default) predicates +.RE +.TP +.BI /vc: variety +Specify the verification condition variety. +Accepted varieties are: +.RS +.TP +.B b +flat block +.TP +.B d +(default) DAG +.TP +.B doomed +doomed +.TP +.B l +local +.TP +.B m +nested block reach +.TP +.B n +nested block +.TP +.B r +flat block reach +.TP +.B s +structured +.RE +.TP +.B /verifySeparately +Verify each input program separately. +.TP +.BI /verifySnapshots: n +Control verification result caching. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Do not use any verification result caching. +.TP +.B 1 +Verify several program snapshots (named +.IR filename .v0.bpl +to +.IR filename .v N .bpl) +using basic verification result caching. +.TP +.B 2 +Use more advanced verification result caching. +.RE +.SS "Verification condition splitting" +.TP +.BI /vcsCores: n +Try to verify +.I n +verification conditions at once. +Defaults to 1. +.TP +.B /vcsDumpSplits +For the +.IR n th +split, dump +.IR split . n .dot +and +.IR split . n .bpl. +Note that this affects error reporting. +.TP +.BI /vcsFinalAssertTimeout: n +Set the timeout, in seconds, for the single last assertion in keep-going mode. +By default, +.I n +is 30. +.TP +.BI /vcsKeepGoingTimeout: n +Set the timeout, in seconds, for a single theorem prover invocation in keep-going mode, except for the final single-assertion case. +By default, +.I n +is 1. +.TP +.BI /vcsLoad: f +Like \fB/vcsCores\fP:\fIn\fP, where +.I n +is the machine's processor count multiplied by +.I f +and rounded to the nearest integer. +.I f +must be in the range [0.0, 3.0]. +This will never set +.I n +less than 1. +.TP +.BI /vcsMaxCost: f +Verification conditions will not be split unless the cost of a verification condition exceeds +.IR f . +.I f +defaults to 2000.0. This does +.I not +apply in the keep-going mode after the first round of splitting. +.TP +.BI /vcsMaxKeepGoingSplits: n +If +.I n +is set to more than 1, this activates keep-going mode, where after the first round of splitting, verification conditions that time out are split into +.I n +pieces and retried until either proving them is successful or there is only one assertion on a single path and it times out. +(In such a case, +.B dafny +reports an error for that assertion). +By default, +.I n +is 1 (that is, keep-going mode is disabled). +.TP +.BI /vcsMaxSplits: n +Set the maximal number of verification conditions generated per method. +In keep-going mode, this only applies to the first round. +By default, +.I n +is 1. +.TP +\fB/vcsPathCostMult\fP:\fIf1\fP, \fB/vcsAssumeMult\fP:\fIf2\fP +Controls the cost of a block. +Block cost is computed according to the formula +.IP "" +.in +4n +(\fIassert-cost\fP \[pl] \fIf2\fP \[mu] \fIassume-cost\fP) \[mu] (1 \[pl] \fIf1\fP \[mu] \fIentering-paths\fP) +.in +.IP "" +where +.I f1 +defaults to\ 1.0 and +.I f2 +defaults to\ 0.01. +The cost of a single assertion or assumption is always 1.0. +.TP +.BI /vcsPathJoinMult: f +Sets a scale factor which +.B dafny +will multiply by the number of paths in a block if more than one path join at a block. +This is intended to reflect the fact that the prover will learn something on one path before proceeding to the next. +By default, +.I f +is 0.8. +.TP +.BI /vcsPathSplitMult:f +If the best path split of a verification condition of cost +.I A +is into verification conditions of cost \fIB\fP\ and\ \fIC\fP, then the split is applied if \fIA\fP \[>=] \fIf\fP \[mu] (\fIB\fP \[pl] \fIC\fP). +Otherwise, assertion splitting will be applied. +By default, +.I f +is 0.5 (that is, always do path splitting if possible). +Increase +.I f +to do less path splitting and more assertion splitting. +.SS "Prover options" +.TP +.BI /errorLimit: n +Limit the number of errors produced for each procedure. +By default, +.I n +is 5, but some provers may only support 1. +.TP +.BI /errorTrace: n +Control whether or not trace labels appear in the error output. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Print no trace labels in the error output. +.TP +.B 1 +(default) Print useful trace labels in error output. +.TP +.B 2 +Print all trace labels in error output. +.RE +.TP +.BI /logPrefix: prefix +Define the expansion of the macro +.BR @PREFIX@ . +.TP +\fB/p\fP:\fIkey\fP[:\fIvalue\/\fP], \fB/proverOpt\fP:\fIkey\fP[:\fIvalue\/\fP] +Provide a prover-specific option. +.TP +\fB/platform\fP:\fIptype\fP,\fIlocation\fP +Set the platform type and location. +.I ptype +may be +.BR v11 , +.BR v2 , +or +.BR cli1 , +and +.I location +should be the platform libraries directory. +.TP +.BI /prover: p +Use theorem prover +.IR p . +.I p +may be a full path to a prover DLL, or it may be one of the following standard provers: +.RS +.TP +.B ContractInference +.TP +.B Simplify +This implies +.B /vc:n +and +.BR /vcBrackets:1 . +.TP +.B SMTLib +(default) Use the SMTLib2 format, and call Z3. +.TP +.B Z3 +Z3 with the Simplify format. +.TP +.B Z3api +Z3 with the managed (CLI) API. +.RE +.TP +.BI /proverLog: file +Log input for the theorem prover. +.IP "" +In addition to the standard file name macros, +.I file +can use the +.B @PROC@ +macro, which causes +.B dafny +to generate one prover log file per verification condition, expanding +.B @PROC@ +to the name of the procedure that the verification condition is for. +.TP +.B /proverLogAppend +Append (do not overwrite) the specified prover log file. +.TP +.BI /proverMemorylimit: n +Limit the prover to +.I n +megabytes of virtual memory before forcing it to restart. +.I n +defaults to 100. +.TP +.BI /proverShutdownLimit n +Set the time, in seconds, between closing the stream to the prover and killing the prover process. +.I n +defaults to 0. +.TP +.BI /proverWarnings: n +Control warning output from the prover. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Don't print warning output from the prover. +.TP +.B 1 +Print warnings to standard output. +.TP +.B 2 +Print warnings to standard error. +.RE +.TP +.B /restartProver +Restart the prover after each query. +.TP +.BI /timeLimit: n +Limit the number of seconds spent trying to verify each procedure. +.TP +.BI /vcBrackets: n +Control whether or not odd-charactered identifier names will be bracketed with pipe characters (\(aq|\(aq). +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +(default) Do not bracket odd-charactered identifier names. +.TP +.B 1 +Bracket odd-charactered identifier names. +.RE +.SS "Prover options (CVC4)" +.TP +.BI /cvc4exe: path +Set the path to the CVC4 executable. +.SS "Prover options (Simplify)" +.TP +.BI /simplifyMatchDepth: n +Set Simplify's matching depth limit. +.SS "Prover options (Z3)" +.TP +.B /useArrayTheory +Use Z3's native array theory, as opposed to axioms. +Implies +.BR /monomorphize . +.TP +.B /useSmtOutputFormat +Output a model in SMTLib2 format. +.TP +.BI /z3exe: path +Set the path to the Z3 executable. +On Debian systems, this defaults to +.BR /usr/bin/z3 . +.TP +.BR /z3lets: n +Configure use of +.BR LET s +in Z3. +Accepted values for\ \fIn\fP are: +.RS +.TP +.B 0 +Do not use +.BR LET s. +.TP +.B 1 +Use only +.BR "LET TERM" . +.TP +.B 2 +Use only +.BR "LET FORMULA" . +.TP +.B 3 +(default) Use any +.BR LET . +.RE +.TP +.B /z3multipleErrors +Report multiple counterexamples for each error. +.TP +.BI /z3opt: option +Set an additional Z3 option. +.TP +.B /z3types +Generate a multi-sorted verification condition that makes use of Z3 types. +.SH SEE ALSO +.BR dot (1) +.SH COPYRIGHT +Dafny is copyright \(co 2003-2015 Microsoft Corporation and licensed under the Microsoft Public License . + +This manual page is copyright \(co 2013, 2015 Benjamin Barenblat and licensed under the Apache License, Version 2.0. diff --git a/debian/dwarf-fortress.links b/debian/dwarf-fortress.links new file mode 100644 index 0000000..5498974 --- /dev/null +++ b/debian/dwarf-fortress.links @@ -0,0 +1,2 @@ +usr/share/games/dwarf-fortress/data usr/lib/games/dwarf-fortress/data +usr/share/games/dwarf-fortress/raw usr/lib/games/dwarf-fortress/raw \ No newline at end of file diff --git a/debian/dwarf-fortress.manpages b/debian/dwarf-fortress.manpages new file mode 100644 index 0000000..32bd1a3 --- /dev/null +++ b/debian/dwarf-fortress.manpages @@ -0,0 +1 @@ +debian/dwarf-fortress.6 diff --git a/debian/install b/debian/install new file mode 100644 index 0000000..2fa5b7e --- /dev/null +++ b/debian/install @@ -0,0 +1,8 @@ +debian/bin/dwarf-fortress usr/games +data usr/share/games/dwarf-fortress +df usr/lib/games/dwarf-fortress +g_src usr/src/dwarf-fortress +libs usr/lib/games/dwarf-fortress +raw usr/share/games/dwarf-fortress +sdl usr/src/dwarf-fortress + diff --git a/debian/menu b/debian/menu new file mode 100644 index 0000000..3aa4e49 --- /dev/null +++ b/debian/menu @@ -0,0 +1,2 @@ +?package(dwarf-fortress):needs="X11" section="Games/Adventure"\ + title="Dwarf Fortress" command="/usr/games/dwarf-fortress" diff --git a/debian/rules b/debian/rules new file mode 100755 index 0000000..ecfbc98 --- /dev/null +++ b/debian/rules @@ -0,0 +1,31 @@ +#!/usr/bin/make -f +# -*- makefile -*- + +%: + dh $@ + +# Remove empty directories. +.PHONY: override_dh_install +override_dh_install: + dh_install + find debian/dwarf-fortress/usr/share/games/dwarf-fortress -type d -empty -delete + +# Fix permissions manually beyond what dh_fixperms(1) will do. +.PHONY: override_dh_fixperms +override_dh_fixperms: + dh_fixperms + find debian/dwarf-fortress/usr/share/games/dwarf-fortress -type f -exec chmod 0644 {} + + find debian/dwarf-fortress/usr/src/dwarf-fortress -type f -exec chmod 0644 {} + + +# Don't run dh_makeshlibs(1). This package doesn't actually install any +# user-visible libraries. +.PHONY: override_dh_makeshlibs +override_dh_makeshlibs: + true + +# Prevent dh_shlibdeps(1) from trying to objdump 'language_ELF.txt', which +# despite its name, is not actually an ELF file but rather a dictionary for +# Elvish. +.PHONY: override_dh_shlibdeps +override_dh_shlibdeps: + dh_shlibdeps --exclude=.txt diff --git a/debian/source/format b/debian/source/format new file mode 100644 index 0000000..163aaf8 --- /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 0000000..32ace0a --- /dev/null +++ b/debian/watch @@ -0,0 +1,2 @@ +version=3 +http://www.bay12games.com/dwarves/df_(\d+)_(\d+)_linux\.(?:zip|tgz|tbz2|txz|tar\.(?:gz|bz2|xz)) -- cgit v1.2.3