From 6b03ff5f346225aaf17e57bee2caf7c899989a84 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Aug 2018 13:58:20 -0400 Subject: Update build instructions regarding submodules, install --- README.md | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'README.md') diff --git a/README.md b/README.md index 05fe28067..3411f047d 100644 --- a/README.md +++ b/README.md @@ -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. -- cgit v1.2.3