kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

YaccError when parsing a model #68

Open landonjefftaylor opened 1 year ago

landonjefftaylor commented 1 year ago

After installing IVy (with no errors during installation), I encountered the following error when compiling:

Traceback (most recent call last):
  File "/usr/local/bin/ivy_check", line 11, in <module>
    load_entry_point('ms-ivy==1.8.23', 'console_scripts', 'ivy_check')()
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-1.8.23-py2.7.egg/ivy/ivy_check.py", line 811, in main
    ivy_init.source_file(sys.argv[1],ivy_init.open_read(sys.argv[1]),create_isolate=False)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-1.8.23-py2.7.egg/ivy/ivy_init.py", line 72, in source_file
    ivy_load_file(f,**kwargs)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-1.8.23-py2.7.egg/ivy/ivy_compiler.py", line 2300, in ivy_load_file
    decls = read_module(f)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-1.8.23-py2.7.egg/ivy/ivy_compiler.py", line 2272, in read_module
    reload(ivy_parser)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-1.8.23-py2.7.egg/ivy/ivy_parser.py", line 3003, in <module>
    parser = yacc.yacc(start='top',tabmodule='ivy_parsetab',errorlog=yacc.NullLogger(),outputdir=tabdir,debug=None)
  File "/usr/local/lib/python2.7/dist-packages/ply-3.11-py2.7.egg/ply/yacc.py", line 3432, in yacc
    raise YaccError('Unable to build parser')
ply.yacc.YaccError: Unable to build parser

When I modified yacc.py to produce a more interpretable eror output, I received the following message:

/usr/local/lib/python2.7/dist-packages/ms_ivy-1.8.23-py2.7.egg/ivy/ivy_parser.py:542: Symbol optwith used, but not defined as a token or a rule

I had never encountered this issue before when installing IVy, but as of a couple of weeks ago, every OS I've tried to install IVy on has reported an identical issue. Currently, I'm having the error on Debian 11.

landonjefftaylor commented 1 year ago

I was able to successfully install IVy 1.7 from the archived repository, so I believe this is a novel issue since IVy 1.8.