Add RealCake properly to build sequence, update some README's

Author: HeikoBecker

README.md

@@ -63,6 +63,10 @@ particular:
 - a list of how CakeML differs from SML and OCaml, and,
 - a number of small CakeML code examples.
 
+[icing](icing):
+Main implementation directory for the RealCake development, presented in
+"Verified Compilation and Optimization of Floating-Point Programs"
+
 [misc](misc):
 Auxiliary files providing glue between a standard HOL installation
 and what we want to use for CakeML development.

developers/README.md

@@ -14,21 +14,3 @@ paths relative to the root directory.
 [bin](bin):
 This directory represents a stage in the build sequence where the latest
 available cake binary is downloaded to perform testing and bootstrapping.
-
-[build-sequence](build-sequence):
-The regression test runs through this list of directories.
-
-[fix_scripts.sml](fix_scripts.sml):
-This is a script that can automation adding a legacy mode line to
-broken HOL4 scripts following changes to HOL4. Update the new_str
-declaration below and run this with poly --script fix_scripts.sml in
-the dir that needs fixing; it will recurse into INCLUDES dirs.
-
-[readme_gen.sml](readme_gen.sml):
-This SML program generates a `README.md` summary for the files
-given as command-line arguments to this script. The contents of the
-summaries are read from a specific style of comment that needs to
-appear at the top of each file.
-
-[wc.sh](wc.sh):
-A script that counts non-blank lines.

developers/build-sequence

@@ -120,6 +120,11 @@ compiler/parsing/tests
 compiler/inference/tests
 compiler/printing/test
 
+# Floating-Point optimizer
+icing/flover
+icing/
+icing/examples
+
 # compiler translation
 compiler/repl
 compiler/bootstrap/translation

developers/icing-sequence

@@ -1,7 +1,8 @@
 Main implementation directory for the RealCake development, presented in
 "Verified Compilation and Optimization of Floating-Point Programs"
+
 ===========================================================================
 
 Content in the directory can be build with `Holmake`.
 
-Files contained in this directory:
+Files contained in this directory: