<commit_before># coq-compile ##########################################################

TODO overview, credits, license?

# Getting Started ######################################################

## Prerequisites #######################################################

### Coq 8.4 ############################################################

coq-ext-lib requires Coq 8.4, which you can download from
http://coq.inria.fr/download.

Since it made some interface changes, you may also want the latest proof 
general:
   http://proofgeneral.inf.ed.ac.uk/devel.

### LLVM & Clang #######################################################

You need version 3.1 of LLVM and clang. If your package manager does not
have these packages available, you can download and build LLVM and clang
by following the instructions at http://llvm.org/docs/GettingStarted.html.
Be sure to replace `/trunk` with `/branches/release_31` in each `svn checkout` 
command.

### ocamlbuild #########################################################

ocamlbuild is used to extract the compiler. If your package manager does
not include ocamlbuild, it is available at (TODO).

## Building ############################################################

TODO

## Running #############################################################

TODO

# Contributing #########################################################

TODO

## Development environment #############################################

### coq-ext-lib ########################################################

TODO

### Using proof general+emacs ##########################################

If you use proof general+emacs, then you can run `make .dir-locals.el`
in the top level directory to produce a .dir-locals.el. This will 
configure your proof general settings for this directory so that you can 
edit files interactively.<commit_msg>updating the README file.<commit_after># coq-compile ##########################################################

This is a compiler from Gallina (the logic language of the Coq proof
assistant) to LLVM. In addition to the core logical language, the
compiler also supports a limited number of extensions to perform input
and output in order to make programs more useful.

## Design Philosophy ###################################################

The compiler is written exclusively in Coq in a Haskell-like style
using coq-ext-lib, an augemented/alternative standard library that
utilizes first-class abstractions like type classes rather than
second-class abstractions like functors and modules.  See the
coq-ext-lib project (https://github.com/coq-ext-lib/coq-ext-lib) for
more information.

## Credits #############################################################

The compiler started as a course project in a graduate seminar on
functional language compilers taught by <NAME>
(http://www.eecs.harvard.edu/~greg/). The course webpage is here
(http://www.eecs.harvard.edu/~greg/cs252rfa12/). The primary
contributers to the core compiler have been (in alphabetical order):

<NAME> (optimization & analysis)
<NAME> (core & optimization & analysis)
<NAME> (runtime)

# Getting Started ######################################################

## Prerequisites #######################################################

### Coq 8.4 ############################################################

coq-ext-lib requires Coq 8.4, which you can download from
http://coq.inria.fr/download.

Since it made some interface changes, you may also want the latest proof 
general:
   http://proofgeneral.inf.ed.ac.uk/devel.

### LLVM & Clang #######################################################

You need version 3.1 of LLVM and clang. If your package manager does not
have these packages available, you can download and build LLVM and clang
by following the instructions at http://llvm.org/docs/GettingStarted.html.
Be sure to replace `/trunk` with `/branches/release_31` in each `svn checkout` 
command.

### ocamlbuild #########################################################

ocamlbuild is used to extract the compiler. If your package manager does
not include ocamlbuild, it is available at (TODO).

## Building ############################################################

TODO

## Running #############################################################

TODO

# Contributing #########################################################

If you're interested in the compiler, we'd love for you to join the
project and learn something about compilers and something about Coq.

Check the issues page on GitHub and file a new issue for the feature(s)
you'd like (if one doesn't already exist). 

## Development environment #############################################

### coq-ext-lib ########################################################

TODO

### Using proof general+emacs ##########################################

If you use proof general+emacs, then you can run `make .dir-locals.el`
in the top level directory to produce a .dir-locals.el. This will 
configure your proof general settings for this directory so that you can 
edit files interactively.
{'fraction_non_alphanumeric': 0.3358150470219436, 'fraction_numerical': 0.0041144200626959246, 'mean_word_length': 6.012362637362638, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 1, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5337151', 'n_tokens_mistral': 1250, 'n_tokens_neox': 1193, 'n_words': 480}