From e61b5826857a7dee27197c1ec4ab34a027f3f6c3 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 8 Jun 2021 11:33:25 +0200 Subject: [PATCH 01/15] Add --help flag to compiler executable --- .../translation/compiler32ProgScript.sml | 20 ++++++++- .../translation/compiler64ProgScript.sml | 20 ++++++++- compiler/compilerScript.sml | 41 +++++++++++++++---- 3 files changed, 71 insertions(+), 10 deletions(-) diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml index 4c257721fd..9396f333e6 100644 --- a/compiler/bootstrap/translation/compiler32ProgScript.sml +++ b/compiler/bootstrap/translation/compiler32ProgScript.sml @@ -224,8 +224,10 @@ val res = format_compiler_result_def val res = translate compile_32_def; val res = translate (has_version_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]) +val res = translate (has_help_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]) val res = translate print_option_def val res = translate current_build_info_str_def +val res = translate compilerTheory.help_string_def; val nonzero_exit_code_for_error_msg_def = Define ` nonzero_exit_code_for_error_msg e = @@ -240,7 +242,9 @@ val main = process_topdecs` let val cl = CommandLine.arguments () in - if compiler_has_version_flag cl then + if compiler_has_help_flag cl then + print compiler_help_string + else if compiler_has_version_flag cl then print compiler_current_build_info_str else case compiler_compile_32 cl (TextIO.inputAll TextIO.stdIn) of @@ -287,6 +291,20 @@ Proof \\ imp_res_tac stdin_get_file_content \\ xlet_auto >- xsimpl \\ xif + >- + (simp[full_compile_32_def] + \\ xapp + \\ CONV_TAC SWAP_EXISTS_CONV + \\ qexists_tac `help_string` + \\ fs [compilerTheory.help_string_def, + fetch "-" "compiler_help_string_v_thm"] + \\ xsimpl + \\ rename1 `add_stdout _ (strlit string)` + \\ CONV_TAC SWAP_EXISTS_CONV + \\ qexists_tac`fs` + \\ xsimpl) + \\ xlet_auto >- xsimpl + \\ xif >- ( simp[full_compile_32_def] \\ xapp diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml index bfbbc5443e..0993bdad34 100644 --- a/compiler/bootstrap/translation/compiler64ProgScript.sml +++ b/compiler/bootstrap/translation/compiler64ProgScript.sml @@ -243,8 +243,10 @@ val res = format_compiler_result_def val res = translate compile_64_def; val res = translate (has_version_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]) +val res = translate (has_help_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]) val res = translate print_option_def val res = translate current_build_info_str_def +val res = translate compilerTheory.help_string_def; val nonzero_exit_code_for_error_msg_def = Define ` nonzero_exit_code_for_error_msg e = @@ -259,7 +261,9 @@ val main = process_topdecs` let val cl = CommandLine.arguments () in - if compiler_has_version_flag cl then + if compiler_has_help_flag cl then + print compiler_help_string + else if compiler_has_version_flag cl then print compiler_current_build_info_str else case compiler_compile_64 cl (TextIO.inputAll TextIO.stdIn) of @@ -306,6 +310,20 @@ Proof \\ imp_res_tac stdin_get_file_content \\ xlet_auto >- xsimpl \\ xif + >- + (simp[full_compile_64_def] + \\ xapp + \\ CONV_TAC SWAP_EXISTS_CONV + \\ qexists_tac `help_string` + \\ fs [compilerTheory.help_string_def, + fetch "-" "compiler_help_string_v_thm"] + \\ xsimpl + \\ rename1 `add_stdout _ (strlit string)` + \\ CONV_TAC SWAP_EXISTS_CONV + \\ qexists_tac`fs` + \\ xsimpl) + \\ xlet_auto >- xsimpl + \\ xif >- ( simp[full_compile_64_def] \\ xapp diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index 403c92a03c..a7df76283d 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -53,7 +53,7 @@ val current_build_info_str_def = Define ` (* ========================================================================= *) -val _ = Datatype` +Datatype: config = <| inferencer_config : inf_env ; backend_config : α backend$config @@ -62,9 +62,28 @@ val _ = Datatype` ; skip_type_inference : bool ; only_print_types : bool ; only_print_sexp : bool - |>`; + |> +End -val _ = Datatype`compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring`; +Datatype: + compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring +End + +val help_string = ‘ +Usage: cake [flags] < input_file > output_file +’ + +fun drop_until p [] = [] + | drop_until p (x::xs) = if p x then x::xs else drop_until p xs; + +val help_string_tm = + help_string |> hd |> (fn QUOTE s => s) |> explode + |> drop_until (fn c => c = #"\n") |> tl |> implode + |> stringSyntax.fromMLstring; + +Definition help_string_def: + help_string = strlit ^help_string_tm +End val locs_to_string_def = Define ` (locs_to_string NONE = implode "unknown location") ∧ @@ -437,12 +456,14 @@ val parse_top_config_def = Define` get_err_str prelude; get_err_str typeinference])` -(* Check for version flag - TODO: fix this -*) +(* Check for version flag *) val has_version_flag_def = Define ` has_version_flag ls = MEM (strlit"--version") ls` +(* Check for version help *) +val has_help_flag_def = Define ` + has_help_flag ls = MEM (strlit"--help") ls` + val format_compiler_result_def = Define` format_compiler_result bytes_export (Failure err) = (List[]:mlstring app_list, error_to_str err) ∧ @@ -498,7 +519,9 @@ val compile_64_def = Define` val full_compile_64_def = Define ` full_compile_64 cl inp fs = - if has_version_flag cl then + if has_help_flag cl then + add_stdout fs help_string + else if has_version_flag cl then add_stdout fs current_build_info_str else let (out, err) = compile_64 cl inp in @@ -535,7 +558,9 @@ val compile_32_def = Define` val full_compile_32_def = Define ` full_compile_32 cl inp fs = - if has_version_flag cl then + if has_help_flag cl then + add_stdout fs help_string + else if has_version_flag cl then add_stdout fs current_build_info_str else let (out, err) = compile_32 cl inp in From 566889f3ad5af5bac25ad4c6cddc208a7bad3d80 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 9 Jun 2021 14:58:17 +0200 Subject: [PATCH 02/15] Add text about compiler options and heap/stack size --- how-to.md | 46 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/how-to.md b/how-to.md index ec4dd5c0b2..6b12bfe96f 100644 --- a/how-to.md +++ b/how-to.md @@ -85,6 +85,52 @@ compiled and run as follows: The last run illustrates that CakeML's integer type is the unbounded mathematical integers (arbitrary precision integers). +Configuring the CakeML compiler +------------------------------- + +The default configuration of the CakeML compiler is usually the right +one to use. However, the CakeML compiler supports a number of +command-line options that can be used to tweak the default +configuration. Type the following for an explanation of the +command-line options. + + $ ./cake --help + +When using the provided `Makefile`, one can specify command-line +options by setting the `CAKEFLAGS` variable. The following example +instructs the CakeML compiler to compile the factorial program with +the `--gc=gen1000` option. This option tells the compiler to install +the generational version of CakeML's GC with a nursery size of 1000 +machine words. + + $ rm -f fac.cake ; export CAKEFLAGS='--gc=gen1000' ; make fac.cake + +Several command-line options can be given at the same time: one can +specify that we want a 50000-word nursery and to use register +allocator settings `3` as follows. + + $ rm -f fac.cake ; export CAKEFLAGS='--gc=gen50000 --reg_alg=3' ; make fac.cake + +The default GC configuration is `--gc=simple`. + +Setting the size of the stack and heap +-------------------------------------- + +If program execution aborts with a message saying that the heap or +stack space has been exhausted, then it might be worth trying to run +the program with more heap or stack space. + +One can run the factorial program from above with 2048 MB of heap +space and 512 MB of stack space by invoking it as follows: + + $ export CML_HEAP_SIZE=2048 ; export CML_STACK_SIZE=512 ; ./fac.cake 50 + +Observe that these variables `CML_HEAP_SIZE` and `CML_STACK_SIZE` are +supplied to the _compiled_ CakeML program `fac.cake` rather than the +CakeML compiler. Note that, since the CakeML compiler is just another +CakeML program, the values of these environment variables also affect +the compiler's execution. + How CakeML differs from SML and OCaml ------------------------------------- From cc26c9d66aa3a3b4a3aa51b5cf9378d313837344 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 9 Jun 2021 15:07:12 +0200 Subject: [PATCH 03/15] Fix a reference so that it points to github --- how-to.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/how-to.md b/how-to.md index 6b12bfe96f..0140eb66d4 100644 --- a/how-to.md +++ b/how-to.md @@ -20,9 +20,9 @@ logic of a theorem prover](https://cakeml.org/itp18-short.pdf). Running the CakeML compiler --------------------------- -The bootstrapped CakeML compiler can be downloaded from the CakeML -website: https://cakeml.org/download.html. Download the `tar.gz` file -which contains among other things: +The bootstrapped CakeML compiler can be downloaded from +[github](https://github.com/CakeML/cakeml/releases). Download the +`tar.gz` file which contains among other things: - `cake.S` — the machine code for the bootstrapped CakeML compiler - `basis_ffi.c` — C code connecting the CakeML basis library to the OS From b026affe5eb1f7261f4225d0cabff699e2e548f4 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 9 Jun 2021 15:23:21 +0200 Subject: [PATCH 04/15] Make a start on a more informative --help message --- compiler/compilerScript.sml | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index a7df76283d..59f0dc06ae 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -21,6 +21,29 @@ open ag32_configTheory export_ag32Theory val _ = new_theory"compiler"; +val help_string = (* beginning of --help string *) ‘ + +Usage: cake [OPTIONS] < input_file > output_file + +The cake executable is usually invoked as shown above. The different +OPTIONS are described in the OPTIONS listing below. + +One can also run the cake execuable as follows to print a listing of +the type of each top-level bindings (including the bindings made in +the standard basis library). + +Usage: cake --types < input_file + +One can invoke the cake executable to print this help message (--help) +or version information (--version) without an input_file: + +Usage: cake --version +Usage: cake --help + +OPTIONS: + +’ (* end of --help string *) + (* == Build info =========================================================== *) val current_version_tm = mlstring_from_proc "git" ["rev-parse", "HEAD"] @@ -69,10 +92,6 @@ Datatype: compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring End -val help_string = ‘ -Usage: cake [flags] < input_file > output_file -’ - fun drop_until p [] = [] | drop_until p (x::xs) = if p x then x::xs else drop_until p xs; From fcd92b03ada17dbaa2e3836608c7fb5e30747817 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 9 Jun 2021 23:08:38 +0200 Subject: [PATCH 05/15] One can write integers in hex --- how-to.md | 1 + 1 file changed, 1 insertion(+) diff --git a/how-to.md b/how-to.md index 0140eb66d4..6ac2329078 100644 --- a/how-to.md +++ b/how-to.md @@ -187,6 +187,7 @@ examples. Note how `Some` and `None` differ from SML. (* some numbers *) 0; 1; + 0xFF; (* integer written in hex *) 5000; ~5000; (* a negative number *) From c3cb6b138b38a12cbad8dc95203af9ef27af9423 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 9 Jun 2021 23:08:53 +0200 Subject: [PATCH 06/15] Start writing help message --- compiler/compilerScript.sml | 54 +++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index 59f0dc06ae..d11edaebc6 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -42,6 +42,60 @@ Usage: cake --help OPTIONS: + --reg_alg=N + + --gc=G specifies garbage collector type; here G is one of: + none - no garbage collector is used + simple - a non-generational Cheney (default) + genN - a generational Cheney garbage collector is + used; the size of the nursery generation is + N machine words (example: --gc=gen5000) + + --target=T specifies that compilation should produce code for target + T, where T can be one of x64, arm8, mips, riscv for + the 64-bit compiler; for the 32-bit compiler T can be + one of arm7 and ag32. + + --sexp=B B can be either true or false; here false means that the + input will be parsed as normal CakeML concrete syntax; + true means that the input is parsed as an s-expression. + + --print_sexp causes the cake to print the given program in + s-expression format; with this option, the compiler + does not generate machine code. + + --exclude_prelude=B here B can be either true or false; the default + is false; setting this to true causes the compiler not + to include the standard basis library. + + --skip_type_inference=B here B can be either true or false; the + default is false; true will make the compiler skip + type inference. There are no gurantees of safety if + the type inferencer is skipped. + + --explore + +ADDITIONAL OPTIONS: + +Optimisations can be configured using the following advanced options. + + --jump=B true means conditional jumps to be used for out-of-stack checks + --multi=B true means clos_to_bvl phase is to use multi optimisation + --known=B true means clos_to_bvl phase is to use known optimisation + --call=B true means clos_to_bvl phase is to use call optimisation + --inline_factor=N threshold used by for inliner pass + --max_app=N max number of optimised curried applications + --max_body_size=N + --inline_size=N + --exp_cut=N + --split=N + --tag_bits=N + --len_bits=N + --pad_bits=N + --len_size=N + --emit_empty_ffi=B + --hash_size=N + ’ (* end of --help string *) (* == Build info =========================================================== *) From 7633843c55b8235762d6cfe894e0bfe1aed9837d Mon Sep 17 00:00:00 2001 From: Yong Kiam Date: Thu, 10 Jun 2021 04:20:38 -0400 Subject: [PATCH 07/15] add help text for reg alloc and others --- compiler/compilerScript.sml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index d11edaebc6..c0c9e79b61 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -42,7 +42,13 @@ Usage: cake --help OPTIONS: - --reg_alg=N + --reg_alg=N N is a natural number that specifies the register + allocation algorithm to use: + 0 - simple allocator, no spill heuristics + 1 - simple allocator, spill heuristics + 2 - IRC allocator, no spill heuristics (default) + 3 - IRC allocator, spill heuristics + >=4 - linear scan allocator --gc=G specifies garbage collector type; here G is one of: none - no garbage collector is used @@ -93,8 +99,8 @@ Optimisations can be configured using the following advanced options. --len_bits=N --pad_bits=N --len_size=N - --emit_empty_ffi=B - --hash_size=N + --emit_empty_ffi=B true emits debugging FFI calls for use with DEBUG_FFI + --hash_size=N size of the memoization table used by instruction encoder ’ (* end of --help string *) From afa266e1e1cce677c7d58b0c2acd5d13b2ff8f07 Mon Sep 17 00:00:00 2001 From: Yong Kiam Date: Thu, 10 Jun 2021 05:01:36 -0400 Subject: [PATCH 08/15] Add a section on profiling --- how-to.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/how-to.md b/how-to.md index 6ac2329078..d26bf0bc62 100644 --- a/how-to.md +++ b/how-to.md @@ -120,6 +120,7 @@ If program execution aborts with a message saying that the heap or stack space has been exhausted, then it might be worth trying to run the program with more heap or stack space. +The default heap and stack size is set to 1024 MB each. One can run the factorial program from above with 2048 MB of heap space and 512 MB of stack space by invoking it as follows: @@ -131,6 +132,36 @@ CakeML compiler. Note that, since the CakeML compiler is just another CakeML program, the values of these environment variables also affect the compiler's execution. +Alternatively, the allocated heap and stack size can be set in `basis_ffi.c` +by modifying these lines in the file. +Note that `cml_heap_sz` and `cml_stack_sz` are given in bytes here. + + unsigned long sz = 1024*1024; // 1 MB unit + unsigned long cml_heap_sz = 1024 * sz; // Default: 1 GB heap + unsigned long cml_stack_sz = 1024 * sz; // Default: 1 GB stack + +Basic profiling +------------------------------------- + +On Linux systems, CakeML executables can be profiled using `perf`. +As an example, we may profile the factorial program by running: + + $ perf record ./fac.cake 30000 + +The report generated by `perf` shows that most of the time is spent in +the bignum library (`LongDiv` is used internally there): + + $ perf report + + Samples: 20K of event 'cycles', Event count (approx.): 15828778212 + Overhead Command Shared Object Symbol + 52.88% fac.cake fac.cake [.] cml__LongDiv_21 + 16.19% fac.cake fac.cake [.] cml__Bignum_50 + 12.10% fac.cake fac.cake [.] cml__Bignum_47 + 6.31% fac.cake fac.cake [.] cml__Replicate_9 + ... + + How CakeML differs from SML and OCaml ------------------------------------- From c3709b7138cfc3897e579f107284c14ffb781154 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 10 Jun 2021 12:37:59 +0200 Subject: [PATCH 09/15] Complete a first draft of the --help message --- compiler/compilerScript.sml | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/compiler/compilerScript.sml b/compiler/compilerScript.sml index c0c9e79b61..b3be55e3d1 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -29,7 +29,7 @@ The cake executable is usually invoked as shown above. The different OPTIONS are described in the OPTIONS listing below. One can also run the cake execuable as follows to print a listing of -the type of each top-level bindings (including the bindings made in +the type of each top-level binding (including the bindings made in the standard basis library). Usage: cake --types < input_file @@ -79,7 +79,8 @@ OPTIONS: type inference. There are no gurantees of safety if the type inferencer is skipped. - --explore + --explore outputs several intermediate forms of the compiled + program in JSON format ADDITIONAL OPTIONS: @@ -89,16 +90,16 @@ Optimisations can be configured using the following advanced options. --multi=B true means clos_to_bvl phase is to use multi optimisation --known=B true means clos_to_bvl phase is to use known optimisation --call=B true means clos_to_bvl phase is to use call optimisation - --inline_factor=N threshold used by for inliner pass - --max_app=N max number of optimised curried applications - --max_body_size=N - --inline_size=N - --exp_cut=N - --split=N - --tag_bits=N - --len_bits=N - --pad_bits=N - --len_size=N + --inline_factor=N threshold used by for ClosLang inliner in known pass + --max_body_size=N threshold used by for ClosLang inliner in known pass + --max_app=N max number of optimised curried applications in multi pass + --inline_size=N threshold used by for BVL inliner pass + --exp_cut=N threshold for when to cut large expression into subfunctions + --split=B true means main expression will be split at sequencing (;) + --tag_bits=N number of tag bits in every pointer + --len_bits=N number of length bits in every pointer + --pad_bits=N number of zero padding in every pointer + --len_size=N size of length field in heap object header cells --emit_empty_ffi=B true emits debugging FFI calls for use with DEBUG_FFI --hash_size=N size of the memoization table used by instruction encoder From f47766246c4ae3d0926153de4bcdd5c437a81c4c Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 10 Jun 2021 16:34:23 +0200 Subject: [PATCH 10/15] Fix List.foldl --- basis/ListProgScript.sml | 2 +- basis/PrettyPrinterProgScript.sml | 7 ++++--- basis/pure/mllistScript.sml | 13 ++++++++----- 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml index c3910580b6..1c107d4fed 100644 --- a/basis/ListProgScript.sml +++ b/basis/ListProgScript.sml @@ -113,7 +113,7 @@ val _ = ml_prog_update open_local_in_block; val result = next_ml_names := ["partition"]; val result = translate mllistTheory.partition_def; -val result = translate FOLDL; +val result = translate foldl_def; val _ = ml_prog_update open_local_block; val result = translate foldli_aux_def; diff --git a/basis/PrettyPrinterProgScript.sml b/basis/PrettyPrinterProgScript.sml index ffc7c123ad..ebeae13caa 100644 --- a/basis/PrettyPrinterProgScript.sml +++ b/basis/PrettyPrinterProgScript.sml @@ -24,6 +24,9 @@ fun tr name def = ( translate def ) +Triviality fromList_thm = + fromList_def |> SIMP_RULE std_ss [mllistTheory.foldl_intro]; + val _ = tr "fromString" fromString_def val _ = tr "fromChar" fromChar_def val _ = tr "fromBool" fromBool_def @@ -34,9 +37,7 @@ val _ = tr "fromWord64" fromWord64_def val _ = tr "fromRat" fromRat_def val _ = tr "fromOption" fromOption_def val _ = tr "fromPair" fromPair_def -val _ = tr "fromList" fromList_def -val _ = tr "fromArray" fromArray_def -val _ = tr "fromVector" fromVector_def +val _ = tr "fromList" fromList_thm val sigs = module_signatures [ "fromString", diff --git a/basis/pure/mllistScript.sml b/basis/pure/mllistScript.sml index 4d86a3ae20..0d6238031d 100644 --- a/basis/pure/mllistScript.sml +++ b/basis/pure/mllistScript.sml @@ -102,12 +102,9 @@ Proof rw [partition_def, FILTER, partition_aux_thm] QED -val foldl_aux_def = Define` - (foldl_aux f e n [] = e) /\ - (foldl_aux f e n (h::t) = foldl_aux f (f h e) (SUC n) t)`; - val foldl_def = Define` - foldl f e l = foldl_aux f e 0 l`; + (foldl f e [] = e) /\ + (foldl f e (h::t) = foldl f (f h e) t)`; val foldli_aux_def = Define` (foldli_aux f e n [] = e) /\ @@ -124,6 +121,12 @@ val foldli_aux_thm = Q.prove ( rw [ADD1] ); +Theorem foldl_intro: + ∀xs x f. FOLDL f x xs = foldl (λx acc. f acc x) x xs +Proof + Induct \\ fs [foldl_def] +QED + Theorem foldli_thm: !f e l. foldli f e l = FOLDRi (\n. f (LENGTH l - (SUC n))) e (REVERSE l) Proof From c58fde72075cfe3576748f861b8cbeebce691ac6 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 11 Jun 2021 09:19:48 +0200 Subject: [PATCH 11/15] Get tutorial to build again --- tutorial/solutions/wordfreqProgScript.sml | 1 + tutorial/wordfreqProgScript.sml | 1 + 2 files changed, 2 insertions(+) diff --git a/tutorial/solutions/wordfreqProgScript.sml b/tutorial/solutions/wordfreqProgScript.sml index d3f9d0f7c7..faccd54e0d 100644 --- a/tutorial/solutions/wordfreqProgScript.sml +++ b/tutorial/solutions/wordfreqProgScript.sml @@ -89,6 +89,7 @@ QED (* Translation of wordfreq helper functions *) +val res = translate FOLDL; val res = translate lookup0_def; val res = translate insert_word_def; val res = translate (insert_line_def |> REWRITE_RULE[splitwords_def]); diff --git a/tutorial/wordfreqProgScript.sml b/tutorial/wordfreqProgScript.sml index f9226fdaf0..45243a0483 100644 --- a/tutorial/wordfreqProgScript.sml +++ b/tutorial/wordfreqProgScript.sml @@ -89,6 +89,7 @@ QED (* Translation of wordfreq helper functions *) +val res = translate FOLDL; val res = translate lookup0_def; val res = translate insert_word_def; val res = translate (insert_line_def |> REWRITE_RULE[splitwords_def]); From b2d68ddc061e1d032927ef851971b935c365d89b Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sun, 13 Jun 2021 09:51:42 +0200 Subject: [PATCH 12/15] Fix for change to List.foldl --- examples/lpr_checker/lpr_commonProgScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/lpr_checker/lpr_commonProgScript.sml b/examples/lpr_checker/lpr_commonProgScript.sml index 0e22ab896f..c76dce630e 100644 --- a/examples/lpr_checker/lpr_commonProgScript.sml +++ b/examples/lpr_checker/lpr_commonProgScript.sml @@ -35,7 +35,7 @@ val _ = translate check_RAT_def; val _ = translate check_PR_def; val _ = translate is_PR_def; -val _ = translate check_lpr_step_def; +val _ = translate (check_lpr_step_def |> SIMP_RULE std_ss [mllistTheory.foldl_intro]); val _ = translate (is_unsat_def |> SIMP_RULE (srw_ss()) [LET_DEF,MEMBER_INTRO]); open mlintTheory; From 1a644f8a7269bb1b4de9636240741fcdfe989d6e Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Sun, 13 Jun 2021 23:10:45 +0200 Subject: [PATCH 13/15] Fix a translation --- examples/opentheory/reader_commonProgScript.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/opentheory/reader_commonProgScript.sml b/examples/opentheory/reader_commonProgScript.sml index 0943a888cf..04db1557e1 100644 --- a/examples/opentheory/reader_commonProgScript.sml +++ b/examples/opentheory/reader_commonProgScript.sml @@ -102,6 +102,7 @@ val r = holSyntaxExtraTheory.tymatch_def |> translate; val _ = (use_mem_intro := false); val r = translate OPTION_MAP_DEF; +val r = translate FOLDL; val r = translate holSyntaxExtraTheory.match_type_def; val r = m_translate find_axiom_def; @@ -313,4 +314,3 @@ Theorem context_spec = mk_app_of_ArrowP (fetch "ml_hol_kernelProg" "context_v_thm"); val _ = export_theory (); - From 2963c5356c89f6c81c70977626e37121a60bbd5d Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 14 Jun 2021 22:48:17 +0200 Subject: [PATCH 14/15] Tweak how-to.md so that the extracted code builds --- how-to.md | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/how-to.md b/how-to.md index d26bf0bc62..7a85dfec55 100644 --- a/how-to.md +++ b/how-to.md @@ -136,9 +136,11 @@ Alternatively, the allocated heap and stack size can be set in `basis_ffi.c` by modifying these lines in the file. Note that `cml_heap_sz` and `cml_stack_sz` are given in bytes here. - unsigned long sz = 1024*1024; // 1 MB unit - unsigned long cml_heap_sz = 1024 * sz; // Default: 1 GB heap - unsigned long cml_stack_sz = 1024 * sz; // Default: 1 GB stack +``` +unsigned long sz = 1024*1024; // 1 MB unit +unsigned long cml_heap_sz = 1024 * sz; // Default: 1 GB heap +unsigned long cml_stack_sz = 1024 * sz; // Default: 1 GB stack +``` Basic profiling ------------------------------------- @@ -146,21 +148,24 @@ Basic profiling On Linux systems, CakeML executables can be profiled using `perf`. As an example, we may profile the factorial program by running: - $ perf record ./fac.cake 30000 +``` +$ perf record ./fac.cake 30000 +``` The report generated by `perf` shows that most of the time is spent in the bignum library (`LongDiv` is used internally there): - $ perf report - - Samples: 20K of event 'cycles', Event count (approx.): 15828778212 - Overhead Command Shared Object Symbol - 52.88% fac.cake fac.cake [.] cml__LongDiv_21 - 16.19% fac.cake fac.cake [.] cml__Bignum_50 - 12.10% fac.cake fac.cake [.] cml__Bignum_47 - 6.31% fac.cake fac.cake [.] cml__Replicate_9 - ... - +``` +$ perf report + +Samples: 20K of event 'cycles', Event count (approx.): 15828778212 +Overhead Command Shared Object Symbol + 52.88% fac.cake fac.cake [.] cml__LongDiv_21 + 16.19% fac.cake fac.cake [.] cml__Bignum_50 + 12.10% fac.cake fac.cake [.] cml__Bignum_47 + 6.31% fac.cake fac.cake [.] cml__Replicate_9 + ... +``` How CakeML differs from SML and OCaml ------------------------------------- From ef772f37fcd1dfa4d3c7e097bf1bbab794c9a573 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Fri, 18 Jun 2021 10:39:20 +0200 Subject: [PATCH 15/15] Update proof for new --help flag --- .../ag32/32/proofs/ag32BootstrapProofScript.sml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml b/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml index 74bde972e3..efd4b1e79a 100644 --- a/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml +++ b/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml @@ -29,15 +29,15 @@ val with_clos_conf_simp = prove( val ffi_names = ``config.lab_conf.ffi_names`` - |> (REWRITE_CONV[ag32BootstrapTheory.config_def] THENC EVAL) + |> (REWRITE_CONV[ag32BootstrapTheory.config_def] THENC EVAL); val LENGTH_code = ``LENGTH code`` - |> (REWRITE_CONV[ag32BootstrapTheory.code_def] THENC listLib.LENGTH_CONV) + |> (REWRITE_CONV[ag32BootstrapTheory.code_def] THENC listLib.LENGTH_CONV); val LENGTH_data = ``LENGTH data`` - |> (REWRITE_CONV[ag32BootstrapTheory.data_def] THENC listLib.LENGTH_CONV) + |> (REWRITE_CONV[ag32BootstrapTheory.data_def] THENC listLib.LENGTH_CONV); Overload cake_machine_config = ``ag32_machine_config (THE config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)`` @@ -281,7 +281,9 @@ Theorem cake_extract_writes: let events = MAP get_output_io_event (cake_io_events cl (stdin_fs inp)) in let out = extract_writes 1 events in let err = extract_writes 2 events in - if has_version_flag (TL cl) then + if has_help_flag (TL cl) then + (out = explode help_string) ∧ (err = "") + else if has_version_flag (TL cl) then (out = explode current_build_info_str) ∧ (err = "") else let (cout, cerr) = compile_32 (TL cl) inp in @@ -294,7 +296,7 @@ Proof \\ simp[wfFS_stdin_fs, STD_streams_stdin_fs] \\ simp[compilerTheory.full_compile_32_def] \\ pairarg_tac \\ simp[] - \\ IF_CASES_TAC \\ fs[] + \\ ntac 2 (IF_CASES_TAC \\ fs[] >- ( simp[TextIOProofTheory.add_stdo_def] \\ SELECT_ELIM_TAC @@ -324,7 +326,7 @@ Proof pop_assum mp_tac \\ rw[] \\ fs[] \\ rw[] \\ pop_assum mp_tac \\ rw[]) - >- ( rw[] \\ rw[OPTREL_def]))) + >- ( rw[] \\ rw[OPTREL_def])))) \\ simp[TextIOProofTheory.add_stdout_fastForwardFD, STD_streams_stdin_fs] \\ DEP_REWRITE_TAC[TextIOProofTheory.add_stderr_fastForwardFD] \\ simp[TextIOProofTheory.STD_streams_add_stdout, STD_streams_stdin_fs]