mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Separate out library code with its own license
This commit is contained in:
parent
51a7fae33e
commit
c502399de4
6 changed files with 107 additions and 1 deletions
2
.gitignore
vendored
2
.gitignore
vendored
|
@ -23,3 +23,5 @@ Deeper.ml*
|
||||||
DeeperWithFail.ml*
|
DeeperWithFail.ml*
|
||||||
*.dir-locals.el
|
*.dir-locals.el
|
||||||
*.cache
|
*.cache
|
||||||
|
fraplib
|
||||||
|
fraplib.tgz
|
||||||
|
|
59
LICENSE
Normal file
59
LICENSE
Normal file
|
@ -0,0 +1,59 @@
|
||||||
|
"Formal Reasoning About Programs" code license information
|
||||||
|
<http://adam.chlipala.net/frap/>
|
||||||
|
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||||
|
|
||||||
|
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.
|
22
Makefile
22
Makefile
|
@ -25,9 +25,29 @@ clean:: Makefile.coq
|
||||||
frap.tgz: Makefile _CoqProject *.v *.tex *.html
|
frap.tgz: Makefile _CoqProject *.v *.tex *.html
|
||||||
git archive --format=tar.gz HEAD >frap.tgz
|
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/
|
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_book.pdf $(WHERE)
|
||||||
rsync frap.tgz $(WHERE)
|
rsync frap.tgz $(WHERE)
|
||||||
|
rsync fraplib.tgz $(WHERE)
|
||||||
rsync index.html $(WHERE)
|
rsync index.html $(WHERE)
|
||||||
|
|
11
Makefile.fraplib
Normal file
11
Makefile.fraplib
Normal file
|
@ -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
|
13
_CoqProject.fraplib
Normal file
13
_CoqProject.fraplib
Normal file
|
@ -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
|
|
@ -15,6 +15,7 @@
|
||||||
<li><a href="https://github.com/achlipala/frap">Source on GitHub</a></li>
|
<li><a href="https://github.com/achlipala/frap">Source on GitHub</a></li>
|
||||||
<li><a href="frap_book.pdf">Quasi-latest PDF draft</a></li>
|
<li><a href="frap_book.pdf">Quasi-latest PDF draft</a></li>
|
||||||
<li><a href="frap.tgz">Quasi-latest source-code tarball</a></li>
|
<li><a href="frap.tgz">Quasi-latest source-code tarball</a></li>
|
||||||
|
<li><a href="fraplib.tgz">Quasi-latest source-code tarball, library only</a> (warning: the author really does not recommend using it in serious projects!)</li>
|
||||||
</ul>
|
</ul>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue