Dependencies

ROSCoq has several specific dependencies. We provide installation instructions for each of them, and the reason why each one is needed.

• OS: We recommend Ubuntu 14.04 LTS, especially if you wish to run ROSCoq programs on robots.

• Git is needed to download sources. Scons is needed to build ROSCoq. On Ubuntu, these can be installed using:
  sudo apt-get install git scons

• Coq v8.5

• CoRN and MathClasses respectively provide the theory of real analysis and abstract algebra used in ROSCoq. Please make sure to install a version that works with Coq 8.5.

The dependencies below are only needed if you wish to run ROSCoq programs on robots.

• ROS (Robot Operating System) is needed to be able to control actual robots. Please follow the instructions here. If you do not have an iRobot Create, skip the section on testing the robot. Note that these instructions install the Indigo version of ROS, which is the latest LTS version. The latest version, Jade, does not yet have drivers for iRobot Create.
• ROSCoq include my fork of roshask as a submodule. roshask provides Haskell bindings for ROS. After extraction to Haskell, ROSCoq programs call roshask functions to interact with ROS. You can install the dependencies of roshask as follows:
  sudo apt-get install haskell-platform libcrypto++-dev libssl-dev
  This fork of roshask also builds Coq types for ROS message types, and directives to extract them to their Haskell counterparts.

Installing ROSCoq

git clone --recursive https://github.com/aa755/ROSCoq.git
cd ROSCoq/
scons -j2 -k

Installing our roshask fork

Now you are ready to develop robotic progams and their proofs of correctness in Coq. Our tutorial can help you get started. You can skip the steps below if you don't intend run those programs on actual robots.
cd roshask
cabal update
cabal install -j2 --force-reinstalls

You also need to set 3 environment variables. So that roshask can correctly compile the Coq files it produces. Please replace ~ by the place where you cloned ROSCoq.
export COQ_ROSCOQ_PHYSICAL=~/ROSCoq/src/
export COQ_CoRN_PHYSICAL=~/ROSCoq/dependencies/corn/
export COQ_MathClasses_PHYSICAL=~/ROSCoq/dependencies/corn/math-classes/src/
You should add the above three lines to ~/.bashrc and then execute source ~/.bashrc