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: Camm Maguire
Subject: Re: [Gcl-devel] Re: ACL2 binaries
Date: 28 Oct 2004 15:29:24 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!

Matt Kaufmann <address@hidden> writes:

> Howdy --
> 
> Thanks.  OK, I checked and your tiny.lisp is the correct one.  You say:
> 
> >> The Debian machine has a chroot running the unstable version of the
> >> distribution, having most notably the latest libc, which will be
> >> required for the presently compiled image.  I would have to rebuild on
> >> hankypanky if you would like to investigate at ut.  Please let me
> >> know.
> 
> This stuff is a mystery to me, but the bottom line is that it could be useful
> for me to investigate at UT.  I'll ask Warren if I can get an account and will
> CC you.  If so, and if you can build ACL2 there for me and re-create this
> problem, that would be ideal.
> 

OK, am trying.  In the mean time, it might not be a bad wager that the
package is still fit for upload, no?

Take care,

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

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah




reply via email to

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