Skip to content

Commit

Permalink
Merge pull request #63 from maximedenes/coq8.8+beta1
Browse files Browse the repository at this point in the history
Coq 8.8+beta1 release.
  • Loading branch information
maximedenes committed Mar 20, 2018
2 parents 5ca3cdf + 64e461a commit a448ac5
Show file tree
Hide file tree
Showing 6 changed files with 34 additions and 4 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ $(DST)/coq-workshop/2009/cfp/index.html:

NEWS:= $(shell cut -f1 -d: NEWSINDEX | sort -r -n)

RECENTNEWS:= 143 142 141
RECENTNEWS:= 144 143 142

NEWSSRC:=$(addprefix news/,$(NEWS))
NEWSDST:=$(patsubst %,$(DST)/news/%.html,$(NEWS))
Expand Down
1 change: 1 addition & 0 deletions NEWSINDEX
Original file line number Diff line number Diff line change
Expand Up @@ -51,3 +51,4 @@
141:coq-871-is-out
142
143:coq-872-is-out
144:coq-88beta1-is-out
12 changes: 11 additions & 1 deletion incl/macros.html
Original file line number Diff line number Diff line change
@@ -1,4 +1,14 @@
<#def BASEURL>https://github.com/coq/coq/releases/tag/</#def>

<#def CURRENTMAJORVERSION>8.7</#def>
<#def CURRENTVERSION>8.7.2</#def>
<#def CURRENTVERSIONDATE>February 2018</#def>
<#def CURRENTVERSIONURL>V8.7.2</#def>
<#def CURRENTVERSIONTAG>V8.7.2</#def>
<#def CURRENTVERSIONURL><#BASEURL><#CURRENTVERSIONTAG></#def>

<#def UPCOMINGMAJORVERSION>8.8</#def>
<#def UPCOMINGMINORVERSION>+beta1</#def>
<#def UPCOMINGVERSION><#UPCOMINGMAJORVERSION><#UPCOMINGMINORVERSION></#def>
<#def UPCOMINGVERSIONDATE>March 2018</#def>
<#def UPCOMINGVERSIONTAG>V8.8+beta1</#def>
<#def UPCOMINGVERSIONURL><#BASEURL><#UPCOMINGVERSIONTAG></#def>
15 changes: 15 additions & 0 deletions news/144
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
<#def ID>144</#def>
<#def TITLE>Coq 8.8+beta1 is out</#def>
<#def AUTHOR>Maxime Dénès</#def>
<#def DATE>19 Mar 2018</#def>
<#def DESCR>
The <a href="https://github.com/coq/coq/releases/tag/V8.8+beta1">first beta
release of Coq 8.8</a> is available for testing. It features better
performances, tactic improvements, many enhancements for universe users, a new
Export modifier for setting options, support for goal selectors in front of
focusing brackets and a new experimental -mangle-names option for linting proof
scripts.

Feedback and <a href="https://github.com/coq/coq/issues">bug reports</a> are extremely welcome.</p>

</#def>
4 changes: 2 additions & 2 deletions pages/download.html
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@
</ul>

<p>A lot of other changes are described in the
<a href="https://github.com/coq/coq/blob/<#CURRENTVERSIONURL>/CHANGES">CHANGES file</a>.</p>
<a href="https://github.com/coq/coq/blob/<#CURRENTVERSIONTAG>/CHANGES">CHANGES file</a>.</p>

<p>This is the second release of Coq developed on a time-based development
cycle. Its development spanned 9 months from the release of Coq 8.6 and was
Expand All @@ -47,7 +47,7 @@

<p>For downloads (in particular to get installers for Windows and Mac OS, or a
tarball of the sources), please go to
<a href="https://github.com/coq/coq/releases/tag/<#CURRENTVERSIONURL>">the release
<a href="<#CURRENTVERSIONURL>">the release
page on GitHub</a>.</p>

</div><!-- frameworkcontent -->
Expand Down
4 changes: 4 additions & 0 deletions pages/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,15 @@
<#CURRENTVERSION></a>, released in <#CURRENTVERSIONDATE>. It features
improved performances, some new tactics, cumulative inductive type support, a
redesigned <tt>coq_makefile</tt> and the integration of the SSReflect plugin.</p>

<p><a href="<#UPCOMINGVERSIONURL>">The upcoming version, Coq <#UPCOMINGVERSION></a>, released
in <#UPCOMINGVERSIONDATE>, is also available for testing.</p>
</div>

<div class="frameworklinks">
<ul>
<li><a href="/download">Get Coq <#CURRENTVERSION></a></li>
<li><a href="<#UPCOMINGVERSIONURL>">Get Coq <#UPCOMINGVERSION></a></li>
</ul>
</div>
</div>
Expand Down

0 comments on commit a448ac5

Please sign in to comment.