Add a command line option to print the Pancake news file

compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml

@@ -348,14 +348,18 @@ Theorem cake_extract_writes:
      (out = explode help_string) ∧ (err = "")
    else if has_version_flag (TL cl) then
      (out = explode current_build_info_str) ∧ (err = "")
-   else if has_pancake_flag (TL cl) then
-     let (cout, cerr) = compile_pancake_32 (TL cl) inp in
-     (out = explode (concat (append cout))) ∧
-     (err = explode cerr)
    else
-     let (cout, cerr) = compile_32 (TL cl) inp in
-     (out = explode (concat (append cout))) ∧
-     (err = explode cerr)
+     case parse_pancake_feature (TL cl) of
+       SOME rest => out = explode(print_bool(query_news rest)) ∧ err = ""
+     | NONE =>
+        if has_pancake_flag (TL cl) then
+          let (cout, cerr) = compile_pancake_32 (TL cl) inp in
+            (out = explode (concat (append cout))) ∧
+            (err = explode cerr)
+        else
+          let (cout, cerr) = compile_32 (TL cl) inp in
+            (out = explode (concat (append cout))) ∧
+            (err = explode cerr)
 Proof
   strip_tac
   \\ qabbrev_tac ‘fs = stdin_fs inp’
@@ -399,6 +403,39 @@ Proof
         \\ pop_assum mp_tac \\ rw[]
         \\ fs[])
       >- ( rw[] \\ rw[OPTREL_def]))))>>
+  reverse PURE_TOP_CASE_TAC
+  >- (simp[TextIOProofTheory.add_stdo_def]
+      \\ SELECT_ELIM_TAC
+      \\ simp[TextIOProofTheory.stdo_def]
+      \\ conj_tac
+      >- (
+       simp[stdin_fs_def]
+       \\ qexists_tac`implode""`
+       \\ simp[] )
+      \\ simp[Once stdin_fs_def, AFUPDKEY_def]
+      \\ Cases \\ simp[] \\ strip_tac \\ rveq
+      \\ pop_assum mp_tac
+      \\ simp[TextIOProofTheory.up_stdo_def]
+      \\ simp[fsFFITheory.fsupdate_def]
+      \\ simp[stdin_fs_def]
+      \\ rw[]
+      \\ (
+       drule (GEN_ALL extract_fs_extract_writes)
+       \\ simp[AFUPDKEY_ALOOKUP]
+       \\ disch_then match_mp_tac
+       \\ rw[fsFFIPropsTheory.inFS_fname_def]
+       \\ fs[]
+       >- (
+         fs[CaseEq"option",CaseEq"bool",FORALL_PROD]
+         \\ rw[] \\ CCONTR_TAC \\ fs[]
+         \\ rveq \\ fs[] )
+       >- (
+         pop_assum mp_tac
+         \\ rw[] \\ fs[] \\ rw[]
+         \\ pop_assum mp_tac \\ rw[]
+         \\ fs[])
+       >- ( rw[] \\ rw[OPTREL_def])))>>
+  simp[]>>
   IF_CASES_TAC>>fs[]
   \\ (simp[TextIOProofTheory.add_stdout_fastForwardFD, STD_streams_stdin_fs]
   \\ DEP_REWRITE_TAC[TextIOProofTheory.add_stderr_fastForwardFD]

compiler/bootstrap/translation/compiler32ProgScript.sml

@@ -389,6 +389,9 @@ 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 res = translate (newsTheory.query_news_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
+val res = translate parse_pancake_feature_def
+val res = translate print_bool_def
 
 Definition nonzero_exit_code_for_error_msg_def:
   nonzero_exit_code_for_error_msg e =
@@ -422,18 +425,24 @@ Quote add_cakeml:
         print compiler_help_string
       else if compiler_has_version_flag cl then
         print compiler_current_build_info_str
-      else if compiler_has_pancake_flag cl then
-        case compiler_compile_pancake_32 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
-          (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
-                     compiler32prog_nonzero_exit_code_for_error_msg e)
       else
-        case compiler_compile_32 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
-          (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
-                     compiler32prog_nonzero_exit_code_for_error_msg e)
+        case compiler_parse_pancake_feature cl of
+          Some rest => print (compiler_print_bool(news_query_news rest))
+        | None =>
+            if compiler_has_pancake_flag cl then
+              case compiler_compile_pancake_32 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
+                (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
+                           compiler32prog_nonzero_exit_code_for_error_msg e)
+            else
+              case compiler_compile_32 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
+                (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
+                           compiler32prog_nonzero_exit_code_for_error_msg e)
     end
 End
 
 val main_v_def = fetch "-" "main_v_def";
+val compiler_help_string_v_thm = fetch "-" "compiler_help_string_v_thm";
+val compiler_current_build_info_str_v_thm = fetch "-" "compiler_current_build_info_str_v_thm";
 
 Theorem main_spec:
    IS_SOME (stdin_content fs) ⇒
@@ -476,29 +485,30 @@ Proof
    (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`
+    \\ irule_at (Pos hd) compiler_help_string_v_thm
+    \\ qexists ‘fs’
     \\ xsimpl)
-  \\ xlet_auto >- xsimpl
+  \\ xlet_auto>-xsimpl
   \\ xif
-  >- (
-    simp[full_compile_32_def]
-    \\ xapp
-    \\ CONV_TAC SWAP_EXISTS_CONV
-    \\ qexists_tac `current_build_info_str`
-    \\ fs [compilerTheory.current_build_info_str_def,
-           fetch "-" "compiler_current_build_info_str_v_thm"]
-    \\ xsimpl
-    \\ rename1 `add_stdout _ (strlit string)`
-    \\ CONV_TAC SWAP_EXISTS_CONV
-    \\ qexists_tac`fs`
-    \\ xsimpl)
-  >> xlet_auto >- xsimpl
+  >- (xapp
+      \\ irule_at (Pos hd) compiler_current_build_info_str_v_thm
+      \\ qexists ‘fs’
+      \\ simp[full_compile_32_def]
+      \\ xsimpl)
+  \\ xlet_auto>-xsimpl
+  \\ gvs[oneline std_preludeTheory.OPTION_TYPE_def]
+  \\ reverse PURE_FULL_CASE_TAC
+  \\ gvs[]
+  >- (xmatch
+      \\ xlet_auto >- xsimpl
+      \\ xlet_auto >- xsimpl
+      \\ simp[full_compile_32_def]
+      \\ xapp
+      \\ first_assum $ irule_at $ Pos hd
+      \\ qexists ‘fs’
+      \\ xsimpl)
+  \\ xmatch
+  \\ xlet_auto >- xsimpl
   \\ rename [‘stdin fs inp pos’]
   \\ ‘stdin_content fs = SOME inp ∧ pos = 0’ by
     (gvs [stdin_def,get_file_content_def]
@@ -571,9 +581,12 @@ Proof
   \\ qmatch_goalsub_abbrev_tac`fs1 = _ with numchars := _`
   \\ qexists_tac`fs1`
   \\ reverse conj_tac >-
-   rw[Abbr`fs1`,full_compile_32_def,UNCURRY,
-      GSYM fastForwardFD_with_numchars,
-      GSYM add_stdo_with_numchars, with_same_numchars]
+   (rw[Abbr`fs1`,full_compile_32_def,UNCURRY,
+       GSYM fastForwardFD_with_numchars,
+       GSYM add_stdo_with_numchars, with_same_numchars]
+    \\ PURE_FULL_CASE_TAC
+    \\ rw[GSYM fastForwardFD_with_numchars,
+          GSYM add_stdo_with_numchars, with_same_numchars, UNCURRY])
   \\ simp [SEP_CLAUSES]
   \\ match_mp_tac (MP_CANON(MATCH_MP app_wgframe (UNDISCH main_spec)))
   \\ xsimpl

compiler/bootstrap/translation/compiler64ProgScript.sml

@@ -428,13 +428,16 @@ 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 res = translate (newsTheory.query_news_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
+val res = translate parse_pancake_feature_def
+val res = translate print_bool_def
 
 Definition nonzero_exit_code_for_error_msg_def:
-                                                 nonzero_exit_code_for_error_msg e =
-if compiler$is_error_msg e then
-  (let a = empty_ffi «nonzero_exit» in
-     ml_translator$force_out_of_memory_error ())
-else ()
+  nonzero_exit_code_for_error_msg e =
+  if compiler$is_error_msg e then
+    (let a = empty_ffi «nonzero_exit» in
+       ml_translator$force_out_of_memory_error ())
+  else ()
 End
 
 val res = translate compilerTheory.is_error_msg_def;
@@ -643,18 +646,24 @@ Quote add_cakeml:
       print compiler_help_string
     else if compiler_has_version_flag cl then
       print compiler_current_build_info_str
-    else if compiler_has_pancake_flag cl then
-      case compiler_compile_pancake_64 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
-        (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
-                   compiler64prog_nonzero_exit_code_for_error_msg e)
     else
-      case compiler_compile_64 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
-        (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
-                   compiler64prog_nonzero_exit_code_for_error_msg e)
+      case compiler_parse_pancake_feature cl of
+        Some rest => print (compiler_print_bool(news_query_news rest))
+      | None =>
+          if compiler_has_pancake_flag cl then
+            case compiler_compile_pancake_64 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
+              (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
+                         compiler64prog_nonzero_exit_code_for_error_msg e)
+          else
+            case compiler_compile_64 cl (String.explode (TextIO.inputAll (TextIO.openStdIn ())))  of
+              (c, e) => (print_app_list c; TextIO.output TextIO.stdErr e;
+                         compiler64prog_nonzero_exit_code_for_error_msg e)
   end
 End
 
 val main_v_def = fetch "-" "main_v_def";
+val compiler_help_string_v_thm = fetch "-" "compiler_help_string_v_thm";
+val compiler_current_build_info_str_v_thm = fetch "-" "compiler_current_build_info_str_v_thm";
 
 Theorem main_spec:
   ¬has_repl_flag (TL cl) ∧ IS_SOME (stdin_content fs) ⇒
@@ -698,7 +707,7 @@ Proof
     \\ CONV_TAC SWAP_EXISTS_CONV
     \\ qexists_tac `help_string`
     \\ fs [compilerTheory.help_string_def,
-           fetch "-" "compiler_help_string_v_thm"]
+           compiler_help_string_v_thm]
     \\ xsimpl
     \\ rename1 `add_stdout _ (strlit string)`
     \\ CONV_TAC SWAP_EXISTS_CONV
@@ -712,12 +721,25 @@ Proof
     \\ CONV_TAC SWAP_EXISTS_CONV
     \\ qexists_tac `current_build_info_str`
     \\ fs [compilerTheory.current_build_info_str_def,
-           fetch "-" "compiler_current_build_info_str_v_thm"]
+           compiler_current_build_info_str_v_thm]
     \\ xsimpl
     \\ rename1 `add_stdout _ (strlit string)`
     \\ CONV_TAC SWAP_EXISTS_CONV
     \\ qexists_tac`fs`
     \\ xsimpl)
+  \\ xlet_auto >- xsimpl
+  \\ gvs[oneline std_preludeTheory.OPTION_TYPE_def]
+  \\ reverse PURE_FULL_CASE_TAC
+  \\ gvs[]
+  >- (xmatch
+      \\ xlet_auto >- xsimpl
+      \\ xlet_auto >- xsimpl
+      \\ simp[full_compile_64_def]
+      \\ xapp
+      \\ first_assum $ irule_at $ Pos hd
+      \\ qexists ‘fs’
+      \\ xsimpl)
+  \\ xmatch
   >> xlet_auto>-xsimpl
   >> xif
   >-
@@ -797,9 +819,12 @@ Proof
   \\ qmatch_goalsub_abbrev_tac`fs1 = _ with numchars := _`
   \\ qexists_tac`fs1`
   \\ reverse conj_tac >-
-   rw[Abbr`fs1`,full_compile_64_def,UNCURRY,
-      GSYM fastForwardFD_with_numchars,
-      GSYM add_stdo_with_numchars, with_same_numchars]
+   (rw[Abbr`fs1`,full_compile_64_def,UNCURRY,
+       GSYM fastForwardFD_with_numchars,
+       GSYM add_stdo_with_numchars, with_same_numchars]
+    \\ PURE_FULL_CASE_TAC
+    \\ rw[GSYM fastForwardFD_with_numchars,
+          GSYM add_stdo_with_numchars, with_same_numchars, UNCURRY])
   \\ simp [SEP_CLAUSES]
   \\ match_mp_tac (MP_CANON(MATCH_MP app_wgframe (UNDISCH main_spec)))
   \\ xsimpl

compiler/compilerScript.sml

@@ -11,7 +11,7 @@ Ancestors
   export_x64 arm8_config export_arm8 riscv_config export_riscv
   mips_config export_mips arm7_config export_arm7 ag32_config
   export_ag32 panPtreeConversion pan_to_target panStatic
-  pan_passes
+  pan_passes news
 Libs
   preamble
 
@@ -82,6 +82,12 @@ OPTIONS:
 
   --pancake     takes a pancake program as input
 
+  --pancake_feature=T  here S can be any string denoting a Pancake feature tag.
+                Prints true or false depending on whether this
+                compiler binary supports feature T.
+                Tags are documented in the NEWS.md in the pancake/
+                subdirectory at code.cakeml.org
+
   --no_warn     silences pancake warning output
 
   --main_return=B   here B can be either true or false; the default is
@@ -343,6 +349,10 @@ Definition parse_bool_def:
   else NONE
 End
 
+Definition print_bool_def:
+  print_bool b = if b then «true» else «false»
+End
+
 (* Finds the first occurence of the flag and
   returns the rest of the string after it *)
 Definition find_str_def:
@@ -520,6 +530,13 @@ Definition parse_gc_def:
     else INR (concat [«Unrecognized GC option: »;rest])
 End
 
+Definition parse_pancake_feature_def:
+  parse_pancake_feature ls =
+  case find_str «--pancake_feature=» ls of
+    NONE => NONE
+  | SOME rest => SOME rest
+End
+
 (*
 EVAL ``parse_gc [«--gc=gen1234,1234,1234»] def``
 *)
@@ -763,13 +780,16 @@ Definition full_compile_64_def:
   else if has_version_flag cl then
     add_stdout fs current_build_info_str
   else
-    let (out, err) =
-        if has_pancake_flag cl then
-          compile_pancake_64 cl inp
-        else
-          compile_64 cl inp
-    in
-      add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err
+    case parse_pancake_feature cl of
+      SOME rest => add_stdout fs $ print_bool $ query_news rest
+    | NONE =>
+        let (out, err) =
+            if has_pancake_flag cl then
+              compile_pancake_64 cl inp
+            else
+              compile_64 cl inp
+        in
+          add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err
 End
 
 Definition compile_32_def:
@@ -839,11 +859,14 @@ Definition full_compile_32_def:
   else if has_version_flag cl then
     add_stdout fs current_build_info_str
   else
-    let (out, err) =
-        if has_pancake_flag cl then
-          compile_pancake_32 cl inp
-        else
-          compile_32 cl inp
-    in
-      add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err
+    case parse_pancake_feature cl of
+      SOME rest => add_stdout fs $ print_bool $ query_news rest
+    | NONE =>
+        let (out, err) =
+            if has_pancake_flag cl then
+              compile_pancake_32 cl inp
+            else
+              compile_32 cl inp
+        in
+          add_stderr (add_stdout (fastForwardFD fs 0) (concat (append out))) err
 End

developers/changes-since-release.md

@@ -8,6 +8,8 @@ Changes since release v3479:
 
 ## Pancake
 
+Queryable feature tags (#1470).
+
 ## Candle
 
 ## Examples