reorg for python package

.gitignore

@@ -5,7 +5,7 @@
 ########################
 # Python Lex Yacc files
 ########################
-concept_space_parsetab.py
+*_parsetab.py
 ivy_formulatab.py
 ivy_parsetab.py
 ivy_termtab.py
@@ -19,3 +19,6 @@ ivy_termtab.py
 *.out
 *.snm
 *.toc
+
+# Python setup creates this
+ms_ivy.egg-info

bin/ivy

@@ -2,4 +2,4 @@
 
 export PYTHONPATH=$Z3DIR/bin:$Z3DIR/lib/python2.7/dist-packages:$IVYDIR/src/ivy:$IVYDIR/src/tkui:$IVYDIR/ivy
 
-python $IVYDIR/src/ivy/ivy.py $@ 
+python $IVYDIR/ivy/core/ivy.py $@ 

bin/ivy_check

@@ -2,4 +2,4 @@
 
 export PYTHONPATH=$Z3DIR/bin:$Z3DIR/lib/python2.7/dist-packages:$IVYDIR/src/ivy:$IVYDIR/src/tkui:$IVYDIR/ivy
 
-python $IVYDIR/src/ivy/ivy_check.py $@ 
+python $IVYDIR/ivy/core/ivy_check.py $@ 

bin/ivy_to_cpp

@@ -2,4 +2,4 @@
 
 export PYTHONPATH=$Z3DIR/bin:$IVYDIR/src/ivy:$IVYDIR/ivy
 
-python $IVYDIR/src/ivy/ivy_to_cpp.py $@ 
+python $IVYDIR/ivy/core/ivy_to_cpp.py $@ 

doc/install.md

@@ -2,60 +2,93 @@
 layout: page
 title: Installing IVy
 ---
-## prerequisites
+## Prerequisites
 
-### python 2.7
+### Python 2.7
 
 Get it from [here](https://www.python.org/downloads) or as part of
-your Linux distribution.
+your Linux distribution. You should make sure to get the `pip`
+utility.  This is standard on versions from 2.7.9.
+
+You can install IVy in a python virtual environment if you don't want
+to pollute your local python setup. Before the following instructions,
+do this:
+
+    $ pip install virtualenv
+    $ virtualenv ivy_env
+    $ cd ivy_env
+    $ . bin/activate
 
 ### Z3
 
 Following the instructions [here](https://github.com/Z3Prover/z3) to
-install Z3. Set the environment variable Z3DIR to the prefix at which
-you installed Z3. By defult this is /usr/local, in which case:
+install Z3. You can test whether Z3 is correctly installed like this:
 
-    $ export Z3DIR = /usr/local
+    $ python
+    >>> import z3
+
+If you want to install Z3 in a virtual environment, you can install Z3
+like this:
+
+    $ make install PREFIX=/path/to/ivy_env
 
 ### Python packages
 
-Install the python packages ply and pygraphviz. On Ubuntu, install them
+Install the python packages ply, pygraphviz and tarjan. On Ubuntu, install them
 like this:
 
     $ sudo apt-get install python-ply python-pygraphviz
+    $ pip install tarjan
 
-### tcl/tk/tcldot
+As an alternative, pip can install all the packages, but you need to make sure
+the dependencies on system packages are met:
+
+    $ sudo apt-get install graphviz graphviz-dev python-dev
+    $ pip install ply pygraphviz tarjan
+
+This latter is the option if you are making a virtual environment.
+
+### Tcl/Tk/Tix
 
 To use the Tk-based user interface, you need to install the python
-package tk, the tix widget set, and the tcldot package (part of
-graphviz). On Ubuntu, install them all like this:
+package tk, and the tix widget set. On Ubuntu, install them like
+this:
 
-    $ sudo apt-get install python-tk tix libgv-tcl
+    $ sudo apt-get install python-tk tix
 
-## install
+## Install IVy
 
 Get the source like this:
 
     $ git clone https://github.com/Microsoft/ivy.git
-
-Set the environment variable IVYDIR to point to the root of Ivy's
-source tree, like this:
-
     $ cd ivy
-    $ export IVYDIR=`pwd`
 
-Add Ivy's bin directory to your path, like this:
+Install into your local Python like this
 
-    $ export PATH=`pwd`/bin:$PATH
+    $ sudo python setup.py install
 
-## run
+If you want to run from the source tree for development purposes, do
+this instead:
 
-Run Ivy on an example, using the Tcl/Tk user interface:
+    $ sudo python setup.py develop
 
-    $ cd examples/ivy
-    $ ivy client_server.ivy
+If you don't want to do a system-wide install (and you aren't using a
+virtual environment) there are various ways to install in your home
+directory. For example:
 
-## emacs mode
+    $ python setup install --home=~
+
+See the [python documenation](https://docs.python.org/2/install/) for
+general instructions on installing python packages.
+
+## Run
+
+Run Ivy on an example, like this:
+
+    $ cd doc/examples
+    $ ivy client_server_example.ivy
+
+## Emacs mode
 
 An emacs major mode for Ivy is available in lib/emacs/ivy-mode.el. Put this file
 somewhere in your emacs load path and add the following code to your

ivy/__init__.py

@@ -0,0 +1,3 @@
+__path__ = [__path__[0]] + [(__path__[0] + '/' + x) for x in ['core','tkui']]
+
+import concept

ivy/core/ivy.py

@@ -2,7 +2,16 @@
 #
 # Copyright (c) Microsoft Corporation. All Rights Reserved.
 #
+
 import sys
+
+# pick up some paths if were are run as main
+if __name__ == "__main__":
+    mypath = sys.path[0]
+    sys.path.insert(0,mypath+'/..')
+    sys.path.insert(0,mypath+'/../tkui')
+#    print "path: {}".format(sys.path)
+
 import pickle
 import string
 from ivy_compiler import IvyError, ivy_new, ivy_load_file
@@ -103,8 +112,10 @@ def ivy_init():
 
     return ag
 
-if __name__ == "__main__":
+def main():
     with ivy_module.Module():
         ui_main_loop(ivy_init())
 
+if __name__ == "__main__":
+    main()
 

ivy/core/ivy_check.py

@@ -30,7 +30,7 @@ def usage():
     print "usage: \n  {} file.ivy".format(sys.argv[0])
     sys.exit(1)
 
-if __name__ == "__main__":
+def main():
     ivy.read_params()
     if len(sys.argv) != 2 or not sys.argv[1].endswith('ivy'):
         usage()
@@ -62,3 +62,7 @@ if __name__ == "__main__":
                             display_cex("safety failed",cex)
     print "OK"
 
+
+if __name__ == "__main__":
+    main()
+

ivy/core/ivy_compiler.py

@@ -482,7 +482,10 @@ def ivy_compile(decls,mod=None,create_isolate=True,**kwargs):
 
 def clear_rules(modname):
     import sys
-    d = sys.modules[modname].__dict__
+    if modname in sys.modules:
+        d = sys.modules[modname].__dict__
+    else:
+        d = sys.modules['ivy.' + modname].__dict__
     for s in list(d):
         if s.startswith('p_'):
             del d[s]

ivy/core/ivy_to_cpp.py

@@ -1249,7 +1249,7 @@ public:
 
 target = iu.EnumeratedParameter("target",["impl","gen"],"gen")
 
-if __name__ == "__main__":
+def main():
     ia.set_determinize(True)
     slv.set_use_native_enums(True)
     iso.set_interpret_all_sorts(True)
@@ -1266,4 +1266,8 @@ if __name__ == "__main__":
         f = open(classname+'.cpp','w')
         f.write(impl)
         f.close()
+
+
+if __name__ == "__main__":
+    main()
         

setup.py

@@ -0,0 +1,20 @@
+from setuptools import setup
+
+setup(name='ms_ivy',
+      version='0.1',
+      description='IVy verification tool',
+      url='http://github.com/microsoft/ivy',
+      author='IVy team',
+      author_email='nomail@example.com',
+      license='MIT',
+      packages=['ivy'],
+      install_requires=[
+          'ply',
+          'pygraphviz',
+          'tarjan'
+      ],
+      entry_points = {
+        'console_scripts': ['ivy=ivy.ivy:main','ivy_check=ivy.ivy_check:main','ivy_to_cpp=ivy.ivy_to_cpp:main',],
+        },
+      zip_safe=False)
+