Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Jun 15, 2020

• Added new :non-executable keyword to defstobj. Fixed a bug in defstobj redundancy. Added some defrec dependencies. Put fix-pkg and unmake-true-list-cons-nest into guard-verified logic mode and docu…

  Show description for f8e9dba
  

  Matt Kaufmann

  committed
  f8e9dba

  Copy full SHA for f8e9dba

Commits on Jun 8, 2020

• Improved CASE-MATCH by adding QUOTEP~ to *ACL2-EXPORTS* and putting SYMBOL-NAME-EQUAL in guard-verified logic mode. Extended the use of COMMENT under HIDE by the prover. Print an observation when r…

  Show description for cdc3862
  

  Matt Kaufmann

  committed
  cdc3862

  Copy full SHA for cdc3862

Commits on May 22, 2020

• Defconst no longer takes an optional doc string.

  Show description for 8d6b64d
  MattKaufmann

  committed
  8d6b64d

  Copy full SHA for 8d6b64d

Commits on Apr 16, 2020

• ACL2 Version 8.3 release

  MattKaufmann

  committed
  4f18d3b

  Copy full SHA for 4f18d3b

Commits on Mar 29, 2020

• Permit recursive calls inside loop$. Provice definductor, for creating an induction scheme for a loop$-recursive function. Added support for new loop$ operator, thereis. Updated *acl2-exports*. Ext…

  Show description for b2218d5
  

  Matt Kaufmann

  committed
  b2218d5

  Copy full SHA for b2218d5

Commits on Nov 7, 2019

• Provide a way to avoid some of the cost of abstract stobj invariance checks. Avoid some indirection in stobj reads and writes. Modified books/build/universal-dependency.certdep to cause cleaning be…

  Show description for e5faa76
  

  Matt Kaufmann

  committed
  e5faa76

  Copy full SHA for e5faa76

Commits on May 7, 2019

• ACL2 Version 8.2 release

  MattKaufmann

  committed
  0602ef9

  Copy full SHA for 0602ef9

Commits on Mar 1, 2019

• Changed concrete-apply$-userfn and concrete-badge to doppelganger-apply$-userfn and doppelganger-badge-userfn, resp. Changed "compileable" to "compilable".

  Show description for 6ac7d08
  

  Matt Kaufmann

  committed
  6ac7d08

  Copy full SHA for 6ac7d08

Commits on Feb 8, 2019

• Added loop$. Changed def-warrant to defwarrant, which can now be redundant. Apply$ handles multiple values.

  Show description for af86270
  

  Matt Kaufmann

  committed
  af86270

  Copy full SHA for af86270

Commits on Dec 12, 2018

• Added names to *acl2-exports*. Changed delete-assoc to remove1-assoc (similarly for related names). Added remove-assoc (and related definitions).

  Show description for 374edd9
  MattKaufmann

  committed
  374edd9

  Copy full SHA for 374edd9

Commits on Oct 27, 2018

• Apply$ enhancements: declare forms may appear in lambda objects and lambda$ provides macro-like convenient way to produce lambdas.

  Show description for fcc9898
  

  Matt Kaufmann

  committed
  fcc9898

  Copy full SHA for fcc9898

Commits on Sep 19, 2018

• ACL2 Version 8.1 release

  MattKaufmann

  committed
  ebe08ba

  Copy full SHA for ebe08ba

Commits on Sep 14, 2018

• Added some documented symbols to *acl2-exports*.

  MattKaufmann

  committed
  27357e4

  Copy full SHA for 27357e4

Commits on Dec 14, 2017

• ACL2 Version 8.0 release

  MattKaufmann

  committed
  5ab2134

  Copy full SHA for 5ab2134

Commits on Dec 7, 2017

• Changed :doc topic name note-7-5 to note-8-0, etc. Updated *acl2-exports*. Tweaked some comments. Fixed a "make" target, chk-include-book-worlds. Fixed a hard error from including an ACL2s book (bu…

  Show description for 1f8e571
  MattKaufmann

  committed
  1f8e571

  Copy full SHA for 1f8e571

Commits on Oct 13, 2017

• Improved magic-ev-fncall, added ev-fncall-w!, and deleted oracle-apply and oracle-funcall.

  Show description for 4008842
  MattKaufmann

  committed
  4008842

  Copy full SHA for 4008842

Commits on Sep 17, 2017

• Added some symbols to *acl2-exports*, including LET, and added a bit of documentation.

  Show description for 076a6de
  MattKaufmann

  committed
  076a6de

  Copy full SHA for 076a6de

Commits on May 18, 2017

• Minor clean-up of documentation, comments, and error messages in SAT proof-checkers; clarified some things about *acl2-exports*

  MattKaufmann

  committed
  a400f48

  Copy full SHA for a400f48

Commits on Apr 23, 2017

• Added two symbols missing from *acl2-exports*. (No more such additions today....)

  MattKaufmann

  committed
  296aa97

  Copy full SHA for 296aa97

• Added register-invariant-risk. Made several improvements to the sys-call family of functions. Extended *acl2-exports* (so cleaning books may be required).

  Show description for 8c257b2
  MattKaufmann

  committed
  8c257b2

  Copy full SHA for 8c257b2

Commits on Mar 21, 2017

• ACL2 Version 7.4 release

  MattKaufmann

  committed
  ab320f0

  Copy full SHA for ab320f0

Commits on Dec 20, 2016

• ACL2 Version 7.3 release

  MattKaufmann

  committed
  59077a3

  Copy full SHA for 59077a3

Commits on Dec 3, 2016

• Improved theory-invariant messages. Fixed :pe for define to show guards and more. Added 3 symbols to *acl2-exports*. Cleaned up rtl :doc. Improved acl2-doc browser, dealing better with `:' and [n],…

  Show description for b4c32dd
  

  Matt Kaufmann

  committed
  b4c32dd

  Copy full SHA for b4c32dd

Commits on Oct 13, 2016

• Added some symbols to *acl2-exports*.

  Show description for bc0e4b3
  MattKaufmann

  committed
  bc0e4b3

  Copy full SHA for bc0e4b3

• Added new books for apply$ from J, along with as-yet unadvertised experimental support for evaluation with apply$ provided by J with a bit of input from me

  

  Matt Kaufmann

  authored and

  Matt Kaufmann

  committed
  136a85b

  Copy full SHA for 136a85b

Commits on Jul 11, 2016

• Name change: "proof-checker" changed to "proof-builder". Extended *acl2-exports*.

  Show description for 248025a
  

  Matt Kaufmann

  authored and

  Matt Kaufmann

  committed
  248025a

  Copy full SHA for 248025a

Commits on Apr 5, 2016

• NOTE: It is likely that you'll need to clean books before certifying

  Show description for de4bf91
  

  Matt Kaufmann

  committed
  de4bf91

  Copy full SHA for de4bf91

Commits on Feb 20, 2016

• A :measure causes an error if definition is not recursive or (even in :program mode) the measure is not a legal term.

  Show description for fca1942
  MattKaufmann

  committed
  fca1942

  Copy full SHA for fca1942

Commits on Feb 11, 2016

• Added CONS-WITH-HINT, and added that symbol and SET-LD-PROMPT to *acl2-exports*.

  Show description for efcbcf8
  

  Matt Kaufmann

  authored and

  Matt Kaufmann

  committed
  efcbcf8

  Copy full SHA for efcbcf8

Commits on Jan 18, 2016

• ACL2 Version 7.2 release

  MattKaufmann

  committed
  a12f619

  Copy full SHA for a12f619

Commits on Jan 13, 2016

• Added set-raw-warning-format and accumulated-persistence-oops. Incorporated type declarations into the guards of macros. Tweaked guard of defcong+ (coi book nary.lisp). Updated "since" date in bin/…

  Show description for 6d30e15
  

  Matt Kaufmann

  authored and

  Matt Kaufmann

  committed
  6d30e15

  Copy full SHA for 6d30e15

Commits on Jan 11, 2016

• Updated copyrights. Updated saved_acl2 for CMUCL to use maximum heap for CMU Common Lisp snapshot-2016-01 and beyond. Avoided x86 books for CMUCL.

  Show description for edd90a8
  MattKaufmann

  committed
  edd90a8

  Copy full SHA for edd90a8

Commits on Jan 1, 2016

• Added missing symbols to *acl2-exports*.

  MattKaufmann

  committed
  36012bf

  Copy full SHA for 36012bf

Commits on Dec 21, 2015

• Forall and exists in defun-sk must be in the "ACL2" package. Defun redundancy now depends on :normalize.

  Show description for 98cd6e7
  

  Matt Kaufmann

  authored and

  Matt Kaufmann

  committed
  98cd6e7

  Copy full SHA for 98cd6e7

Commits on Dec 20, 2015

• Improved defevaluator performance (from J). Introduced macro getpropc as abbreviation for getprop. Added utilities gthm and tthm for guard and termination theorems. Added to :doc system-utilities. …

  Show description for f532319
  

  Matt Kaufmann

  authored and

  Matt Kaufmann

  committed
  f532319

  Copy full SHA for f532319

Pagination

Previous

Next