Permalink
Browse files

Make readme_gen read 1st paragraph from markdown; update READMEs

  • Loading branch information...
myreen committed Dec 27, 2018
1 parent 60b1806 commit 71bba8329616f6ab39a9ac773feacec21b4da784
@@ -3,7 +3,7 @@ INCLUDES = developers compiler/bootstrap/compilation/x64/64/proofs
all: $(DEFAULT_TARGETS) README.md cake-x64-64.tar.gz
.PHONY: all

README_SOURCES = COPYING developers examples build-instructions.sh
README_SOURCES = COPYING developers examples build-instructions.sh how-to.md
DIRS = $(wildcard */)
README.md: developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
developers/readme_gen $(README_SOURCES)
@@ -55,6 +55,14 @@ generating README.md files.
[examples](examples):
Examples of verified programs built using CakeML infrastructure.

[how-to.md](how-to.md):
This text introduces how to use the CakeML compiler, in particular
this document provides:

- a description of how to invoke the CakeML compiler
- a list of how CakeML differs from SML and OCaml
- a number of small CakeML code examples

[misc](misc):
Auxiliary files providing glue between a standard HOL installation
and what we want to use for CakeML development.
@@ -1 +1,5 @@
(*
A hello world program used for testing that the bootstrapped
compiler was built succesfully.
*)
print "Hello!\n";
@@ -0,0 +1,2 @@
This directory represents a stage in the build sequence where the latest
available cake binary is downloaded to perform testing and bootstrapping.
@@ -26,7 +26,7 @@ val MAX_CODE_LINE_LENGTH = 200
val PREFIX_FILENAME = "readmePrefix"
val OUTPUT_FILENAME = "README.md"
val CHECK_OPT = "--check"
val AUTO_INCLUDE_SUFFIXES = ["Script.sml","Syntax.sml","Lib.sml",".lem",".c"]
val AUTO_INCLUDE_SUFFIXES = ["Script.sml","Syntax.sml","Lib.sml",".lem",".c",".cml"]
val FIRST_TARGET_PREFIX = "all: $(DEFAULT_TARGETS) README.md"

val HOLMAKEFILE_SUGGESTION =
@@ -258,6 +258,31 @@ fun read_comment_from_raw filename = let
in all_lines end handle e => (TextIO.closeIn(f); raise e)
end;

(* Read from a markdown file, e.g. how-to.md *)

(*
val filename = "../how-to.md"
*)
fun read_comment_from_markdown filename = let
val lines = Option.valOf (read_all_lines filename)
val line = List.nth (lines,1) handle Subscript => "\n"
val line2 = List.nth (lines,2) handle Subscript => "\n"
val lines = if String.isPrefix "==" line orelse String.isPrefix "--" line
then List.drop(lines,if is_blank_line line2 then 3 else 2)
else lines
fun take_until p [] = []
| take_until p (x::xs) = if p x then [] else x :: take_until p xs
fun drop_until p [] = []
| drop_until p (x::xs) = if p x then x::xs else drop_until p xs
fun until_next_blank_line [] = []
| until_next_blank_line (x::xs) =
if is_blank_line x then [] else
if String.isSuffix ":\n" x then
x :: take_until (not o is_blank_line) xs
@ until_next_blank_line (drop_until (not o is_blank_line) xs)
else x :: until_next_blank_line xs
in until_next_blank_line lines end;

(* Read first paragraph of header from directory *)

fun file_exists filename =
@@ -387,13 +412,16 @@ fun create_summary write_output path extra_files = let
in if is_dir path_file then
TitleAndContent (filename,read_comment_from_dir path_file)
else if String.isSuffix ".sml" filename orelse
String.isSuffix ".cml" filename orelse
String.isSuffix ".lem" filename then
TitleAndContent (filename,read_comment_from_sml path_file)
else if String.isSuffix ".c" filename orelse
String.isSuffix ".css" filename then
TitleAndContent (filename,read_comment_from_c path_file)
else if String.isSuffix ".sh" filename then
TitleAndContent (filename,read_comment_from_script path_file)
else if String.isSuffix ".md" filename then
TitleAndContent (filename,read_comment_from_markdown path_file)
else
(TitleAndContent (filename,read_comment_from_script path_file)
handle ReadmeExn msg =>
@@ -1,6 +1,10 @@
This directory contains files that create an unverified bootstrap of
the 32-bit compiler.

[basis_ffi.c](basis_ffi.c):
Implements the foreign function interface (FFI) used in the CakeML basis
library, as a thin wrapper around the relevant system calls.

[x64SexprScript.sml](x64SexprScript.sml):
Produces an sexp print-out of the bootstrap translated compiler
definition for the 32-bit version of the compiler.
@@ -1,3 +1,7 @@
(*
A CakeML program that extracts the indented code snippets from a
markdown file. This is used for checking the code how-to.md file.
*)

val lines =
let
@@ -39,4 +43,6 @@ fun get_code_lines lines =
get_code_lines (dropUntil normal_text_line lines)
else get_code_lines rest;

print (String.concat ["(", "*\n This file has been generated by extract_code.cml.\n*",")\n"]);

List.map print (get_code_lines lines);

0 comments on commit 71bba83

Please sign in to comment.