[acl2-books] r988 committed - slight clean up of xdoc/xdoc-impl package stuff
acl2-...@googlecode.com
Author: jared.c.davis
Date: Tue Feb 28 10:56:33 2012
Log: slight clean up of xdoc/xdoc-impl package stuff
http://code.google.com/p/acl2-books/source/detail?r=988
Added:
/trunk/xdoc-impl/portcullis.acl2
/trunk/xdoc-impl/portcullis.lisp
Modified:
/trunk/xdoc/portcullis.acl2
/trunk/xdoc-impl/cert.acl2
/trunk/xdoc-impl/extra-packages.acl2
=======================================
--- /dev/null
+++ /trunk/xdoc-impl/portcullis.acl2 Tue Feb 28 10:56:33 2012
@@ -0,0 +1,23 @@
+; XDOC Documentation System for ACL2
+; Copyright (C) 2009-2011 Centaur Technology
+;
+; Contact:
+; Centaur Technology Formal Verification Group
+; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
+; http://www.centtech.com/
+;
+; This program is free software; you can redistribute it and/or modify it
under
+; the terms of the GNU General Public License as published by the Free
Software
+; Foundation; either version 2 of the License, or (at your option) any
later
+; version. This program is distributed in the hope that it will be useful
but
+; WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or
+; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
+; more details. You should have received a copy of the GNU General Public
+; License along with this program; if not, write to the Free Software
+; Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335,
USA.
+;
+; Original author: Jared Davis <ja...@centtech.com>
+
+(ld "xdoc/package.lsp" :dir :system)
+(ld "str/package.lsp" :dir :system)
+(certify-book "portcullis" ? t :ttags :all)
=======================================
--- /dev/null
+++ /trunk/xdoc-impl/portcullis.lisp Tue Feb 28 10:56:33 2012
@@ -0,0 +1,30 @@
+; XDOC Documentation System for ACL2
+; Copyright (C) 2009-2011 Centaur Technology
+;
+; Contact:
+; Centaur Technology Formal Verification Group
+; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
+; http://www.centtech.com/
+;
+; This program is free software; you can redistribute it and/or modify it
under
+; the terms of the GNU General Public License as published by the Free
Software
+; Foundation; either version 2 of the License, or (at your option) any
later
+; version. This program is distributed in the hope that it will be useful
but
+; WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or
+; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
+; more details. You should have received a copy of the GNU General Public
+; License along with this program; if not, write to the Free Software
+; Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335,
USA.
+;
+; Original author: Jared Davis <ja...@centtech.com>
+
+
+; portcullis.lisp
+;
+; This book gets included by cert.acl2, rather than directly putting in the
+; declaration of the xdoc package. This way, the resulting .cert files for
+; the other xdoc books just contain an (include-book "portcullis") command,
+; rather than the whole package declaration for the XDOC package.
+
+(in-package "XDOC")
+
=======================================
--- /trunk/xdoc/portcullis.acl2 Thu Feb 23 16:57:09 2012
+++ /trunk/xdoc/portcullis.acl2 Tue Feb 28 10:56:33 2012
@@ -19,6 +19,4 @@
; Original author: Jared Davis <ja...@centtech.com>
(ld "package.lsp")
-(ld ; break dependency
- "str/package.lsp" :dir :system)
(certify-book "portcullis" ? t :ttags :all)
=======================================
--- /trunk/xdoc-impl/cert.acl2 Fri Dec 30 09:23:49 2011
+++ /trunk/xdoc-impl/cert.acl2 Tue Feb 28 10:56:33 2012
@@ -19,4 +19,4 @@
; Original author: Jared Davis <ja...@centtech.com>
(in-package "ACL2")
-(include-book "../xdoc/portcullis")
+(include-book "portcullis")
=======================================
--- /trunk/xdoc-impl/extra-packages.acl2 Fri Dec 30 09:23:49 2011
+++ /trunk/xdoc-impl/extra-packages.acl2 Tue Feb 28 10:56:33 2012
@@ -30,6 +30,7 @@
(ld "hacking/hacker-pkg.lsp" :dir :system)
(ld "cutil/package.lsp" :dir :system)
(ld "serialize/package.lsp" :dir :system)
+(ld "finite-set-theory/osets/sets.defpkg" :dir :system)
(ld "str/package.lsp" :dir :system)
(ld "tools/flag-package.lsp" :dir :system)
(certify-book "extra-packages" ? t)