diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-31 13:58:20 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-09-11 20:32:40 -0400 |
| commit | 6b03ff5f346225aaf17e57bee2caf7c899989a84 (patch) | |
| tree | ad8e51ba17942b75830a6c1dad441225432f85e0 /README.md | |
| parent | c50611790812ba94c052ec51364e13d773d5c64a (diff) | |
Update build instructions regarding submodules, install
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -8,6 +8,10 @@ Build Requirements This repository requires: - To build the proofs and almost-C-like outputs: [Coq 8.7](https://github.com/coq/coq/releases/tag/V8.7.2) or [Coq 8.8](https://github.com/coq/coq/releases/tag/V8.8.0) (tested with 8.7.2, 8.8.0) +If you checked out this repository via `git`, you should run + + git submodule update --init --recursive + To build (if your COQPATH variable is empty): make @@ -17,6 +21,8 @@ To build: export COQPATH="$(pwd)/coqprime${COQPATH:+:}$COQPATH" make +You may get non-fatal errors such as `make: execvp: /bin/sh: Argument list too long`; this is an artifact of the [old pipeline](#old-pipeline) and is a [bug in Coq](https://github.com/coq/coq/issues/7584) that will prevent `make install` from succeeding, but will not impact the build itself. + New Pipeline ----- The new pipeline (nearly finished) generates binaries that take in arguments on the command line and print out C code on stdout. |