Fix many package descriptions

(My OCD kicked in today...)

Remove repeated package names, capitalize first word, remove trailing
periods and move overlong descriptions to longDescription.

I also simplified some descriptions as well, when they were particularly
long or technical, often based on Arch Linux' package descriptions.

I've tried to stay away from generated expressions (and I think I
succeeded).

Some specifics worth mentioning:
 * cron, has "Vixie Cron" in its description. The "Vixie" part is not
   mentioned anywhere else. I kept it in a parenthesis at the end of the
   description.

 * ctags description started with "Exuberant Ctags ...", and the
   "exuberant" part is not mentioned elsewhere. Kept it in a parenthesis
   at the end of description.

 * nix has the description "The Nix Deployment System". Since that
   doesn't really say much what it is/does (especially after removing
   the package name!), I changed that to "Powerful package manager that
   makes package management reliable and reproducible" (borrowed from
   nixos.org).

 * Tons of "GNU Foo, Foo is a [the important bits]" descriptions
   is changed to just [the important bits]. If the package name doesn't
   contain GNU I don't think it's needed to say it in the description
   either.

5 files changed, 5 insertions, 5 deletions

diff --git a/pkgs/applications/science/logic/alt-ergo/default.nix b/pkgs/applications/science/logic/alt-ergo/default.nix
index 2a95d0cd65bb..62359baf2bc6 100644
--- a/pkgs/applications/science/logic/alt-ergo/default.nix
+++ b/pkgs/applications/science/logic/alt-ergo/default.nix
@@ -14,7 +14,7 @@ stdenv.mkDerivation rec {
     [ ocaml findlib ocamlgraph zarith lablgtk gmp ];
 
   meta = {
-    description = "Alt-Ergo is a high-performance theorem prover and SMT solver";
+    description = "High-performance theorem prover and SMT solver";
     homepage    = "http://alt-ergo.ocamlpro.com/";
     license     = stdenv.lib.licenses.cecill-c; # LGPL-2 compatible
     platforms   = stdenv.lib.platforms.linux;
diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix
index 678ec6a4b049..da77a4c5a9aa 100644
--- a/pkgs/applications/science/logic/coq/default.nix
+++ b/pkgs/applications/science/logic/coq/default.nix
@@ -45,7 +45,7 @@ stdenv.mkDerivation {
   buildFlags = "revision coq coqide";
 
   meta = {
-    description = "Coq proof assistant";
+    description = "Formal proof management system";
     longDescription = ''
       Coq is a formal proof management system.  It provides a formal language
       to write mathematical definitions, executable algorithms and theorems
diff --git a/pkgs/applications/science/logic/matita/default.nix b/pkgs/applications/science/logic/matita/default.nix
index f601f97de62e..0f393b419f1d 100644
--- a/pkgs/applications/science/logic/matita/default.nix
+++ b/pkgs/applications/science/logic/matita/default.nix
@@ -47,7 +47,7 @@ stdenv.mkDerivation {
 
   meta = {
     homepage = http://matita.cs.unibo.it/;
-    description = "Matita is an experimental, interactive theorem prover";
+    description = "Experimental, interactive theorem prover";
     license = stdenv.lib.licenses.gpl2Plus;
     maintainers = [ stdenv.lib.maintainers.roconnor ];
   };
diff --git a/pkgs/applications/science/logic/prooftree/default.nix b/pkgs/applications/science/logic/prooftree/default.nix
index caaf4a94a1ed..94b1d5907620 100644
--- a/pkgs/applications/science/logic/prooftree/default.nix
+++ b/pkgs/applications/science/logic/prooftree/default.nix
@@ -15,7 +15,7 @@ stdenv.mkDerivation (rec {
   configureFlags = [ "--prefix" "$(out)" ];
 
   meta = {
-    description = "Prooftree is a program for proof-tree visualization";
+    description = "A program for proof-tree visualization";
     longDescription = ''
       Prooftree is a program for proof-tree visualization during interactive
       proof development in a theorem prover. It is currently being developed
diff --git a/pkgs/applications/science/logic/twelf/default.nix b/pkgs/applications/science/logic/twelf/default.nix
index c6c7e4d9c1a7..f9680b475797 100644
--- a/pkgs/applications/science/logic/twelf/default.nix
+++ b/pkgs/applications/science/logic/twelf/default.nix
@@ -30,7 +30,7 @@ stdenv.mkDerivation rec {
   '';
 
   meta = {
-    description = "Twelf logic proof assistant";
+    description = "Logic proof assistant";
     longDescription = ''
       Twelf is a language used to specify, implement, and prove properties of
       deductive systems such as programming languages and logics. Large