[acl2/acl2] 5851fe: Limited floating-point support in JVM M5 model

1 view

Skip to first unread message

GitHub

unread,

Oct 6, 2015, 3:23:40 PM10/6/15

to acl2-...@googlegroups.com

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 5851fecf731af6718250ecfd4b28dbf02f4f9427
https://github.com/acl2/acl2/commit/5851fecf731af6718250ecfd4b28dbf02f4f9427
Author: nadezhin <Dmitry....@gmail.com>
Date: 2015-09-23 (Wed, 23 Sep 2015)

Changed paths:
M books/models/jvm/m5/apprentice.lisp
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
Limited floating-point support in JVM M5 model

Commit: a612abf0ac59cd98c0fec777f2793853412b03e1
https://github.com/acl2/acl2/commit/a612abf0ac59cd98c0fec777f2793853412b03e1
Author: nadezhin <Dmitry....@gmail.com>
Date: 2015-09-24 (Thu, 24 Sep 2015)

Changed paths:
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
cp-make functions fix their argument

Commit: a012f147d9d227ec5e1600f752913c734ea44a97
https://github.com/acl2/acl2/commit/a012f147d9d227ec5e1600f752913c734ea44a97
Author: nadezhin <Dmitry....@gmail.com>
Date: 2015-10-04 (Sun, 04 Oct 2015)

Changed paths:
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
Fix my bugs in JVM M5 found by J

Commit: bac2e5aa4f4fa27f7807a67a0db8a2bfe3a1826c
https://github.com/acl2/acl2/commit/bac2e5aa4f4fa27f7807a67a0db8a2bfe3a1826c
Author: David L. Rager <rag...@gmail.com>
Date: 2015-10-06 (Tue, 06 Oct 2015)

Changed paths:
M books/models/jvm/m5/apprentice.lisp
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
Merge pull request #519 from nadezhin/jvm

After some feedback from J, @nadezhin has patched up this pull request. As such, I think it's good to go, and I will merge it. Thanks Dima!

Compare: https://github.com/acl2/acl2/compare/0596c6354576...bac2e5aa4f4f

GitHub

unread,

Oct 6, 2015, 9:06:38 PM10/6/15

to acl2-...@googlegroups.com

Branch: refs/heads/master

Home: https://github.com/acl2/acl2
Commit: 5851fecf731af6718250ecfd4b28dbf02f4f9427
https://github.com/acl2/acl2/commit/5851fecf731af6718250ecfd4b28dbf02f4f9427
Author: nadezhin <Dmitry....@gmail.com>
Date: 2015-09-23 (Wed, 23 Sep 2015)

Changed paths:
M books/models/jvm/m5/apprentice.lisp
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
Limited floating-point support in JVM M5 model

Commit: a612abf0ac59cd98c0fec777f2793853412b03e1
https://github.com/acl2/acl2/commit/a612abf0ac59cd98c0fec777f2793853412b03e1
Author: nadezhin <Dmitry....@gmail.com>
Date: 2015-09-24 (Thu, 24 Sep 2015)

Changed paths:
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
cp-make functions fix their argument

Commit: bd47d2ba6f32357c6afe71b459178b22b2c0f26e
https://github.com/acl2/acl2/commit/bd47d2ba6f32357c6afe71b459178b22b2c0f26e
Author: Sol Swords <ssw...@centtech.com>
Date: 2015-09-27 (Sun, 27 Sep 2015)

Changed paths:
A books/centaur/misc/bound-rewriter.lisp

Log Message:
-----------
add bound-rewriter book

Commit: a012f147d9d227ec5e1600f752913c734ea44a97
https://github.com/acl2/acl2/commit/a012f147d9d227ec5e1600f752913c734ea44a97
Author: nadezhin <Dmitry....@gmail.com>
Date: 2015-10-04 (Sun, 04 Oct 2015)

Changed paths:
M books/models/jvm/m5/m5.lisp

Log Message:
-----------
Fix my bugs in JVM M5 found by J

Commit: 499b2cc461c1a43e64a16f7115079afb9f33b96e
https://github.com/acl2/acl2/commit/499b2cc461c1a43e64a16f7115079afb9f33b96e
Author: Sol Swords <ssw...@centtech.com>

Date: 2015-10-06 (Tue, 06 Oct 2015)

Changed paths:

M books/centaur/misc/bound-rewriter.lisp
M books/clause-processors/sublis-var-meaning.lisp
M books/clause-processors/unify-subst.lisp

Log Message:
-----------
Add bound-rewriter book

Commit: b70303521af9bbf98b3b415b7cc53a7c63652ec4
https://github.com/acl2/acl2/commit/b70303521af9bbf98b3b415b7cc53a7c63652ec4
Author: Sol Swords <ssw...@centtech.com>

Date: 2015-10-06 (Tue, 06 Oct 2015)

Changed paths:

M acl2.lisp
M axioms.lisp
M basis-a.lisp
M books/GNUmakefile
M books/clause-processors/SULFA/README
M books/coi/defung/defung-defpkg.lsp
M books/coi/defung/defung-test.lisp
M books/coi/defung/defung.lisp
M books/coi/defung/map-ec-call.lisp
M books/coi/nary/cert.acl2
A books/coi/nary/nary-defpkg.lsp
A books/coi/nary/new.lisp
M books/coi/util/defun.lisp
M books/coi/util/mv-nth.lisp
M books/coi/util/pseudo-translate.lisp
M books/demos/proofs/tightness-lemma.lisp
M books/system/doc/acl2-doc.lisp
A books/workshops/2015/jain-manolios/support/memory-controller/cert.acl2
A books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-2.lisp
A books/workshops/2015/jain-manolios/support/memory-controller/mem-array-cap-3.lisp
A books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-2.lisp
A books/workshops/2015/jain-manolios/support/stack-machine/buffered-stack-cap-3.lisp
A books/workshops/2015/jain-manolios/support/stack-machine/cert.acl2
A books/workshops/2015/jain-manolios/support/vectorizing-transformation/cert.acl2
A books/workshops/2015/jain-manolios/support/vectorizing-transformation/data-struct.lisp
A books/workshops/2015/jain-manolios/support/vectorizing-transformation/op-semantics.lisp
A books/workshops/2015/jain-manolios/support/vectorizing-transformation/scalar-vector.lisp
M books/xdoc/top.lisp
M boot-strap-pass-2.lisp
M defpkgs.lisp
M doc.lisp
M history-management.lisp
M interface-raw.lisp
M other-events.lisp
M translate.lisp

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

Commit: 0596c63545767fa7c123d687fc9fd9bc29e63d02
https://github.com/acl2/acl2/commit/0596c63545767fa7c123d687fc9fd9bc29e63d02