AU: 1 updated - Coq

[skip ci] https://gist.github.com/747b3ede98c9404e5cb6a399595e7ad1/90470ace0f38b719323f4b4f5cf163296b09785d

automatic/coq/Changelog.md

@@ -1,6 +1,6 @@
 # Package changelog for [coq](https://chocolatey.org/packages/coq)
 
-## Upcoming
+## Version: 8.7.0 (2017-10-18)
 - **ENHANCEMENT:** Embedded the installer
 
 ## Version: 8.6 (2017-06-09)

automatic/coq/coq.nuspec

@@ -2,8 +2,8 @@
 <!-- Do not remove this test for UTF-8: if “Ω” doesn’t appear as greek uppercase omega letter enclosed in quotation marks, you should use an editor that supports UTF-8, not this one. -->
 <package xmlns="http://schemas.microsoft.com/packaging/2015/06/nuspec.xsd">
   <metadata>
-    <id>coq</id>
-    <version>8.6.1</version>
+    <id>Coq</id>
+    <version>8.7.0</version>
     <packageSourceUrl>https://github.com/AdmiringWorm/chocolatey-packages/tree/master/automatic/coq</packageSourceUrl>
     <owners>AdmiringWorm, murray</owners>
     <title>The Coq proof assistant</title>
@@ -20,11 +20,23 @@
     <tags>coq admin management mathematical algorithms foss cross-platform</tags>
     <summary>An interactive theorem proof assistant.</summary>
     <!-- Do not touch the description here in the nuspec file. Description is imported during update from the Readme.md file -->
-    <description>Dummy</description>
+    <description><![CDATA[Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the [certification of properties of programming languages](https://coq.inria.fr/cocorico/List%20of%20Coq%20PL%20Projects) (e.g. the [CompCert](http://compcert.inria.fr/) compiler certification project, or the [Bedrock](http://plv.csail.mit.edu/bedrock/) verified low-level programming library), the [formalization of mathematics](https://coq.inria.fr/cocorico/List%20of%20Coq%20Math%20Projects) (e.g. the full formalization of the [Feit-Thompson theorem](http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/) or [homotopy type theory](https://coq.inria.fr/cocorico/CoqInTheClassroom)) and [teaching](https://coq.inria.fr/cocorico/CoqInTheClassroom).
+
+Coq implements a program specification and mathematical higher-level language called Gallina that is based on an expressive formal language called the Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, Coq allows:
+
+- to define functions or predicates, that can be evaluated efficiently;
+- to state mathematical theorems and software specifications;
+- to interactively develop formal proofs of these theorems;
+- to machine-check these proofs by a relatively small certification "kernel";
+- to extract certified programs to languages like Objective Caml, Haskell or Scheme.
+
+As a proof development system, Coq provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for - letting the user define its own proof methods. Connection with external computer algebra system or theorem provers is available.
+
+As a platform for the formalization of mathematics or the development of programs, Coq provides support for high-level notations, implicit contents and various other useful kinds of macros.
+]]></description>
     <releaseNotes>
-[Software Changelog](https://coq.inria.fr/distrib/V8.6.1/CHANGES)
-[Package Changelog](https://github.com/AdmiringWorm/chocolatey-packages/blob/master/automatic/coq/Changelog.md)
-  </releaseNotes>
+[Software Changelog](https://github.com/coq/coq/blob/V8.7.0/CHANGES)
+[Package Changelog](https://github.com/AdmiringWorm/chocolatey-packages/blob/master/automatic/coq/Changelog.md)</releaseNotes>
     <dependencies>
       <dependency id="chocolatey-core.extension" version="1.3.3" />
       <!--We could set chocolatey to version 0.10.4, but that version was broken so we use 0.10.5-->

automatic/coq/legal/VERIFICATION.txt

@@ -7,15 +7,15 @@ location on <https://github.com/coq/coq/releases/latest>
 and can be verified by doing the following:
 
 1. Download the following:
-  32-Bit software: <>
-  64-Bit software: <>
+  32-Bit software: <https://github.com/coq/coq/releases/download/V8.7.0/coq-8.7.0-installer-windows-i686.exe>
+  64-Bit software: <https://github.com/coq/coq/releases/download/V8.7.0/coq-8.7.0-installer-windows-x86_64.exe>
 2. Get the checksum using one of the following methods:
   - Using powershell function 'Get-FileHash'
   - Use chocolatey utility 'checksum.exe'
 3. The checksums should match the following:
 
-  checksum type:
-  checksum32:
-  checksum64:
+  checksum type: sha256
+  checksum32: 63071A7E2758F80370639059D5D13A765CBFB067CA9462CE20BF690222A74095
+  checksum64: CC8B0856870F71ACCA49A8326E2402A02DA52DD5C2AA34B33586D3D1E915F6AC
 
 The file 'LICENSE.txt' has been obtained from <https://github.com/coq/coq/blob/27950e8d20578abb2b348618feb28f0426638820/LICENSE>

automatic/coq/tools/chocolateyInstall.ps1

@@ -5,8 +5,8 @@ $toolsPath = "$(Split-Path -parent $MyInvocation.MyCommand.Definition)"
 $packageArgs = @{
   packageName    = $env:ChocolateyPackageName
   fileType       = 'exe'
-  file           = "$toolsPath\"
-  file64         = "$toolsPath\"
+  file           = "$toolsPath\coq-8.7.0-installer-windows-i686.exe"
+  file64         = "$toolsPath\coq-8.7.0-installer-windows-x86_64.exe"
   softwareName   = 'coq*'
   silentArgs     = '/S'
   validExitCodes = @(0)