[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: ACL2 binaries
|
From: |
Matt Kaufmann |
|
Subject: |
Re: [Gcl-devel] Re: ACL2 binaries |
|
Date: |
Thu, 28 Oct 2004 14:38:38 -0500 |
Hi again --
> OK, am trying. In the mean time, it might not be a bad wager that the
> package is still fit for upload, no?
I don't know the rules for "fit". But probably you're right. I think it's a
reasonable guess that this latest failure is due to something related to ia64,
assuming you've successfully certified tiny.lisp on another platform.
-- Matt
Cc: address@hidden, address@hidden, address@hidden,
address@hidden, address@hidden
From: Camm Maguire <address@hidden>
Date: 28 Oct 2004 15:29:24 -0400
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Content-Type: text/plain; charset=us-ascii
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-232 required=180
Greetings!
Matt Kaufmann <address@hidden> writes:
> Howdy --
>
> Thanks. OK, I checked and your tiny.lisp is the correct one. You say:
>
> >> The Debian machine has a chroot running the unstable version of the
> >> distribution, having most notably the latest libc, which will be
> >> required for the presently compiled image. I would have to rebuild on
> >> hankypanky if you would like to investigate at ut. Please let me
> >> know.
>
> This stuff is a mystery to me, but the bottom line is that it could be
useful
> for me to investigate at UT. I'll ask Warren if I can get an account and
will
> CC you. If so, and if you can build ACL2 there for me and re-create this
> problem, that would be ideal.
>
OK, am trying. In the mean time, it might not be a bad wager that the
package is still fit for upload, no?
Take care,
> Thanks --
> -- Matt
> Cc: address@hidden, address@hidden, address@hidden,
> address@hidden, address@hidden
> From: Camm Maguire <address@hidden>
> Date: 28 Oct 2004 14:28:49 -0400
> User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> Content-Type: text/plain; charset=us-ascii
> X-SpamAssassin-Status: No, hits=0.3 required=5.0
> X-UTCS-Spam-Status: No, hits=-174 required=180
>
> Greetings!
>
>
> Matt Kaufmann <address@hidden> writes:
>
> > Thanks. Well, at this point I have no theory for why the proof
failed. We
> > tested this in quite a few Lisps (GCL, Allegro, CLISP, CMUCL,
Lispworks,
> > OpenMCL) on Linux, Sun/Solaris, MacOS X, and Windows (though the
workshops
> > books were only tested with one Lisp per platform other than Linux).
So I'd
> > first like to rule out the possibility of an "administrative" problem.
> >
> > So the first step would be to tar up books/workshops/1999/simulator/
and send
> > it to me, so that I can make sure it agrees with what we distributed
with ACL2
> > 2.9. Would you mind doing that?
>
> OK
> --[[application/octet-stream; type=tar+gzip
> Content-Disposition: attachment; filename="simulator.tar.gz"][base64]]
>
H4sIAI45gUEAA+xc/3PbNrLPr+ZfgXNnXqiLqEiybCdO2qubpE3u6rQTu5d3PzUQCUmo+UUlSFm6
>
6by//e0uABKkKNnJc9q5edW0tUQCi8VisfvZxaJKJmXMiyx//OCzfYbwOT0e4t/xcDTCv6PJhH7b
>
z4PRcHR0eno8moxPH8DX8fDoATv+fCzVn1IVPGfsQciTZF+7l2Iqebr7vZ2I/fsf8lHV+l/wazGT
>
sbj/MVAeJ5PJzvU/GR7j+o+PTuE/kyNY/8nJEaz/7yLE/+frL9MwLiPBBoPH+h+rBsFcpCKXoeed
>
v/h+zL6sW8A/iq9E9DMP47HnfcFeiqVII5GGUqgzzxNrkYdSCTUIRV6csfp3LNVy63Uh0w199bzq
>
q3lK7Z2H1fg8l8UiEYUMHxfZUvfuahfxggeqyMuwKHOhHgPBIojEDDqr3b2AMKf/7G4iF0Asm2dL
>
FcQiSfgeatj01zIrpEiLIBcJlyCrvNHtD1z/ev+/e3X+8uLV5xjjlv0Pu338YHg6ROt/Ojym/T88
>
nfy5/3+Pz9VCKhbJXISgAxsWZmkBCqpYcZMxNAOKZTNGFkCmy7JgXKkslLwQEbuBPegdvpbzRXC5
>
FPDgPOXx5t98Ggt2adVKHfbZiwVfFiJnT5BWsRDsH3F5A7/PQx6JBEzMNMuu2eGLLIERYGucywio
>
vRNcZalM52d6/BdcAd2ijMDKHA6MsUALccDYFRAtsg1LeLiQqWCHV2/e/uuQlQrozLKcyTiGdc55
>
IbMUJsI8tvVBvkLNaJ/xNGKcLfMMGIZ/OFMJj2OGVPHpPOeJa+eQC6RxmcUlDqFoUAHM2BkbyrUt
>
9LzLLBH2NRibRRYpJpNlLENZII/wHCZMawAMKXYjgAP4m5W5l4A5WdFs4BWLhApzuaTJGYIoDGA0
>
FLBcdj4480iG3LTzFtkNEGV8uYw3ZrRChItU/lrisqcsFzyuqSAXuWBRFpYJmDKQrEw9EOTFgL2X
>
cQQL1WcvB+y7XKwEfXvNc3jaZ4evZjOYFPSxamEY/TbLQaxA4kc7BrvIIhGrQzZ6+vTJgDH/KkP+
>
BOxQkIhuzy6ssFJ2uVGFSIDCS6HknJZ2DJvvGctyOZegjuzqHeMrLmPSSl6wZTbN1oMwSx7/zyK7
>
luIxzEcNep7nveQrGWn2SV4XvCjszLzzZS5jov1HGuvP8Kntf1Od73OM/fZ/PKFnZP9PjiYn8Hx0
>
Mjwd/2n/f4+PL9NgycNrPgeriXb2sOd98ZvnkV9A41O7BFVZtyIjI1NpDO47xxF4d3YEXYbfu83w
>
792o34ppXnLwZLRXvd++8DzfYNxAj4Z+AybpPWNkgadcyZDNyjTEuT0GD5JnYFFnMpVmsgswGzfg
>
QdhUaI9SLPKsnC+ysgBufGirO71Ji6Mx89c99sHHyflokkQUTDeFYEfjHuuvez23w8X5f//85u3V
>
86PxV8zvMTYG/DN5cnQyOe25rd68dVsFVasnDWKPdIM12+D4hpdHMCbrb3o4LqxqcF8f75VZevZk
>
MGIe/CwgAqAlBacB8JZpppYAurWv4NNshW6JLWDJQC+wqVoKgBIx+x5hPnjMRLEQ1xoXFbQuQgfw
>
TiQimaJPplfXYsN0S/RFaVYwseJxiXjkLz1gY4l9ZYGElnwqY1lsnEGV43Iz+E9uVl8Ci3ORe9lS
>
aIwAyl6C8wZvCyAf+vbxr0RPKooQ2LoCBeNlkSXQOgRksAESCpA8amCxWYKXFGHMLS0gnzGFvl2w
>
WBRsin44nZNbV2UCX7WSEWCABh42gBnC/lunZcJwhmJwj6tHuwI0p0xhnZbBLGU+/Ity7aFHP7zg
>
y+21hCY9BouYA2MYR6Eg7baB1ZgTKlCHSMCXM+bDCgIq0kQ1xPrg+30Yp++HYHHpBeyJr33DAnIR
>
RvaF7pPK2G4Z4vVaQNyEEVwYK+bj12kWbTTTL4DbQgu4If02FJtmJejICkJINFDK2jcwPIwgrYZe
>
RAdZGbRnVI+qZ4VsMN83i8poclUb4P4Apk06sW0P/JnMVaUP2JZpgTTniVJxKHaLBmUY2Fa0nk3x
>
3LKmWjLQk+Cunfx9zL09S2aUQAnc4/Xk69k3p2L14m4SQJq1CKpfnyAD4q5LCA7RhhTAgyVaBHUL
>
IwMzZS0IbNdri0E/bMmgnowVgkt5nxTAVjpSsL8+RQpodWkfMPY2K4RHoRIYK2wG1lhVEY5tuG2Z
>
EXfjYKyQiehrCiUGNNApxZaJ4UizYviyzCR/2VqAej67FqBq0VJCEvOdRF9JsBK9Q7Mh+mcQfcww
>
6iT3wqOIgAP4tcObHIMXI2KIakhw2jhpD1iZTSCCnisXBSwi2XttuFyPBUFLAqaWgs06AabdYQOI
>
0CfQeICzqYMHApCV/trnverrlGbU7D8yeAKaMRdPuP1HHd2Crm7Bvm7gWddZ3sWtfnMXjrWX3kED
>
BXs3GnInH/LOfIA+d4lAv3Fo9JxdqzX+Z/LDlRMGsJzOhUkPcMTDqAiuQrSVwKhQWOZKrkS8QSXd
>
u7XIC2awFUmnVDkNDAqzLpESJcYpdplC17v7ZAHMPjPTOMAXz9g7sYx5KO6szTq1ZDqb/QIuW8C8
>
NCIXuchmA0MftVLDC62z9KlxxQczaRdc9EzPwPYMPrbn6JHpOaoHvWPP4FN7Gl3+4DvqfueeqMEf
>
fEfJ79xzbXuuP7YnavwH39kUt/W0a97pokhrXRVqqZHtbMMKaxgPau38YJTU0K1cQBuMOua/YjQt
>
FsjruD1PIvBB/+ly3XtlBH4LJQR/+lvAp+rYYNI7ONDbzfqRDsDY6FD3sLP+umMut0u+4a8IHKQb
>
ps8zMOwx/W1EUAu+0Nredy3D3VSI7CCz83bMrO1SG0udAEaACoavybxUgEZuMBQtIBjUYZgB9bXd
>
tWN8riB57HnvwcgJnVWep4EqNrG1ygQLdMynQJQUHRNrEcumv4iwYOUyAiClPMrjxnF2o9EBLgkE
>
l3kWlaFNqroBJv7G2DZPRIQ5e6+KegDNfYtx0ZqjOPog3Mur4Md3P3z3lr1+f3l1fvUKRe/rcYOR
>
fUi23qAtQikjtL4TdlxhoqrPmJkGtitIVy2yMo5gVArTTRZpluGEgF3EMJq06dIxPo2ygwHPgYJt
>
CtvcWLflPLi/lXcCbFUEesXRu4P+mx+V5r7BcBNzbTaUxpQ8pgVEjbPrPqjNvMolQBSOszDumhBC
>
irkIe4qgCoyIjfIQOgDR61eummyFuC0eHbkSDwSxnTZkPrZQgWt3W6jgoDZ9/a/xITxC9O27woL2
>
ZBMaA9nexqhopvrQtF9ZRxz2LpQ0h3bjIz1VNM2MpQHrxv4rF9uL1xylQZ9MCaUv//LVWZHzVIGm
>
du2x5qd7x7Xa7N1/3fS6diPzv3915e6Vn358CX/bu43I6Jb/PP/+p1ftHccaTdrExsx02qJZf5xX
>
RmK0gUiEn8ccH3nejzklJGGL9dkc4HJKR55H42BKx2+UEFS1w+uzZVwqAjG0+XTUZponYIBjOqOi
>
blUMCFb2NTw7Y//KSrD1G3bD0wLtXglcACwS6wJ3pae/Bo8C82yWZ4k27gtFOXLSrRUdiyI0pnck
>
qghMQC6nlJf3MMuI2Ge2ob2+NDMEkzEVC74C4HefSUTvUohaKDSg+RHcZPk1HQrUVRyfZx0nnvfG
>
rgbmS60NJcvJw1AsC9WxrjbCRtljyJ3roELm7Xbw/UbqtcI8L3aANX3PVdNme9ogQ2AFoCPLCZXC
>
7zXykVZi+Rt7v9j87R4FgaDHMGxiIwIAOkqQilmuiIuiq7GHvIF2hBw1kuIqjZcI8s3AL1PGyZyE
>
kOpp8iCFS6LuNXKtqsSjXqFzrubUN9TaiOPPS55HOnVPygn+iCsZb8DzY25JLxvq9UOlcQuCNu6e
>
azdGizKhKNNkmPcq8Gmbv3l9CV5ymvN804fQAVUyyxEamj0IwgB3m5Rg2iPYPJmX8LTEfH4fXqM/
>
5ZrnAALgwvXqjWyD56DxHale3rSV3Y2mGvf6a7A6ip3VIwOk9w/nGY8P2Rmy7Z/JFHx7iiF1TSNY
>
BrokCSn/W5P0JcN0xS9Am3zjAYOuAYgGiz38MgVh6V8SREkNdKzw0G8Q7jmvfLA5dLTXNXTPeNYq
>
4WODVpQTvgCbzj6PLTj2vBc8DvG0EWG22iTTDLAOQh7w3aoyC+a3UCbOUWVMZxliLcJSn+DAcyr1
>
qHQQt7beQiaNeIO6pAvLXH2ryrs8UyVi9wnaZHd05EZrGBHlYWFsVmrgmg6wPGFsm6GvAV2l93w2
>
E2HhHGeZ5upe7fx72LhYC6hTuZQutcyqG3SSZAuxaIR26nRTyR53klfJVcfs4BEach3DpAToLHQr
>
8g01y9ghmYdDGC0vY5SFpyMFQIqeL36FLQp7CCnBWoCWA3DzvBLlDhZIFqSdi80yo6IWjHXoNPuQ
>
6nkOQdoyFlEfZRpmZa5En4EDBUMAtiyXK2HPMW8gYCsAFzhLVjlm4g+UoiyWZYEuAdZmkd14U4E2
>
0wB3GJOEhckzXOFaXqIS18CrzEqxSEg8TpHgOCDhEDpHLRKKAjD0W7QVVbGkydOP57A1i0zhAzYa
>
Doew77/6svnMtDQSRB0N6dXYvjFqC7uZwk8Q718B3BDI/Su20gEg9dcd6lXwXLyZFgtt8IZsPGkG
>
hvCKjXYjX3r9hNItCDTH+tuYwLn+PtJAvQPt7qD2tKI2+jRqDcp1py5s7ow73uafelG/s7Zdd8yy
>
SEmDU4SCZdo0xJ/ZiJ54WH4ROQDTlHtVXjjOsiVoZYYHG6D430mqwrCZBFJ4j/TfAhA5k6BJ042z
>
q4Te1rWsAudrJGcz2pHezUKGC3ZDOQM0d4BhhUtzAYzupoFdPNyluYwikRr4MONo7heizAE5y9CA
>
GpqAiYzP3Bl6NgC4V4v6Ax4WYYGBNg/geT1XcSbsYQgCNAG08+II/PJSzlkIgrkWaY88dqunn2QI
>
ERYZGDamUn4teiwmrXmPM90jLyp6QROvEBdJCHka6RmP1FMkyHkoRKSalsuhZpZoA7vcmBqvOY/P
>
M8FPHUN3PkOVDADEETTAoz3Pe/YMDbvNsCGqcHD2HkmS/pcGYiAVq3eNzdMpuxapwPRsewA6SzJm
>
PJ3JNZOjnv027rlmujF3OWKrUfPJmK3GKAIU1PaL7c6xQXi6SIxwN2kFzRk9tMjjjYX36GpBj5wA
>
oyECdi3Qu90+fe14qVKV6kwRUQJwN0iUzJVHgZcgRIQ26RYL0y19q7nj/yjN3eNKLFbfLQi9mr99
>
8UcXIv75+UM+df1vlau59zH21/+eHp8eHT2AP8cn8G0yPHkwHB2PRsd/1v/+Hh9Ekl3FvnRboI7S
>
7GmTrp619yz6FKKuwZJLwohxdQEDrLwS4AemHAtmwWF+k21E/lAfQlxkYKrhO12q8GpaytxkmNLd
>
AvZRV0u8PRXFt1wloeiNxyrz7GU4e99jKtJwkfD82l760F4utGkG1Qz6KUq/QTI6e2wDT5Ks1I2p
>
G93vgEEEpV0o92BlSMXV01LGkcfpFoe7Cmb0FCuROUkE4RoWfZQYYqrC5BQSnm48NO4ix+SBvV1C
>
Aa/NWkAz6uHQxzPbSwEQBxayvreSzoHHBMJBuoKBYhk9ffoU2czFLMb8AzhNdPeafZlSEr+PudAF
>
LGAM/xZ0bI9VJHNzs8VeiAERvUnZkueAxTGF3scwHPxhwM4jCkBtFgcAP0YBPBHIJTb4ifyYDlUS
>
vDZik3qXVz9883esHaYvug+Qzc0iq3KqwLcDs6Cfen50Fkk5202dX8d+1fwN11HOZ4VJG8eCdLuq
>
SrH3pMaDyaCnWXxhqevQw5SUY0uTieVR1MhJ8lUmI+IEVCaHQahuRguWx0U2F5jm2d4qrkSpQF7s
>
qI9nuMLQDEuq9TrayCNif8fcp6mc71Wl81u3A1rl9DvuZO5puO9S5p5u1a3MPW22rmViob+vRBGk
>
ZWBizzxAbTEI3wKkCjCZvw8NlSqj3LOEYL0BIAY6lR0IkEyeCqUwDaUhJWDb6S9Mn8zarIDOtJzp
>
tG8jpGejYQ8RG2gG1ZEPNRBPAFGb5jzP+WY7WeyPhuNJr6svJXw+Yqzw7u2rmCgyFY92e+pNZr1E
>
nIWNrL0WCW1haoREKP2e2vChWcBI4gIieN9h6NbXgVjMY8ZG7gucs30zdl+EzosjzT5d+9B3+xQ6
>
lxLLRlBZ6izcQgQiz7M8SCFa8epQqnrB6J7Fxp4XY6cWtiZLuztxtwF3uV4yH28GiyVLR7Z+YetN
>
O5zDSCBtBnEpxGpVDIfn8G5kmFaRIZKChpZCbFNRjcjX989skqaRCdHVrj1tE9rhRS2XtJFj6DkS
>
10WwpCMgm5VI6Uagk1zNZo3jnT03a9iOuzV1j7e8GA3duzjbit3q4V7GYXe8jsO2LuR0tns0arc8
>
bY/89vzq+WhoR4atfdTRIhhRG9Ni3KhVgPX9bTT8DafsYWWEEYAtf3XG0DNvdE74ur495DlVq/DC
>
uUHUednIY93XjbZzJ7TZNuTzqoNa1AbjC0Fl0wJMjdCJJwBISCPNikBlgenruM3mWS8lW5zTvvpo
>
FmjwaYb5fcomJph2W3A89IQhQPdWWABbZSzqVL4+EMbusJnkiscCj9uKjG6hkPUyxo0sSYUQHB4G
>
JATMkVSn5OQ1jO3JkS6AkiOWyLQs9JVbwHY/xUXOYYHxZm+cpXMkgoXzJCu8elMUcZV2GVQnktUY
>
H3EkSaeNO88inbQ2sKDx2HSj4cQ/BsTOahycnjVONrvPLr/blePeSm736qNDMnpozZ7DtIcVP/To
>
qy/ZlOEJh9ZErs9OTWXMUpWJfdP8w/VOMPuyh7Xo+lySJHGLwJCsbarZooGGploRHzfHdIfSvdFp
>
HbhNNauOrbAyqAfZmqcdbOdkeYuineKdJ2hF3JxfNS2Htu6jZdLgwUysJWx7PGx09tF0RXZdm5Fb
>
+VuTw2W6thgPR7TNoceOI26Woex2wa7qISne2/FiqrWyOvXy66oXsx6+nok55O443aFTe+fYvl3x
>
0zixhzkRJTy39wMYeL0s2Bjf6mreg08i1KICXLv7EaGtjRhDUdcEdG9U9tBvDewsLK6BCYGXAV5d
>
UIF26TxeOqsBX0wjBm7ar5qwdQcqsWi9RR0XomOBHdJY/VD9mBr1qR5YAe0aEOzea6C3ofNbZRxJ
>
7YQonKu4Ih2AKMNceqWwgqtANyc2je6549d6Q29qKWy9eu4+Yg7oYM8w/q2O2dr2mTrjQbDT28Us
>
Xfr6f1ePreIQ0hFNFzaDthiOHu9UmIPKuK5b20znx/eUwrT2A34btbfGNpmmctXDg1X9/ofvzt++
>
ZOdsMn46eXpyOn56XJfXQ5Np1eSbRhO7OTqQc2VKaGq9XqNRt5MktbzoRNPORRoXrRlkaNFaCxtq
>
g62RWxMptlAfaHw37qsm0YUVUzGHaOBnDeC9ump3rRG4ltxtlr9qaEZEB/UlWP6Wo2v6pvr62brl
>
eFQ5bczk9vH3YSXtlXwrHuCqnrOWRoddBMy3Zbocg9iyE2YKeNnwwu51XPt/mvPI8eCEcj2zMqdC
>
ILv5a4PAS1iPND3rOvaCsHq500/iSwy8qyqTFKFHSo/Ms4rP1DwAc5OyRrWIodOIWrEM05A5MCOS
>
lJ9/2XB7I4xaeWyW4Dn1ary8xf4dNFhESncuwXAj2Zb024Kl8SgB6KzJoJI2z6coZiAeaPj/EfIe
>
bwkcJDSkcL7ZFQVn8gHYuIW/6jbNXeL0aK9n492d61ZIWrs9KhZb1GVtWij6XkMzEtxAMPZOYOZp
>
cC+C/8Mk3mzipgvoPZ3lP3eeM//t1eta7KDfKUS/MHU8PMBKxMFHLKUFW27FABifn2EZOzr1mAX7
>
z/fR3qsn+p2DZLZf4v85MEhLzELfSckQPrd3kNmQ5/EN3yiwACtdX0Cml/ICmbkgSI69qBQiFkoF
>
0Ko7Q9dOv23aK471HSgctMiYA/TJ4Af/296zNqeRJHlfza+o9XwwjNyom4ckNPZcYNTSsItBB2g8
>
vouLjRZqWaylhuUhS4758ZeZ9ewn3Vjy7OzRu2NBU1WZlZWVlZWVmcUFvVniUUhtLEG/q1VMlHhr
>
NvI2uZW3ZjNvdTvbGO4y9vCUI8WHsaLTD4qxNEwVy2qSVhLzTKPJfb5e3qCfDDrYA6eKQYDxW6Dz
>
6uRzVdkroOAasEZpzl0YNy3Ceg0QRgYyK6O384orYdzqoLwizVgxsokrV0hJ4wjAuI0QK4QDyzCW
>
SKwKwIxTxhvmigYiGHIMlCV5Ia6G0WfLkb6AnGizuabZ9XUqyWZzpBjoGWgyTaFavBOi/Na0C0z0
>
DXfS/GQMNtNRdqpM3wIFJZWcgR7MRM4TSSlubxP4bvLd+I7OVvi/RfhuspFekwy+kwUnxrhNcrKd
>
ppjBdZM/gutM7BUFC3HdZipGuG6ymesmEa4TqT+MkAEjKgAkLT/2Fc7v3DstHGyA1l2k+3pBZ/VG
>
fcWyAd/IRgifj6TGu1goiZLpPDJE7UlvsDA/zhFSmksePnWUlVbYH+loU/uSA0QuIwxxC68m/FXh
>
mcDbpZbEcJrjiZ4qfOw0fDVuG6b1NFCtMRGmCq9KL37C3gLGdgLTiM5ypuRfapJbuB1ByGh1HEPI
>
hSqIOShqETygKwAuO9tBFAsph5QPcBT4FKDXngB6HJwBCSYbgKnnA+OEwCTUia2pYcRM3JTdQp5q
>
GbhSVQGMpkFqId2+BCDFAPTtH+s75JlGtEs5+UC18RUaaSoRKBrhxo40tMlAL2OzNsMTZSNjalB6
>
s1ylShlDwxsNzCmpxiRt9IyVCUiBqxBQ4kBRAk/8cnSuSC+gyc19QLihHpSl/pA0JzjyPKIU0D/M
>
gf4k3Pnnxj5NMwiTf7m+BPSPvv9MlQfRIHuViS5lIqqIxNTpnDxTr9Y4UVvb9C1R2JkzUcu6G+92
>
BWAoKo8iiGXkj9qGwvps4cIe24DqkC76XKbVX3ZAaAQUdYW4B8+mE2h1QCAwVwyasqAGXC1AaYXZ
>
ssjgoC0EXKwGaGKgra/8Lj/Z+AtmkJlSEEMgw4elH5VwqDKGTRNGLuIyGE3KcMcy4XIKgsIFD6pd
>
pypamKzomD4SFbUxbwTTpWApDEw+1lm1dIIbwPF+dnuPVZbVVVWkalnyaGIKVfLI/RUbIe0C/dzQ
>
bIsRpFVMeu0v13dA4UduvbqRUeWYaWIxnchc5eQcSGrijOd+4cU9Fd7tzYFZMcElduMKHTnvuMr5
>
5YbcBY3AeGxGBryjok/OWSby0xXZmpbcvRMLvsacNBPQXe/9xWO4Q9RTXkr8PAdiBdxbzFI2WQOA
>
dlfAAENpzrm8nU0+6x0GJRf9Fm035KInsvQJxiSmFLksp2L5ldyzYYtAuS2nepq/KCf0gcsEWQc9
>
ryh1pa6GmCTQAHqPifVzdztfF6lN3UejhwmoTzzoIK+BWOsvoSkWwhn7ZhaqhIeXS6n5hNz2igxq
>
Su9SJPbc1PtTlp+WbUf6ES3Gl0FblQsNr9mDUD/9YILOpOXZPLFnKR2h2UOOhfDlFWwZpHsLfEF1
>
HN1EjK9TFV37Clf0uvyCCiNrmN++sqb8Shv5A/kNZik7lF9gaWXS+PwK3R9b8gsuW6hfGD1E4+Id
>
LgNl7GmRXpoZU3lNvtNC3z658GMZvUbw3KlQtmJ8RoMjJ7L+WTvBGOhdhX81EqOSpZdHMiNZ/IUI
>
aNa1X5UFpW2xIWIOeZnJL8AWRNCaTWo6EDah7YRGYWidFi5rNZtvsunNkfjMx/oIfm2E3rT4N1LD
>
8APpLPiBj3H9IN4WYRVthv2kigpQkYZ5e42mJGf6w3mtZbSGtPqp0WQJ/VK9DlVQvwMz8g8mny3W
>
gSWCiElwWDzXQTlIkxoxrgsJkqjE0AIJ9mg0lYkR4VuMLSriJxhrPawVUw4qRSOgHvzwO8h0mevp
>
n5gNfaryHdBrTOZmYTpcaAu4nWIgMTgE11gL86NjYnGyCEH3eueVKrX2c5nc/soplHFEpBHf1dFd
>
HVT+mDm1Kr33J8vSgrRFeC3eO+J9+Ycyzvofyjbj/6vRfw6r479Q+wD734A//Ocm/wPDaiPHOuKf
>
FjtiLaRJE7iS/9QANuQ/UaEj+Am4pAHMQzCojK1+PmQSARubsb/9f7tmds3smtk1s2tm18y/SDOw
>
eDqs6fyLYPNkzTj1wu2QynHUalXgD+UoqvD7JX/m8YbSNgMP3QqGSbDI55ZCe6PRuKI4/uFhFlTh
>
0v80lcnqMBAWgzxup3fTwCOPVQoXIV+HNZpaMDCYw6BmRMsioRfG7D7O/SoHgVHC4moDCpr1l/wS
>
NJEiTsSBcHy1leiLz6j2ml+PIDI0ymvYRJ7G2XV2cKGNwYXQSJdnsUIUXzKRowm681IG3L1EdLQB
>
6z/VGW44rZPMQ4sRzbLqpp15dE8n6lfkXXrKQwY/a5e/qQ4GRBuISh2LVfUuLp52SiVsJRiYbl0h
>
KuqpZK3k8w8lofbs8zrdkTEWWSe1+Th0fIMAo35O+tWbt4zCCnlgnenqxV+ggzEVuPU5+YXtJxzG
>
JxJT8bBGeT7DxFuLBQRQVk9yjIq75SA85a+Y6HEc6q1JRO7Azs2KqVQMOe2rL4+KAA/aN9Pe7JtJ
>
laTzk1lRtfe4VXuPsfZCxOd+5BTDqQNIcpGX10zIyZVExNpTUDGHh6umop1EtwItPEa9diWluG8a
>
p5bwU/tGigk7KLnkkSe6hWGP1g26nqSRjbwwH/QUfBChklGahrog/NxFWRleksP5Nyn1WniY7TwD
>
/A1jmuAJ/ZA8PnaOjuVnYmFmWHiYvOF2GsTEQYosjeZmDLg/KS0bX7EUiXZuF5bHN3RME1RyMJR5
>
IBWywk72xMV3wJ5cAD/ImOfHeL8me6UoprDcCDGA0W8cP/HLg/TvT8AM0+4bBQtHzWBNDJYJjACq
>
hP5O9sw+6BAC7yGB/fLHPmFwL4+BMVqHlxZ6yJY0M5vpHt/oakwuhQQUYzTx4ADjFSchaSsrTgyI
>
/B2eEuJ7r8L/XkaOSKk6dtOC/2V39bIS6nclhr7WSST6Hj+IvBTFk8rhb6FyeUUHVE4fTvox2ksM
>
odmqm1G8eVwTleRvPGaHyaoYaA0q8aNlRUGmR6GICjIWJdbgXn5xaKx5UShyQU7LNYCTxoBO/twU
>
TpO9dhh0i7y4VCLaVj/SSiPnjPDQ91AYR5kUwc8N+PWSCV8xIbTnifAYzk3yM4EpJSAYxc+MsqkY
>
EowCcvY4asgTOlFDCoaNghi+3R5FXL/2FN2EudwUNbblWZcmFipegdDRXEzz0TZbqyhVRdX5eXMd
>
80vx2WxgPpv7QZaeokK1N8jjqFjiabJxR7ugq0svYcQmNx46AgSRHCOw1b2mbPPe0l/OMTEAOpQm
>
5yOpRQVyVhoRjnZmHpHSi3u58TPSieRUrAyQaqeSnEXFiZA4IfNlGK/YwrOxn6FsKGl4RDX5TNIU
>
xOA+dAzmz30PnVvgtdxwf1WBdXSqyVulI6p7vMOIVyAlitoyemH0gFdMygkKrVBsFmg+eF0hLjii
>
0Sn9IM7L7rcY33Rs8D8MUkFLjL9IXPV4yFXFCDm8jWzjQsGEYkd9W+H/z4lrNF/NBnzzIoqaenin
>
f+tU1MeMDK2BUYjq3DpSIPAsYUZZ9PRZ6hR7InE8z5RGXv05EsxGO/QHJ5bdgsFKuQOhymWARL1I
>
GWUzE6x356fOFyf6QnY0Vi43H6bxIHCTxWejgQ2ymJ6j9xU1QrGqRo8u/dWKzzSzlYgguMW2cC1C
>
i5tqNDT7ign42No58RYGVgY6aBlMREeIwCnlriIvrC0lEWNh4nB3zugMMKiDu9NGJfpWuoGKCCIs
>
knfnKgwdaJuGfc3yc5Q0sEsUW4EUVTbdcpS8F3iUAYbijdgb2/Ex4aI/Oh5iQVBbY23/fRDGXPn3
>
MdLkVVKTVxublCsQFhWo48dI68aeKckEk65zCWHtVSIafohutpE4hVrTGyn5+ZKTMD54SeNmpjYx
>
ob2Rex3+9yu5xsKQfU2SauEMKLTpIdvLVfauJwo7brrxKik/qH26biNCLtoS7QExHjjqoFeTDvuQ
>
MkGjWXAMmlF6D75LKD/S+HxVTVfilhU5oTrtfsft/f28dzGyeu5odG51BsOh2xnHN2kmudINs89M
>
L9ElYfJ4kBT7Nnp9peYen5hec4Jjza7pb3oeJbE5Fkur2v9M6+q77j4Wqsd3qHw6B96K4rLTjKrG
>
7tKJbjdrxl5V/poSsh8VkaiaWzw3op7f8DJQvYnW4MVJ64/ViMlVftVqVK7yt6SuarWwgM6abh4h
>
s6oweV+D+rOgE6HoilxKiuiWKWjIOR4T7v/11VIms9PGnutrS2fCUltvLnWvr5lM5hV+ypez2a3v
>
BWpapfz6WAn/LIimMn9tkonKqJUtFZOSbEY267SnMxkswaSpDGJYOJBOuuZ7ziYZs9vIOyQJS1M7
>
3jif4kmNyw3CB7ogarHilwVSgmedtSp8gk7lXRWOulgHFDGA6jJsJSYYeeR99vWFR3TFQ+jSo4rc
>
saKLJKnZWM8SIa4yWtXgu7LM6lohP1UW+VWcgYqYnfBtQDq+bU/cv3OUeHKK4XuWKNFKKFExIuVM
>
2PSPSCGrg4tYTpAvWA6gkQCsgN9HZDkJwM3L1nLBxw1WDgxUi8kFYugpnOIoanf/vHdNVBIzW4Fo
>
CtnVJCvpHc/zXnslnec3XXulVjVbODUAndW1UaH3R+b7UOGkErR2vs0ohueEPy38q3Vw5QUrflGZ
>
ugFpKVxHjL7Jg7dDkUY6aW5KZ46wQHr1Kv0SqnBGRBo0IXK0CCHR8QXztk5XzMe7rMkDJ8C0Yf/A
>
QCGRw6Zs3seHMgaa2SRlQrwBbUetgt/MGWin1ikG7JrNs7YYr5xnZ6JkHvr5qXkoiVucesxKo6V1
>
eLlWWeOC0I1q5YkpwJIkVWzRx0ef3msASYtCYuXoJW92SrHkpuMyf0Nt3Uy6OM7dRK5lIG9rutk9
>
vRAk4bdFk4xlLSxboBjpee1peh5B9psGJ6XRyIqZhymNJXTbQQ41NzGaS554ArdvEO/5RbsXPINo
>
T9+Z/9uJ9kyZnSimG1ExzdVoLarp67YSmlRALpELaefMTtSqSSKnaL7JCrdUUO2wuppfZX7xwpYf
>
8skZUfjFZhVblolKgQ2acxa+f/D85un3cH6HchaJubyaqYg0mv7kl8ZvTX8gr+XHqrEBpNmLLPhZ
>
HOjpzKrJ6QDIYBh+9Shy3NlkECXnPm0NME6jyWDqNEhpoZ8me+yQVN0ELCx1UYdxxhoqmiexEndm
>
kGlrQxOVNuXmlBdIJaJjuqPRWa+855fcl8VV1OWAzUOU+zqHF9J/js4Y55ouwt1YGB6TG7SoCtaS
>
l9hMF3h/0T2ogxZe2ejdLq3ZZ3b8xVsEITKZuzFL+rtBL9jyCcd2pSiWCE4OYdpuJsHSu4eupI2c
>
7kCSeOrFXLqViEyPe4woT/ftmO42c/FOzKitM5Ri+tHIkVh6mtLbuFOJsfioL2iYTzoxjyXh9Yyb
>
YzBxdbnbH7tn7vCc3fORMlKFy1f35tUo3+wVEHVPamZbmn9ml8TRaqaFOr7ZyUu9mAjKCPt11E8p
>
2URq+O7xNNKO5V1dORadbJEJmI+Qcap1q+ZqpLjDTXt40oqmPJ4pQvQqFNxgGFSk+THF7chwlDCI
>
E4Qsmc/sQqHNA2ZshlaeDNkT7YfhexAwJ4xnNIIlnEeaFCgdtPEiUWVTv29xjB0NmqjwTDL8FmeP
>
LScL/8sj3TmLN9qtXmF2GOglKGIrdfttBCPKeGwmZsH7qDBqp5pGOZE5IXnsuTOtiBjh/KxjT/jb
>
QB1W3Gu/lMR8vkEliXVE0/heB8JkDIyDjYeHho9pZp3kFOHxZnIMYARO2O8szqj61CvdwBTy7OPO
>
y5EzLvRjZqtQw2rh0jdHYnqcP/FWR56IJ2xr5AF5ykaIn3zaioa8+LJmZG9K1J30MWk4vIwcVTgx
>
8IxkiZI0WQ9Kv+ljAzeluPGX9N5GXtSw4tZR/curciyUwlD+dQxBivIDKOugsJej9SUix3509p2q
>
gwo/bLhpqzd037e7/RN3aJ0PB2fW0B1d9MY8jbgj0ok7bDRONzfwIi2zaCWiqhbUlpP1cYNdomqz
>
BPVpBrQQlw5aeiRFOpCc4P9UkynFPvAmak0wRYomzGQGC+pkpXcoobmkBk5lnwq7sWZSW5Ete8KZ
>
TJW2B0kf+LxTUt0dE3KJSBOtYoqVNwuWLNRUM1FJJ99fxmuwZM+LBDnAN+I/sRG/bs5bsdl6YaSa
>
E1fL0gGtumMY1IbpFSZZm3h04y30qUqtnM4Wq3UABLh9fM3eTZc3sGt/t4COvhKX3d3gFbjcZbxa
>
yrxCFU/FMfWewRDGdaoxDpxmr2bxUDgzii8e/Mi3iSFJn8xU3HUKQBsBI8aK+y82MRDPJ5gG8SkQ
>
EwVCdOe6/zty/zsqSE9+x3j2/e/w1Jv/AeK0fnjYdBp2E+9/h3317v737/F8gGVpAJpG7ZA5B8fN
>
5nG9zi7GHbwEupGPg3bPn/mJzP/ZevX0MLLnf+2gXrP1/K8dwvxvHMKf3fz/Ds9Zp8fKZ/0L1pnd
>
3YGu0Zsu53j3cfWg2mSd3qqHdxezkT9nmBkOhAL8c9xoHdfs0gi0FVh+etOJHyz9Y9Y7O++VP01u
>
X3+6m1deM/y2DvAQ4fXl9VWl9A4zsDzq4liAXa3pTl34+MrnF9/PArzt/hj3NO2TXrfvsou++5vb
>
qZS4fZUnAdEJWi69IAC1SOaixUC5ALSXCd3P61GTUIOcjTjk0ol/ha3wQw50ixM5PqH8hyobTUAv
>
xECJ0gWus6gkVrDgJ1Ah6GKcS285nbBpQIZzfss56Faowc0oyQtQFNSrqL23xS7XU9BZQNbO8Nil
>
VnvNyYn0bNaO63a1BGMwf1ygfsjKnYr4+SKYkh64IgTH/oO3xJQvbejvNBBgoJO+OJRtvxsNehdj
>
t/eR9QfsQ3s4bPfHHzHZIBIL/n+98EF/mV2vvuD+iU5yZusSZbb54t9iSzz3L+itq8X0Eg+Apiu2
>
Jt1z4i+IwJNZwO++XELDpzzrsDe9Xb4usaXPL8NAljrzYWRAPTpfX+Id8WLkkThdrldNv8IgENrl
>
br877rZ73f92LerSq26/07s4ca13g8Hf2I/4zjpvj0ZWzTrt9tzRjyk72f31crG/vIHu7NMlU0D5
>
/QqQdiTwuppN1nj1mLwjao6X189WPrTbIjs9KFB4D8fkxgs++XgtPdBx7P7lLzIf0QrotyRyCc2e
>
UgAhfjyjowztv/ExMJqBbjZBumBuGkFFlRZyySfQ1RSVNroELeCZha69ib9PNfdxFrx3q4D2T6yE
>
w/WauBZTLs8CkfGIUNIZJI9H4/ZwjJaAwak1HrquvJuagJaQW+5w3EUWStZD1MwiYRpxpHVrVZ6x
>
yeRtaKXn3/u3zIFPncsrVnq5fwOctI9CVY8D7jSW+3QrL2xOlvtOq9Xa1wvQy2ppjInFjyk7E44F
>
fhAvuT5++ejTZPznGngSpzYo9rDfQY8CnB00CiWZivPJ8nCWfnjzEj+8ZHNv8tn75P8sk1b9OQjB
>
yjB6v7rGGKJg6Hf7Z2zwbuQOf22Pu4M+c391++OKrPQ/o7MOwa416qwz6I+g8zghquXmYe2AYXwd
>
MnoFXozftuxKFYvDfml541/9bymzditauxmpXerNvCscuXTi6ZtO92kPRhfHV2cl4QGtsnZfPQbe
>
3XRSYfZDTe03Dq9sv2mzUwGQMmltB64QojIuxMJ42nkRZL1tkY2BVAPjtBw2Or3oq4E5OGxEB6Z2
>
GB2ZQv2dBtsNzfW2vY0ALIRs4K3m1ny2LDIu141tMTWhbcVDRQh63fpW9ilMTVhYiyDob4sgh1Ma
>
rWFJWzyWQBe5A82yzELagzZuhWu+ZNVqtVIarm99UDj73V7pg7fAOAj4xvqgiJbG0zvUVJ169aCJ
>
eZNn6PxWJje2Y2ZXbfs1o5VEfqH7Po55+UqW7I90AWbn/GUOCl95K8/izjprIOk+zmqLzOYF+MGp
>
FZN92UCzBAq8iQiUVq2wQEkDD/Qr1OliMnQD1Nwcl9VObv47qtoHG9nPUewHxbO5L7NzeXkRuNfb
>
xxQExRmwUS80FgmQcqKH//AwYVoYCqDYLCbaU6DpyeE4jbAedNBq1CKzo15zCs+OCGA6wi7QzYNi
>
oiAFWhE0MRl98eE4LLaEpYErgGgR5IotXyaI3HJEVcotNJrVhl1gzcLimUJDo80lhFbxD9hp97f+
>
xXuTt+tR3q5HtwjFJf96NS2qTDoFlckskJsRxrMz+I+OjfLjWHMOCuEYgZIfLem4UAS1y61QMyBl
>
s0kjxiYHhdkEgd7OPsFG2uK3rXLLVP5Oto4KdzIRnu6qfdAKS/sjpx6dEc2j4rqQAZofyBbopVdM
>
hCaByi2tYpVzS61Gs1rfrGofKrEF5WtHmXIr3hEuvxCJWIe6fWv8izsYfmTlkTu2Trqnp+7Q7Xdc
>
/rrrjqgjeXpiV2uHBeQvFq+UagcH9VItgdAn7uloPHj3VzYa5961VA/qRTYtULxSGo2Tgb9vd4YD
>
tCCddXqDTl4UAECjEA3sRqUkgWQh8t59/9xocBBZSJyMB6PnxkLAyEKjUxiNImyBxSulThYa41/e
>
M5geljscDoZWfzA4D+FSLh9DITLwD/q6oPaOKB8P3Q/D7thlnZOhhXITJthTEjGMXHon+uNfrIvz
>
k/bYtfAjYjLO6Eof1jOzF3hMdTFuv+u5UPWiP3aH5+3hmHVPcxQafeyfm8VO239zreFF37VOAe3x
>
x3PXAoGE45pEtzDiWdSrOQnUc5qp1DuolJKokik5T7oj7F8RSdkqJilbICkP7aOsWdHtj+u1Z52a
>
BCELhX577NjPOi0JQqacbP/2d8CTbtJ9VmGp4WSi0+1vgU5xuhhwcqKz5zwvfUxImwYMRvWNYz//
>
gAk4OdCxnO+FEIeUhRII3UKzqjgqBGEDVb7HjNrEvr/vYYnfnxUNASMZjYs+w0xiMVqEl8nIKmn8
>
ImLNrGG7f+Za5yml+oNxyi+j7lnfPbHefRyn144urCnr75scZd51++3hR2svR1H3t/NxHtVABNvl
>
KHpBsK10HQF9ZdrDqIaQT4+A3z60hydW55d2l86FQ5S1xM9mjffuuJ2RTS5BR3lj7Vl996w97v7q
>
WrblJJVpj0aDTheLdMcfrcFpmNZKSxy8fw8UEqVqOcullTod9E64UjOyQIlJLHPR73ZEG7b5O9Hz
>
fOiOOsPueQJLpipijaodN87Vq04t2aJvV49gcyjnWupk/H3v3a/12u/RufhcPBDvfW9w5v42JhBP
>
QiZQTYst/hgULqiQruZLOlofBsO/jTIkl2gpRbKky7VfuifuM4k8ifufTyL+10W793SSM+fWK798
>
5az7RwtiUVfMo3cA9mSUKXaJrP+uYleQAWZTfwxtJRUZds9+GVucIj3yYyL6fqMUN+VYqnCqVxtx
>
fQpkeCNNONUBaulH8bDTdrfnnjD1nVwUj08GHXbtTW/XC5+xtLJx0dZxh+Pu6Udhh0VX7vyHy/Xq
>
QdwocFBtOGY/Wqofh4dVx3mqjjyhqx53yfuj/an/bI/2OgRqLibTpb988iAgPIDIHf9D/v8Hdn3n
>
//9dnlj8T9PZxf/8P3qS5v9TBwFtmP+NWiz+p3lYd3bz/3s8u/ifXfzPLv5nF/+zi//Zxf+E4n9E
>
bXexAPjAHVFfH73HPEbhgrklQLoEMxISXE77JaDK9RRmA/ZhG0pQTDK560BvNnkfFdr1ohNRscOQ
>
w++0eVd6WIG+OEmn+hlW0t3+fffsnt2ze3bP7tk9u2f37J7ds3t2z+7ZPbtn9+ye3bN7ds/u2T27
> Z/fsnt2ze3bP7vl3ev4P8aQhWQAYAQA=
>
>
> >
> > Might it help if I try to get an account on Warren Hunt's ia64
machine at UT?
> > Specifically, is the ACL2 built there equivalent somehow to the one
you're
> > using?
>
> The Debian machine has a chroot running the unstable version of the
> distribution, having most notably the latest libc, which will be
> required for the presently compiled image. I would have to rebuild on
> hankypanky if you would like to investigate at ut. Please let me
> know.
>
> Take care,
>
> >
> > Thanks --
> > -- Matt
> > Cc: address@hidden, address@hidden, address@hidden,
> > address@hidden, address@hidden
> > From: Camm Maguire <address@hidden>
> > Date: 28 Oct 2004 13:06:44 -0400
> > User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > Content-Type: text/plain; charset=us-ascii
> > X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> > X-UTCS-Spam-Status: No, hits=-232 required=180
> >
> > Greetings, and thanks as always!
> >
> > Matt Kaufmann <address@hidden> writes:
> >
> > > Howdy --
> > >
> > > The second error is a consequence of the first. But the first
is completely
> > > surprising. Are you using the copy of workshops/1999/simulator/
derived from
> > >
/stage/ftp/pub/moore/acl2/v2-9/acl2-sources/books/workshops.tar.gz?
> > >
> > > If so, then I'm at a loss. A first step would be for you to
submit the
> > > following to the shell and send me the log. It might also be
interesting for
> > > you to execute (expt 2 32) after starting up ACL2, and also in
GCL, and verify
> >
> > ^^^^^^^^^^^
> >
> > This works.
> >
> > > the results.
> > >
> > > cd /home/camm/acl2-2.9/books/workshops/1999/simulator/
> > > acl2
> > > (rebuild "tiny.lisp" 'plus<32>-works)
> > > :u
> > > (defthm plus<32>-works
> > > (implies
> > > (and
> > > (signed-byte-p 32 a)
> > > (signed-byte-p 32 b))
> > > (equal
> > > (plus<32> a b)
> > > (+bv32 a b)))
> > > :hints (("goal" :use ((:instance logext-+-logext (size 32) (i
(+ a b)) (j (- (expt 2 32))))
> > > (:instance logext-+-logext (size 32) (i (+ a
b)) (j (expt 2 32))))
> > > :in-theory (set-difference-theories (enable signed-byte-p)
'(logext-+-logext)))))
> > >
> >
> > Here is the output on ia64:
> >
=============================================================================
> > GCL (GNU Common Lisp) 2.6.5 CLtL1 Sep 3 2004 20:49:20
> > Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> > Binary License: GPL due to GPL'ed components: (READLINE UNEXEC)
> > Modifications of this banner must retain notice of a compatible
license
> > Dedicated to the memory of W. Schelter
> >
> > Use (help) to get some basic information on how to use GCL.
> >
> > ACL2 Version 2.9 built October 22, 2004 20:52:30.
> > Copyright (C) 2004 University of Texas at Austin
> > ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software
and you
> > are welcome to redistribute it under certain conditions. For
details,
> > see the GNU General Public License.
> >
> > Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK
*ACL2-PASS-2-FILES*
> > /usr/share/acl2-2.9/).
> > See the documentation topic note-2-9 for recent changes.
> >
> > NOTE!! Proof trees are disabled in ACL2. To enable them in
emacs,
> > look under the ACL2 source directory in
interface/emacs/README.doc;
> > and, to turn on proof trees, execute :START-PROOF-TREE in the
ACL2
> > command loop. Look in the ACL2 documentation under PROOF-TREE.
> >
> > ACL2 Version 2.9. Level 1. Cbd
> > "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
> > Type :help for help.
> > Type (good-bye) to quit completely out of ACL2.
> >
> > ACL2 !>(rebuild "tiny.lisp" 'plus<32>-works)
> >
> > ACL2 loading "tiny.lisp".
> > "ACL2"
> > [SGC for 243 CONS pages..(5727 writable)..(T=93).GC finished]
> > [SGC for 243 CONS pages..(5729 writable)..(T=90).GC finished]
> > Loading /home/camm/acl2-2.9/books/arithmetic/equalities.o
> > start address (dynamic) 0x20000000007d0e50 Finished loading
/home/camm/acl2-2.9/books/arithmetic/equalities.o
> > Loading /home/camm/acl2-2.9/books/arithmetic/rational-listp.o
> > start address (dynamic) 0x20000000007d0ea0 Finished loading
/home/camm/acl2-2.9/books/arithmetic/rational-listp.o
> > [SGC for 191 SFUN pages..(6712 writable)..(T=266).GC finished]
> > Loading /home/camm/acl2-2.9/books/arithmetic/inequalities.o
> > start address (dynamic) 0x20000000007d0ef0 Finished loading
/home/camm/acl2-2.9/books/arithmetic/inequalities.o
> > Loading /home/camm/acl2-2.9/books/arithmetic/natp-posp.o
> > start address (dynamic) 0x20000000007d0f40 Finished loading
/home/camm/acl2-2.9/books/arithmetic/natp-posp.o
> > Loading /home/camm/acl2-2.9/books/arithmetic/rationals.o
> > start address (dynamic) 0x20000000007d0f90 Finished loading
/home/camm/acl2-2.9/books/arithmetic/rationals.o
> > Loading /home/camm/acl2-2.9/books/arithmetic/top.o
> > start address (dynamic) 0x20000000007d0fe0 Finished loading
/home/camm/acl2-2.9/books/arithmetic/top.o
> > "/home/camm/acl2-2.9/books/arithmetic/top.lisp"
> > Loading /home/camm/acl2-2.9/books/data-structures/list-defuns.o
> > start address (dynamic) 0x20000000007d1250 Finished loading
/home/camm/acl2-2.9/books/data-structures/list-defuns.o
> > [SGC for 191 SFUN pages..(6754 writable)..(T=285).GC finished]
> > Loading /home/camm/acl2-2.9/books/data-structures/list-defthms.o
> > start address (dynamic) 0x20000000007d12a0 Finished loading
/home/camm/acl2-2.9/books/data-structures/list-defthms.o
> > "/home/camm/acl2-2.9/books/data-structures/list-defthms.lisp"
> > Loading /home/camm/acl2-2.9/books/meta/term-defuns.o
> > start address (dynamic) 0x20000000007d1430 Finished loading
/home/camm/acl2-2.9/books/meta/term-defuns.o
> > Loading /home/camm/acl2-2.9/books/meta/meta-plus-equal.o
> > start address (dynamic) 0x20000000007d1540 Finished loading
/home/camm/acl2-2.9/books/meta/meta-plus-equal.o
> > [SGC for 1114 CONS pages..(6945 writable)..(T=317).GC finished]
> > Loading /home/camm/acl2-2.9/books/meta/meta-plus-lessp.o
> > start address (dynamic) 0x20000000007d1650 Finished loading
/home/camm/acl2-2.9/books/meta/meta-plus-lessp.o
> > Loading /home/camm/acl2-2.9/books/meta/meta-times-equal.o
> > start address (dynamic) 0x20000000007d1790 Finished loading
/home/camm/acl2-2.9/books/meta/meta-times-equal.o
> > Loading /home/camm/acl2-2.9/books/meta/meta.o
> > start address (dynamic) 0x20000000007d17e0 Finished loading
/home/camm/acl2-2.9/books/meta/meta.o
> > "/home/camm/acl2-2.9/books/meta/meta.lisp"
> > [SGC for 26 FIXNUM pages..(6946 writable)..(T=328).GC finished]
> > Loading /home/camm/acl2-2.9/books/data-structures/utilities.o
> > start address (dynamic) 0x20000000007d1ef0 Finished loading
/home/camm/acl2-2.9/books/data-structures/utilities.o
> > Loading /home/camm/acl2-2.9/books/ihs/ihs-init.o
> > start address (dynamic) 0x20000000007d2160 Finished loading
/home/camm/acl2-2.9/books/ihs/ihs-init.o
> > Loading /home/camm/acl2-2.9/books/ihs/ihs-theories.o
> > start address (dynamic) 0x20000000007d21b0 Finished loading
/home/camm/acl2-2.9/books/ihs/ihs-theories.o
> > [SGC for 26 FIXNUM pages..(6947 writable)..(T=337).GC finished]
> > Loading /home/camm/acl2-2.9/books/ihs/logops-definitions.o
> > start address (dynamic) 0x20000000007d2980 Finished loading
/home/camm/acl2-2.9/books/ihs/logops-definitions.o
> > [SGC for 2069 CONS pages..(8135 writable)..(T=576).GC finished]
> > Loading /home/camm/acl2-2.9/books/ihs/logops-lemmas.o
> > start address (dynamic) 0x20000000007d2a90 Finished loading
/home/camm/acl2-2.9/books/ihs/logops-lemmas.o
> > "/home/camm/acl2-2.9/books/ihs/logops-lemmas.lisp"
> > NIL
> > 2663
> > 2
> > ST
> > PROGCLOC
> > MEMLOC
> > DTOSLOC
> > CTOSLOC
> >
> > ACL2 Warning [Non-rec] in ( DEFTHM THE-ERROR-NOOP ...): The
:REWRITE
> > rule generated from THE-ERROR-NOOP will be triggered only by terms
> > containing the non-recursive function symbol THE-ERROR. Unless
this
> > function is disabled, THE-ERROR-NOOP is unlikely ever to be used.
> >
> >
> > ACL2 Warning [Subsume] in ( DEFTHM THE-ERROR-NOOP ...): The newly
> > proposed :REWRITE rule THE-ERROR-NOOP probably subsumes the
previously
> > added :REWRITE rule THE-ERROR, in the sense that THE-ERROR-NOOP
will
> > now probably be applied whenever the old rule would have been.
> >
> >
> > ACL2 Warning [Subsume] in ( DEFTHM THE-ERROR-NOOP ...): The
previously
> > added rule THE-ERROR subsumes the newly proposed :REWRITE rule THE-
> > ERROR-NOOP, in the sense that the old rule rewrites a more general
> > target. Because the new rule will be tried first, it may
nonetheless
> > find application.
> >
> > THE-ERROR-NOOP
> >
> > ACL2 Warning [Subsume] in ( DEFTHM NTH-UPDATE-NTH-CONST ...): The
> > previously added rule NTH-UPDATE-NTH subsumes the newly proposed
:REWRITE
> > rule NTH-UPDATE-NTH-CONST, in the sense that the old rule rewrites
> > a more general target. Because the new rule will be tried first,
it
> > may nonetheless find application.
> >
> > NTH-UPDATE-NTH-CONST
> > 2708
> > INT32
> > NAT10
> > MAX_INT<32>
> > MIN_INT<32>
> > MIN_INT<32>+1
> > MAX_NAT<10>
> > MAX_NAT-1<10>
> > FIX10
> > MAX<32>
> > |+<32>|
> > PLUS<32>
> > |+BV32|
> >
> > ACL2 Warning [Non-rec] in ( DEFTHM PLUS<32>-WORKS ...): The
:REWRITE
> > rule generated from PLUS<32>-WORKS will be triggered only by terms
> > containing the non-recursive function symbol PLUS<32>. Unless this
> > function is disabled, PLUS<32>-WORKS is unlikely ever to be used.
> >
> > PLUS<32>-WORKS
> >
> > Finished loading "tiny.lisp".
> > T
> > ACL2 !>:u
> >
> > V 26:x(DEFUN |+BV32| (X Y) ...)
> > ACL2 !>(defthm plus<32>-works
> > (implies
> > (and
> > (signed-byte-p 32 a)
> > (signed-byte-p 32 b))
> > (equal
> > (plus<32> a b)
> > (+bv32 a b)))
> > :hints (("goal" :use ((:instance logext-+-logext (size 32) (i (+
a b)) (j (- (expt 2 32))))
> > (:instance logext-+-logext (size 32) (i (+ a
b)) (j (expt 2 32))))
> > :in-theory (set-difference-theories (enable
signed-byte-p) '(logext-+-logext)))))
> >
> > ACL2 Warning [Non-rec] in ( DEFTHM PLUS<32>-WORKS ...): The
:REWRITE
> > rule generated from PLUS<32>-WORKS will be triggered only by terms
> > containing the non-recursive function symbol PLUS<32>. Unless this
> > function is disabled, PLUS<32>-WORKS is unlikely ever to be used.
> >
> >
> > [Note: A hint was supplied for our processing of the goal above.
> > Thanks!]
> >
> > We now augment the goal above by adding the hypotheses indicated by
> > the :USE hint. These hypotheses can be derived from
LOGEXT-+-LOGEXT
> > via instantiation. The augmented goal is shown below.
> >
> > Goal'
> > (IMPLIES
> > (AND (IMPLIES (AND (INTEGERP (+ A B))
> > (INTEGERP (- (EXPT 2 32))))
> > (EQUAL (LOGEXT 32
> > (+ (+ A B) (LOGEXT 32 (- (EXPT 2
32)))))
> > (LOGEXT 32 (+ (+ A B) (- (EXPT 2 32))))))
> > (IMPLIES (AND (INTEGERP (+ A B))
> > (INTEGERP (EXPT 2 32)))
> > (EQUAL (LOGEXT 32 (+ (+ A B) (LOGEXT 32 (EXPT 2
32))))
> > (LOGEXT 32 (+ (+ A B) (EXPT 2 32))))))
> > (IMPLIES (AND (SIGNED-BYTE-P 32 A)
> > (SIGNED-BYTE-P 32 B))
> > (EQUAL (PLUS<32> A B) (|+BV32| A B)))).
> >
> > By the simple :definitions |+BV32|, INTEGER-RANGE-P and
SIGNED-BYTE-
> > P, the :executable-counterparts of EXPT, INTEGERP, LOGEXT and
UNARY-
> > - and the simple :rewrite rule ASSOCIATIVITY-OF-+ we reduce the
conjecture
> > to
> >
> > Goal''
> > (IMPLIES (AND (IMPLIES (INTEGERP (+ A B))
> > (EQUAL (LOGEXT 32 (+ A B 0))
> > (LOGEXT 32 (+ A B -4294967296))))
> > (IMPLIES (INTEGERP (+ A B))
> > (EQUAL (LOGEXT 32 (+ A B 0))
> > (LOGEXT 32 (+ A B 4294967296))))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648))
> > (EQUAL (PLUS<32> A B)
> > (LOGEXT 32 (+ A B)))).
> >
> > This simplifies, using the :definitions FIX, INTEGER-RANGE-P,
PLUS<32>,
> > SIGNED-BYTE-P and SYNP, the :executable-counterparts of <,
BINARY-+,
> > EXPT, INTEGERP and UNARY--, linear arithmetic, primitive type
reasoning
> > and the :rewrite rules <-+-NEGATIVE-0-1, COMMUTATIVITY-2-OF-+,
COMMUTATIVITY-
> > OF-+, FOLD-CONSTS-IN-+, LOGEXT-IDENTITY and UNICITY-OF-0, to the
following
> > six conjectures.
> >
> > Subgoal 6
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B))
> > (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (< (+ A B) 2147483648))
> > (EQUAL (+ A B) (LOGEXT 32 (+ A B)))).
> >
> > But simplification reduces this to T, using the :definitions
INTEGER-
> > RANGE-P and SIGNED-BYTE-P, the :executable-counterparts of <,
BINARY-
> > +, EQUAL, EXPT, FIX, INTEGERP and UNARY--, linear arithmetic,
primitive
> > type reasoning, the :linear rule LOGEXT-BOUNDS, the :meta rule
CANCEL_-
> > PLUS-EQUAL-CORRECT and the :rewrite rule LOGEXT-IDENTITY.
> >
> > Subgoal 5
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B))
> > (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B)
> > (<= 2147483648 (+ A B)))
> > (EQUAL (+ -18446744073709551616 A B)
> > (LOGEXT 32 (+ A B)))).
> >
> > We now use the first hypothesis by substituting (+ -4294967296 A B)
> > for (LOGEXT 32 (+ A B)) and hiding the hypothesis. This produces
> >
> > Subgoal 5'
> > (IMPLIES (AND (HIDE (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B)))
> > (EQUAL (+ -4294967296 A B)
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B)
> > (<= 2147483648 (+ A B)))
> > (EQUAL (+ -18446744073709551616 A B)
> > (+ -4294967296 A B))).
> >
> > By the :executable-counterparts of EQUAL and FIX and the simple
:rewrite
> > rule RIGHT-CANCELLATION-FOR-+ we reduce the conjecture to
> >
> > Subgoal 5''
> > (IMPLIES (AND (HIDE (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B)))
> > (EQUAL (+ -4294967296 A B)
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > We remove HIDE from the first hypothesis, which was used
heuristically
> > to transform Subgoal 5 by substituting into the rest of that goal.
> > This produces
> >
> > Subgoal 5'''
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B))
> > (EQUAL (+ -4294967296 A B)
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > This simplifies, using primitive type reasoning, to
> >
> > Subgoal 5'4'
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B))
> > (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > We now use the second hypothesis by substituting
> > (LOGEXT 32 (+ 4294967296 A B)) for (LOGEXT 32 (+ A B)) and hiding
the
> > hypothesis. This produces
> >
> > Subgoal 5'5'
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ 4294967296 A B))
> > (+ -4294967296 A B))
> > (HIDE (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B))))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > We remove HIDE from the second hypothesis, which was used
heuristically
> > to transform Subgoal 5'4' by substituting into the rest of that
goal.
> > This produces
> >
> > Subgoal 5'6'
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ 4294967296 A B))
> > (+ -4294967296 A B))
> > (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > This simplifies, using linear arithmetic, primitive type reasoning
> > and the :type-prescription rule LOGEXT-TYPE, to
> >
> > Subgoal 5'7'
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 B A))
> > (EQUAL (LOGEXT 32 (+ 4294967296 A B))
> > (+ -4294967296 A B))
> > (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > This simplifies, using primitive type reasoning and the :rewrite
rule
> > COMMUTATIVITY-OF-+, to
> >
> > Subgoal 5'8'
> > (IMPLIES (AND (EQUAL (LOGEXT 32 (+ A B))
> > (+ -4294967296 A B))
> > (EQUAL (LOGEXT 32 (+ A B))
> > (LOGEXT 32 (+ 4294967296 A B)))
> > (INTEGERP A)
> > (<= -2147483648 A)
> > (< A 2147483648)
> > (INTEGERP B)
> > (<= -2147483648 B)
> > (< B 2147483648)
> > (<= 0 A)
> > (<= 0 B))
> > (< (+ A B) 2147483648)).
> >
> > Normally we would attempt to prove this formula by induction.
However,
> > we prefer in this instance to focus on the original input
conjecture
> > rather than this simplified special case. We therefore abandon our
> > previous work on this conjecture and reassign the name *1 to the
original
> > conjecture. (See :DOC otf-flg.) [Note: Thanks again for the
hint.]
> >
> > No induction schemes are suggested by *1. Consequently, the proof
> > attempt has failed.
> >
> > Summary
> > Form: ( DEFTHM PLUS<32>-WORKS ...)
> > Rules: ((:DEFINITION |+BV32|)
> > (:DEFINITION FIX)
> > (:DEFINITION HIDE)
> > (:DEFINITION INTEGER-RANGE-P)
> > (:DEFINITION NOT)
> > (:DEFINITION PLUS<32>)
> > (:DEFINITION SIGNED-BYTE-P)
> > (:DEFINITION SYNP)
> > (:EXECUTABLE-COUNTERPART <)
> > (:EXECUTABLE-COUNTERPART BINARY-+)
> > (:EXECUTABLE-COUNTERPART EQUAL)
> > (:EXECUTABLE-COUNTERPART EXPT)
> > (:EXECUTABLE-COUNTERPART FIX)
> > (:EXECUTABLE-COUNTERPART INTEGERP)
> > (:EXECUTABLE-COUNTERPART LOGEXT)
> > (:EXECUTABLE-COUNTERPART UNARY--)
> > (:FAKE-RUNE-FOR-LINEAR NIL)
> > (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > (:LINEAR LOGEXT-BOUNDS)
> > (:META CANCEL_PLUS-EQUAL-CORRECT)
> > (:REWRITE <-+-NEGATIVE-0-1)
> > (:REWRITE ASSOCIATIVITY-OF-+)
> > (:REWRITE COMMUTATIVITY-2-OF-+)
> > (:REWRITE COMMUTATIVITY-OF-+)
> > (:REWRITE FOLD-CONSTS-IN-+)
> > (:REWRITE LOGEXT-IDENTITY)
> > (:REWRITE RIGHT-CANCELLATION-FOR-+)
> > (:REWRITE UNICITY-OF-0)
> > (:TYPE-PRESCRIPTION LOGEXT-TYPE))
> > Warnings: Non-rec
> > Time: 3.99 seconds (prove: 3.19, print: 0.45, other: 0.35)
> >
> > ******** FAILED ******** See :DOC failure ******** FAILED
********
> > ACL2 !>
> >
=============================================================================
> >
> > > Thanks --
> > > -- Matt
> > > Cc: address@hidden, address@hidden, address@hidden,
> > > address@hidden, address@hidden
> > > From: Camm Maguire <address@hidden>
> > > Date: 28 Oct 2004 10:27:09 -0400
> > > User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
> > > Content-Type: text/plain; charset=us-ascii
> > > X-SpamAssassin-Status: No, hits=-2.6 required=5.0
> > > X-UTCS-Spam-Status: No, hits=-232 required=180
> > >
> > > Greetings!
> > >
> > > Matt Kaufmann <address@hidden> writes:
> > >
> > > > > I'm hoping that the make will bomb and exit with an error
code if one
> > > > > of the certification steps fails.
> > > >
> > > > Hmmm, that's a good point and I don't think we do that.
Rather, we print ** to
> > > > the log file. I've made a note to improve this before the
next release (time
> > > > permitting) to return a non-zero error code.
> > > >
> > >
> > > OK, thank you for clarifying. Then we have two issues on
ia64, with
> > > which I hope to seek your help, as I cannot yet make sense of
the
> > > output:
> > >
> > >
=============================================================================
> > > workshops/1999/simulator/tiny.out
> > >
=============================================================================
> > > GCL (GNU Common Lisp) 2.6.5 CLtL1 Sep 3 2004 20:49:20
> > > Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> > > Binary License: GPL due to GPL'ed components: (READLINE
UNEXEC)
> > > Modifications of this banner must retain notice of a
compatible license
> > > Dedicated to the memory of W. Schelter
> > >
> > > Use (help) to get some basic information on how to use GCL.
> > >
> > > ACL2 Version 2.9 built October 22, 2004 20:52:30.
> > > Copyright (C) 2004 University of Texas at Austin
> > > ACL2 comes with ABSOLUTELY NO WARRANTY. This is free
software and you
> > > are welcome to redistribute it under certain conditions.
For details,
> > > see the GNU General Public License.
> > >
> > > Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK
*ACL2-PASS-2-FILES*
> > > /usr/share/acl2-2.9/).
> > > See the documentation topic note-2-9 for recent changes.
> > >
> > > NOTE!! Proof trees are disabled in ACL2. To enable them in
emacs,
> > > look under the ACL2 source directory in
interface/emacs/README.doc;
> > > and, to turn on proof trees, execute :START-PROOF-TREE in
the ACL2
> > > command loop. Look in the ACL2 documentation under
PROOF-TREE.
> > >
> > > ACL2 Version 2.9. Level 1. Cbd
> > > "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
> > > Type :help for help.
> > > Type (good-bye) to quit completely out of ACL2.
> > >
> > > ACL2 !>
> > > Exiting the ACL2 read-eval-print loop. To re-enter, execute
(LP).
> > > ACL2>
> > > #<"ACL2" package>
> > >
> > > ACL2>
> > > ACL2 Version 2.9. Level 1. Cbd
> > > "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
> > > Type :help for help.
> > > Type (good-bye) to quit completely out of ACL2.
> > >
> > > ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
> > > ACL2 !>[SGC for 243 CONS pages..(5726 writable)..(T=90).GC
finished]
> > > [SGC for 243 CONS pages..(5729 writable)..(T=95).GC finished]
> > >
> > > Loading /home/camm/acl2-2.9/books/arithmetic/equalities.o
> > > start address (dynamic) 0x20000000007d0e50 Finished loading
/home/camm/acl2-2.9/books/arithmetic/equalities.o
> > > Loading /home/camm/acl2-2.9/books/arithmetic/rational-listp.o
> > > start address (dynamic) 0x20000000007d0ea0 Finished loading
/home/camm/acl2-2.9/books/arithmetic/rational-listp.o
> > > [SGC for 191 SFUN pages..(6749 writable)..(T=275).GC finished]
> > > Loading /home/camm/acl2-2.9/books/arithmetic/inequalities.o
> > > start address (dynamic) 0x20000000007d0ef0 Finished loading
/home/camm/acl2-2.9/books/arithmetic/inequalities.o
> > > Loading /home/camm/acl2-2.9/books/arithmetic/natp-posp.o
> > > start address (dynamic) 0x20000000007d0f40 Finished loading
/home/camm/acl2-2.9/books/arithmetic/natp-posp.o
> > > Loading /home/camm/acl2-2.9/books/arithmetic/rationals.o
> > > start address (dynamic) 0x20000000007d0f90 Finished loading
/home/camm/acl2-2.9/books/arithmetic/rationals.o
> > > Loading /home/camm/acl2-2.9/books/arithmetic/top.o
> > > start address (dynamic) 0x20000000007d0fe0 Finished loading
/home/camm/acl2-2.9/books/arithmetic/top.o
> > >
> > > Summary
> > > Form: ( INCLUDE-BOOK "../../../arithmetic/top" ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 13.65 seconds (prove: 0.00, print: 0.00, other: 13.65)
> > > "/home/camm/acl2-2.9/books/arithmetic/top.lisp"
> > > Loading
/home/camm/acl2-2.9/books/data-structures/list-defuns.o
> > > start address (dynamic) 0x20000000007d1250 Finished loading
/home/camm/acl2-2.9/books/data-structures/list-defuns.o
> > > [SGC for 191 SFUN pages..(6791 writable)..(T=292).GC finished]
> > > Loading
/home/camm/acl2-2.9/books/data-structures/list-defthms.o
> > > start address (dynamic) 0x20000000007d12a0 Finished loading
/home/camm/acl2-2.9/books/data-structures/list-defthms.o
> > >
> > > Summary
> > > Form: ( INCLUDE-BOOK "../../../data-structures/list-defthms"
...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 8.06 seconds (prove: 0.00, print: 0.01, other: 8.05)
> > > "/home/camm/acl2-2.9/books/data-structures/list-defthms.lisp"
> > > Loading /home/camm/acl2-2.9/books/meta/term-defuns.o
> > > start address (dynamic) 0x20000000007d1430 Finished loading
/home/camm/acl2-2.9/books/meta/term-defuns.o
> > > Loading /home/camm/acl2-2.9/books/meta/meta-plus-equal.o
> > > start address (dynamic) 0x20000000007d1540 Finished loading
/home/camm/acl2-2.9/books/meta/meta-plus-equal.o
> > > [SGC for 1114 CONS pages..(6942 writable)..(T=321).GC
finished]
> > > Loading /home/camm/acl2-2.9/books/meta/meta-plus-lessp.o
> > > start address (dynamic) 0x20000000007d1650 Finished loading
/home/camm/acl2-2.9/books/meta/meta-plus-lessp.o
> > > Loading /home/camm/acl2-2.9/books/meta/meta-times-equal.o
> > > start address (dynamic) 0x20000000007d1790 Finished loading
/home/camm/acl2-2.9/books/meta/meta-times-equal.o
> > > Loading /home/camm/acl2-2.9/books/meta/meta.o
> > > start address (dynamic) 0x20000000007d17e0 Finished loading
/home/camm/acl2-2.9/books/meta/meta.o
> > >
> > > Summary
> > > Form: ( INCLUDE-BOOK "../../../meta/meta" ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 5.40 seconds (prove: 0.00, print: 0.00, other: 5.40)
> > > "/home/camm/acl2-2.9/books/meta/meta.lisp"
> > > [SGC for 26 FIXNUM pages..(6943 writable)..(T=330).GC
finished]
> > > Loading /home/camm/acl2-2.9/books/data-structures/utilities.o
> > > start address (dynamic) 0x20000000007d1ef0 Finished loading
/home/camm/acl2-2.9/books/data-structures/utilities.o
> > > Loading /home/camm/acl2-2.9/books/ihs/ihs-init.o
> > > start address (dynamic) 0x20000000007d2160 Finished loading
/home/camm/acl2-2.9/books/ihs/ihs-init.o
> > > Loading /home/camm/acl2-2.9/books/ihs/ihs-theories.o
> > > start address (dynamic) 0x20000000007d21b0 Finished loading
/home/camm/acl2-2.9/books/ihs/ihs-theories.o
> > > [SGC for 26 FIXNUM pages..(6944 writable)..(T=336).GC
finished]
> > > Loading /home/camm/acl2-2.9/books/ihs/logops-definitions.o
> > > start address (dynamic) 0x20000000007d2980 Finished loading
/home/camm/acl2-2.9/books/ihs/logops-definitions.o
> > > [SGC for 2069 CONS pages..(8133 writable)..(T=582).GC
finished]
> > > Loading /home/camm/acl2-2.9/books/ihs/logops-lemmas.o
> > > start address (dynamic) 0x20000000007d2a90 Finished loading
/home/camm/acl2-2.9/books/ihs/logops-lemmas.o
> > >
> > > Summary
> > > Form: ( INCLUDE-BOOK "../../../ihs/logops-lemmas" ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 45.35 seconds (prove: 0.00, print: 0.07, other: 45.28)
> > > "/home/camm/acl2-2.9/books/ihs/logops-lemmas.lisp"
> > > NIL
> > >
> > > Summary
> > > Form: (IN-THEORY (SET-DIFFERENCE-THEORIES ...))
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.27 seconds (prove: 0.00, print: 0.00, other: 0.27)
> > > 2663
> > > 2
> > >
> > > Summary
> > > Form: ( DEFSTOBJ ST ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 1.63 seconds (prove: 0.00, print: 0.00, other: 1.63)
> > > ST
> > >
> > > Summary
> > > Form: ( DEFMACRO PROGCLOC ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > PROGCLOC
> > >
> > > Summary
> > > Form: ( DEFMACRO MEMLOC ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > MEMLOC
> > >
> > > Summary
> > > Form: ( DEFMACRO DTOSLOC ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > DTOSLOC
> > >
> > > Summary
> > > Form: ( DEFMACRO CTOSLOC ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
> > > CTOSLOC
> > >
> > > Summary
> > > Form: ( DEFTHM THE-ERROR-NOOP ...)
> > > Rules: ((:DEFINITION THE-ERROR)
> > > (:REWRITE CDR-CONS))
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > THE-ERROR-NOOP
> > >
> > > Summary
> > > Form: ( DEFTHM NTH-UPDATE-NTH-CONST ...)
> > > Rules: ((:DEFINITION NFIX)
> > > (:EXECUTABLE-COUNTERPART IF)
> > > (:EXECUTABLE-COUNTERPART SYNP)
> > > (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > > (:REWRITE NTH-UPDATE-NTH))
> > > Warnings: None
> > > Time: 0.21 seconds (prove: 0.15, print: 0.00, other: 0.06)
> > > NTH-UPDATE-NTH-CONST
> > >
> > > Summary
> > > Form: (IN-THEORY (DISABLE ...))
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.29 seconds (prove: 0.00, print: 0.00, other: 0.29)
> > > 2708
> > >
> > > Summary
> > > Form: ( DEFMACRO INT32 ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > INT32
> > >
> > > Summary
> > > Form: ( DEFMACRO NAT10 ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
> > > NAT10
> > >
> > > Summary
> > > Form: ( DEFMACRO MAX_INT<32> ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > MAX_INT<32>
> > >
> > > Summary
> > > Form: ( DEFMACRO MIN_INT<32> ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
> > > MIN_INT<32>
> > >
> > > Summary
> > > Form: ( DEFMACRO MIN_INT<32>+1 ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > MIN_INT<32>+1
> > >
> > > Summary
> > > Form: ( DEFMACRO MAX_NAT<10> ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > MAX_NAT<10>
> > >
> > > Summary
> > > Form: ( DEFMACRO MAX_NAT-1<10> ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > MAX_NAT-1<10>
> > >
> > > Summary
> > > Form: ( DEFMACRO FIX10 ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > FIX10
> > >
> > > Summary
> > > Form: ( DEFMACRO MAX<32> ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > MAX<32>
> > >
> > > Summary
> > > Form: ( DEFMACRO |+<32>| ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
> > > |+<32>|
> > >
> > > Summary
> > > Form: ( DEFUN PLUS<32> ...)
> > > Rules: ((:DEFINITION FIX)
> > > (:DEFINITION INTEGER-RANGE-P)
> > > (:DEFINITION NOT)
> > > (:DEFINITION SIGNED-BYTE-P)
> > > (:DEFINITION SYNP)
> > > (:EXECUTABLE-COUNTERPART <)
> > > (:EXECUTABLE-COUNTERPART BINARY-+)
> > > (:EXECUTABLE-COUNTERPART EXPT)
> > > (:EXECUTABLE-COUNTERPART INTEGERP)
> > > (:EXECUTABLE-COUNTERPART UNARY--)
> > > (:FAKE-RUNE-FOR-LINEAR NIL)
> > > (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > > (:FORWARD-CHAINING SIGNED-BYTE-P-FORWARD)
> > > (:META CANCEL_PLUS-LESSP-CORRECT)
> > > (:REWRITE <-+-NEGATIVE-0-1)
> > > (:REWRITE ASSOCIATIVITY-OF-+)
> > > (:REWRITE COMMUTATIVITY-2-OF-+)
> > > (:REWRITE COMMUTATIVITY-OF-+)
> > > (:REWRITE FOLD-CONSTS-IN-+)
> > > (:REWRITE UNICITY-OF-0)
> > > (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
> > > Warnings: None
> > > Time: 4.00 seconds (prove: 3.12, print: 0.01, other: 0.87)
> > > PLUS<32>
> > >
> > > Summary
> > > Form: ( DEFUN |+BV32| ...)
> > > Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
> > > (:FORWARD-CHAINING SIGNED-BYTE-P-FORWARD)
> > > (:TYPE-PRESCRIPTION LOGEXT-TYPE)
> > > (:TYPE-PRESCRIPTION SIGNED-BYTE-P))
> > > Warnings: None
> > > Time: 0.13 seconds (prove: 0.00, print: 0.00, other: 0.13)
> > > |+BV32|
> > >
> > > Summary
> > > Form: ( DEFTHM PLUS<32>-WORKS ...)
> > > Rules: ((:DEFINITION |+BV32|)
> > > (:DEFINITION FIX)
> > > (:DEFINITION HIDE)
> > > (:DEFINITION INTEGER-RANGE-P)
> > > (:DEFINITION NOT)
> > > (:DEFINITION PLUS<32>)
> > > (:DEFINITION SIGNED-BYTE-P)
> > > (:DEFINITION SYNP)
> > > (:EXECUTABLE-COUNTERPART <)
> > > (:EXECUTABLE-COUNTERPART BINARY-+)
> > > (:EXECUTABLE-COUNTERPART EQUAL)
> > > (:EXECUTABLE-COUNTERPART EXPT)
> > > (:EXECUTABLE-COUNTERPART FIX)
> > > (:EXECUTABLE-COUNTERPART INTEGERP)
> > > (:EXECUTABLE-COUNTERPART LOGEXT)
> > > (:EXECUTABLE-COUNTERPART UNARY--)
> > > (:FAKE-RUNE-FOR-LINEAR NIL)
> > > (:FAKE-RUNE-FOR-TYPE-SET NIL)
> > > (:LINEAR LOGEXT-BOUNDS)
> > > (:META CANCEL_PLUS-EQUAL-CORRECT)
> > > (:REWRITE <-+-NEGATIVE-0-1)
> > > (:REWRITE ASSOCIATIVITY-OF-+)
> > > (:REWRITE COMMUTATIVITY-2-OF-+)
> > > (:REWRITE COMMUTATIVITY-OF-+)
> > > (:REWRITE FOLD-CONSTS-IN-+)
> > > (:REWRITE LOGEXT-IDENTITY)
> > > (:REWRITE RIGHT-CANCELLATION-FOR-+)
> > > (:REWRITE UNICITY-OF-0)
> > > (:TYPE-PRESCRIPTION LOGEXT-TYPE))
> > > Warnings: None
> > > Time: 3.44 seconds (prove: 3.14, print: 0.00, other: 0.30)
> > >
> > > ******** FAILED ******** See :DOC failure ******** FAILED
********
> > >
> > > Summary
> > > Form: (CERTIFY-BOOK "tiny" ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 83.61 seconds (prove: 6.41, print: 0.09, other: 77.11)
> > >
> > > ******** FAILED ******** See :DOC failure ******** FAILED
********
> > > ACL2 !>
> > > Exiting the ACL2 read-eval-print loop. To re-enter, execute
(LP).
> > >
> > > ACL2>
> > >
=============================================================================
> > > workshops/1999/simulator/exercises.out
> > >
=============================================================================
> > > GCL (GNU Common Lisp) 2.6.5 CLtL1 Sep 3 2004 20:49:20
> > > Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
> > > Binary License: GPL due to GPL'ed components: (READLINE
UNEXEC)
> > > Modifications of this banner must retain notice of a
compatible license
> > > Dedicated to the memory of W. Schelter
> > >
> > > Use (help) to get some basic information on how to use GCL.
> > >
> > > ACL2 Version 2.9 built October 22, 2004 20:52:30.
> > > Copyright (C) 2004 University of Texas at Austin
> > > ACL2 comes with ABSOLUTELY NO WARRANTY. This is free
software and you
> > > are welcome to redistribute it under certain conditions.
For details,
> > > see the GNU General Public License.
> > >
> > > Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK
*ACL2-PASS-2-FILES*
> > > /usr/share/acl2-2.9/).
> > > See the documentation topic note-2-9 for recent changes.
> > >
> > > NOTE!! Proof trees are disabled in ACL2. To enable them in
emacs,
> > > look under the ACL2 source directory in
interface/emacs/README.doc;
> > > and, to turn on proof trees, execute :START-PROOF-TREE in
the ACL2
> > > command loop. Look in the ACL2 documentation under
PROOF-TREE.
> > >
> > > ACL2 Version 2.9. Level 1. Cbd
> > > "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
> > > Type :help for help.
> > > Type (good-bye) to quit completely out of ACL2.
> > >
> > > ACL2 !>
> > > Exiting the ACL2 read-eval-print loop. To re-enter, execute
(LP).
> > > ACL2>
> > > #<"ACL2" package>
> > >
> > > ACL2>
> > > ACL2 Version 2.9. Level 1. Cbd
> > > "/home/camm/acl2-2.9/books/workshops/1999/simulator/".
> > > Type :help for help.
> > > Type (good-bye) to quit completely out of ACL2.
> > >
> > > ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
> > > ACL2 !>
> > >
> > > ACL2 Error in ( INCLUDE-BOOK "tiny" ...): There is no
certificate
> > > on file for
"/home/camm/acl2-2.9/books/workshops/1999/simulator/tiny.lisp".
> > >
> > >
> > > Summary
> > > Form: ( INCLUDE-BOOK "tiny" ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)
> > >
> > > ******** FAILED ******** See :DOC failure ******** FAILED
********
> > >
> > > Summary
> > > Form: (CERTIFY-BOOK "exercises" ...)
> > > Rules: NIL
> > > Warnings: None
> > > Time: 0.11 seconds (prove: 0.00, print: 0.00, other: 0.11)
> > >
> > > ******** FAILED ******** See :DOC failure ******** FAILED
********
> > > ACL2 !>
> > > Exiting the ACL2 read-eval-print loop. To re-enter, execute
(LP).
> > >
> > > ACL2>
> > >
=============================================================================
> > > Take care,
> > > --
> > > Camm Maguire
address@hidden
> > >
==========================================================================
> > > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> > >
> > >
> > >
> >
> > --
> > Camm Maguire
address@hidden
> >
==========================================================================
> > "The earth is but one country, and mankind its citizens." --
Baha'u'llah
> >
> >
> >
>
> --
> Camm Maguire address@hidden
>
==========================================================================
> "The earth is but one country, and mankind its citizens." --
Baha'u'llah
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
- [Gcl-devel] Re: ACL2 binaries, (continued)
- [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/25
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Matt Kaufmann, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/28
- Re: [Gcl-devel] Re: ACL2 binaries,
Matt Kaufmann <=