[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Re: ACL2 binaries
|
From: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] Re: ACL2 binaries |
|
Date: |
28 Oct 2004 14:28:49 -0400 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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
- [Gcl-devel] Re: ACL2 binaries, Camm Maguire, 2004/10/25
- [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 <=
- 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