[acl2/acl2] 4668ff: Merge from acl2/acl2.
0 views
Skip to first unread message
GitHub
Jul 23, 2016, 12:01:30 PM7/23/16
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 4668ff9ee36fdda57f2c95bafc8537fdec3a6776
https://github.com/acl2/acl2/commit/4668ff9ee36fdda57f2c95bafc8537fdec3a6776
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-09 (Thu, 09 Jun 2016)
Changed paths:
A books/system/all-ffn-symbs-logic.lisp
M books/system/doc/acl2-doc.lisp
M books/system/termp.lisp
M books/system/top.lisp
M boot-strap-pass-2.lisp
M other-processes.lisp
M prove.lisp
M rewrite.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 3d81db6ba2e2d88fe469505e0c7543496e686e5c
https://github.com/acl2/acl2/commit/3d81db6ba2e2d88fe469505e0c7543496e686e5c
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-09 (Thu, 09 Jun 2016)
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 13b1874cfbfdabf1b71d05873ce194d69a8b0534
https://github.com/acl2/acl2/commit/13b1874cfbfdabf1b71d05873ce194d69a8b0534
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-10 (Fri, 10 Jun 2016)
Changed paths:
M books/centaur/sv/vl/elaborate.lisp
M books/centaur/sv/vl/vl-svstmt.lisp
M books/centaur/vl/kit/lint.lisp
M books/centaur/vl/lint/suppress-warnings.lisp
M books/centaur/vl/mlib/json.lisp
M books/centaur/vl/mlib/print-warnings.lisp
M books/centaur/vl/mlib/writer.lisp
M books/centaur/vl/util/warnings.lisp
M books/clause-processors/meta-extract-user.lisp
M books/std/strings/strsubst.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/def-functional-instance.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 6a22bc780a9b438d66f2fe2d8070bae7e85f6197
https://github.com/acl2/acl2/commit/6a22bc780a9b438d66f2fe2d8070bae7e85f6197
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-10 (Fri, 10 Jun 2016)
Changed paths:
M books/kestrel/system/directed-untranslate.lisp
M books/system/doc/acl2-doc.lisp
M boot-strap-pass-2.lisp
M doc.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 017b84ac74adbcab7eb629a29118f3ad08845752
https://github.com/acl2/acl2/commit/017b84ac74adbcab7eb629a29118f3ad08845752
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-13 (Mon, 13 Jun 2016)
Changed paths:
M books/misc/check-acl2-exports.lisp
M books/projects/apply/apply-prim.lisp
M books/projects/apply/apply.lisp
M books/projects/apply/chronology.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 8e1e830ed9e93943dd50afb8b50eed05fec98370
https://github.com/acl2/acl2/commit/8e1e830ed9e93943dd50afb8b50eed05fec98370
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-13 (Mon, 13 Jun 2016)
Changed paths:
M books/kestrel/system/defun-sk-queries.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 9819662d42bfae379110361852dbe55bf1335570
https://github.com/acl2/acl2/commit/9819662d42bfae379110361852dbe55bf1335570
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-14 (Tue, 14 Jun 2016)
Changed paths:
A books/system/kestrel.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 5045b36d102945a014647810e65c0a6886e4cf5c
https://github.com/acl2/acl2/commit/5045b36d102945a014647810e65c0a6886e4cf5c
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-14 (Tue, 14 Jun 2016)
Changed paths:
M books/kestrel/system/defun-sk-queries.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: d350155c9f05f7c85dcc21421199afde6cbfec29
https://github.com/acl2/acl2/commit/d350155c9f05f7c85dcc21421199afde6cbfec29
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-15 (Wed, 15 Jun 2016)
Changed paths:
M books/system/kestrel.lisp
M interface-raw.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: b0e4a504088ad9ed1b5bc06f4a6a7b736948233a
https://github.com/acl2/acl2/commit/b0e4a504088ad9ed1b5bc06f4a6a7b736948233a
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-16 (Thu, 16 Jun 2016)
Changed paths:
M books/centaur/aignet/construction.lisp
M books/centaur/fty/bitstruct.lisp
M books/clause-processors/meta-extract-user.lisp
A books/kestrel/general/alists-tests.lisp
A books/kestrel/system/guards-program-mode.lisp
M books/kestrel/system/top.lisp
M books/std/util/defines.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M ld.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 1c78e9ae8987d8b3344f599268b3acd850ba31b0
https://github.com/acl2/acl2/commit/1c78e9ae8987d8b3344f599268b3acd850ba31b0
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-16 (Thu, 16 Jun 2016)
Changed paths:
R books/kestrel/system/guards-program-mode.lisp
M books/kestrel/system/top.lisp
A books/kestrel/system/verify-guards-program.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 099d17f6ed2897ea176e67659dace2d0e7d4f3ce
https://github.com/acl2/acl2/commit/099d17f6ed2897ea176e67659dace2d0e7d4f3ce
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-17 (Fri, 17 Jun 2016)
Changed paths:
M books/kestrel/soft/top.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: cfd7fa65eeed8189b42425c2e95c49ab05b8f707
https://github.com/acl2/acl2/commit/cfd7fa65eeed8189b42425c2e95c49ab05b8f707
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-17 (Fri, 17 Jun 2016)
Changed paths:
M books/kestrel/system/world-queries.lisp
M books/system/kestrel.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 0ce65ea8504f0ff89ab8b9f71244f5fea38bdcab
https://github.com/acl2/acl2/commit/0ce65ea8504f0ff89ab8b9f71244f5fea38bdcab
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-18 (Sat, 18 Jun 2016)
Changed paths:
M books/kestrel/general/testing.lisp
M books/kestrel/system/world-queries.lisp
M books/system/kestrel.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 7b7a3bd867d8f4c9777f308b8b2a469588b50188
https://github.com/acl2/acl2/commit/7b7a3bd867d8f4c9777f308b8b2a469588b50188
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-20 (Mon, 20 Jun 2016)
Changed paths:
M acl2.lisp
M axioms.lisp
M bin/purity.sh
M books/kestrel/general/testing-tests.lisp
M books/kestrel/general/testing.lisp
M books/kestrel/system/verify-guards-program.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M interface-raw.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: cde10b4a3d7f3258904fa46a2c5d3a3c19188c07
https://github.com/acl2/acl2/commit/cde10b4a3d7f3258904fa46a2c5d3a3c19188c07
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-20 (Mon, 20 Jun 2016)
Changed paths:
M books/kestrel/general/testing-tests.lisp
M books/kestrel/general/testing.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 908f0e21ab53219f820f9afe9dcea23ec96c0b77
https://github.com/acl2/acl2/commit/908f0e21ab53219f820f9afe9dcea23ec96c0b77
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-22 (Wed, 22 Jun 2016)
Changed paths:
M GNUmakefile
M axioms.lisp
M basis-a.lisp
M books/GNUmakefile
M books/kestrel/system/verify-guards-program.lisp
M books/system/doc/acl2-doc.lisp
M books/system/kestrel.lisp
M books/system/top.lisp
M boot-strap-pass-2.lisp
M defuns.lisp
M doc.lisp
M history-management.lisp
M induct.lisp
M interface-raw.lisp
M other-events.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: d4dd927e4ca988bc284f2da2cb2b07e70470b479
https://github.com/acl2/acl2/commit/d4dd927e4ca988bc284f2da2cb2b07e70470b479
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-23 (Thu, 23 Jun 2016)
Changed paths:
M books/centaur/aig/bddify-correct.lisp
M books/centaur/aig/bddify.lisp
M books/centaur/sv/svtv/process.lisp
M books/demos/Readme.lsp
M books/kestrel/system/world-queries.lisp
M books/std/util/da-base.lisp
M books/system/parallel/Readme.lsp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 38fd53c6ffed203e42504b2f421509c826f44d1b
https://github.com/acl2/acl2/commit/38fd53c6ffed203e42504b2f421509c826f44d1b
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-23 (Thu, 23 Jun 2016)
Changed paths:
M books/kestrel/general/alists.lisp
R books/kestrel/general/ensure-tests.lisp
R books/kestrel/general/ensure.lisp
M books/kestrel/general/top.lisp
M books/kestrel/system/minimize-ruler-extenders.lisp
M books/kestrel/system/prove-interface.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/ubi.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: cb43ff6963e68a94c457a91ae6c1d04a145dbc41
https://github.com/acl2/acl2/commit/cb43ff6963e68a94c457a91ae6c1d04a145dbc41
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-24 (Fri, 24 Jun 2016)
Changed paths:
A books/kestrel/system/event-forms.lisp
M books/kestrel/system/top.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: e99632f92a48987bc2a554637925d49f0b3bb71d
https://github.com/acl2/acl2/commit/e99632f92a48987bc2a554637925d49f0b3bb71d
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-28 (Tue, 28 Jun 2016)
Changed paths:
M books/centaur/gl/auto-bindings.lisp
M books/centaur/sv/svtv/process.lisp
M books/centaur/vl/server/public/main.html
M books/tools/templates.lisp
M books/xdoc/parse-xml.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 37b734b31a7c6825d6fe2db7d8734e6fbedc95a7
https://github.com/acl2/acl2/commit/37b734b31a7c6825d6fe2db7d8734e6fbedc95a7
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-28 (Tue, 28 Jun 2016)
Changed paths:
A books/kestrel/system/applicability-conditions-tests.lisp
A books/kestrel/system/applicability-conditions.lisp
A books/kestrel/system/event-forms-tests.lisp
M books/kestrel/system/event-forms.lisp
A books/kestrel/system/fresh-names-tests.lisp
A books/kestrel/system/fresh-names.lisp
A books/kestrel/system/install-not-norm-event-tests.lisp
A books/kestrel/system/install-not-norm-event.lisp
A books/kestrel/system/numbered-names-tests.lisp
A books/kestrel/system/numbered-names.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/top.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 6c22bb49766552a8edaeec7f9dbdac84ca2415c2
https://github.com/acl2/acl2/commit/6c22bb49766552a8edaeec7f9dbdac84ca2415c2
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-28 (Tue, 28 Jun 2016)
Changed paths:
M bdd.lisp
M books/centaur/aignet/aignet-logic.lisp
M books/centaur/fty/fixequiv.lisp
M books/centaur/gl/symbolic-arithmetic.lisp
M books/centaur/sv/vl/moddb.lisp
M books/centaur/vl/mlib/blocks.lisp
M books/centaur/vl2014/mlib/blocks.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/stobj-preservation.lisp
M books/doc/relnotes.lisp
M books/kestrel/system/auto-termination.lisp
M books/kestrel/system/world-queries.lisp
M books/projects/quadratic-reciprocity/euclid.lisp
M books/std/util/defines.lisp
M books/std/util/returnspecs.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/stobj-frame.lisp
M books/xdoc/topics.lisp
M doc.lisp
M rewrite.lisp
M tau.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 592f1e91594b163c10bf0ca1134fb2f8d7e0b488
https://github.com/acl2/acl2/commit/592f1e91594b163c10bf0ca1134fb2f8d7e0b488
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-29 (Wed, 29 Jun 2016)
Changed paths:
M basis-a.lisp
M books/projects/doc.lisp
A books/projects/x86isa/doc.acl2
A books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-ia32e-paging.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
A books/projects/x86isa/proofs/dataCopy/dataCopy-init.lisp
A books/projects/x86isa/proofs/dataCopy/dataCopy-loop-base.lisp
A books/projects/x86isa/proofs/dataCopy/dataCopy-loop-recur.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy.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/disjoint.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
A 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
A books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-top.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-utils.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/acl2-customization.lsp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/cert.acl2
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/common-paging-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/gather-paging-structures-thms.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/gather-paging-structures.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/la-to-pa-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/page-dir-ptr-table-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/page-directory-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/page-table-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/paging-basics.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/paging-top.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/pml4-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/acl2-customization.lsp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/cert.acl2
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/common-paging-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/gather-paging-structures-thms.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/gather-paging-structures.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/la-to-pa-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-dir-ptr-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-directory-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/paging-basics.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/pml4-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/physical-memory-utils.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/symbolic-simulation-in-marking-mode.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/top.lisp
R books/projects/x86isa/proofs/wordCount/cert.acl2
A books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/wordCount/wc.acl2
M books/projects/x86isa/proofs/wordCount/wc.lisp
R books/projects/x86isa/proofs/zeroCopy/acl2-customization.lsp
R books/projects/x86isa/proofs/zeroCopy/cert.acl2
A books/projects/x86isa/proofs/zeroCopy/marking-mode/acl2-customization.lsp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/cert.acl2
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-1.lisp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-2.lisp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
A books/projects/x86isa/proofs/zeroCopy/non-marking-mode/acl2-customization.lsp
A books/projects/x86isa/proofs/zeroCopy/non-marking-mode/cert.acl2
A books/projects/x86isa/proofs/zeroCopy/non-marking-mode/zeroCopy.lisp
R books/projects/x86isa/proofs/zeroCopy/zeroCopy-in-marking-mode.lisp
R books/projects/x86isa/proofs/zeroCopy/zeroCopy-in-non-marking-mode.lisp
M books/projects/x86isa/tools/execution/examples/dataCopy/dataCopy.lsp
M books/projects/x86isa/top.lisp
M books/system/doc/acl2-doc.lisp
M books/xdoc/topics.lisp
M doc.lisp
M other-events.lisp
M rewrite.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 70f6c6cdd4d8619f90dbc5b41dc3d8eecfbe6eae
https://github.com/acl2/acl2/commit/70f6c6cdd4d8619f90dbc5b41dc3d8eecfbe6eae
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-29 (Wed, 29 Jun 2016)
Changed paths:
A books/kestrel/general/define-sk-tests.lisp
A books/kestrel/general/define-sk.lisp
M books/kestrel/general/top.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 69e8b9a139edd5878731cd45fd29c62dff998bf8
https://github.com/acl2/acl2/commit/69e8b9a139edd5878731cd45fd29c62dff998bf8
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-29 (Wed, 29 Jun 2016)
Changed paths:
M axioms.lisp
M books/centaur/sv/vl/moddb.lisp
M books/system/doc/acl2-doc.lisp
M books/xdoc/topics.lisp
M other-events.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: c34109c74b8a75fb73281f290c1fc600a973d3bf
https://github.com/acl2/acl2/commit/c34109c74b8a75fb73281f290c1fc600a973d3bf
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-30 (Thu, 30 Jun 2016)
Changed paths:
M books/centaur/aig/best-aig.lisp
M books/centaur/vl2014/parsetree.lisp
M books/doc/relnotes.lisp
M books/kestrel/system/terms.lisp
M books/std/lists/abstract.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 416e303b4fb7f6b55d9f1549d38abe918668c5a7
https://github.com/acl2/acl2/commit/416e303b4fb7f6b55d9f1549d38abe918668c5a7
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-30 (Thu, 30 Jun 2016)
Changed paths:
M books/kestrel/general/alists.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/event-forms-tests.lisp
M books/kestrel/system/event-forms.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
M books/kestrel/system/numbered-names.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/top.lisp
A books/kestrel/system/user-interface-tests.lisp
A books/kestrel/system/user-interface.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 4df905e686a0bd38e9318bdc4985949f34a9d1c2
https://github.com/acl2/acl2/commit/4df905e686a0bd38e9318bdc4985949f34a9d1c2
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-01 (Fri, 01 Jul 2016)
Changed paths:
A books/kestrel/general/auto-termination-tests.acl2
A books/kestrel/general/auto-termination-tests.lisp
A books/kestrel/general/auto-termination.lisp
M books/kestrel/general/top.lisp
A books/kestrel/general/ubi.lisp
R books/kestrel/system/auto-termination-tests.acl2
R books/kestrel/system/auto-termination-tests.lisp
R books/kestrel/system/auto-termination.lisp
M books/kestrel/system/top.lisp
R books/kestrel/system/ubi.lisp
M books/misc/check-acl2-exports.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: fac47c52a0068bfeb919c4aba724bb58e26ed138
https://github.com/acl2/acl2/commit/fac47c52a0068bfeb919c4aba724bb58e26ed138
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-01 (Fri, 01 Jul 2016)
Changed paths:
A books/centaur/bitops/limited-shifts.lisp
M books/centaur/gl/g-logapp.lisp
M books/centaur/gl/gl-misc-defs.lisp
M books/centaur/gl/symbolic-arithmetic.lisp
M books/centaur/sv/svex/a4vec-ops.lisp
M books/centaur/sv/svex/aig-arith.lisp
M books/centaur/sv/vl/vl-svstmt.lisp
M books/centaur/vl/loader/parser/statements.lisp
M books/centaur/vl/parsetree.lisp
M books/projects/regex/regex-ui.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: c8e11fb1ae23c5326b184761c8ee09786f882c34
https://github.com/acl2/acl2/commit/c8e11fb1ae23c5326b184761c8ee09786f882c34
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-03 (Sun, 03 Jul 2016)
Changed paths:
M books/coi/defpun/defpun.lisp
M books/finite-set-theory/set-theory.lisp
M books/finite-set-theory/total-ordering.lisp
M books/models/y86/LICENSE
M books/projects/symbolic/m5/demo.lisp
M books/projects/symbolic/m5/utilities.lisp
M books/sorting/Readme.lsp
M books/system/doc/acl2-doc.lisp
A books/workshops/2003/kaufmann/LICENSE
M books/workshops/2003/kaufmann/support/rtl/tool/simplify-defuns.lisp
M books/workshops/2003/moore_vcg/support/demo.lisp
M books/workshops/2003/moore_vcg/support/utilities.lisp
M books/workshops/2006/kaufmann-moore/support/Readme.lsp
M doc.lisp
M emacs/acl2-doc.el
M emacs/emacs-acl2.el
M emacs/monitor.el
M history-management.lisp
M interface-raw.lisp
M rewrite.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 0e9e9308a0c147c2b9ba44f9518c9cec8f39deba
https://github.com/acl2/acl2/commit/0e9e9308a0c147c2b9ba44f9518c9cec8f39deba
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-04 (Mon, 04 Jul 2016)
Changed paths:
A books/models/jvm/guard-verified-m1/LICENSE
A books/models/jvm/m1-original/LICENSE
A books/models/jvm/m1/LICENSE
A books/models/jvm/m5/LICENSE
M books/models/jvm/m5/demo.lisp
M books/models/jvm/m5/idemo.lisp
M books/models/jvm/m5/jvm-fact-setup.lisp
M books/models/jvm/m5/utilities.lisp
M books/projects/symbolic/m5/demo.lisp
M books/projects/symbolic/m5/utilities.lisp
M books/sorting/Readme.lsp
M books/workshops/2003/moore_vcg/support/demo.lisp
M books/workshops/2003/moore_vcg/support/m5.lisp
M books/workshops/2003/moore_vcg/support/utilities.lisp
M books/workshops/2003/moore_vcg/support/vcg-examples.lisp
M emacs/emacs-acl2.el
Log Message:
-----------
Merge from acl2/acl2.
Commit: 18f87ce4f9b1c85a6280e9e7b5da7b72016f72b8
https://github.com/acl2/acl2/commit/18f87ce4f9b1c85a6280e9e7b5da7b72016f72b8
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-06 (Wed, 06 Jul 2016)
Changed paths:
M books/kestrel/system/user-interface.lisp
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M boot-strap-pass-2.lisp
M doc.lisp
M emacs/emacs-acl2.el
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 4345e7327b9fb4c94466689307a934208b8e6722
https://github.com/acl2/acl2/commit/4345e7327b9fb4c94466689307a934208b8e6722
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-07 (Thu, 07 Jul 2016)
Changed paths:
M books/kestrel/system/user-interface.lisp
M books/misc/check-acl2-exports.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: a063cb32fe24d8908dca39e139726029e66eb8b8
https://github.com/acl2/acl2/commit/a063cb32fe24d8908dca39e139726029e66eb8b8
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-08 (Fri, 08 Jul 2016)
Changed paths:
M books/kestrel/general/define-sk.lisp
M books/kestrel/system/defun-sk-queries.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 5363aac524ffb317c3f2404e3d28fbe8da99e8fe
https://github.com/acl2/acl2/commit/5363aac524ffb317c3f2404e3d28fbe8da99e8fe
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-11 (Mon, 11 Jul 2016)
Changed paths:
M GNUmakefile
M acl2-fns.lisp
M acl2.lisp
M all-files.txt
M axioms.lisp
M basis-a.lisp
M books/acl2s/cgen/prove-cgen.lisp
M books/centaur/gl/factor-fns.lisp
M books/centaur/gl/gify.lisp
M books/centaur/jared-customization.lsp
M books/clause-processors/SULFA/scripts/sulfa-exec-smt.isf
M books/clause-processors/SULFA/scripts/sulfa-smt-saved-exec
M books/clause-processors/SULFA/scripts/sulfa-smt-saved-exec.isf
M books/clause-processors/SULFA/scripts/sulfa-smt.isf
M books/coi/super-ihs/symbols.lsp
M books/demos/patterned-congruences.lisp
M books/doc/relnotes.lisp
M books/interface/infix/infix.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
M books/misc/bash.lisp
M books/misc/check-acl2-exports.lisp
M books/misc/rtl-untranslate.lisp
M books/nonstd/workshops/1999/calculus/book/refinement-makes-i-small-change.lisp
M books/nonstd/workshops/1999/calculus/book/riemann-bound.lisp
M books/nonstd/workshops/1999/calculus/book/riemann-lemmas.lisp
M books/nonstd/workshops/1999/calculus/book/split-integral-by-subintervals.lisp
M books/nonstd/workshops/1999/calculus/solutions/mesh-make-partition.lisp
M books/nonstd/workshops/2011/reid-gamboa-differentiator/support/differentiator.lisp
M books/projects/milawa/ACL2/count.lsp
M books/projects/sidekick/explore.lisp
M books/projects/sidekick/public/explore.js
M books/projects/x86isa/machine/x86-syscalls.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/fadd-extra0.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/lextra-proofs.lisp
M books/rtl/rel4/support/bits-extra.lisp
M books/rtl/rel4/support/lextra-proofs.lisp
M books/rtl/rel9/support/support/fadd-extra0.lisp
M books/rtl/rel9/support/support/lextra-proofs.lisp
M books/system/dead-source-code.lisp
M books/system/doc/acl2-doc.lisp
M books/unicode/read-utf8.lisp
M books/unicode/uchar.lisp
M books/unicode/utf8-decode.lisp
M books/unicode/utf8-encode.lisp
R books/unicode/utf8-table35.lisp
M books/unicode/utf8-table36.lisp
A books/unicode/utf8-table37.lisp
M books/workshops/1999/calculus/solutions/mesh-make-partition.lisp
M books/workshops/2003/gamboa-cowles-van-baalen/support/kalman-proof.lisp
M books/workshops/2004/legato/support/generic-theory-loop-invariant-mult.lisp
M books/workshops/2006/kaufmann-moore/support/mini-proveall.lisp
M books/workshops/2007/erickson/bprove/bash.lisp
M books/xdoc/top.lisp
M defpkgs.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M emacs/emacs-acl2.el
M installation/requirements.html
M interface-raw.lisp
M ld.lisp
M other-events.lisp
A proof-builder-a.lisp
A proof-builder-b.lisp
A proof-builder-pkg.lisp
R proof-checker-a.lisp
R proof-checker-b.lisp
R proof-checker-pkg.lisp
M prove.lisp
M rewrite.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: c32af95aff6924fe1ac3d9496a737a423fb84236
https://github.com/acl2/acl2/commit/c32af95aff6924fe1ac3d9496a737a423fb84236
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-12 (Tue, 12 Jul 2016)
Changed paths:
M books/data-structures/top.lisp
M books/kestrel/system/directed-untranslate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 3fc543eae65c1611213cf824dd59076d52ee9444
https://github.com/acl2/acl2/commit/3fc543eae65c1611213cf824dd59076d52ee9444
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-12 (Tue, 12 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/defun-sk-queries.lisp
M books/kestrel/system/event-forms.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
M books/kestrel/system/numbered-names-tests.lisp
M books/kestrel/system/numbered-names.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/user-interface.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 0f7f9ecf10a0278c7cb0ed9c125452120dc16bf1
https://github.com/acl2/acl2/commit/0f7f9ecf10a0278c7cb0ed9c125452120dc16bf1
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-13 (Wed, 13 Jul 2016)
Changed paths:
M books/kestrel/soft/acl2-customization.lsp
M books/kestrel/soft/implementation.lisp
M books/kestrel/soft/top.lisp
M books/kestrel/soft/workshop-paper-examples.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 84315192ca43984bfaa192465762291dfcbce043
https://github.com/acl2/acl2/commit/84315192ca43984bfaa192465762291dfcbce043
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-13 (Wed, 13 Jul 2016)
Changed paths:
M books/doc/more-topics.lisp
M books/misc/file-io.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M history-management.lisp
M installation/requirements.html
M tau.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 3435343cb3902bdada50c545b0802f7c4ad07244
https://github.com/acl2/acl2/commit/3435343cb3902bdada50c545b0802f7c4ad07244
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-13 (Wed, 13 Jul 2016)
Changed paths:
M acl2.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/soft/implementation.lisp
A books/kestrel/system/defchoose-queries-tests.lisp
A books/kestrel/system/defchoose-queries.lisp
M books/kestrel/system/top.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
M books/misc/check-acl2-exports.lisp
M defthm.lisp
M defuns.lisp
M futures-raw.lisp
M history-management.lisp
M ld.lisp
M memoize-raw.lisp
M other-events.lisp
M prove.lisp
M rewrite.lisp
M tau.lisp
M translate.lisp
M type-set-b.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: d87f7ed3e30cfa8e38eb3a70d28859a7152196e7
https://github.com/acl2/acl2/commit/d87f7ed3e30cfa8e38eb3a70d28859a7152196e7
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-15 (Fri, 15 Jul 2016)
Changed paths:
M books/ihs/math-lemmas.lisp
M books/projects/doc.lisp
A books/projects/paco/LICENSE
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 60d71f8c8c2dfab2f2d40ea48ef1832fb46061e3
https://github.com/acl2/acl2/commit/60d71f8c8c2dfab2f2d40ea48ef1832fb46061e3
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-15 (Fri, 15 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: e8ed1a01e402f26a9bcbf4dd69b9c629edd92b44
https://github.com/acl2/acl2/commit/e8ed1a01e402f26a9bcbf4dd69b9c629edd92b44
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-16 (Sat, 16 Jul 2016)
Changed paths:
M books/kestrel/system/verify-guards-program.lisp
M induct.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: a4ac63b63a67abce7fe8358da96142ade3b08a3d
https://github.com/acl2/acl2/commit/a4ac63b63a67abce7fe8358da96142ade3b08a3d
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-18 (Mon, 18 Jul 2016)
Changed paths:
M books/centaur/memoize/old/profile.lisp
M books/projects/doc.lisp
A books/projects/farray/LICENSE
A books/projects/farray/acl2-customization.lsp
A books/projects/farray/cert.acl2
A books/projects/farray/farray.lisp
A books/projects/farray/package.lsp
A books/projects/farray/portcullis.acl2
A books/projects/farray/portcullis.lisp
M books/xdoc/save.lisp
M books/xdoc/topics.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 27673e06eb108f5c69f575795e3475e3141f4a89
https://github.com/acl2/acl2/commit/27673e06eb108f5c69f575795e3475e3141f4a89
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-19 (Tue, 19 Jul 2016)
Changed paths:
M acl2-fns.lisp
M books/centaur/README.html
M books/centaur/sv/vl/vl-svstmt.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/x86-abstract-state.lisp
M books/projects/x86isa/machine/x86-register-readers-and-writers-raw.lsp
M books/projects/x86isa/machine/x86-register-readers-and-writers.lisp
M books/projects/x86isa/proofs/factorial/fact-wormhole-abstraction.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.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/tools/execution/examples/dataCopy/dataCopy.c
A books/std/strings/stringless.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M interface-raw.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 360a8ea5bdc4fec249381a60d7e2bfefc52c216e
https://github.com/acl2/acl2/commit/360a8ea5bdc4fec249381a60d7e2bfefc52c216e
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-21 (Thu, 21 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/misc/eval.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 8794de894edcc31b7455b60c51cf66e2f004fc0b
https://github.com/acl2/acl2/commit/8794de894edcc31b7455b60c51cf66e2f004fc0b
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-21 (Thu, 21 Jul 2016)
Changed paths:
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 75f2c242f533889bfd2a11b44d02f93aebc174e2
https://github.com/acl2/acl2/commit/75f2c242f533889bfd2a11b44d02f93aebc174e2
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/centaur/misc/hons-extra.lisp
M books/projects/x86isa/machine/guard-helpers.lisp
M books/projects/x86isa/machine/x86-environment.lisp
M books/projects/x86isa/machine/x86-top-level-memory.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/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/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
M books/system/doc/acl2-doc.lisp
M doc.lisp
M simplify.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 0cc980ea376246170c956ff7d5110b46015250bc
https://github.com/acl2/acl2/commit/0cc980ea376246170c956ff7d5110b46015250bc
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/kestrel/system/fresh-names-tests.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: b811ab8931cbc3de367554d64bacb52f0eaaab00
https://github.com/acl2/acl2/commit/b811ab8931cbc3de367554d64bacb52f0eaaab00
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 013e72529847e7a68341f3e7f7c9b0725c843022
https://github.com/acl2/acl2/commit/013e72529847e7a68341f3e7f7c9b0725c843022
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/system/doc/acl2-doc.lisp
Log Message:
-----------
Fix name of parameter in xdoc, add defpointer for all-calls.
Commit: 0c6a873fa03079e636b0fee66968fb505418d89c
https://github.com/acl2/acl2/commit/0c6a873fa03079e636b0fee66968fb505418d89c
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/std/util/defconsts.lisp
Log Message:
-----------
Add missing paren in xdoc.
Commit: 5cb08c87e7d7958b2b28980c5083a137d0906fa9
https://github.com/acl2/acl2/commit/5cb08c87e7d7958b2b28980c5083a137d0906fa9
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
A books/kestrel/system/verify-guards-program-tests.lisp
M books/kestrel/system/verify-guards-program.lisp
Log Message:
-----------
Change verify-guards-program to return an error if anything went wrong, uncomment tests and move into a separate -tests file.
Commit: 2c73e2f8bb6ffd5fc497780e54eb5ab591b28c7e
https://github.com/acl2/acl2/commit/2c73e2f8bb6ffd5fc497780e54eb5ab591b28c7e
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
A books/kestrel/system/verify-guards-program-tests.acl2
Log Message:
-----------
Add .acl2 file for verify-guards-program-tests (needed for the ttag).
Commit: bed2bb125750ce1ad2e1bfa976203f6238a60349
https://github.com/acl2/acl2/commit/bed2bb125750ce1ad2e1bfa976203f6238a60349
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/misc/check-acl2-exports.lisp
Log Message:
-----------
Add all-calls to *acl2-exports-exclusions*.
Commit: 414750d54bcae51702d22ef5653c37981b4f3abb
https://github.com/acl2/acl2/commit/414750d54bcae51702d22ef5653c37981b4f3abb
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2016-07-23 (Sat, 23 Jul 2016)
Changed paths:
A books/kestrel/system/verify-guards-program-tests.acl2
A books/kestrel/system/verify-guards-program-tests.lisp
M books/kestrel/system/verify-guards-program.lisp
M books/misc/check-acl2-exports.lisp
M books/std/util/defconsts.lisp
M books/system/doc/acl2-doc.lisp
Log Message:
-----------
Merge pull request #623 from ericsmithkestrel/master
Change verify-guards-program + small doc fixes
(Note: I'm doing this before pushing the "unrelated change" I mentioned in a comment. That will come later.)
Compare: https://github.com/acl2/acl2/compare/9fe1bde12607...414750d54bca
Home: https://github.com/acl2/acl2
Commit: 4668ff9ee36fdda57f2c95bafc8537fdec3a6776
https://github.com/acl2/acl2/commit/4668ff9ee36fdda57f2c95bafc8537fdec3a6776
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-09 (Thu, 09 Jun 2016)
Changed paths:
A books/system/all-ffn-symbs-logic.lisp
M books/system/doc/acl2-doc.lisp
M books/system/termp.lisp
M books/system/top.lisp
M boot-strap-pass-2.lisp
M other-processes.lisp
M prove.lisp
M rewrite.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 3d81db6ba2e2d88fe469505e0c7543496e686e5c
https://github.com/acl2/acl2/commit/3d81db6ba2e2d88fe469505e0c7543496e686e5c
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-09 (Thu, 09 Jun 2016)
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 13b1874cfbfdabf1b71d05873ce194d69a8b0534
https://github.com/acl2/acl2/commit/13b1874cfbfdabf1b71d05873ce194d69a8b0534
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-10 (Fri, 10 Jun 2016)
Changed paths:
M books/centaur/sv/vl/elaborate.lisp
M books/centaur/sv/vl/vl-svstmt.lisp
M books/centaur/vl/kit/lint.lisp
M books/centaur/vl/lint/suppress-warnings.lisp
M books/centaur/vl/mlib/json.lisp
M books/centaur/vl/mlib/print-warnings.lisp
M books/centaur/vl/mlib/writer.lisp
M books/centaur/vl/util/warnings.lisp
M books/clause-processors/meta-extract-user.lisp
M books/std/strings/strsubst.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/def-functional-instance.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 6a22bc780a9b438d66f2fe2d8070bae7e85f6197
https://github.com/acl2/acl2/commit/6a22bc780a9b438d66f2fe2d8070bae7e85f6197
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-10 (Fri, 10 Jun 2016)
Changed paths:
M books/kestrel/system/directed-untranslate.lisp
M books/system/doc/acl2-doc.lisp
M boot-strap-pass-2.lisp
M doc.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 017b84ac74adbcab7eb629a29118f3ad08845752
https://github.com/acl2/acl2/commit/017b84ac74adbcab7eb629a29118f3ad08845752
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-13 (Mon, 13 Jun 2016)
Changed paths:
M books/misc/check-acl2-exports.lisp
M books/projects/apply/apply-prim.lisp
M books/projects/apply/apply.lisp
M books/projects/apply/chronology.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 8e1e830ed9e93943dd50afb8b50eed05fec98370
https://github.com/acl2/acl2/commit/8e1e830ed9e93943dd50afb8b50eed05fec98370
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-13 (Mon, 13 Jun 2016)
Changed paths:
M books/kestrel/system/defun-sk-queries.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 9819662d42bfae379110361852dbe55bf1335570
https://github.com/acl2/acl2/commit/9819662d42bfae379110361852dbe55bf1335570
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-14 (Tue, 14 Jun 2016)
Changed paths:
A books/system/kestrel.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 5045b36d102945a014647810e65c0a6886e4cf5c
https://github.com/acl2/acl2/commit/5045b36d102945a014647810e65c0a6886e4cf5c
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-14 (Tue, 14 Jun 2016)
Changed paths:
M books/kestrel/system/defun-sk-queries.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: d350155c9f05f7c85dcc21421199afde6cbfec29
https://github.com/acl2/acl2/commit/d350155c9f05f7c85dcc21421199afde6cbfec29
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-15 (Wed, 15 Jun 2016)
Changed paths:
M books/system/kestrel.lisp
M interface-raw.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: b0e4a504088ad9ed1b5bc06f4a6a7b736948233a
https://github.com/acl2/acl2/commit/b0e4a504088ad9ed1b5bc06f4a6a7b736948233a
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-16 (Thu, 16 Jun 2016)
Changed paths:
M books/centaur/aignet/construction.lisp
M books/centaur/fty/bitstruct.lisp
M books/clause-processors/meta-extract-user.lisp
A books/kestrel/general/alists-tests.lisp
A books/kestrel/system/guards-program-mode.lisp
M books/kestrel/system/top.lisp
M books/std/util/defines.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M ld.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 1c78e9ae8987d8b3344f599268b3acd850ba31b0
https://github.com/acl2/acl2/commit/1c78e9ae8987d8b3344f599268b3acd850ba31b0
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-16 (Thu, 16 Jun 2016)
Changed paths:
R books/kestrel/system/guards-program-mode.lisp
M books/kestrel/system/top.lisp
A books/kestrel/system/verify-guards-program.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 099d17f6ed2897ea176e67659dace2d0e7d4f3ce
https://github.com/acl2/acl2/commit/099d17f6ed2897ea176e67659dace2d0e7d4f3ce
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-17 (Fri, 17 Jun 2016)
Changed paths:
M books/kestrel/soft/top.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: cfd7fa65eeed8189b42425c2e95c49ab05b8f707
https://github.com/acl2/acl2/commit/cfd7fa65eeed8189b42425c2e95c49ab05b8f707
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-17 (Fri, 17 Jun 2016)
Changed paths:
M books/kestrel/system/world-queries.lisp
M books/system/kestrel.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 0ce65ea8504f0ff89ab8b9f71244f5fea38bdcab
https://github.com/acl2/acl2/commit/0ce65ea8504f0ff89ab8b9f71244f5fea38bdcab
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-18 (Sat, 18 Jun 2016)
Changed paths:
M books/kestrel/general/testing.lisp
M books/kestrel/system/world-queries.lisp
M books/system/kestrel.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 7b7a3bd867d8f4c9777f308b8b2a469588b50188
https://github.com/acl2/acl2/commit/7b7a3bd867d8f4c9777f308b8b2a469588b50188
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-20 (Mon, 20 Jun 2016)
Changed paths:
M acl2.lisp
M axioms.lisp
M bin/purity.sh
M books/kestrel/general/testing-tests.lisp
M books/kestrel/general/testing.lisp
M books/kestrel/system/verify-guards-program.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M interface-raw.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: cde10b4a3d7f3258904fa46a2c5d3a3c19188c07
https://github.com/acl2/acl2/commit/cde10b4a3d7f3258904fa46a2c5d3a3c19188c07
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-20 (Mon, 20 Jun 2016)
Changed paths:
M books/kestrel/general/testing-tests.lisp
M books/kestrel/general/testing.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 908f0e21ab53219f820f9afe9dcea23ec96c0b77
https://github.com/acl2/acl2/commit/908f0e21ab53219f820f9afe9dcea23ec96c0b77
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-22 (Wed, 22 Jun 2016)
Changed paths:
M GNUmakefile
M axioms.lisp
M basis-a.lisp
M books/GNUmakefile
M books/kestrel/system/verify-guards-program.lisp
M books/system/doc/acl2-doc.lisp
M books/system/kestrel.lisp
M books/system/top.lisp
M boot-strap-pass-2.lisp
M defuns.lisp
M doc.lisp
M history-management.lisp
M induct.lisp
M interface-raw.lisp
M other-events.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: d4dd927e4ca988bc284f2da2cb2b07e70470b479
https://github.com/acl2/acl2/commit/d4dd927e4ca988bc284f2da2cb2b07e70470b479
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-23 (Thu, 23 Jun 2016)
Changed paths:
M books/centaur/aig/bddify-correct.lisp
M books/centaur/aig/bddify.lisp
M books/centaur/sv/svtv/process.lisp
M books/demos/Readme.lsp
M books/kestrel/system/world-queries.lisp
M books/std/util/da-base.lisp
M books/system/parallel/Readme.lsp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 38fd53c6ffed203e42504b2f421509c826f44d1b
https://github.com/acl2/acl2/commit/38fd53c6ffed203e42504b2f421509c826f44d1b
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-23 (Thu, 23 Jun 2016)
Changed paths:
M books/kestrel/general/alists.lisp
R books/kestrel/general/ensure-tests.lisp
R books/kestrel/general/ensure.lisp
M books/kestrel/general/top.lisp
M books/kestrel/system/minimize-ruler-extenders.lisp
M books/kestrel/system/prove-interface.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/ubi.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: cb43ff6963e68a94c457a91ae6c1d04a145dbc41
https://github.com/acl2/acl2/commit/cb43ff6963e68a94c457a91ae6c1d04a145dbc41
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-24 (Fri, 24 Jun 2016)
Changed paths:
A books/kestrel/system/event-forms.lisp
M books/kestrel/system/top.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: e99632f92a48987bc2a554637925d49f0b3bb71d
https://github.com/acl2/acl2/commit/e99632f92a48987bc2a554637925d49f0b3bb71d
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-28 (Tue, 28 Jun 2016)
Changed paths:
M books/centaur/gl/auto-bindings.lisp
M books/centaur/sv/svtv/process.lisp
M books/centaur/vl/server/public/main.html
M books/tools/templates.lisp
M books/xdoc/parse-xml.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 37b734b31a7c6825d6fe2db7d8734e6fbedc95a7
https://github.com/acl2/acl2/commit/37b734b31a7c6825d6fe2db7d8734e6fbedc95a7
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-28 (Tue, 28 Jun 2016)
Changed paths:
A books/kestrel/system/applicability-conditions-tests.lisp
A books/kestrel/system/applicability-conditions.lisp
A books/kestrel/system/event-forms-tests.lisp
M books/kestrel/system/event-forms.lisp
A books/kestrel/system/fresh-names-tests.lisp
A books/kestrel/system/fresh-names.lisp
A books/kestrel/system/install-not-norm-event-tests.lisp
A books/kestrel/system/install-not-norm-event.lisp
A books/kestrel/system/numbered-names-tests.lisp
A books/kestrel/system/numbered-names.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/top.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 6c22bb49766552a8edaeec7f9dbdac84ca2415c2
https://github.com/acl2/acl2/commit/6c22bb49766552a8edaeec7f9dbdac84ca2415c2
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-28 (Tue, 28 Jun 2016)
Changed paths:
M bdd.lisp
M books/centaur/aignet/aignet-logic.lisp
M books/centaur/fty/fixequiv.lisp
M books/centaur/gl/symbolic-arithmetic.lisp
M books/centaur/sv/vl/moddb.lisp
M books/centaur/vl/mlib/blocks.lisp
M books/centaur/vl2014/mlib/blocks.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/stobj-preservation.lisp
M books/doc/relnotes.lisp
M books/kestrel/system/auto-termination.lisp
M books/kestrel/system/world-queries.lisp
M books/projects/quadratic-reciprocity/euclid.lisp
M books/std/util/defines.lisp
M books/std/util/returnspecs.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/stobj-frame.lisp
M books/xdoc/topics.lisp
M doc.lisp
M rewrite.lisp
M tau.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 592f1e91594b163c10bf0ca1134fb2f8d7e0b488
https://github.com/acl2/acl2/commit/592f1e91594b163c10bf0ca1134fb2f8d7e0b488
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-29 (Wed, 29 Jun 2016)
Changed paths:
M basis-a.lisp
M books/projects/doc.lisp
A books/projects/x86isa/doc.acl2
A books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/x86-decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/x86-ia32e-paging.lisp
M books/projects/x86isa/machine/x86-top-level-memory.lisp
A books/projects/x86isa/proofs/dataCopy/dataCopy-init.lisp
A books/projects/x86isa/proofs/dataCopy/dataCopy-loop-base.lisp
A books/projects/x86isa/proofs/dataCopy/dataCopy-loop-recur.lisp
M books/projects/x86isa/proofs/dataCopy/dataCopy.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/disjoint.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
A 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
A books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-top.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/non-marking-mode-utils.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/acl2-customization.lsp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/cert.acl2
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/common-paging-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/gather-paging-structures-thms.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/gather-paging-structures.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/la-to-pa-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/page-dir-ptr-table-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/page-directory-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/page-table-lemmas.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/paging-basics.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/paging-top.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/paging-lib/pml4-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/acl2-customization.lsp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/cert.acl2
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/common-paging-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/gather-paging-structures-thms.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/gather-paging-structures.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/la-to-pa-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-dir-ptr-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-directory-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/page-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/paging-basics.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/pml4-table-lemmas.lisp
A books/projects/x86isa/proofs/utilities/system-level-mode/paging/top.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/physical-memory-utils.lisp
R books/projects/x86isa/proofs/utilities/system-level-mode/symbolic-simulation-in-marking-mode.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/top.lisp
R books/projects/x86isa/proofs/wordCount/cert.acl2
A books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/wordCount/wc.acl2
M books/projects/x86isa/proofs/wordCount/wc.lisp
R books/projects/x86isa/proofs/zeroCopy/acl2-customization.lsp
R books/projects/x86isa/proofs/zeroCopy/cert.acl2
A books/projects/x86isa/proofs/zeroCopy/marking-mode/acl2-customization.lsp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/cert.acl2
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-init.lisp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-1.lisp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy-part-2.lisp
A books/projects/x86isa/proofs/zeroCopy/marking-mode/zeroCopy.lisp
A books/projects/x86isa/proofs/zeroCopy/non-marking-mode/acl2-customization.lsp
A books/projects/x86isa/proofs/zeroCopy/non-marking-mode/cert.acl2
A books/projects/x86isa/proofs/zeroCopy/non-marking-mode/zeroCopy.lisp
R books/projects/x86isa/proofs/zeroCopy/zeroCopy-in-marking-mode.lisp
R books/projects/x86isa/proofs/zeroCopy/zeroCopy-in-non-marking-mode.lisp
M books/projects/x86isa/tools/execution/examples/dataCopy/dataCopy.lsp
M books/projects/x86isa/top.lisp
M books/system/doc/acl2-doc.lisp
M books/xdoc/topics.lisp
M doc.lisp
M other-events.lisp
M rewrite.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 70f6c6cdd4d8619f90dbc5b41dc3d8eecfbe6eae
https://github.com/acl2/acl2/commit/70f6c6cdd4d8619f90dbc5b41dc3d8eecfbe6eae
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-29 (Wed, 29 Jun 2016)
Changed paths:
A books/kestrel/general/define-sk-tests.lisp
A books/kestrel/general/define-sk.lisp
M books/kestrel/general/top.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 69e8b9a139edd5878731cd45fd29c62dff998bf8
https://github.com/acl2/acl2/commit/69e8b9a139edd5878731cd45fd29c62dff998bf8
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-29 (Wed, 29 Jun 2016)
Changed paths:
M axioms.lisp
M books/centaur/sv/vl/moddb.lisp
M books/system/doc/acl2-doc.lisp
M books/xdoc/topics.lisp
M other-events.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: c34109c74b8a75fb73281f290c1fc600a973d3bf
https://github.com/acl2/acl2/commit/c34109c74b8a75fb73281f290c1fc600a973d3bf
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-30 (Thu, 30 Jun 2016)
Changed paths:
M books/centaur/aig/best-aig.lisp
M books/centaur/vl2014/parsetree.lisp
M books/doc/relnotes.lisp
M books/kestrel/system/terms.lisp
M books/std/lists/abstract.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 416e303b4fb7f6b55d9f1549d38abe918668c5a7
https://github.com/acl2/acl2/commit/416e303b4fb7f6b55d9f1549d38abe918668c5a7
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-06-30 (Thu, 30 Jun 2016)
Changed paths:
M books/kestrel/general/alists.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/event-forms-tests.lisp
M books/kestrel/system/event-forms.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
M books/kestrel/system/numbered-names.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/top.lisp
A books/kestrel/system/user-interface-tests.lisp
A books/kestrel/system/user-interface.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 4df905e686a0bd38e9318bdc4985949f34a9d1c2
https://github.com/acl2/acl2/commit/4df905e686a0bd38e9318bdc4985949f34a9d1c2
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-01 (Fri, 01 Jul 2016)
Changed paths:
A books/kestrel/general/auto-termination-tests.acl2
A books/kestrel/general/auto-termination-tests.lisp
A books/kestrel/general/auto-termination.lisp
M books/kestrel/general/top.lisp
A books/kestrel/general/ubi.lisp
R books/kestrel/system/auto-termination-tests.acl2
R books/kestrel/system/auto-termination-tests.lisp
R books/kestrel/system/auto-termination.lisp
M books/kestrel/system/top.lisp
R books/kestrel/system/ubi.lisp
M books/misc/check-acl2-exports.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: fac47c52a0068bfeb919c4aba724bb58e26ed138
https://github.com/acl2/acl2/commit/fac47c52a0068bfeb919c4aba724bb58e26ed138
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-01 (Fri, 01 Jul 2016)
Changed paths:
A books/centaur/bitops/limited-shifts.lisp
M books/centaur/gl/g-logapp.lisp
M books/centaur/gl/gl-misc-defs.lisp
M books/centaur/gl/symbolic-arithmetic.lisp
M books/centaur/sv/svex/a4vec-ops.lisp
M books/centaur/sv/svex/aig-arith.lisp
M books/centaur/sv/vl/vl-svstmt.lisp
M books/centaur/vl/loader/parser/statements.lisp
M books/centaur/vl/parsetree.lisp
M books/projects/regex/regex-ui.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: c8e11fb1ae23c5326b184761c8ee09786f882c34
https://github.com/acl2/acl2/commit/c8e11fb1ae23c5326b184761c8ee09786f882c34
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-03 (Sun, 03 Jul 2016)
Changed paths:
M books/coi/defpun/defpun.lisp
M books/finite-set-theory/set-theory.lisp
M books/finite-set-theory/total-ordering.lisp
M books/models/y86/LICENSE
M books/projects/symbolic/m5/demo.lisp
M books/projects/symbolic/m5/utilities.lisp
M books/sorting/Readme.lsp
M books/system/doc/acl2-doc.lisp
A books/workshops/2003/kaufmann/LICENSE
M books/workshops/2003/kaufmann/support/rtl/tool/simplify-defuns.lisp
M books/workshops/2003/moore_vcg/support/demo.lisp
M books/workshops/2003/moore_vcg/support/utilities.lisp
M books/workshops/2006/kaufmann-moore/support/Readme.lsp
M doc.lisp
M emacs/acl2-doc.el
M emacs/emacs-acl2.el
M emacs/monitor.el
M history-management.lisp
M interface-raw.lisp
M rewrite.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 0e9e9308a0c147c2b9ba44f9518c9cec8f39deba
https://github.com/acl2/acl2/commit/0e9e9308a0c147c2b9ba44f9518c9cec8f39deba
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-04 (Mon, 04 Jul 2016)
Changed paths:
A books/models/jvm/guard-verified-m1/LICENSE
A books/models/jvm/m1-original/LICENSE
A books/models/jvm/m1/LICENSE
A books/models/jvm/m5/LICENSE
M books/models/jvm/m5/demo.lisp
M books/models/jvm/m5/idemo.lisp
M books/models/jvm/m5/jvm-fact-setup.lisp
M books/models/jvm/m5/utilities.lisp
M books/projects/symbolic/m5/demo.lisp
M books/projects/symbolic/m5/utilities.lisp
M books/sorting/Readme.lsp
M books/workshops/2003/moore_vcg/support/demo.lisp
M books/workshops/2003/moore_vcg/support/m5.lisp
M books/workshops/2003/moore_vcg/support/utilities.lisp
M books/workshops/2003/moore_vcg/support/vcg-examples.lisp
M emacs/emacs-acl2.el
Log Message:
-----------
Merge from acl2/acl2.
Commit: 18f87ce4f9b1c85a6280e9e7b5da7b72016f72b8
https://github.com/acl2/acl2/commit/18f87ce4f9b1c85a6280e9e7b5da7b72016f72b8
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-06 (Wed, 06 Jul 2016)
Changed paths:
M books/kestrel/system/user-interface.lisp
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M boot-strap-pass-2.lisp
M doc.lisp
M emacs/emacs-acl2.el
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 4345e7327b9fb4c94466689307a934208b8e6722
https://github.com/acl2/acl2/commit/4345e7327b9fb4c94466689307a934208b8e6722
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-07 (Thu, 07 Jul 2016)
Changed paths:
M books/kestrel/system/user-interface.lisp
M books/misc/check-acl2-exports.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: a063cb32fe24d8908dca39e139726029e66eb8b8
https://github.com/acl2/acl2/commit/a063cb32fe24d8908dca39e139726029e66eb8b8
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-08 (Fri, 08 Jul 2016)
Changed paths:
M books/kestrel/general/define-sk.lisp
M books/kestrel/system/defun-sk-queries.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 5363aac524ffb317c3f2404e3d28fbe8da99e8fe
https://github.com/acl2/acl2/commit/5363aac524ffb317c3f2404e3d28fbe8da99e8fe
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-11 (Mon, 11 Jul 2016)
Changed paths:
M GNUmakefile
M acl2-fns.lisp
M acl2.lisp
M all-files.txt
M axioms.lisp
M basis-a.lisp
M books/acl2s/cgen/prove-cgen.lisp
M books/centaur/gl/factor-fns.lisp
M books/centaur/gl/gify.lisp
M books/centaur/jared-customization.lsp
M books/clause-processors/SULFA/scripts/sulfa-exec-smt.isf
M books/clause-processors/SULFA/scripts/sulfa-smt-saved-exec
M books/clause-processors/SULFA/scripts/sulfa-smt-saved-exec.isf
M books/clause-processors/SULFA/scripts/sulfa-smt.isf
M books/coi/super-ihs/symbols.lsp
M books/demos/patterned-congruences.lisp
M books/doc/relnotes.lisp
M books/interface/infix/infix.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
M books/misc/bash.lisp
M books/misc/check-acl2-exports.lisp
M books/misc/rtl-untranslate.lisp
M books/nonstd/workshops/1999/calculus/book/refinement-makes-i-small-change.lisp
M books/nonstd/workshops/1999/calculus/book/riemann-bound.lisp
M books/nonstd/workshops/1999/calculus/book/riemann-lemmas.lisp
M books/nonstd/workshops/1999/calculus/book/split-integral-by-subintervals.lisp
M books/nonstd/workshops/1999/calculus/solutions/mesh-make-partition.lisp
M books/nonstd/workshops/2011/reid-gamboa-differentiator/support/differentiator.lisp
M books/projects/milawa/ACL2/count.lsp
M books/projects/sidekick/explore.lisp
M books/projects/sidekick/public/explore.js
M books/projects/x86isa/machine/x86-syscalls.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/fadd-extra0.lisp
M books/rtl/rel11/rel9-rtl-pkg/support/support/lextra-proofs.lisp
M books/rtl/rel4/support/bits-extra.lisp
M books/rtl/rel4/support/lextra-proofs.lisp
M books/rtl/rel9/support/support/fadd-extra0.lisp
M books/rtl/rel9/support/support/lextra-proofs.lisp
M books/system/dead-source-code.lisp
M books/system/doc/acl2-doc.lisp
M books/unicode/read-utf8.lisp
M books/unicode/uchar.lisp
M books/unicode/utf8-decode.lisp
M books/unicode/utf8-encode.lisp
R books/unicode/utf8-table35.lisp
M books/unicode/utf8-table36.lisp
A books/unicode/utf8-table37.lisp
M books/workshops/1999/calculus/solutions/mesh-make-partition.lisp
M books/workshops/2003/gamboa-cowles-van-baalen/support/kalman-proof.lisp
M books/workshops/2004/legato/support/generic-theory-loop-invariant-mult.lisp
M books/workshops/2006/kaufmann-moore/support/mini-proveall.lisp
M books/workshops/2007/erickson/bprove/bash.lisp
M books/xdoc/top.lisp
M defpkgs.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M emacs/emacs-acl2.el
M installation/requirements.html
M interface-raw.lisp
M ld.lisp
M other-events.lisp
A proof-builder-a.lisp
A proof-builder-b.lisp
A proof-builder-pkg.lisp
R proof-checker-a.lisp
R proof-checker-b.lisp
R proof-checker-pkg.lisp
M prove.lisp
M rewrite.lisp
M translate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: c32af95aff6924fe1ac3d9496a737a423fb84236
https://github.com/acl2/acl2/commit/c32af95aff6924fe1ac3d9496a737a423fb84236
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-12 (Tue, 12 Jul 2016)
Changed paths:
M books/data-structures/top.lisp
M books/kestrel/system/directed-untranslate.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 3fc543eae65c1611213cf824dd59076d52ee9444
https://github.com/acl2/acl2/commit/3fc543eae65c1611213cf824dd59076d52ee9444
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-12 (Tue, 12 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/defun-sk-queries.lisp
M books/kestrel/system/event-forms.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
M books/kestrel/system/numbered-names-tests.lisp
M books/kestrel/system/numbered-names.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/kestrel/system/user-interface.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 0f7f9ecf10a0278c7cb0ed9c125452120dc16bf1
https://github.com/acl2/acl2/commit/0f7f9ecf10a0278c7cb0ed9c125452120dc16bf1
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-13 (Wed, 13 Jul 2016)
Changed paths:
M books/kestrel/soft/acl2-customization.lsp
M books/kestrel/soft/implementation.lisp
M books/kestrel/soft/top.lisp
M books/kestrel/soft/workshop-paper-examples.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 84315192ca43984bfaa192465762291dfcbce043
https://github.com/acl2/acl2/commit/84315192ca43984bfaa192465762291dfcbce043
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-13 (Wed, 13 Jul 2016)
Changed paths:
M books/doc/more-topics.lisp
M books/misc/file-io.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M history-management.lisp
M installation/requirements.html
M tau.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 3435343cb3902bdada50c545b0802f7c4ad07244
https://github.com/acl2/acl2/commit/3435343cb3902bdada50c545b0802f7c4ad07244
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-13 (Wed, 13 Jul 2016)
Changed paths:
M acl2.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/soft/implementation.lisp
A books/kestrel/system/defchoose-queries-tests.lisp
A books/kestrel/system/defchoose-queries.lisp
M books/kestrel/system/top.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
M books/misc/check-acl2-exports.lisp
M defthm.lisp
M defuns.lisp
M futures-raw.lisp
M history-management.lisp
M ld.lisp
M memoize-raw.lisp
M other-events.lisp
M prove.lisp
M rewrite.lisp
M tau.lisp
M translate.lisp
M type-set-b.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: d87f7ed3e30cfa8e38eb3a70d28859a7152196e7
https://github.com/acl2/acl2/commit/d87f7ed3e30cfa8e38eb3a70d28859a7152196e7
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-15 (Fri, 15 Jul 2016)
Changed paths:
M books/ihs/math-lemmas.lisp
M books/projects/doc.lisp
A books/projects/paco/LICENSE
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 60d71f8c8c2dfab2f2d40ea48ef1832fb46061e3
https://github.com/acl2/acl2/commit/60d71f8c8c2dfab2f2d40ea48ef1832fb46061e3
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-15 (Fri, 15 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: e8ed1a01e402f26a9bcbf4dd69b9c629edd92b44
https://github.com/acl2/acl2/commit/e8ed1a01e402f26a9bcbf4dd69b9c629edd92b44
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-16 (Sat, 16 Jul 2016)
Changed paths:
M books/kestrel/system/verify-guards-program.lisp
M induct.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: a4ac63b63a67abce7fe8358da96142ade3b08a3d
https://github.com/acl2/acl2/commit/a4ac63b63a67abce7fe8358da96142ade3b08a3d
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-18 (Mon, 18 Jul 2016)
Changed paths:
M books/centaur/memoize/old/profile.lisp
M books/projects/doc.lisp
A books/projects/farray/LICENSE
A books/projects/farray/acl2-customization.lsp
A books/projects/farray/cert.acl2
A books/projects/farray/farray.lisp
A books/projects/farray/package.lsp
A books/projects/farray/portcullis.acl2
A books/projects/farray/portcullis.lisp
M books/xdoc/save.lisp
M books/xdoc/topics.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 27673e06eb108f5c69f575795e3475e3141f4a89
https://github.com/acl2/acl2/commit/27673e06eb108f5c69f575795e3475e3141f4a89
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-19 (Tue, 19 Jul 2016)
Changed paths:
M acl2-fns.lisp
M books/centaur/README.html
M books/centaur/sv/vl/vl-svstmt.lisp
M books/kestrel/system/world-queries-tests.lisp
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/x86-abstract-state.lisp
M books/projects/x86isa/machine/x86-register-readers-and-writers-raw.lsp
M books/projects/x86isa/machine/x86-register-readers-and-writers.lisp
M books/projects/x86isa/proofs/factorial/fact-wormhole-abstraction.lisp
M books/projects/x86isa/proofs/utilities/system-level-mode/marking-mode-utils.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/tools/execution/examples/dataCopy/dataCopy.c
A books/std/strings/stringless.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M interface-raw.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 360a8ea5bdc4fec249381a60d7e2bfefc52c216e
https://github.com/acl2/acl2/commit/360a8ea5bdc4fec249381a60d7e2bfefc52c216e
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-21 (Thu, 21 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
M books/misc/eval.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 8794de894edcc31b7455b60c51cf66e2f004fc0b
https://github.com/acl2/acl2/commit/8794de894edcc31b7455b60c51cf66e2f004fc0b
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-21 (Thu, 21 Jul 2016)
Changed paths:
M books/kestrel/system/world-queries-tests.lisp
M books/kestrel/system/world-queries.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 75f2c242f533889bfd2a11b44d02f93aebc174e2
https://github.com/acl2/acl2/commit/75f2c242f533889bfd2a11b44d02f93aebc174e2
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/centaur/misc/hons-extra.lisp
M books/projects/x86isa/machine/guard-helpers.lisp
M books/projects/x86isa/machine/x86-environment.lisp
M books/projects/x86isa/machine/x86-top-level-memory.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/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/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
M books/system/doc/acl2-doc.lisp
M doc.lisp
M simplify.lisp
Log Message:
-----------
Merge from acl2/acl2.
Commit: 0cc980ea376246170c956ff7d5110b46015250bc
https://github.com/acl2/acl2/commit/0cc980ea376246170c956ff7d5110b46015250bc
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/kestrel/system/fresh-names-tests.lisp
M books/kestrel/system/fresh-names.lisp
M books/kestrel/system/install-not-norm-event.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: b811ab8931cbc3de367554d64bacb52f0eaaab00
https://github.com/acl2/acl2/commit/b811ab8931cbc3de367554d64bacb52f0eaaab00
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/kestrel/system/applicability-conditions-tests.lisp
M books/kestrel/system/applicability-conditions.lisp
M books/kestrel/system/terms-tests.lisp
M books/kestrel/system/terms.lisp
Log Message:
-----------
Merge from KestrelInstitute/acl2.
Commit: 013e72529847e7a68341f3e7f7c9b0725c843022
https://github.com/acl2/acl2/commit/013e72529847e7a68341f3e7f7c9b0725c843022
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/system/doc/acl2-doc.lisp
Log Message:
-----------
Fix name of parameter in xdoc, add defpointer for all-calls.
Commit: 0c6a873fa03079e636b0fee66968fb505418d89c
https://github.com/acl2/acl2/commit/0c6a873fa03079e636b0fee66968fb505418d89c
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/std/util/defconsts.lisp
Log Message:
-----------
Add missing paren in xdoc.
Commit: 5cb08c87e7d7958b2b28980c5083a137d0906fa9
https://github.com/acl2/acl2/commit/5cb08c87e7d7958b2b28980c5083a137d0906fa9
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
A books/kestrel/system/verify-guards-program-tests.lisp
M books/kestrel/system/verify-guards-program.lisp
Log Message:
-----------
Change verify-guards-program to return an error if anything went wrong, uncomment tests and move into a separate -tests file.
Commit: 2c73e2f8bb6ffd5fc497780e54eb5ab591b28c7e
https://github.com/acl2/acl2/commit/2c73e2f8bb6ffd5fc497780e54eb5ab591b28c7e
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
A books/kestrel/system/verify-guards-program-tests.acl2
Log Message:
-----------
Add .acl2 file for verify-guards-program-tests (needed for the ttag).
Commit: bed2bb125750ce1ad2e1bfa976203f6238a60349
https://github.com/acl2/acl2/commit/bed2bb125750ce1ad2e1bfa976203f6238a60349
Author: Eric Smith <eric....@kestrel.edu>
Date: 2016-07-22 (Fri, 22 Jul 2016)
Changed paths:
M books/misc/check-acl2-exports.lisp
Log Message:
-----------
Add all-calls to *acl2-exports-exclusions*.
Commit: 414750d54bcae51702d22ef5653c37981b4f3abb
https://github.com/acl2/acl2/commit/414750d54bcae51702d22ef5653c37981b4f3abb
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2016-07-23 (Sat, 23 Jul 2016)
Changed paths:
A books/kestrel/system/verify-guards-program-tests.acl2
A books/kestrel/system/verify-guards-program-tests.lisp
M books/kestrel/system/verify-guards-program.lisp
M books/misc/check-acl2-exports.lisp
M books/std/util/defconsts.lisp
M books/system/doc/acl2-doc.lisp
Log Message:
-----------
Merge pull request #623 from ericsmithkestrel/master
Change verify-guards-program + small doc fixes
(Note: I'm doing this before pushing the "unrelated change" I mentioned in a comment. That will come later.)
Compare: https://github.com/acl2/acl2/compare/9fe1bde12607...414750d54bca
GitHub
Jul 23, 2016, 2:12:52 PM7/23/16
to acl2-...@googlegroups.com
Branch: refs/heads/master
Reply all
Reply to author
Forward
0 new messages