-------------------------------------------------------------------------------

                     RUBY INTERFACE TO THE ACL2 BRIDGE

-------------------------------------------------------------------------------

Files:

   ACL2Bridge.rb -- Core library for connecting to an ACL2 Bridge and
                    communicating with it.

   demo.rb       -- Trivial demo program that uses ACL2Bridge.rb to
                    implement a lousy read-eval-print loop.

   to_lisp.rb    -- Optional, extends Ruby's Integer, String, Array, and
                    Hash classes with a .to_lisp method.  Useful for web
                    applications that want to send form input to ACL2.


Supporting software:

   Ruby Version: 1.9.3p0

   Gems: getopt, hash_keyword_args


Documentation:

   To use any of this you will need to know about the ACL2 Bridge.  It is
   documented in the Centaur Books Manual, under "Bridge".  If you don't know
   where the Centaur Books Manual is, please see the file:

      books/centaur/README.html

   in your ACL2 distribution.

   This Ruby code is just an interface to the ACL2 Bridge.  The source code has
   lots of comments that explain what is happening, so just start reading
   ACL2Bridge.rb for usage info.


Trying the Demo:

   First, install Ruby and the required gems:
      conda install -y ruby
      gem install getopt hash_keyword_args
   Certify the ACL2 Bridge books:
      `cert.pl $ACL2_SYSTEM_BOOKS/centaur/bridge/top`

   To try the demo, you'll need to first start an ACL2 Bridge:
      1. Start ACL2
      2. At the ACL2> prompt:
         ```
         (include-book "centaur/bridge/top" :dir :system)
         (bridge::start "./demo-bridge")
         ```
   then in a different terminal run
   "./demo.rb --help" for information on how to connect.  You can connect
   multiple clients at a time, of course.


Questions:

   For help, ask Jared Davis <jared@centtech.com>

-------------------------------------------------------------------------------
