From c502399de4d362ab83925c89e7c479e7c56b53b5 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 17 Mar 2020 09:22:06 -0400 Subject: [PATCH] Separate out library code with its own license --- .gitignore | 2 ++ LICENSE | 59 +++++++++++++++++++++++++++++++++++++++++++++ Makefile | 22 ++++++++++++++++- Makefile.fraplib | 11 +++++++++ _CoqProject.fraplib | 13 ++++++++++ index.html | 1 + 6 files changed, 107 insertions(+), 1 deletion(-) create mode 100644 LICENSE create mode 100644 Makefile.fraplib create mode 100644 _CoqProject.fraplib diff --git a/.gitignore b/.gitignore index e073285..f30f860 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,5 @@ Deeper.ml* DeeperWithFail.ml* *.dir-locals.el *.cache +fraplib +fraplib.tgz diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..b41933f --- /dev/null +++ b/LICENSE @@ -0,0 +1,59 @@ +"Formal Reasoning About Programs" code license information + +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +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. + +However, a few of the library modules used here are sufficiently +useful that they are released separately under a BSD license, included +below. However, the author's advice is: 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, +sacrificing practicality (and minimal use of axioms) for simplicity. + +The following license applies ONLY to the source files: +Relations.v +Map.v +Var.v +Invariant.v +ModelCheck.v +FrapWithoutSets.v +Sets.v +Frap.v +AbstractInterpret.v +SepCancel.v + +~~~~~~~~~~~ +BSD LICENSE +~~~~~~~~~~~ + +Copyright (c) 2016-2020, 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. diff --git a/Makefile b/Makefile index a0c622e..e38bf34 100644 --- a/Makefile +++ b/Makefile @@ -25,9 +25,29 @@ clean:: Makefile.coq frap.tgz: Makefile _CoqProject *.v *.tex *.html git archive --format=tar.gz HEAD >frap.tgz +fraplib.tgz: Makefile + rm -rf fraplib + mkdir fraplib + cp LICENSE fraplib/ + cp Makefile.fraplib fraplib/Makefile + cp _CoqProject.fraplib fraplib/_CoqProject + cp Relations.v fraplib/ + cp Map.v fraplib/ + cp Var.v fraplib/ + cp Invariant.v fraplib/ + cp ModelCheck.v fraplib/ + cp FrapWithoutSets.v fraplib/ + cp Sets.v fraplib/ + cp Frap.v fraplib/ + cp Imp.v fraplib/ + cp AbstractInterpret.v fraplib/ + cp SepCancel.v fraplib/ + tar cf fraplib.tgz fraplib/* + WHERE=chlipala.net:sites/chlipala/adam/frap/ -install: index.html frap_book.pdf frap.tgz +install: index.html frap_book.pdf frap.tgz fraplib.tgz rsync frap_book.pdf $(WHERE) rsync frap.tgz $(WHERE) + rsync fraplib.tgz $(WHERE) rsync index.html $(WHERE) diff --git a/Makefile.fraplib b/Makefile.fraplib new file mode 100644 index 0000000..5d62089 --- /dev/null +++ b/Makefile.fraplib @@ -0,0 +1,11 @@ +.PHONY: coq + +coq: Makefile.coq + $(MAKE) -f Makefile.coq + +Makefile.coq: Makefile _CoqProject *.v + coq_makefile -f _CoqProject -o Makefile.coq + +clean:: Makefile.coq + $(MAKE) -f Makefile.coq clean + rm -f Makefile.coq diff --git a/_CoqProject.fraplib b/_CoqProject.fraplib new file mode 100644 index 0000000..72daee3 --- /dev/null +++ b/_CoqProject.fraplib @@ -0,0 +1,13 @@ +-R . Frap +-arg -w -arg -undeclared-scope +Map.v +Var.v +Sets.v +Relations.v +Invariant.v +ModelCheck.v +Imp.v +AbstractInterpret.v +FrapWithoutSets.v +Frap.v +SepCancel.v diff --git a/index.html b/index.html index 9174503..5f97a67 100644 --- a/index.html +++ b/index.html @@ -15,6 +15,7 @@
  • Source on GitHub
  • Quasi-latest PDF draft
  • Quasi-latest source-code tarball
    • +
  • Quasi-latest source-code tarball, library only (warning: the author really does not recommend using it in serious projects!)