[acl2/acl2] 1779c4: add a book containing theorems (un)signed-byte-p-b...

2 views
Skip to first unread message

GitHub

unread,
Aug 11, 2016, 3:03:10 PM8/11/16
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 1779c47f5fe648257cfe11307bb2070f889e9e31
https://github.com/acl2/acl2/commit/1779c47f5fe648257cfe11307bb2070f889e9e31
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-07-21 (Thu, 21 Jul 2016)

Changed paths:
A books/centaur/bitops/width-find-rule.lisp

Log Message:
-----------
add a book containing theorems (un)signed-byte-p-by-find-rule, for proving widths greater than already-proven ones


Commit: 4c7d36780ba93e3f738220814ed29fd9805e5bef
https://github.com/acl2/acl2/commit/4c7d36780ba93e3f738220814ed29fd9805e5bef
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M books/centaur/bitops/merge.lisp
M books/centaur/bitops/width-find-rule.lisp
M books/centaur/sv/svex/rewrite-rules.lisp
M books/centaur/sv/svtv/process.lisp

Log Message:
-----------
bitops and svex updates


Commit: d58032ea3b0f36e49dfe33f7b3954518219d4a92
https://github.com/acl2/acl2/commit/d58032ea3b0f36e49dfe33f7b3954518219d4a92
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M acl2-fns.lisp
M acl2-init.lisp
M acl2.lisp
M axioms.lisp
M basis-a.lisp
M basis-b.lisp
M books/GNUmakefile
M books/centaur/misc/hons-extra.lisp
R books/kestrel/general/alists-tests.lisp
R books/kestrel/general/alists.lisp
R books/kestrel/general/auto-termination-tests.acl2
R books/kestrel/general/auto-termination-tests.lisp
R books/kestrel/general/auto-termination.lisp
R books/kestrel/general/define-sk-tests.lisp
R books/kestrel/general/define-sk.lisp
R books/kestrel/general/testing-tests.lisp
R books/kestrel/general/testing.lisp
R books/kestrel/general/top.lisp
R books/kestrel/general/ubi.lisp
M books/kestrel/soft/implementation.lisp
R books/kestrel/system/applicability-conditions-tests.lisp
R books/kestrel/system/applicability-conditions.lisp
R books/kestrel/system/defchoose-queries-tests.lisp
R books/kestrel/system/defchoose-queries.lisp
R books/kestrel/system/defun-sk-queries-tests.lisp
R books/kestrel/system/defun-sk-queries.lisp
R books/kestrel/system/directed-untranslate.acl2
R books/kestrel/system/directed-untranslate.lisp
R books/kestrel/system/event-forms-tests.lisp
R books/kestrel/system/event-forms.lisp
R books/kestrel/system/fresh-names-tests.lisp
R books/kestrel/system/fresh-names.lisp
R books/kestrel/system/install-not-norm-event-tests.lisp
R books/kestrel/system/install-not-norm-event.lisp
R books/kestrel/system/minimize-ruler-extenders.lisp
R books/kestrel/system/numbered-names-tests.lisp
R books/kestrel/system/numbered-names.lisp
R books/kestrel/system/prove-interface-tests.lisp
R books/kestrel/system/prove-interface.lisp
R books/kestrel/system/terms-tests.lisp
R books/kestrel/system/terms.lisp
R books/kestrel/system/top.lisp
R books/kestrel/system/user-interface-tests.lisp
R books/kestrel/system/user-interface.lisp
R books/kestrel/system/verify-guards-program.lisp
R books/kestrel/system/world-queries-tests.lisp
R books/kestrel/system/world-queries.lisp
M books/kestrel/top.lisp
A books/kestrel/utilities/applicability-conditions-tests.lisp
A books/kestrel/utilities/applicability-conditions.lisp
A books/kestrel/utilities/auto-termination-tests.acl2
A books/kestrel/utilities/auto-termination-tests.lisp
A books/kestrel/utilities/auto-termination.lisp
A books/kestrel/utilities/defchoose-queries-tests.lisp
A books/kestrel/utilities/defchoose-queries.lisp
A books/kestrel/utilities/define-sk-tests.lisp
A books/kestrel/utilities/define-sk.lisp
A books/kestrel/utilities/defun-sk-queries-tests.lisp
A books/kestrel/utilities/defun-sk-queries.lisp
A books/kestrel/utilities/directed-untranslate.acl2
A books/kestrel/utilities/directed-untranslate.lisp
A books/kestrel/utilities/event-forms-tests.lisp
A books/kestrel/utilities/event-forms.lisp
A books/kestrel/utilities/fresh-names-tests.lisp
A books/kestrel/utilities/fresh-names.lisp
A books/kestrel/utilities/install-not-norm-event-tests.lisp
A books/kestrel/utilities/install-not-norm-event.lisp
A books/kestrel/utilities/minimize-ruler-extenders.lisp
A books/kestrel/utilities/non-ascii-pathnames-raw.lsp
A books/kestrel/utilities/non-ascii-pathnames.acl2
A books/kestrel/utilities/non-ascii-pathnames.lisp
A books/kestrel/utilities/numbered-names-tests.lisp
A books/kestrel/utilities/numbered-names.lisp
A books/kestrel/utilities/prove-interface-tests.lisp
A books/kestrel/utilities/prove-interface.lisp
A books/kestrel/utilities/terms-tests.lisp
A books/kestrel/utilities/terms.lisp
A books/kestrel/utilities/testing-tests.lisp
A books/kestrel/utilities/testing.lisp
A books/kestrel/utilities/theorems/all-vars.lisp
A books/kestrel/utilities/theorems/list-sets.lisp
A books/kestrel/utilities/theorems/top.lisp
A books/kestrel/utilities/theorems/true-list-listp.lisp
A books/kestrel/utilities/theorems/world.lisp
A books/kestrel/utilities/top.lisp
A books/kestrel/utilities/types.lisp
A books/kestrel/utilities/ubi.lisp
A books/kestrel/utilities/user-interface-tests.lisp
A books/kestrel/utilities/user-interface.lisp
A books/kestrel/utilities/verify-guards-program-tests.acl2
A books/kestrel/utilities/verify-guards-program-tests.lisp
A books/kestrel/utilities/verify-guards-program.lisp
A books/kestrel/utilities/world-queries-tests.lisp
A books/kestrel/utilities/world-queries.lisp
M books/misc/check-acl2-exports.lisp
M books/misc/eval.lisp
M books/projects/x86isa/machine/guard-helpers.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-arithmetic-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-bitscan-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-convert-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-logical-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mov-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-mxcsr-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-shuffle-and-unpack-instructions.lisp
M books/projects/x86isa/machine/instructions/fp/x86-fp-simd-integer-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-arith-and-logic-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-bit-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-conditional-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-divide-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-exchange-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-jump-and-loop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-move-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-multiply-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-push-and-pop-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-rotate-and-shift-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-segmentation-instructions.lisp
M books/projects/x86isa/machine/instructions/x86-subroutine-instructions.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-environment.lisp
M books/projects/x86isa/machine/x86-register-readers-and-writers.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/portcullis/sharp-dot-constants.lisp
A books/projects/x86isa/proofs/dissertation-examples/acl2-customization.lsp
A books/projects/x86isa/proofs/dissertation-examples/cert.acl2
A books/projects/x86isa/proofs/dissertation-examples/clc-stc-programmer-mode.lisp
A books/projects/x86isa/proofs/dissertation-examples/clc-stc-system-level-marking-mode.lisp
A books/projects/x86isa/proofs/dissertation-examples/clc-stc-system-level-non-marking-mode.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/popcount/popcount.lisp
M books/projects/x86isa/proofs/top.lisp
M books/projects/x86isa/proofs/utilities/general-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/programmer-level-mode/programmer-level-memory-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/common-system-level-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/gl-lemmas.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/physical-memory-utils.lisp
A books/projects/x86isa/proofs/wordCount/cert.acl2
R books/projects/x86isa/proofs/wordCount/wc.acl2
M books/projects/x86isa/proofs/wordCount/wc.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
M books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
M books/projects/x86isa/proofs/zeroCopy/non-marking-mode/zeroCopy.lisp
A books/projects/x86isa/tools/execution/examples/documenting-edge-cases/README
A books/projects/x86isa/tools/execution/examples/documenting-edge-cases/acl2-customization.lsp
A books/projects/x86isa/tools/execution/examples/documenting-edge-cases/cert.acl2
A books/projects/x86isa/tools/execution/examples/documenting-edge-cases/disp-immed-fault.lsp
A books/projects/x86isa/tools/execution/examples/documenting-edge-cases/imm-bytes-for-rip-relative-addressing.lsp
A books/projects/x86isa/tools/execution/examples/documenting-edge-cases/redundant-prefixes.lsp
A books/projects/x86isa/tools/execution/examples/nop-sequence/acl2-customization.lsp
A books/projects/x86isa/tools/execution/examples/nop-sequence/cert.acl2
A books/projects/x86isa/tools/execution/examples/nop-sequence/nop.lsp
M books/projects/x86isa/utils/decoding-utilities.lisp
M books/projects/x86isa/utils/utilities.lisp
M books/std/util/defconsts.lisp
M books/system/doc/acl2-doc.lisp
M books/system/kestrel.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M history-management.lisp
M hons-raw.lisp
M hons.lisp
M installation/windows7.html
M interface-raw.lisp
M ld.lisp
M other-events.lisp
M rewrite.lisp
M simplify.lisp
M translate.lisp
M type-set-b.lisp

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/testing'


Commit: 48f303e6e143d0940b4397a272f613810bea40fe
https://github.com/acl2/acl2/commit/48f303e6e143d0940b4397a272f613810bea40fe
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M books/projects/x86isa/machine/x86-top-level-memory.lisp

Log Message:
-----------
fix x86 book for merge change


Commit: b4858079829f42c01a8ab46bbc99e4422ac2e88b
https://github.com/acl2/acl2/commit/b4858079829f42c01a8ab46bbc99e4422ac2e88b
Author: Sol Swords <ssw...@centtech.com>
Date: 2016-08-11 (Thu, 11 Aug 2016)

Changed paths:
M books/centaur/vl/server/public/describe.js

Log Message:
-----------
change vl server so modules clicked in describe windows open in main window


Compare: https://github.com/acl2/acl2/compare/d0bd52802479...b4858079829f

GitHub

unread,
Aug 11, 2016, 3:42:14 PM8/11/16
to acl2-...@googlegroups.com
Branch: refs/heads/master
Reply all
Reply to author
Forward
0 new messages