[acl2/acl2] 5a3f9a: include std/strings/fast-cat in fewer places; add ...

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 5a3f9a7101b0d19f44dcd05dd9f797aed934d053
https://github.com/acl2/acl2/commit/5a3f9a7101b0d19f44dcd05dd9f797aed934d053
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-05 (Thu, 05 Apr 2018)

Changed paths:
M books/centaur/vl/loader/parser/top.lisp
M books/centaur/vl/simpconfig.lisp
M books/centaur/vl/transforms/unparam/lineup.lisp
M books/centaur/vl/transforms/unparam/top.lisp
M books/centaur/vl/util/defs.lisp
M books/centaur/vl2014/loader/top.lisp
M books/centaur/vl2014/util/defs.lisp
M books/xdoc/display.lisp

Log Message:
-----------
include std/strings/fast-cat in fewer places; add a configuration tweak for vl


Commit: 1a8c3835baf05a786784004809c7f9219d038a12
https://github.com/acl2/acl2/commit/1a8c3835baf05a786784004809c7f9219d038a12
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-05 (Thu, 05 Apr 2018)

Changed paths:
M apply-raw.lisp
M apply.lisp
M axioms.lisp
M basis-a.lisp
M books/README.md
M books/doc/relnotes.lisp
M books/doc/top.lisp
M books/finite-set-theory/set-theory.acl2
M books/finite-set-theory/set-theory.lisp
M books/kestrel/utilities/directed-untranslate-tests.lisp
M books/kestrel/utilities/directed-untranslate.lisp
M books/kestrel/utilities/make-executable.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/pltpa/jacm-proveall.lsp
M books/projects/pltpa/pltpa.lisp
M books/projects/pltpa/standard-proveall.lsp
M books/projects/translators/l3-to-acl2/examples/mips/mips.lisp
M books/projects/translators/l3-to-acl2/examples/thacker/Makefile
M books/projects/translators/l3-to-acl2/examples/thacker/gold/tiny-logic.lisp
M books/projects/translators/l3-to-acl2/examples/thacker/gold/tiny.lisp
M books/projects/translators/l3-to-acl2/examples/thacker/tiny-manual.lisp
M books/projects/translators/l3-to-acl2/translator/l3-to-acl2.lisp
M books/projects/translators/l3-to-acl2/translator/l3.lisp
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/top-level-memory.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.lisp
M books/system/apply/apply.lisp
M books/system/doc/acl2-doc.lisp
A books/system/doc/developers-guide.lisp
M books/system/tests/apply-timings.lisp
M boot-strap-pass-2-a.lisp
M doc.lisp
M interface-raw.lisp
M other-events.lisp
M rewrite.lisp
M translate.lisp
M type-set-b.lisp
M workshops.html

Log Message:
-----------
Merge branch 'testing' of github.com:acl2/acl2


Commit: 5e3794c2e319e07edf169dfdedc74695f5a4739b
https://github.com/acl2/acl2/commit/5e3794c2e319e07edf169dfdedc74695f5a4739b
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-10 (Tue, 10 Apr 2018)

Changed paths:
M books/GNUmakefile
M books/build/certlib.pl
M books/centaur/aignet/balance.lisp
M books/centaur/aignet/cnf.lisp
M books/centaur/aignet/ipasir.lisp
M books/centaur/aignet/observability.lisp
A books/centaur/bitops/logsaturate.lisp
M books/centaur/fty/top.lisp
M books/centaur/sv/svex/rewrite-rules.lisp
M books/doc/relnotes.lisp
M books/kestrel/apt/restrict-design.lisp
M books/kestrel/apt/restrict-reference.lisp
M books/kestrel/apt/restrict-tests.lisp
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec-design.lisp
M books/kestrel/apt/tailrec-reference.lisp
M books/kestrel/apt/tailrec.lisp
M books/kestrel/utilities/bytes.lisp
A books/kestrel/utilities/digits-any-base-tests.lisp
A books/kestrel/utilities/digits-any-base.lisp
M books/kestrel/utilities/directed-untranslate-tests.lisp
M books/kestrel/utilities/directed-untranslate.lisp
M books/kestrel/utilities/top.lisp
M books/kestrel/utilities/typed-list-theorems.lisp
A books/kestrel/utilities/zp-lists-tests.lisp
A books/kestrel/utilities/zp-lists.lisp
M books/projects/translators/l3-to-acl2/examples/mips/mips.lisp
M books/projects/translators/l3-to-acl2/examples/thacker/gold/tiny-logic.lisp
M books/projects/translators/l3-to-acl2/examples/thacker/gold/tiny.lisp
M books/projects/translators/l3-to-acl2/examples/thacker/tiny-manual.lisp
M books/projects/translators/l3-to-acl2/translator/l3-to-acl2.lisp
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/top-level-memory.lisp
M books/projects/x86isa/proofs/codewalker-examples/factorial.lisp
M books/projects/x86isa/proofs/codewalker-examples/popcount-32.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy.lisp
M books/projects/x86isa/proofs/dataCopy/init.lisp
M books/projects/x86isa/proofs/dataCopy/loop-base.lisp
M books/projects/x86isa/proofs/dataCopy/loop-recur.lisp
M books/projects/x86isa/proofs/factorial/fact-inductive-assertions.lisp
M books/projects/x86isa/proofs/factorial/fact-wormhole-abstraction.lisp
M books/projects/x86isa/proofs/powOfTwo/powOfTwo.lisp
M books/projects/x86isa/proofs/wordCount/wc.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-1.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-2.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
M books/projects/x86isa/proofs/zeroCopy/non-marking-mode/zeroCopy.lisp
M books/std/basic/defs.lisp
M books/system/doc/acl2-doc.lisp
M books/system/to-do.txt
A books/tools/table-replay.lisp
M doc.lisp
M doc/home-page.lisp
M ld.lisp
M translate.lisp

Log Message:
-----------
Merge branch 'testing' of github.com:acl2/acl2


Commit: 82ee2187e6dcacea2977bc20820bc4a46c8ec46a
https://github.com/acl2/acl2/commit/82ee2187e6dcacea2977bc20820bc4a46c8ec46a
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-12 (Thu, 12 Apr 2018)

Changed paths:
M books/std/util/define.lisp
M books/std/util/defines.lisp
M books/std/util/returnspecs.lisp

Log Message:
-----------
refine and document substitutions performed by defret and define returnspec theorems

fix xdoc problem in defret documentation


Commit: d3113c6cef1c00ca4a67339516a0c3144744000b
https://github.com/acl2/acl2/commit/d3113c6cef1c00ca4a67339516a0c3144744000b
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-12 (Thu, 12 Apr 2018)

Changed paths:
M books/centaur/bitops/sparseint.lisp

Log Message:
-----------
sparseint -- localize some internal theorems


Commit: f61dde162b7e4fdc92d90a26b45c10d6066aab10
https://github.com/acl2/acl2/commit/f61dde162b7e4fdc92d90a26b45c10d6066aab10
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-12 (Thu, 12 Apr 2018)

Changed paths:
M books/acl2s/cgen/top.lisp
M books/doc/relnotes.lisp
M books/kestrel/abnf/abstractor.lisp
M books/kestrel/apt/restrict.lisp
M books/kestrel/apt/tailrec.lisp
M books/kestrel/utilities/error-checking.lisp
M books/kestrel/utilities/make-executable.lisp
M books/kestrel/utilities/term-function-recognizers.lisp
M books/kestrel/utilities/terms.lisp
M books/kestrel/utilities/world-queries-tests.lisp
M books/kestrel/utilities/world-queries.lisp
M books/projects/smtlink/doc.lisp
M books/projects/smtlink/examples/examples.lisp
M books/projects/smtlink/trusted/z3-py/translator.lisp
M books/projects/smtlink/verified/Smtlink.lisp
M books/projects/smtlink/verified/goal-generator.lisp
M books/projects/smtlink/verified/hint-interface.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/top-level-memory.lisp
M books/projects/x86isa/machine/x86.lisp

Log Message:
-----------
Merge branch 'testing' of github.com:acl2/acl2


Compare: https://github.com/acl2/acl2/compare/d816b4738eb4...f61dde162b7e

[GitHub]

Branch: refs/heads/master

Commit: 31c7a43f424aebadb1ee3cd7411a0728df34bf96
https://github.com/acl2/acl2/commit/31c7a43f424aebadb1ee3cd7411a0728df34bf96
Author: Sol Swords <ssw...@centtech.com>
Date: 2018-04-11 (Wed, 11 Apr 2018)

Changed paths:
M books/doc/relnotes.lisp
M books/doc/top.lisp
A books/xdoc/archive.lisp
M books/xdoc/preprocess.lisp
A books/xdoc/tests/archtest-top.lisp
A books/xdoc/tests/archtest.lisp
A books/xdoc/tests/archtest2.lisp

Log Message:
-----------
add xdoc feature to support books that contain some documentation without the events it's based on

Commit: 37844644370b41466ab196cc32a7097418348fbf
https://github.com/acl2/acl2/commit/37844644370b41466ab196cc32a7097418348fbf
Author: solswords <ssw...@gmail.com>

Date: 2018-04-12 (Thu, 12 Apr 2018)

Changed paths:

M books/doc/relnotes.lisp
M books/doc/top.lisp
A books/xdoc/archive.lisp
M books/xdoc/preprocess.lisp
A books/xdoc/tests/archtest-top.lisp
A books/xdoc/tests/archtest.lisp
A books/xdoc/tests/archtest2.lisp

Log Message:
-----------
Merge pull request #836 from solswords/xdoc_archive

add xdoc feature to support books that contain some documentation wit…


Compare: https://github.com/acl2/acl2/compare/d816b4738eb4...37844644370b