Mercurial > cpdt > repo
changeset 517:136d4b84eb96
Build an open-source release of library modules
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 05 Dec 2013 15:51:33 -0500 |
parents | a8377999fcf9 |
children | 2bd6b00f831f |
files | .hgignore Makefile src/LICENSE staging/index.html |
diffstat | 4 files changed, 69 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/.hgignore Wed Oct 16 10:41:23 2013 -0400 +++ b/.hgignore Thu Dec 05 15:51:33 2013 -0500 @@ -17,6 +17,8 @@ staging/html/.dir cpdt.tgz +cpdtlib.tgz +cpdtlib *.glob *.v.d
--- a/Makefile Wed Oct 16 10:41:23 2013 -0400 +++ b/Makefile Thu Dec 05 15:51:33 2013 -0500 @@ -52,8 +52,16 @@ cpdt.tgz: hg archive -t tgz $@ -install: cpdt.tgz latex/cpdt.pdf latex/exercises.pdf html - cp cpdt.tgz staging/ +cpdtlib.tgz: Makefile + mkdir -p cpdtlib + cp src/LICENSE cpdtlib + cp src/CpdtTactics.v cpdtlib + cp src/MoreSpecif.v cpdtlib + cp src/DepList.v cpdtlib + tar zcf cpdtlib.tgz cpdtlib/* + +install: cpdt.tgz cpdtlib.tgz latex/cpdt.pdf latex/exercises.pdf html + cp cpdt*.tgz staging/ cp latex/cpdt.pdf staging/ cp latex/exercises.pdf staging/ex/ cp -R html staging/
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/LICENSE Thu Dec 05 15:51:33 2013 -0500 @@ -0,0 +1,56 @@ +"Certified Programming with Dependent Types" code license information +<http://adam.chlipala.net/cpdt/> +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +CAUTION: Most of the source files in this distribution are NOT +open-source in the usual sense. See the comment at the beginning of +each source file for its license, which is Creative Commons, oriented +more toward free distribution of books than the usual collaborative +model of open-source software. The author really is trying to keep +you from remixing your own versions of the book, which MIT Press might +not be too happy about. + +However, a few of the library modules used here are sufficiently +useful that they are released separately under a BSD license, included +below. The author wants to repeat some advice from the book text, +though: please don't use these library modules in real projects. They +are not designed for any use beside getting the reader up and running +quickly in reading the book. All of their content, including the +"crush" functionality, is rather trivial to implement from scratch for +your own projects, using the techniques that the book presents. + + +The following license applies ONLY to the source files: +CpdtTactics.v +MoreSpecif.v +DepList.v + +~~~~~~~~~~~ +BSD LICENSE +~~~~~~~~~~~ + +Copyright (c) 2006-2013, Adam Chlipala +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +- Redistributions of source code must retain the above copyright notice, + this list of conditions and the following disclaimer. +- Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. +- The names of contributors may not be used to endorse or promote products + derived from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE +LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR +CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF +SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS +INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN +CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) +ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE +POSSIBILITY OF SUCH DAMAGE.
--- a/staging/index.html Wed Oct 16 10:41:23 2013 -0400 +++ b/staging/index.html Thu Dec 05 15:51:33 2013 -0500 @@ -23,6 +23,7 @@ <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li> <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a> [note that the author focuses on the PDF version and doesn't make an effort to keep the HTML version particularly pleasant to use]</li> <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li> +<li> <a href="cpdtlib.tgz">Tarball of a few generally useful library modules from the book</a> (which are released under an open-source license, while the book generally isn't)</li> <li> <a href="repo">Public, read-only Mercurial repository</a></li> <li> <a href="updates.rss">RSS feed of updates</a></li> </ul>