<commit_before># hs-to-coq

## Setup (run once)

```
stack setup
```

## Build and run

```
stack build
stack exec hs-to-coq -- -I $GHC_PATH/compiler -I $GHC_PATH/compiler/stage2 -I $GHC_PATH/compiler/stage2/build -o $OUTPUT_FILE -p $PREAMBLE -r $RENAMINGS -e $EDITS -m $MODULES -d $GHC_PATH $INPUT_FILES
```

## Example command line

```
stack exec hs-to-coq -- -I ~/prog/ghc/compiler -I ~/prog/ghc/compiler/stage2 -I ~/prog/ghc/compiler/stage2/build -o test.v -p preamble.v -r renamings.txt -e edits.txt -m modules.txt -d ~/prog/ghc
```

## GHC API

```
https://downloads.haskell.org/~ghc/8.0.2/docs/html/libraries/ghc-8.0.2/
```

## GHC version

* Use [GHC 8.0.2](https://www.haskell.org/ghc/download_ghc_8_0_2.html) for
  compilation (handled by Stack) and translation

## Files:

* `preamble.v`: Coq code inserted at the start of the injected output<commit_msg>Put -DSTAGE=2 into the README<commit_after># hs-to-coq

## Setup (run once)

```
stack setup
```

## Build and run

```
stack build
stack exec hs-to-coq -- -I $GHC_PATH/compiler -I $GHC_PATH/compiler/stage2 -I $GHC_PATH/compiler/stage2/build -o $OUTPUT_FILE -p $PREAMBLE -r $RENAMINGS -e $EDITS -m $MODULES -d $GHC_PATH $INPUT_FILES
```

## Example command line

```
stack exec hs-to-coq -- -I ~/prog/ghc/compiler -I ~/prog/ghc/compiler/stage2 -I ~/prog/ghc/compiler/stage2/build -o test.v -p preamble.v -r renamings.txt -e edits.txt -m modules.txt -d ~/prog/ghc --ghc -DSTAGE=2
```

## GHC API

```
https://downloads.haskell.org/~ghc/8.0.2/docs/html/libraries/ghc-8.0.2/
```

## GHC version

* Use [GHC 8.0.2](https://www.haskell.org/ghc/download_ghc_8_0_2.html) for
  compilation (handled by Stack) and translation

## Files:

* `preamble.v`: Coq code inserted at the start of the injected output
{'fraction_non_alphanumeric': 0.17346938775510204, 'fraction_numerical': 0.01927437641723356, 'mean_word_length': 3.401496259351621, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 4, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4183871', 'n_tokens_mistral': 778, 'n_tokens_neox': 731, 'n_words': 175}