Merge remote-tracking branch 'origin/master' into remove-cheats

basis/basis_ffi.c

@@ -81,7 +81,7 @@ void ffiopen_in (unsigned char *c, long clen, unsigned char *a, long alen) {
 }
 
 void ffiopen_out (unsigned char *c, long clen, unsigned char *a, long alen) {
-  int fd = open((const char *) c, O_RDWR|O_CREAT|O_TRUNC);
+  int fd = open((const char *) c, O_RDWR|O_CREAT|O_TRUNC, S_IRUSR|S_IWUSR|S_IRGRP|S_IROTH);
   if (0 <= fd){
     a[0] = 0;
     int_to_byte8(fd, &a[1]);

basis/pure/mlprettyprinterScript.sml

@@ -41,7 +41,7 @@ val fromWord8_def = Define`
 
 val fromWord64_def = Define`
   fromWord64 (w : 64 word) =
-  List [strlit "0wx", mlnum$toString (words$w2n w)]
+  List [strlit "0wx"; mlnum$toString (words$w2n w)]
 `
 
 val fromRat_def = Define`

candle/standard/opentheory/readerIOProofScript.sml

@@ -184,7 +184,7 @@ val readLines_EQ = Q.store_thm("readLines_EQ",
 
 val readFile_correct = Q.store_thm("readFile_correct",
   `readFile fname c = (res, c_out) /\
-   read_file c.stdio c.holrefs fname = (succ, fs, refs)
+   read_file c.stdio c.holrefs fname = (succ, fs, refs, fstate)
    ==>
    res = Success () /\ fs = c_out.stdio /\ refs = c_out.holrefs`,
   rw [readFile_def, read_file_def, st_ex_bind_def, st_ex_return_def,
@@ -195,7 +195,7 @@ val readFile_correct = Q.store_thm("readFile_correct",
 
 val readMain_correct = Q.store_thm ("readMain_correct",
   `readMain () c = (res, c_out) /\
-   reader_main c.stdio c.holrefs (TL c.cl) = (succ, fs, refs)
+   reader_main c.stdio c.holrefs (TL c.cl) = (succ, fs, refs, fstate)
    ==>
    res = Success () /\ fs = c_out.stdio`,
   simp [readMain_def, st_ex_bind_def, case_eq_thms, arguments_def, liftM_def,

candle/standard/opentheory/readerProgScript.sml

@@ -235,7 +235,7 @@ val read_file_spec = Q.store_thm("read_file_spec",
      (POSTv u.
        &UNIT_TYPE () u *
        STDIO (FST (SND (read_file fs refs fnm))) *
-       HOL_STORE (SND (SND (read_file fs refs fnm))))`,
+       HOL_STORE (FST (SND (SND (read_file fs refs fnm)))))`,
   xcf "read_file" (get_ml_prog_state())
   \\ reverse (Cases_on `STD_streams fs`)
   >- (fs [TextIOProofTheory.STDIO_def] \\ xpull)

candle/standard/opentheory/readerProofScript.sml

@@ -1705,20 +1705,20 @@ val read_file_def = Define`
     (if inFS_fname fs (File fnm) then
        (case readLines (all_lines fs (File fnm)) init_state refs of
         | (Success (s,_), refs) =>
-            (T, add_stdout fs (msg_success s refs.the_context), refs)
-        | (Failure (Fail e), refs) => (F, add_stderr fs e, refs))
+            (T, add_stdout fs (msg_success s refs.the_context), refs, SOME s)
+        | (Failure (Fail e), refs) => (F, add_stderr fs e, refs, NONE))
      else
-       (F, add_stderr fs (msg_bad_name fnm), refs))`;
+       (F, add_stderr fs (msg_bad_name fnm), refs, NONE))`;
 
 val reader_main_def = Define `
    reader_main fs refs cl =
        case cl of
          [fnm] =>
           (case init_reader () refs of
             (Success _, refs) => read_file fs refs fnm
-          | (Failure (Fail e), refs) => (F, add_stderr fs (msg_axioms e), refs)
-          | (_, refs) => (F, fs, refs))
-       | _ => (F, add_stderr fs msg_usage, refs)`;
+          | (Failure (Fail e), refs) => (F, add_stderr fs (msg_axioms e), refs, NONE)
+          | (_, refs) => (F, fs, refs, NONE))
+       | _ => (F, add_stderr fs msg_usage, refs, NONE)`;
 
 (* ------------------------------------------------------------------------- *)
 (* Specs imply that invariants are preserved.                                *)
@@ -1743,12 +1743,14 @@ val process_line_inv = Q.store_thm("process_line_inv",
    \\ rpt (disch_then drule) \\ rw []);
 
 val reader_proves = Q.store_thm("reader_proves",
-  `reader_main fs init_refs cl = (T,outp,refs)
+  `reader_main fs init_refs cl = (T,outp,refs,sopt)
    ==>
-   ?s ctxt.
-     (!asl c. MEM (Sequent asl c) s.thms ==> (thyof ctxt, asl) |- c) /\
-     outp = add_stdout fs (msg_success s ctxt) /\
-     ctxt extends init_ctxt`,
+   ?s.
+     sopt = SOME s /\
+     (!asl c.
+        MEM (Sequent asl c) s.thms ==> (thyof refs.the_context, asl) |- c) /\
+     outp = add_stdout fs (msg_success s refs.the_context) /\
+     refs.the_context extends init_ctxt`,
   rw [reader_main_def, case_eq_thms, read_file_def, bool_case_eq, PULL_EXISTS]
   \\ imp_res_tac init_reader_ok
   \\ `READER_STATE defs init_state` by fs [READER_STATE_init_state]
@@ -1758,9 +1760,7 @@ val reader_proves = Q.store_thm("reader_proves",
   \\ first_x_assum (assume_tac o REWRITE_RULE [THM_def] o
                     Q.GENL [`a`,`b`] o Q.SPEC `Sequent a b`)
   \\ fs [STATE_def, CONTEXT_def] \\ rveq
-  \\ CONV_TAC SWAP_EXISTS_CONV
-  \\ qexists_tac `ds ++ refs'.the_context` \\ fs []
-  \\ metis_tac []);
+  \\ fs [EQ_SYM_EQ]);
 
 val _ = export_theory();
 

candle/standard/opentheory/readerSoundnessScript.sml

@@ -9,23 +9,25 @@ val reader_sound = Q.store_thm("reader_sound",
    is_set_theory ^mem ==>
    (* if the reader completes a successful run (executes all commands *)
    (* in the article file) when started from the initial candle state *)
-   reader_main fs init_refs cl = (T,outp,refs)
+   reader_main fs init_refs cl = (T,outp,refs,fstate)
    ==>
    (* then there is a final state s for the reader and a final context *)
-   (* ctxt for the candle kernel, and ...                              *)
-   ?s ctxt.
+   (* refs.the_context for the candle kernel, and ...                  *)
+   ?s.
+     fstate = SOME s /\
      (* anything on the reader theorem stack in the final state s is a *)
-     (* theorem in the prover context ctxt, and ...                    *)
-     (!asl c. MEM (Sequent asl c) s.thms ==> (thyof ctxt, asl) |= c) /\
-     (* the context ctxt is the result of a series of legal updates to *)
+     (* theorem in the prover context refs.the_context, and ...        *)
+     (!asl c.
+        MEM (Sequent asl c) s.thms ==> (thyof refs.the_context, asl) |= c) /\
+     (* the context is the result of a series of legal updates to      *)
      (* the initial context.                                           *)
-     ctxt extends init_ctxt /\
+     refs.the_context extends init_ctxt /\
      (* the output consists of a message displaying the context and    *)
      (* the contents of the theorem stack.                             *)
-     outp = add_stdout fs (msg_success s ctxt)`,
+     outp = add_stdout fs (msg_success s refs.the_context)`,
   rpt strip_tac
   \\ drule (GEN_ALL reader_proves) \\ rw []
-  \\ Q.LIST_EXISTS_TAC [`s`,`ctxt`] \\ rw []
+  \\ rw []
   \\ irule proves_sound \\ fs []);
 
 val _ = export_theory ();

compiler/backend/proofs/word_allocProofScript.sml

@@ -3989,30 +3989,31 @@ val ssa_cc_trans_props = Q.prove(`
     (* Install *)
     (rpt gen_tac>> strip_tac>>
     simp[Once (GSYM markerTheory.Abbrev_def)]>>
-    qpat_x_assum`_= (_,_,_)` mp_tac>>LET_ELIM_TAC>>
-    fs[next_var_rename_def]>>rw[]>>
-    imp_res_tac list_next_var_rename_move_props_2>>
-    rw[]>>fs[]>>
-    rfs[]>>
-    qabbrev_tac`na2 = na''+2`>>
-    `is_alloc_var na2` by fs[Abbr`na2`,is_stack_var_flip]>>
-    rw[]>>
-    qmatch_asmsub_abbrev_tac`list_next_var_rename_move sss _ _ = _`>>
-    Q.ISPECL_THEN[`ls`,`sss`,`na''+6`] mp_tac list_next_var_rename_move_props>>
-    simp[]>>
-    `is_alloc_var (na2+4)` by metis_tac[is_alloc_var_add]>>
-    `na''+6 = na2+4` by fs[Abbr`na2`]>>
-    impl_tac>-
-      (simp[Abbr`sss`,Abbr`ssa_cut`]>>
-      match_mp_tac ssa_map_ok_extend>>
-      CONJ_TAC>-
-       (match_mp_tac ssa_map_ok_inter>>
-       fs[Abbr`na2`]>>
-       match_mp_tac (GEN_ALL ssa_map_ok_more)>>
-       asm_exists_tac>>fs[])>>
-      metis_tac[convention_partitions])>>
-    strip_tac>>
-    fs[Abbr`na2`,markerTheory.Abbrev_def])>>
+    qpat_x_assum`_= (_,_,_)` mp_tac>>LET_ELIM_TAC >>
+    ( (* multiple goals *)
+      fs[next_var_rename_def]>>rw[]>>
+      imp_res_tac list_next_var_rename_move_props_2>>
+      rw[]>>fs[]>>
+      rfs[]>>
+      qabbrev_tac`na2 = na''+2`>>
+      `is_alloc_var na2` by fs[Abbr`na2`,is_stack_var_flip]>>
+      rw[]>>
+      qmatch_asmsub_abbrev_tac`list_next_var_rename_move sss _ _ = _`>>
+      Q.ISPECL_THEN[`ls`,`sss`,`na''+6`] mp_tac list_next_var_rename_move_props>>
+      simp[]>>
+      `is_alloc_var (na2+4)` by metis_tac[is_alloc_var_add]>>
+      `na''+6 = na2+4` by fs[Abbr`na2`]>>
+      impl_tac>-
+        (simp[Abbr`sss`,Abbr`ssa_cut`]>>
+        match_mp_tac ssa_map_ok_extend>>
+        CONJ_TAC>-
+         (match_mp_tac ssa_map_ok_inter>>
+         fs[Abbr`na2`]>>
+         match_mp_tac (GEN_ALL ssa_map_ok_more)>>
+         asm_exists_tac>>fs[])>>
+        metis_tac[convention_partitions])>>
+      strip_tac>>
+      fs[Abbr`na2`,markerTheory.Abbrev_def]))>>
   strip_tac>-
     (* CBW *)
     (rw[]>>fs[])>>

compiler/bootstrap/compilation/x64/32/Makefile

@@ -3,7 +3,8 @@
 
 # To set the stack and heap directives available to your own
 # CakeML programs, use the --stack_size and --heap_size
-# command-line arguments to the CakeML compiler.
+# command-line arguments to the CakeML compiler. The unit of
+# measure for both arguments is mebibytes, i.e. 1024^2 bytes.
 
 # Build the CakeML compiler.
 cake: cake.o basis_ffi.o

compiler/bootstrap/compilation/x64/64/Makefile

@@ -6,7 +6,8 @@
 
 # To set the stack and heap directives available to your own
 # CakeML programs, use the --stack_size and --heap_size
-# command-line arguments to the CakeML compiler.
+# command-line arguments to the CakeML compiler. The unit of
+# measure for both arguments is mebibytes, i.e. 1024^2 bytes.
 
 # Build the CakeML compiler.
 cake: cake.o basis_ffi.o

compiler/bootstrap/translation/compiler64ProgScript.sml

@@ -8,6 +8,9 @@ val _ = new_theory"compiler64Prog";
 
 val _ = translation_extends "mipsProg";
 
+val _ = (ml_translatorLib.trace_timing_to
+    := SOME "compiler64Prog_translate_timing.txt")
+
 val () = Globals.max_print_depth := 15;
 
 val () = use_long_names := true;

compiler/compilerScript.sml

@@ -25,7 +25,7 @@ val _ = new_theory"compiler";
 val current_version_tm = mlstring_from_proc "git" ["rev-parse", "HEAD"]
 (*"*)
 val poly_version_tm = mlstring_from_proc "poly" ["-v"]
-val hol_version_tm = mlstring_from_proc_from Globals.HOLDIR "git" ["rev-parse", "HEAD"]
+val hol_version_tm = mlstring_from_proc "git" ["-C", Globals.HOLDIR, "rev-parse", "HEAD"]
 
 val date_str = Date.toString (Date.fromTimeUniv (Time.now ())) ^ " UTC\n"
 val date_tm = Term `strlit^(stringSyntax.fromMLstring date_str)`
@@ -388,7 +388,7 @@ val parse_target_32_def = Define`
     if rest = strlit"arm6" then INL (arm6_backend_config,arm6_export)
     else INR (concat [strlit"Unrecognized 32-bit target option: ";rest])`
 
-(* Default stack and heap limits *)
+(* Default stack and heap limits. Unit of measure is mebibytes, i.e. 1024^2B. *)
 val default_heap_sz_def = Define`
   default_heap_sz = 1000n`
 

developers/artefacts

@@ -2,3 +2,4 @@ compiler/bootstrap/compilation/x64/64/cake-x64-64.tar.gz
 compiler/bootstrap/compilation/x64/32/cake-x64-32.tar.gz
 unverified/sexpr-bootstrap/x64/64/cake-unverified-x64-64.tar.gz
 unverified/sexpr-bootstrap/x64/32/cake-unverified-x64-32.tar.gz
+compiler/bootstrap/translation/compiler64Prog_translate_timing.txt

developers/build-sequence

@@ -65,6 +65,7 @@ candle/standard/semantics
 candle/standard/monadic
 candle/standard/ml_kernel
 candle/standard/opentheory
+candle/standard/opentheory/compilation
 
 # examples and tests
 characteristic/examples

misc/preamble.sml

@@ -475,11 +475,6 @@ fun mlstring_from_proc cmd args =
     NONE => Term `NONE : mlstring option`
   | SOME s => Term `SOME (strlit ^(stringSyntax.fromMLstring s))`
 
-fun mlstring_from_proc_from dir cmd args =
-  case read_process (cmd, args, SOME dir) of
-    NONE => Term `NONE : mlstring option`
-  | SOME s => Term `SOME (strlit ^(stringSyntax.fromMLstring s))`
-
 (* ========================================================================= *)
 (* ========================================================================= *)
 

translator/ml_translatorLib.sig

@@ -148,6 +148,8 @@ sig
     val prove_EvalPatRel_fail : term ref
     val get_term :string -> term
 
+    val trace_timing_to : string option ref
+
     (* returns the induction theorem for the latest rec translation *)
     val latest_ind : unit -> thm