-
Notifications
You must be signed in to change notification settings - Fork 1
Installation
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
-
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.
git clone --recursive https://github.com/aa755/ROSCoq.git
cd ROSCoq/
scons -j2 -k
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