From 1013e52d5a7ce5c6b50b980a448255c9e39d16cf Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Sat, 20 Sep 2025 14:56:42 +0200
Subject: [PATCH 1/2] Use no_sig_docs instead of TheoryPP.include_docs

---
 basis/pure/basis_cvScript.sml                            | 3 +--
 compiler/bootstrap/translation/ag32ProgScript.sml        | 3 +--
 compiler/bootstrap/translation/arm7ProgScript.sml        | 3 +--
 compiler/bootstrap/translation/arm8ProgScript.sml        | 3 +--
 compiler/bootstrap/translation/basis_defProgScript.sml   | 3 +--
 compiler/bootstrap/translation/caml_lexProgScript.sml    | 3 +--
 compiler/bootstrap/translation/caml_parserProgScript.sml | 3 +--
 compiler/bootstrap/translation/compiler32ProgScript.sml  | 3 +--
 compiler/bootstrap/translation/compiler64ProgScript.sml  | 3 +--
 compiler/bootstrap/translation/decodeProgScript.sml      | 3 +--
 compiler/bootstrap/translation/explorerProgScript.sml    | 3 +--
 compiler/bootstrap/translation/inferProgScript.sml       | 3 +--
 compiler/bootstrap/translation/lexerProgScript.sml       | 3 +--
 compiler/bootstrap/translation/mipsProgScript.sml        | 3 +--
 compiler/bootstrap/translation/pancake_lexProgScript.sml | 3 +--
 compiler/bootstrap/translation/parserProgScript.sml      | 3 +--
 compiler/bootstrap/translation/printingProgScript.sml    | 3 +--
 compiler/bootstrap/translation/reg_allocProgScript.sml   | 3 +--
 compiler/bootstrap/translation/riscvProgScript.sml       | 3 +--
 compiler/bootstrap/translation/to_bviProgScript.sml      | 3 +--
 compiler/bootstrap/translation/to_bvlProgScript.sml      | 3 +--
 compiler/bootstrap/translation/to_closProgScript.sml     | 3 +--
 compiler/bootstrap/translation/to_dataProgScript.sml     | 3 +--
 compiler/bootstrap/translation/to_flatProgScript.sml     | 3 +--
 compiler/bootstrap/translation/to_target32ProgScript.sml | 3 +--
 compiler/bootstrap/translation/to_target64ProgScript.sml | 3 +--
 compiler/bootstrap/translation/to_word32ProgScript.sml   | 3 +--
 compiler/bootstrap/translation/to_word64ProgScript.sml   | 3 +--
 compiler/bootstrap/translation/x64ProgScript.sml         | 3 +--
 compiler/encoders/arm7/arm7_eval_encodeScript.sml        | 3 +--
 compiler/encoders/x64/x64_eval_encodeScript.sml          | 3 +--
 compiler/inference/infer_cvScript.sml                    | 3 +--
 compiler/inference/tests/basisTypeCheckScript.sml        | 3 +--
 compiler/repl/repl_init_typesScript.sml                  | 3 +--
 cv_translator/backend_32_cvScript.sml                    | 3 +--
 cv_translator/backend_64_cvScript.sml                    | 3 +--
 cv_translator/backend_ag32_cvScript.sml                  | 3 +--
 cv_translator/backend_arm8_cvScript.sml                  | 3 +--
 cv_translator/backend_cvScript.sml                       | 3 +--
 cv_translator/backend_x64_cvScript.sml                   | 3 +--
 cv_translator/to_data_cvScript.sml                       | 3 +--
 41 files changed, 41 insertions(+), 82 deletions(-)

diff --git a/basis/pure/basis_cvScript.sml b/basis/pure/basis_cvScript.sml
index 49038ec35b..005aaf631b 100644
--- 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
index 297b6daf68..71ae36af56 100644
--- 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
index dfa8057904..25e8a95eb1 100644
--- 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
index ac65179bdc..23066958ff 100644
--- 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
index 6c042d7690..aac5ce00e1 100644
--- 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
index 4fca1c36bc..093f1ce40d 100644
--- 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
index 9e1ac44c04..4b54969c9c 100644
--- 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
index 765f50d688..bcd3695a0e 100644
--- 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
index 16e05c47d1..c3d0b410bb 100644
--- 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
index 30fa9a22d0..3ddff4d2cb 100644
--- 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
index ff2ce94efb..fa6003131e 100644
--- 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
index fa16b8bca1..ccc2781e26 100644
--- 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
index cabae9e34f..b406f59571 100644
--- 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
index 7099a61b87..140f684053 100644
--- 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
index d0f8f308e4..6b684e3967 100644
--- 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
index 3e1d6b4701..29de69b126 100644
--- 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
index 4adecfe8d8..89e8bec3ac 100644
--- 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
index 5d91833e67..85a12d8630 100644
--- 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
index 9d83a9cc88..a1c6f7a22e 100644
--- 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
index 3831556507..1e53680841 100644
--- 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
index 60c897fd1c..092080fde5 100644
--- 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
index 6ba6974eaa..380c320c91 100644
--- 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
index 7d550d7fde..ff0c728472 100644
--- 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
index f425a30dce..bfeb8edc6e 100644
--- 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;
diff --git a/compiler/bootstrap/translation/to_target32ProgScript.sml b/compiler/bootstrap/translation/to_target32ProgScript.sml
index d37d7d13c9..c0f615d3f6 100644
--- a/compiler/bootstrap/translation/to_target32ProgScript.sml
+++ b/compiler/bootstrap/translation/to_target32ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the final part of the compiler backend for 32-bit targets.
 *)
-Theory to_target32Prog
+Theory to_target32Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator to_word32Prog std_prelude word_to_stack
   stack_alloc stack_remove stack_names stack_to_lab lab_filter
@@ -399,7 +399,6 @@ val res = presLangTheory.stack_prog_to_display_def |> spec32
           |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
 val res = presLangTheory.stack_fun_to_display_def |> spec32 |> translate;
 
-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_target64ProgScript.sml b/compiler/bootstrap/translation/to_target64ProgScript.sml
index e52c7eb9f5..2ea532c4f3 100644
--- a/compiler/bootstrap/translation/to_target64ProgScript.sml
+++ b/compiler/bootstrap/translation/to_target64ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the final part of the compiler backend for 64-bit targets.
 *)
-Theory to_target64Prog
+Theory to_target64Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator to_word64Prog std_prelude word_to_stack
   stack_alloc stack_remove stack_names stack_to_lab lab_filter
@@ -400,7 +400,6 @@ val res = presLangTheory.stack_prog_to_display_def |> spec64
           |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
 val res = presLangTheory.stack_fun_to_display_def |> spec64 |> translate;
 
-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_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml
index 72fa71d695..aec9496345 100644
--- a/compiler/bootstrap/translation/to_word32ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word32ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the data_to_word part of the 32-bit compiler.
 *)
-Theory to_word32Prog
+Theory to_word32Prog[no_sig_docs]
 Ancestors
   ml_translator basis_defProg std_prelude data_to_word word_simp
   word_alloc word_inst backend[qualified]
@@ -710,7 +710,6 @@ val r = presLangTheory.word_prog_to_display_def
 
 val r = presLangTheory.word_fun_to_display_def |> conv32 |> translate
 
-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_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml
index 90fd40f29a..f1930ef39f 100644
--- a/compiler/bootstrap/translation/to_word64ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word64ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the data_to_word part of the 64-bit compiler.
 *)
-Theory to_word64Prog
+Theory to_word64Prog[no_sig_docs]
 Ancestors
   ml_translator printingProg std_prelude data_to_word word_simp
   word_alloc word_inst backend[qualified]
@@ -704,7 +704,6 @@ val r = presLangTheory.word_prog_to_display_def
 
 val r = presLangTheory.word_fun_to_display_def |> conv64 |> translate
 
-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/x64ProgScript.sml b/compiler/bootstrap/translation/x64ProgScript.sml
index e8cd814d0c..2a5c492d1d 100644
--- a/compiler/bootstrap/translation/x64ProgScript.sml
+++ b/compiler/bootstrap/translation/x64ProgScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate the x64 instruction encoder and x64-specific config.
 *)
-Theory x64Prog
+Theory x64Prog[no_sig_docs]
 Ancestors
   evaluate ml_translator from_pancake64Prog x64_target x64
 Libs
@@ -540,7 +540,6 @@ val res = translate def;
 
 Theorem x64_config_v_thm[allow_rebind] = translate (x64_config_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/encoders/arm7/arm7_eval_encodeScript.sml b/compiler/encoders/arm7/arm7_eval_encodeScript.sml
index ff4f77a5bf..1016502aeb 100644
--- a/compiler/encoders/arm7/arm7_eval_encodeScript.sml
+++ b/compiler/encoders/arm7/arm7_eval_encodeScript.sml
@@ -1,12 +1,11 @@
 (* --------------------------------------------------------------------------
    Pre-evaluate encoder (to help speed up EVAL)
    -------------------------------------------------------------------------- *)
-Theory arm7_eval_encode
+Theory arm7_eval_encode[no_sig_docs]
 Ancestors
   arm arm7_target alignment
 
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0
 
 local
   val n = ["skip", "const", "binop reg", "binop imm", "shift", "div",
diff --git a/compiler/encoders/x64/x64_eval_encodeScript.sml b/compiler/encoders/x64/x64_eval_encodeScript.sml
index d843aa9c4a..6e72a08aca 100644
--- a/compiler/encoders/x64/x64_eval_encodeScript.sml
+++ b/compiler/encoders/x64/x64_eval_encodeScript.sml
@@ -1,11 +1,10 @@
 (*
   Pre-evaluate encoder (to help speed up EVAL)
 *)
-Theory x64_eval_encode
+Theory x64_eval_encode[no_sig_docs]
 Ancestors
   x64 x64_target
 
-val () = Feedback.set_trace "TheoryPP.include_docs" 0
 
 Triviality not_fail:
   (case a ++ b :: c of [] => x64_dec_fail | v2::v3 => v2::v3) =
diff --git a/compiler/inference/infer_cvScript.sml b/compiler/inference/infer_cvScript.sml
index 86280d8009..a56fc86ddd 100644
--- a/compiler/inference/infer_cvScript.sml
+++ b/compiler/inference/infer_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translating inferTheory to cv equations for use with cv_eval
 *)
-Theory infer_cv
+Theory infer_cv[no_sig_docs]
 Ancestors
   misc ast namespace infer inferProps basis_cv unify_cv
 Libs
@@ -410,4 +410,3 @@ val _ = cv_auto_trans (infertype_prog_inc_eq |> SRULE [extend_dec_ienv_def]);
 (* main results stored as: cv_infertype_prog_thm
                            cv_infertype_prog_inc_thm *)
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/compiler/inference/tests/basisTypeCheckScript.sml b/compiler/inference/tests/basisTypeCheckScript.sml
index 3419097784..8c0826cc45 100644
--- a/compiler/inference/tests/basisTypeCheckScript.sml
+++ b/compiler/inference/tests/basisTypeCheckScript.sml
@@ -3,7 +3,7 @@
   type inferencer. This file also acts as a test of cv_compute
   evaluation of the type inferencer.
 *)
-Theory basisTypeCheck
+Theory basisTypeCheck[no_sig_docs]
 Ancestors
   basisProg infer_cv
 Libs
@@ -33,4 +33,3 @@ val print_types = let
   val _ = print "\n"
   in () end
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/compiler/repl/repl_init_typesScript.sml b/compiler/repl/repl_init_typesScript.sml
index 7de6fe0130..f99c64148e 100644
--- a/compiler/repl/repl_init_typesScript.sml
+++ b/compiler/repl/repl_init_typesScript.sml
@@ -3,7 +3,7 @@
   Candle kernel and REPL module, i.e. everything in the user-visible
   initial environment of the read-eval-print loop.
 *)
-Theory repl_init_types
+Theory repl_init_types[no_sig_docs]
 Ancestors
   infer_cv repl_moduleProg repl_check_and_tweak
 Libs
@@ -98,4 +98,3 @@ Proof
   rewrite_tac [Repl_charsFrom_lemma]
 QED
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/backend_32_cvScript.sml b/cv_translator/backend_32_cvScript.sml
index 53c9e51335..88e6afc687 100644
--- a/cv_translator/backend_32_cvScript.sml
+++ b/cv_translator/backend_32_cvScript.sml
@@ -4,7 +4,7 @@
 
 (* The following line is (and shall remain) the only difference between
    the 32-bit and 64-bit versions of this file. *)
-Theory backend_32_cv
+Theory backend_32_cv[no_sig_docs]
 Ancestors
   cv_std backend_cv to_data_cv backend
 Libs
@@ -574,4 +574,3 @@ QED
 
 val _ = word_allocTheory.get_heuristics_def |> arch_spec |> cv_auto_trans;
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/backend_64_cvScript.sml b/cv_translator/backend_64_cvScript.sml
index 4debddf481..7b29d5be5d 100644
--- a/cv_translator/backend_64_cvScript.sml
+++ b/cv_translator/backend_64_cvScript.sml
@@ -4,7 +4,7 @@
 
 (* The following line is (and shall remain) the only difference between
    the 32-bit and 64-bit versions of this file. *)
-Theory backend_64_cv
+Theory backend_64_cv[no_sig_docs]
 Ancestors
   cv_std backend_cv to_data_cv backend
 Libs
@@ -574,4 +574,3 @@ QED
 
 val _ = word_allocTheory.get_heuristics_def |> arch_spec |> cv_auto_trans;
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/backend_ag32_cvScript.sml b/cv_translator/backend_ag32_cvScript.sml
index 3d44f99fd5..3e1831f6e3 100644
--- a/cv_translator/backend_ag32_cvScript.sml
+++ b/cv_translator/backend_ag32_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate ag32-specialised functions to cv equations.
 *)
-Theory backend_ag32_cv
+Theory backend_ag32_cv[no_sig_docs]
 Ancestors
   cv_std backend_cv backend_32_cv backend_ag32 ag32 ag32_target
   to_data_cv export_ag32 ag32_config
@@ -189,4 +189,3 @@ Proof
   irule backendTheory.set_asm_conf_id \\ EVAL_TAC
 QED
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/backend_arm8_cvScript.sml b/cv_translator/backend_arm8_cvScript.sml
index 1624ef64b5..8a076adf0b 100644
--- a/cv_translator/backend_arm8_cvScript.sml
+++ b/cv_translator/backend_arm8_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate arm8-specialised functions to cv equations.
 *)
-Theory backend_arm8_cv
+Theory backend_arm8_cv[no_sig_docs]
 Ancestors
   cv_std backend_cv backend_64_cv backend_arm8 arm8 arm8_target
   to_data_cv export_arm8 arm8_config
@@ -319,4 +319,3 @@ Proof
   irule backendTheory.set_asm_conf_id \\ EVAL_TAC
 QED
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/backend_cvScript.sml b/cv_translator/backend_cvScript.sml
index 149c9c8b74..7ac3aee6e6 100644
--- a/cv_translator/backend_cvScript.sml
+++ b/cv_translator/backend_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate non-target-specific backend functions to cv equations.
 *)
-Theory backend_cv
+Theory backend_cv[no_sig_docs]
 Libs
   preamble cv_transLib
 Ancestors
@@ -1062,4 +1062,3 @@ QED
 
 val _ = cv_trans word_copyTheory.copy_prop_def;
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/backend_x64_cvScript.sml b/cv_translator/backend_x64_cvScript.sml
index 058bec62b7..8bb04a523a 100644
--- a/cv_translator/backend_x64_cvScript.sml
+++ b/cv_translator/backend_x64_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translate x64-specialised functions to cv equations.
 *)
-Theory backend_x64_cv
+Theory backend_x64_cv[no_sig_docs]
 Ancestors
   cv_std backend_cv backend_64_cv backend_x64 x64 x64_target
   to_data_cv export_x64 x64_config
@@ -304,4 +304,3 @@ Proof
   irule backendTheory.set_asm_conf_id \\ EVAL_TAC
 QED
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;
diff --git a/cv_translator/to_data_cvScript.sml b/cv_translator/to_data_cvScript.sml
index c0f6f3c6e3..534a5d5728 100644
--- a/cv_translator/to_data_cvScript.sml
+++ b/cv_translator/to_data_cvScript.sml
@@ -1,7 +1,7 @@
 (*
   Translation of the to_data compiler function.
 *)
-Theory to_data_cv
+Theory to_data_cv[no_sig_docs]
 Ancestors
   cv_std basis_cv backend backend_asm unify_cv infer_cv
 Libs
@@ -2950,4 +2950,3 @@ val _ = cv_auto_trans presLangTheory.word_prog_to_display_def;
 
 val _ = cv_auto_trans presLangTheory.stack_prog_to_display_def;
 
-val _ = Feedback.set_trace "TheoryPP.include_docs" 0;

From 4809f91a58f68e48a5f258d1b282dae03efca687 Mon Sep 17 00:00:00 2001
From: Daniel Nezamabadi <55559979+dnezam@users.noreply.github.com>
Date: Sat, 20 Sep 2025 14:39:07 +0200
Subject: [PATCH 2/2] Ban TheoryPP.include_docs

---
 developers/readme_gen.sml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/developers/readme_gen.sml b/developers/readme_gen.sml
index b2952f47c8..7c0ed7027b 100644
--- a/developers/readme_gen.sml
+++ b/developers/readme_gen.sml
@@ -54,7 +54,8 @@ val ILLEGAL_STRINGS =
    ("Hol_corel"^"n`","Use CoInductive ... End instead of old Hol_coreln."),
    (* HACK Stop readme_gen from flagging itself by using \ \ in strings *)
    ("new_\ \theory","Use Theory syntax instead of old new_\ \theory"),
-   ("export_\ \theory","Use Theory sytnax instead of old export_\ \theory")]
+   ("export_\ \theory","Use Theory sytnax instead of old export_\ \theory"),
+   ("TheoryPP.include_\ \docs","Add the no_sig_docs tag to the theory name instead of TheoryPP.include_\ \docs.")]
 
 (* Helper functions *)