Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1026


Synopsis:        Latex Errors
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Mar  4 11:55:00 2008
Originator:      Eddy Seager
Organization:    cs.man.ac.uk
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  
  --dDRMvlgZJXvWKvBx
  Content-Type: text/plain; charset=us-ascii
  Content-Disposition: inline
  
  Dear Sam,
  
  I have found some bugs when producing Latex output for my proofs. The 
  first are "Bad math environment delimiter", in log_deriv.tex which was 
  generated from the derivative_log theory. 
  
  The second bug is that pvs won't generate latex for Cos_Integral - I get 
  the error "Error: Attempt to store the wrong type of value in an array" 
  when running M-x latex-proof. I then get the option of scroll, ignore 
  keep, abort or break. This proof uses strategies I wrote in 
  pvs-strategies and I think it is to do with the label commands. When I 
  comment out the labeling I do not get these errors and PVS produces 
  latex fine.
  
  Other info:
  > uname -a                                                 08-03-04 
  11:29:12
  Linux edward-laptop 2.6.20-16-386 #2 Sun Sep 23 19:47:10 UTC 2007 i686 
  GNU/Linux
  
  I am using Pvs 4.1 Allegro CL Enterprise Edition and GNU Emacs 21.4.1.
  
  Regards,
  -- 
  Eddy Seager
  University of Manchester Undergrad
  
  --dDRMvlgZJXvWKvBx
  Content-Type: application/x-gzip
  Content-Disposition: attachment; filename="pvsBugs.tar.gz"
  Content-Transfer-Encoding: base64
  
  H4sIADtHzUcAA+0daXPayDJfl18xS5KNiMFGHL7e8yYkJhu/9bWGpJKKUpSMBqyNkIgOH8Hs
  b389M7ovsCF2vJkuH9Jo+pjpnu4eITXjc+uVM7TWHn1HqFartY1qFf43qxv1GjmHlgb7z+CR
  WN1Yr9ca9YYI18Vatdl4hJrfUygPHMuWTYQeWVgeYhNn8hzKI2zdhUB3C2NX/wo21XPZVs9x
  TzOGq2NzsDweRMHrmfoXQes1T/+1em0D9N9sbqw/QtXliZANP7n+heuo5q8LSLjeOzjuDRxd
  gSHrtqz17DNsmHjU675+LV6jagHN6FOBXod7+6jeqDY3m5tb9ap7uNWorgM2EopFJOy3Dw5a
  qNg3dB33baz0FGMkq3qxhAR6/fjk6Lj1oUQpwW+JHpUQNL9v71IqwnUc+Rq9OTo5eLffquy2
  X1M0FB+gS0tEVdRlxzOGXJtjyLUbDVk37J6h4x7WMCF1oxHHcBcacP8MpqxnOhpOqDZ2ab7h
  tTqddwd7h39UACUYRVR+E8PMAVXV6tkGmUXDBHmBeuugXfnfu90/2gftwy4qCqGrLz4RrM+l
  IqGBEKMxNo2xxQZHm13SQ5uQtmxT7dt5HBipopDs6XObwei7jGFsWOQKtB0dtg+Oux8r3Y/H
  7Ur7r5B+Kap9NcYR1N/R66PDTpf1K54ahuYOIMpAJytm2Lstk535uKSRf3NydBBjkDKtYxMr
  1xEmn3RndIrN3kDFmoIqvyPCFcv65/TxhTrPkCDcNZtItkQxWWaRi0sTFySCc3jUjbIkjDyG
  hJvLOMqINOZqNRMLGrPli2JRtA20GbipdH9Sy/Ynee6yIfr+pPPnUQeQPfe4B9OBVlDx8ldx
  RfSdJjid9kk37jRL/gCj3vPmmrjp9HxPE1rQrJeywG61tG9lmPM6mwVd2nxMbu+YiUJS9RbB
  zdTaSkJXtE8ZeUdEY95xvhG5Y+iNNcfq6To9hhjmD611fLy/97rV3Ts6DIcx93okcoVGSamL
  4tYW2tgMZxiQe/RoKuL5Ab8hvvq3QtnEVmL1M+HD+ZOmMzryqYaL7LrX481+q9ttH3qNMcS+
  MYLBqLZqhCiQnA66FAdFVBz8KsLfYZHwKJYCKijqbELtMQ6Uao/w8cmG6KYRDkictI/3W6/b
  qNKIX0/0EJM9vD5v93bbldb+fuXVuy5K7ecPBtT9sdL+APPVAZW39ve6H9E2wX+BuumIHmr7
  w3HrcBcVnxez+sV7Gjk9433X5nLu2fTyrmZfy7qS3p7WmmyLt0TPw2fBcWrgCpt8Ws4P1/Hl
  +JqYF/zvDXRlregt+0yrTyMUBGogJuuydmWpVkBL06OxgzqGfPY85t5PzO2msSXdYuzStouM
  RJfaR2u/4nPuvHsVU0Q29s8d9KOB4BYrLbTcU2QNpt1Kw34e1XqXqJzuP71NLcjUo3tPuoID
  xKMIYrcO/aFrn/qO5G51scxmLalqsAayJA0bf3XovId4fQNCt2SUmUIRmvPnT0ynVJ1J7jM0
  cu2mQtl6mUVA/zaXLeaNfH478HNFBUbsHS+eK4adoq2OsNXzCOdSdaNMxi0DIiKbnFsQopSa
  m6i5Ablr5+1Rp9v6swSthfu+M3s3kHX//3yJ97rz7/9XRbGWuP+/Lor8/v9dQFTvn7rb1LOt
  IJJdME8BLW/bRycfC4VX7T/2DgsFWDDejd4CXYbxm/Bom3U4JqvPT3YhAMKuBAmXZXQFPbql
  MhK+wQFhUkLbkbT5Ev13B31DZDPwjRxeIdgI7u+1O4glNcK3EmMduxs+gzNlC3/aH/Y63Q4S
  rryGSwSx6IqQbB/uhgcHbI9OunCCPH/8MuUTgE/dz+WI/H7nIMZ/6pZd3xjr62fML1kSTdgO
  QKb3rRPEHLaHBxfgx99FbyO25/QTBWFQ8uYpa2skBJ01HRkIMGCSMzdStLffc8c9h8M1OCfi
  wHShqAn9JH7z3wKe//etatXGl0vmke//6/V6oxH4/0YT/H+juV7n/v8u4CnqnmE0MDTNuFD1
  IbKcU8tWbYck/BaSTbhmGiNkk06qhrcLT8EtrJ0ZI7yGlQvZVNbAgg7xxZ4O86hp5KwCFrQK
  dAqSggeShW3LAHQT/KRxju0LY6A/Fh/XJhPhcQ2RyyNVdywkTR6L0rQ0nT5Fb40LZBtobKrg
  0b3dByKEVhkRdKHaZyCcal8hoVaKMZIVJc6l74znZADI+dQVdTAAO9H70aGIoaE8rs3iEhDJ
  Z0a2jyyyQZAjzCYTCcZvaqqOYTjTGWwC9AgbMc4GMLFpYYoZH1VfHs8xoDCF/CE5ehoTZx4m
  FDWfOvs0FyI0HPYhNBNzxja9lFAXvTQHW/cTYtb/xQz+s/jhr/NwnIfVCJNtapwLZF+z6TPU
  VPLG2DgL0YQl01fN/uNaNsWjDDqwK1MVHKG1lkdnLYMO3SZGRaJNebSeZ8rkrTt/PVXIMsqi
  U0ldN2E6EcEqeTJVMmQiH8ZEqKzkUVmJU3mPzVPDwtDPMAbgyE00kWybZIkSC+jTVUjZY23b
  00JBOrfGch8/n1RXRVWfSmf+aQ1OC9IpHqr6xJZPHU02p5PrvgaNsBYcW5KkM+KBCk+kiTQ6
  NS4nkjlC4lSaPkG/uXjgCdUxRNTpJ/vzpLnaBJIT9xKECdueSoIEwsKxVEISRA1VmQjQOJBK
  20gSJqTp1JT7X7CtTaWSJHRJP0Ey1eEZBGzTuAjw3Px4GkUzCRrrUJqS7YV74mfA0yhbvy9h
  YzljWCkSvTkQdMshECyciduq6dPpZDCNEb7AyhAHojMN3ZzODpuNyCqbpNMc+HgxMhLWFVcZ
  7NjXmSQVaIOnfN9YXFvh9sTtabn21PliQKKifiMpqKwraKDJto11OC0vzdgi1lW5qXnlKfvZ
  nLOwDDNfxHieLct64oRuYj7PwvbzbFkG1II4ekWsR9Ol4ENO9MMbjz+rN9FLKtJO1PFJmjw6
  VeRoo029YczL+T4tqUJxOrHn1VB0hmp8ef0rl5eiWn/TXBR24ZYK20t1oPZlmppCsuq6bdhl
  fHVg1/nj++7kSroTE39Ya7nO1/K/ci2HngsKxUyJfCaMLs5gf4voRxFDbFto8KtIPrYYsjNN
  //GXdtTWslQ4Vzj2svfclH8uA7iPALqIj1tg6T8sH9fgPu7f5OM6LDUhbq6MTHxhgpcjh2Rv
  aeK+YSrEAdJbaQruqxbJX8am0ceKY2LrATg37m24t7kvb3NPfmEp2xfCRaKPZcbznFii8yNn
  OgvNffB5yiQgkyAye1ExHsHZbD3m6/C73T9Ysqtc3m5oEVe5gAd5WK6yyV3lnbrKEzzW5D7x
  lY5F/g4McwRdweJ+TkcIbWwBBOZv55p+muFzn8l9JveZP5/PFLnP5D6T+0zuM7+fz3xAq/I+
  XfSfGI+JaxbpLcAzld7/e74897zcJ5m4Sm9yUwdf2lgnt3BlTbWvflSdPiCt+u6LeLPLZ4lc
  oIDc8dxK5ZnEFzGG9uUYFjaxBvKqgoIHgEqfSjAGfJnnGIRP8PLZTYwkFc1zBw/MPIyHYR4J
  nfpzF9XCotp7WMpb48pbMBKne4AM+RaL2At/Kts9Uy3E3mqysUXNgb33AD9prz38tdpe3V29
  73fsfmQYu+9/wv8K2L9sgxUv+z3HGe//18Lvf5JawFWxscHf/7wbEMCdWjYeI/IG35DoHwka
  HtgdcCCIvhxBj36D9QerC49GslUqCLDw9AKi/16yShyafIo1jwh58tqtPCZYXwzynKh7Rimg
  Yugd+jqpkSYXUVGmJdJOyS8c5dQKK74phiQjZds8gUulsDAhJn7BNBDARoLQly1MzB0J5Fad
  bNPqKcXg3fh/WpnvxbNX4EmHHfRPC2V16xs6+DbHcCzSNyxwcOSJXfjlF1IHwB9ECTEBTXpb
  ESNPWja8/yAB04CIiivFeEsl0fI80bKWaDH8FvcBXu9Utixs2uTMnb4zIndIy6E5dnswt44r
  mmrZT3yLoZdiYiekTgidkDkhclTisMAIwbT+Qv9T4YsQKM5pzAB1k8DhjkIjsYOc+1ZPSw+x
  4OLrihA8vUKyt+UMGzANX5QCDJlQY4MmJlz0VhXggMAFf7WFZ0kIJklQB0jQHU2LTpz1RR1X
  RtYQjB2CrXWGlUASl5nbky1MCv+xzSuPDyIVKCw0UE3LLiOsWZBGGQzVq57IFgZIR4zP9PgT
  W6TdPb0i6FHy1jE59gvYuRRMSkGJUIjahEmwiGooIjMuMlemo7uz7rKCQD8icwtZgOxPCeiN
  dhqq51inU04n2s8mgglhRgA/9+1jf2Tw4v9rw+rtuStiudX/Z8b/Zq3Z9OP/OgT+qtgUyfc/
  8Pj//UEIKx5Cel5Zf1bGNb/wP9JVDZFv8WiKm1vNJjvcrFUbTb+uK/hoBzYNw4rd75dof/gt
  IeqfFXourjfht+pfK+ULVpspWG0uwbxUxa09qurgyhLlpt0IE8gW+ksosWGwqp1Bsd1wcTLq
  u92XZip/O8qQVWhwa5PR0mQ+NRIN6Lv6uqHj0di+qpBiahXYHWlMAlY7M9TfraKXheCVXExw
  CFXNJMmLZTOc9KKZkRJ5GaRiEpAyInG5kwT8aplpMqQVy4xPF53gPM4p85smLv46W9iVhJD5
  lZmTdFjp5PV1VK8i2zf1PixJPzuhph1uyTRlsbrpm3JmOh4xdC9yM5R5U3OagAuWqpdo8k2E
  K4WK2gohAdJS8KBXJG+OpryhXJxympGOu312mDDzJOVM6lhNYib6zBw3juDlK27xZ5CF1n7O
  KuLsdydaDUSqpRZIjqEQ2v7UAEbcDSUopLUm2+It0fPwWXCc5fButPoWXu8Le5wler/but75
  nTtYTEQ8FjLAKIgpwd4CFW3YskTKL8PFm6JENjfusyyBVCkhNqVaKf26imyXmjIXpNhfZOpJ
  nzKKfe9FCmLwtncYndXJDdVUTRFyJ8qwW0bdqKbpVhC2FTjBjz48nhhWPjt6NcYyVJA1Hzlw
  FCnDDC72vEoxmQJ4/impWWYUKQYRc1Q3wIz6q7kQKWZ9c3MLbZCgaJ0ZkKF/+YlKst4ppO//
  lln9deb+r9oUxWD/t8H2f+t8/3cnENY7SpR6Dcqfegv0JVux5UJuPVRWrhRABgfu1jIlbYVC
  OJP1Cpju+bnWC4EglN2ckqZxnnCRK4UdloAKpyVUcQ/lUuHpdQVFkudt8iUKR2/IXs69u/3E
  TRHd/DWasSVTspSM66/2LgyMFD6NbJ3vW5G3hPDnP6TAo7UqO3db/xMg+Pyn3iD9xEaDf//j
  3YBkYk2+RAVJxxd0zzbxK8FOJ5PpRJxOH6ppc5gDkuv/ruv/Vqt1WOzR7/9tNEUe/+8EnqKW
  Yxsj2Hb0ZU27QkOsYxInFfJx1/H7DmqsioWCpBh9h8T4viZb1qeBhr/qZbE2tj9PZBNQNTwt
  SI6Fx3L/C0zjZOBoGnkmpGw5Y2y6D4SU6VMjZQ2oX1pXo3J+FWH/IR2PNXmeZCSbX+hncpPQ
  gx5S3G9Jqj527HADODciToE9oBJQvO/Z58CBAwcOHDhw4MCBAwcOHDhw4MCBAwcOHDhw4MCB
  AwcOHDhw4MCBA4fbw/8Bs3jPtwCgAAA=
  
  --dDRMvlgZJXvWKvBx--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools