gcl-devel
[Top][All Lists]
Advanced

[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 13:50:45 -0500

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.

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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]