This project provides a set of tools to test out CoqR.

It executes R code with both an R and Coq interpreter, and then proceeds to compare their outputs.

Setup

Requirements:

• Python 3.5
• R binary (tested on v3.4.2)
• coqR

First of all, Python libraries should be installed. You can do it with the following command:

$ pip install -r requirements.txt
or
$ pip3 install -r requirements.txt

You may need to provide permissions to install (or install in a virtualenv)

Scripts

It is possible to either execute the whole process with both interpreters or to execute different stages of the process separately.

Run all

Executes the whole process with both interpreters and outputs general statistics of the process.

It requires a .env file in the directory where it's run, with the following content:

# Contents of .env file
# Without ''

COQ_INTERP=path/to/coq-interpreter-executable
COQR_INITIAL_STATE=path/to/initial-state
RSCRIPT=path/to/rscript  # Or just name if it's in global scope

# If sending data to server
URL=https://...
TOKEN=token-authentication

Doc of the script:

usage: run_all.py [-h] [-o OUTPUT] [-d] [-s] [-r] [-t TITLE] [-m MESSAGE] src

Run given file with R and Coq interpreters, processes outputs and compares

positional arguments:
  src                   File to be interpreted

optional arguments:
  -h, --help            show this help message and exit
  -o OUTPUT, --output OUTPUT
                        Creates a JSON file with the results in the given
                        path.
  -d, --debug           Allows printing debug information in the console
                        output. If the -o option is used, it will attempt to
                        create debug files in the same directory given.
  -s, --server          Send results to a server. It requires URL and TOKEN
                        env variables to be defined.
  -r, --recursive       Allows interpretation of a directory to be recursive.
  -t TITLE, --title TITLE
                        Adds a title to the test.
  -m MESSAGE, --message MESSAGE
                        Adds a custom message (description) to the test.

Usage of the script:

$ ./run_all src

The output will be in the output directory specified, with a JSON format.

It will also print general stats about the execution.

Runner

It runs every expression in a file. It requires that either RSCRIPT or COQ_INTERP environmental variables are defined. If both are, it will prefer the R case.

# Running R on a file
$ RSCRIPT='rscript' python -m coqr.scripts.runner input.R output.json

# Running CoqR 
$ COQ_INTERP=/path/to/CoqR/ python -m coqr.scripts.runner input.R output.json

Cleaner

Reads a file (in JSON format), processes the output and returns a file with a new processed output.

You must indicate which interpreter generated the output, either R or Coq.

$ python -m coqr.scripts.cleaner R input.json output.json

$ python -m coqr.scripts.cleaner Coq input.json output.json

Stats

It reads a file generated by the comparison (See 'run all') and prints stats or info about it.

You can either display general stats (total of Pass, Fail, etc. cases) or ask for information on a particular case.

# General stats
$ ./stats.py -g out/result.json

# Case info
$ ./stats.py -status Pass out/result.json