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 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] 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..b3be55e3d1 100644 --- a/compiler/compilerScript.sml +++ b/compiler/compilerScript.sml @@ -21,6 +21,90 @@ 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 binding (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: + + --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 + 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 outputs several intermediate forms of the compiled + program in JSON format + +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 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 + +’ (* end of --help string *) + (* == Build info =========================================================== *) val current_version_tm = mlstring_from_proc "git" ["rev-parse", "HEAD"] @@ -53,7 +137,7 @@ val current_build_info_str_def = Define ` (* ========================================================================= *) -val _ = Datatype` +Datatype: config = <| inferencer_config : inf_env ; backend_config : α backend$config @@ -62,9 +146,24 @@ val _ = Datatype` ; skip_type_inference : bool ; only_print_types : bool ; only_print_sexp : bool - |>`; + |> +End + +Datatype: + compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring +End + +fun drop_until p [] = [] + | drop_until p (x::xs) = if p x then x::xs else drop_until p xs; -val _ = Datatype`compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring`; +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 +536,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 +599,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 +638,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 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; 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 (); - diff --git a/how-to.md b/how-to.md index ec4dd5c0b2..7a85dfec55 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 @@ -85,6 +85,88 @@ 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. + +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: + + $ 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. + +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 ------------------------------------- @@ -141,6 +223,7 @@ examples. Note how `Some` and `None` differ from SML. (* some numbers *) 0; 1; + 0xFF; (* integer written in hex *) 5000; ~5000; (* a negative number *) 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]);