More description fixes

* Remove package name
* Start with upper case letter
* Remove trailing period

Also reword some descriptions and move some long descriptions to
longDescription.

I'm not touching generated packages.

6 files changed, 13 insertions, 17 deletions

diff --git a/pkgs/applications/science/electronics/ngspice/default.nix b/pkgs/applications/science/electronics/ngspice/default.nix
index 70153eee61b4..579492248ea3 100644
--- a/pkgs/applications/science/electronics/ngspice/default.nix
+++ b/pkgs/applications/science/electronics/ngspice/default.nix
@@ -13,7 +13,7 @@ stdenv.mkDerivation {
   configureFlags = [ "--enable-x" "--with-x" "--with-readline" ];
 
   meta = {
-    description = "The Next Generation Spice (Electronic Circuit Simulator).";
+    description = "The Next Generation Spice (Electronic Circuit Simulator)";
     homepage = "http://ngspice.sourceforge.net";
     license = ["BSD" "GPLv2"];
     maintainers = with stdenv.lib.maintainers; [viric];
diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix
index 18a16114c507..4223c52b7d48 100644
--- a/pkgs/applications/science/logic/hol/default.nix
+++ b/pkgs/applications/science/logic/hol/default.nix
@@ -39,9 +39,8 @@ stdenv.mkDerivation {
   '';
 
   meta = {
-    description = "HOL4, an interactive theorem prover based on Higher-Order Logic.";
+    description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
-
       HOL4 is the latest version of the HOL interactive proof
       assistant for higher order logic: a programming environment in
       which theorems can be proved and proof tools
@@ -52,7 +51,6 @@ stdenv.mkDerivation {
       engines. HOL4 is particularly suitable as a platform for
       implementing combinations of deduction, execution and property
       checking.
-
     '';
     homepage = "http://hol.sourceforge.net/";
     license = "BSD";
diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix
index f9549241a45c..d6c1c0c18781 100644
--- a/pkgs/applications/science/logic/hol_light/default.nix
+++ b/pkgs/applications/science/logic/hol_light/default.nix
@@ -26,15 +26,15 @@ stdenv.mkDerivation {
   '';
 
   meta = {
-    description = "An interactive theorem prover based on Higher-Order Logic.";
+    description = "Interactive theorem prover based on Higher-Order Logic";
     longDescription = ''
-HOL Light is a computer program to help users prove interesting mathematical
-theorems completely formally in Higher-Order Logic.  It sets a very exacting
-standard of correctness, but provides a number of automated tools and
-pre-proved mathematical theorems (e.g., about arithmetic, basic set theory and
-real analysis) to save the user work.  It is also fully programmable, so users
-can extend it with new theorems and inference rules without compromising its
-soundness.
+      HOL Light is a computer program to help users prove interesting
+      mathematical theorems completely formally in Higher-Order Logic.  It sets
+      a very exacting standard of correctness, but provides a number of
+      automated tools and pre-proved mathematical theorems (e.g., about
+      arithmetic, basic set theory and real analysis) to save the user work.
+      It is also fully programmable, so users can extend it with new theorems
+      and inference rules without compromising its soundness.
     '';
     homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
     license = stdenv.lib.licenses.bsd2;
diff --git a/pkgs/applications/science/logic/logisim/default.nix b/pkgs/applications/science/logic/logisim/default.nix
index 009bed3ffe2a..ab46efa9a961 100644
--- a/pkgs/applications/science/logic/logisim/default.nix
+++ b/pkgs/applications/science/logic/logisim/default.nix
@@ -26,7 +26,7 @@ stdenv.mkDerivation {
   
   meta = {
     homepage = "http://ozark.hendrix.edu/~burch/logisim";
-    description = "Logisim is an educational tool for designing and simulating digital logic circuits.";
+    description = "Educational tool for designing and simulating digital logic circuits";
     license = "GPLv2+";
   };
 }
diff --git a/pkgs/applications/science/logic/prover9/default.nix b/pkgs/applications/science/logic/prover9/default.nix
index 93b1657aa14a..d92c7887210e 100644
--- a/pkgs/applications/science/logic/prover9/default.nix
+++ b/pkgs/applications/science/logic/prover9/default.nix
@@ -31,14 +31,12 @@ stdenv.mkDerivation {
   meta = {
     homepage = "http://www.cs.unm.edu/~mccune/mace4/";
     license = "GPL";
-    description = "Prover9 is an automated theorem prover for first-order and equational logic.";
-
+    description = "Automated theorem prover for first-order and equational logic";
     longDescription = ''
       Prover9 is a resolution/paramodulation automated theorem prover
       for first-order and equational logic. Prover9 is a successor of
       the Otter Prover. This is the LADR command-line version.
     '';
-
     platforms = stdenv.lib.platforms.unix;
     maintainers = [];
   };
diff --git a/pkgs/applications/science/math/wxmaxima/default.nix b/pkgs/applications/science/math/wxmaxima/default.nix
index e9e6ca7bead7..47baf446d0ac 100644
--- a/pkgs/applications/science/math/wxmaxima/default.nix
+++ b/pkgs/applications/science/math/wxmaxima/default.nix
@@ -26,7 +26,7 @@ stdenv.mkDerivation {
   enableParallelBuilding = true;
 
   meta = {
-    description = "Cross platform GUI for the computer algebra system Maxima.";
+    description = "Cross platform GUI for the computer algebra system Maxima";
     license = "GPL2";
     homepage = http://wxmaxima.sourceforge.net;
     platforms = stdenv.lib.platforms.linux;