Permalink
Browse files

Add resource usage warning to readme and build doc

Closes #490
  • Loading branch information...
xrchz committed May 23, 2018
1 parent 8495d8e commit 5b0e7d5130d24f8fe2ac9a5bf8f4536091c4f7b8
Showing with 13 additions and 3 deletions.
  1. +7 −3 README.md
  2. +2 −0 build-instructions.sh
  3. +4 −0 readmePrefix
View
@@ -5,12 +5,16 @@ CakeML is a verified implementation of a significant subset of
Standard ML.
The source and proofs for CakeML are developed in the [HOL4 theorem
prover](http://hol-theorem-prover.org). We use the latest development
prover](http://hol-theorem-prover.org). We use the latest development
version of [HOL4](https://github.com/HOL-Theorem-Prover/HOL), which we
build on [PolyML 5.7](http://www.polyml.org).
Example build instructions can be found in
[build-instructions.sh](build-instructions.sh).
Building all of CakeML (including the bootstrapped compiler and its proofs)
requires significant resources. Built copies of the compiler and resource
usage for our regression tests are [online](https://cakeml.org/regression.cgi).
The [master](../../tree/master) branch contains the latest development
version of CakeML. See the [version2](../../tree/version2) or
[version1](../../tree/version1) branch for previous versions.
@@ -44,8 +48,8 @@ A verified compiler for CakeML, including:
- targets: code generation to x86, ARM, and more
[developers](developers):
This directory contains scripts for automating routine tasks, e.g. for
running regression tests.
This directory contains scripts for automating routine tasks, e.g., for
generating README.md files.
[documentation](documentation):
Work-in-progress documentation regarding the CakeML language.
View
@@ -34,6 +34,8 @@ bin/build
# export PATH=$HOLDIR/bin:$PATH
## build CakeML
## note: a full build (including the bootstrapped compiler)
## takes a long time (~20 hours) and requires much RAM (~16 GB)
cd
git clone https://github.com/CakeML/cakeml
cd cakeml
View
@@ -11,6 +11,10 @@ build on [PolyML 5.7](http://www.polyml.org).
Example build instructions can be found in
[build-instructions.sh](build-instructions.sh).
Building all of CakeML (including the bootstrapped compiler and its proofs)
requires significant resources. Built copies of the compiler and resource
usage for our regression tests are [online](https://cakeml.org/regression.cgi).
The [master](../../tree/master) branch contains the latest development
version of CakeML. See the [version2](../../tree/version2) or
[version1](../../tree/version1) branch for previous versions.

0 comments on commit 5b0e7d5

Please sign in to comment.