CakeML · tanyongkiam · Sep 26, 2025 · Sep 20, 2025 · Sep 20, 2025
diff --git a/basis/pure/basis_cvScript.sml b/basis/pure/basis_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translation of basis types and functions for use with cv_compute.
 *)
-Theory basis_cv
+Theory basis_cv[no_sig_docs]
 Ancestors
   cv_std
 Libs
@@ -51,4 +51,3 @@ QED
 val _ = cv_trans (mlintTheory.toString_def |> SRULE [Num_ABS]);
 val _ = cv_trans mlintTheory.num_to_str_def;
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/compiler/bootstrap/translation/ag32ProgScript.sml b/compiler/bootstrap/translation/ag32ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the ag32 instruction encoder and ag32-specific config.
 *)
-Theory ag32Prog
+Theory ag32Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator ag32_target ag32 arm7Prog[qualified]
 Libs
@@ -143,6 +143,5 @@ val res = translate def;
 
 val r = translate (format_def ag32_config_def);
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = (ml_translatorLib.clean_on_exit := true);
diff --git a/compiler/bootstrap/translation/arm7ProgScript.sml b/compiler/bootstrap/translation/arm7ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the ARMv7 instruction encoder and ARMv7-specific config.
 *)
-Theory arm7Prog
+Theory arm7Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator from_pancake32Prog arm7_target arm
   to_target32Prog[qualified]
@@ -485,7 +485,6 @@ val res = translate def;
 
 val res = translate (arm7_config_def |> SIMP_RULE std_ss[valid_immediate_def] |> gconv)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/arm8ProgScript.sml b/compiler/bootstrap/translation/arm8ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the ARMv8 instruction encoder and ARMv8-specific config.
 *)
-Theory arm8Prog
+Theory arm8Prog[no_sig_docs]
 Ancestors
   arm8_target arm8 evaluate ml_translator x64Prog
 Libs
@@ -515,7 +515,6 @@ val _ = translate (valid_immediate_def |> SIMP_RULE bool_ss
 Theorem arm8_config_v_thm[allow_rebind] =
   translate (arm8_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPTY]|> econv)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/basis_defProgScript.sml b/compiler/bootstrap/translation/basis_defProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the basis library term.
 *)
-Theory basis_defProg
+Theory basis_defProg[no_sig_docs]
 Ancestors
   ml_translator sexp_parserProg
 Libs
@@ -21,4 +21,3 @@ val res = translate basisProgTheory.basis_def;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/compiler/bootstrap/translation/caml_lexProgScript.sml b/compiler/bootstrap/translation/caml_lexProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translation of the OCaml lexer.
  *)
-Theory caml_lexProg
+Theory caml_lexProg[no_sig_docs]
 Ancestors
   caml_lex parserProg ml_translator
 Libs
@@ -170,6 +170,5 @@ val r = translate (caml_lexTheory.next_sym_def |> REWRITE_RULE [GSYM sub_check_d
 
 val r = translate caml_lexTheory.lexer_fun_def;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val () = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/caml_parserProgScript.sml b/compiler/bootstrap/translation/caml_parserProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translation of the functions in caml_parserScript.sml
  *)
-Theory caml_parserProg
+Theory caml_parserProg[no_sig_docs]
 Ancestors
   misc[qualified] camlPEG camlPtreeConversion caml_parser
   ml_translator caml_lexProg
@@ -300,6 +300,5 @@ QED
 
 val _ = update_precondition run_side;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val () = ml_translatorLib.clean_on_exit := true;
 
diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Finish translation of the 32-bit version of the compiler.
 *)
-Theory compiler32Prog
+Theory compiler32Prog[no_sig_docs]
 Ancestors
   compiler export ml_translator ag32Prog[qualified]
   arm7Prog[qualified] basis_ffi[qualified]
@@ -531,5 +531,4 @@ Theorem semantics_compiler32_prog =
   |> DISCH_ALL
   |> SIMP_RULE (srw_ss()) [AND_IMP_INTRO,GSYM CONJ_ASSOC]
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.reset_translation(); (* because this translation won't be continued *)
diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Finish translation of the 64-bit version of the compiler.
 *)
-Theory compiler64Prog
+Theory compiler64Prog[no_sig_docs]
 Ancestors
   mipsProg compiler export ml_translator basis_ffi[qualified]
 Libs
@@ -785,5 +785,4 @@ Theorem Decls_FRONT_compiler64_prog = th1
 
 Theorem LAST_compiler64_prog = EVAL “LAST compiler64_prog”;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.reset_translation(); (* because this translation won't be continued *)
diff --git a/compiler/bootstrap/translation/decodeProgScript.sml b/compiler/bootstrap/translation/decodeProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the compiler's state decoder.
 *)
-Theory decodeProg
+Theory decodeProg[no_sig_docs]
 Ancestors
   num_list_enc_dec num_tree_enc_dec backend_enc_dec explorerProg
   ml_translator
@@ -260,7 +260,6 @@ val res = translate backend_inc_config_dec_def;
 
 val res = translate decode_backend_config_def;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/explorerProgScript.sml b/compiler/bootstrap/translation/explorerProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the compiler explorer parts of the compiler.
 *)
-Theory explorerProg
+Theory explorerProg[no_sig_docs]
 Ancestors
   inferProg
 Libs
@@ -114,7 +114,6 @@ val r = presLangTheory.clos_to_display_def
 val r = translate presLangTheory.clos_dec_to_display_def;
 val r = translate presLangTheory.clos_to_strs_def;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/inferProgScript.sml b/compiler/bootstrap/translation/inferProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the compiler's type inferencer.
 *)
-Theory inferProg
+Theory inferProg[no_sig_docs]
 Ancestors
   parserProg reg_allocProg infer ml_translator semanticPrimitives
   inferProps
@@ -736,7 +736,6 @@ Theorem infertype_prog_side_thm = Q.prove(`
   \\ match_mp_tac (CONJUNCT2 infer_d_side_thm) \\ fs [])
   |> update_precondition;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/lexerProgScript.sml b/compiler/bootstrap/translation/lexerProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the compiler's lexer.
 *)
-Theory lexerProg
+Theory lexerProg[no_sig_docs]
 Ancestors
   lexer_fun lexer_impl to_dataProg ml_translator
 Libs
@@ -133,7 +133,6 @@ val lexer_fun_side = Q.prove(`
   ∀x. lexer_fun_side x ⇔ T`,
   EVAL_TAC>>fs[lexer_fun_aux_side]) |> update_precondition
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/mipsProgScript.sml b/compiler/bootstrap/translation/mipsProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the MIPS instruction encoder and MIPS-specific config.
 *)
-Theory mipsProg
+Theory mipsProg[no_sig_docs]
 Ancestors
   evaluate ml_translator riscvProg mips_target mips
 Libs
@@ -391,7 +391,6 @@ val res = translate def;
 Theorem mips_config_v_thm[allow_rebind] = translate
   (mips_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPTY]|> econv);
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/pancake_lexProgScript.sml b/compiler/bootstrap/translation/pancake_lexProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate pancake's lexer
 *)
-Theory pancake_lexProg
+Theory pancake_lexProg[no_sig_docs]
 Ancestors
   panLexer location caml_parserProg ml_translator
 Libs
@@ -135,7 +135,6 @@ QED
 
 val _ = update_precondition pancake_lex_side;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/parserProgScript.sml b/compiler/bootstrap/translation/parserProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the compiler's parser.
 *)
-Theory parserProg
+Theory parserProg[no_sig_docs]
 Ancestors
   cmlParse cmlPEG lexerProg ml_translator semanticPrimitives
 Libs
@@ -234,7 +234,6 @@ Theorem parse_prog_side_lemma = Q.prove(`
   THEN CONV_TAC (DEPTH_CONV ETA_CONV) THEN FULL_SIMP_TAC std_ss [])
   |> update_precondition;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/printingProgScript.sml b/compiler/bootstrap/translation/printingProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the pretty printing functions for the REPL
 *)
-Theory printingProg
+Theory printingProg[no_sig_docs]
 Ancestors
   infer[qualified] misc[qualified] ml_translator basis_defProg
   std_prelude printTweaks
@@ -133,7 +133,6 @@ val lemma5 = prove(“printtweaks_add_print_then_read_side x y = T”,
   |> update_precondition;
 
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/reg_allocProgScript.sml b/compiler/bootstrap/translation/reg_allocProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the compiler's register allocator.
 *)
-Theory reg_allocProg
+Theory reg_allocProg[no_sig_docs]
 Libs
   preamble ml_monad_translatorLib
 Ancestors
@@ -413,7 +413,6 @@ val res = translate apply_bij_on_clash_tree_def;
 val res = translate size_of_clash_tree_def;
 val res = translate linear_scan_reg_alloc_def;
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 (*
 TODO: update the following code (comes from the non-monadic register allocator

diff --git a/compiler/bootstrap/translation/riscvProgScript.sml b/compiler/bootstrap/translation/riscvProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the RISC-V instruction encoder and RISC-V-specific config.
 *)
-Theory riscvProg
+Theory riscvProg[no_sig_docs]
 Ancestors
   evaluate ml_translator arm8Prog riscv_target riscv
 Libs
@@ -380,7 +380,6 @@ val res = translate def;
 Theorem riscv_config_v_thm[allow_rebind] = translate
   (riscv_config_def |> SIMP_RULE bool_ss [IN_INSERT, NOT_IN_EMPTY]|> econv);
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 

diff --git a/compiler/bootstrap/translation/to_bviProgScript.sml b/compiler/bootstrap/translation/to_bviProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the backend phase from BVL to BVI.
 *)
-Theory to_bviProg
+Theory to_bviProg[no_sig_docs]
 Ancestors
   ml_translator to_bvlProg
 Libs
@@ -153,6 +153,5 @@ val r = translate bvl_to_bviTheory.bvl_to_bvi_compile_inc_all_def;
 
 (* ------------------------------------------------------------------------- *)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/to_bvlProgScript.sml b/compiler/bootstrap/translation/to_bvlProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the backend phase from closLang to BVL.
 *)
-Theory to_bvlProg
+Theory to_bvlProg[no_sig_docs]
 Ancestors
   ml_translator to_closProg backend[qualified]
 Libs
@@ -349,6 +349,5 @@ val res = translate clos_to_bvlTheory.clos_to_bvl_compile_inc_def
 
 (* ------------------------------------------------------------------------- *)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/to_closProgScript.sml b/compiler/bootstrap/translation/to_closProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the backend phase from flatLang to closLang.
 *)
-Theory to_closProg
+Theory to_closProg[no_sig_docs]
 Ancestors
   ml_translator to_flatProg flat_to_clos[qualified]
   clos_mti[qualified] clos_number[qualified]
@@ -418,6 +418,5 @@ val r = translate clos_ticksTheory.compile_inc_def;
 
 (* ------------------------------------------------------------------------- *)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/to_dataProgScript.sml b/compiler/bootstrap/translation/to_dataProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the backend phase from BVI to dataLang.
 *)
-Theory to_dataProg
+Theory to_dataProg[no_sig_docs]
 Ancestors
   ml_translator to_bviProg backend[qualified]
 Libs
@@ -104,6 +104,5 @@ val r = translate bvi_to_dataTheory.compile_prog_def;
 
 (* ------------------------------------------------------------------------- *)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = ml_translatorLib.clean_on_exit := true;
diff --git a/compiler/bootstrap/translation/to_flatProgScript.sml b/compiler/bootstrap/translation/to_flatProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate backend phases up to and including flatLang.
 *)
-Theory to_flatProg
+Theory to_flatProg[no_sig_docs]
 Ancestors
   ml_translator decProg source_to_flat[qualified]
   source_to_source[qualified]
@@ -158,6 +158,5 @@ val _ = (length (hyp res) = 0)
 
 (* ------------------------------------------------------------------------- *)
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 val _ = ml_translatorLib.clean_on_exit := true;