This repository contains the parts parser combinator library. This is a Coq library that supports extraction to OCaml. We include several examples, tests, and benchmarks.

Prereqs

Install coq and coq-stpp:

$ opam repo add coq-released https://coq.inria.fr/opam/released
$ opam pin add coq 8.11.0
$ opam install coq coq-stdpp

Install other ocaml prereqs:

$ opam install ounit2 core_bench

Running

To run tests or benchmarks:

$ make test
$ make benchmarks

This will compile the Coq, extracting parsers, and compiling the ocaml for you. You will see warnings regarding Pervasives, which can safely be ignored.

If you want to run an individual benchmark, you can do:

$ make bench_<foo>

Where <foo> is one of the benchmark names (json, sexp, or as currently).

Note that the benchmarks target also executes ulimit -s unlimited to remove process limits on stack space. Like the TAAP work, we're not hitting the tail call optimization all the time.

If you want to run just extraction, you can do:

make extract

Adding files / modifying the build

The top-level build stuff is defined in the Makefile. It relies on the _CoqProject file to compile the Coq code and the Dune build system to compile the OCaml.

To add a coq file: add it in both the _CoqProject file and in the V_FILENAMES list in the top-level Makefile.

To add an OCaml file that's generated by extraction: add it to the GEN_ML_FILENAMES list in the top-level Makefile.

To add a static OCaml file: add it to STATIC_ML_FILENAMES in the top-level Makefile.

To add a benchmark: Look in src/benchmarks. You'll want to make a new file following the pattern of bench_json.ml, bench_sexp.ml, etc. Then add your new benchmark to src/benchmarks/dune, and add the name of your benchmark in the BENCHMARKS list at the top of the top-level Makefile.

Profiling

Setup

OCaml 4.09+ removed support for more convenient profiling, so we need to use perf, a somewhat complicated linux utility. First install it:

$ sudo apt-get install linux-tools-common
$ sudo apt-get install linux-tools-`uname -r`

Second, perf requires the ability monitor various system events to collect profiling data, I guess. By default, your user account probably doesn't have access to this information. To confirm, look at the file:

/proc/sys/kernel/perf_event_paranoid

Which probably has a number greater than 0 in it. Change it to 0. You can make this change permanent by adding this line to /etc/sysctl.conf:

kernel.perf_event_paranoid = 0

I have no idea what the security consequences of this are.

Execution

Once that's done, you can profile! Just do:

make prof_<foo>

where <foo> is one of the benchmark names (e.g., json or sexp). This will run (a shortened version of) the benchmark while capturing performance data with perf, and then run the interactive perf data explorer for you to view the results. It takes a few minutes for perf to process the data, so be patient (but you should see a progress bar).

The raw perf data will also be present in the directory, so you can quit the call to perf that I've included in the makefile if you want to invoke it with different options.

These targets run a drastically reduced version of the benchmarks where each test within a benchmark is run only once (whereas the normal version runs each test repeatedly for 10 seconds). This is done because of the massive amount of data perf captures. For this cut down version of the benchmarks, the perf file is around 1GB. For a full run, it's much larger.

Dealing with OCaml build errors

Currently, any top-level extracted term of type (fee, fie, fo, fum) machine will result in a compile-time error, due to a value restriction.

The workaround is to add |> Obj.magic to the end of each of these definitions directly in the extracted code. Not ideal, but (we think) type-safe.

Builds may also stack-overflow at compile time, since some of the parsers we generate are large. ulimit -s unlimited will fix this on most machines.

Acknowledgement

This work is sponsored by DARPA/AFRL Contract HR001120C0016. Its content does not necessarily reflect the position or policy of the US Government and no official endorsement should be inferred.