Add tracing kernel

.gitignore

@@ -5,6 +5,8 @@
 *.uo
 *.ui
 *.o
+*.tr
+*.tr.gz
 .hollogs
 .holobjs
 .HOLMK

Manual/Developers/developers.md

@@ -112,6 +112,9 @@ The experimental kernel can be selected by passing the `--expk` option to `build
 The *OpenTheory kernel* is based on the experimental kernel, but adds proof-logging to the primitive inference rules so that OpenTheory theory packages can be exported from HOL.
 This kernel can be selected by passing the `--otknl` option to `build`.
 
+The *tracing kernel* uses the same proof-logging to the primitive inference rules as OpenTheory, but exports inference rules without additional translation.
+This kernel can be selected by passing the `--trknl` option to `build`.
+
 ## Build Sequences
 
 When `build` runs, it choreographs its calls to `Holmake` by referring to a specified sequence of directories.

developers/git-regression-build.sh

@@ -66,7 +66,7 @@ else
     die "ML system \"$ML\" is not executable."
 fi
 
-case $kernel in --expk | --stdknl | --otknl ) : ;; * ) die "Bad kernel spec \"$kernel\"."
+case $kernel in --expk | --stdknl | --otknl | --trknl) : ;; * ) die "Bad kernel spec \"$kernel\"."
 esac
 
 if git pull > update-log 2>&1

src/portableML/Portable.sig

@@ -260,4 +260,5 @@ sig
   end
 
   val reraise : exn -> 'a
+  val export : string * 'a -> unit
 end

src/postkernel/Theory.sml

@@ -1031,6 +1031,7 @@ fun export_theory () = let
         theory_out (TheoryPP.pp_sig (!pp_thm) sigthry) ostrm1;
         theory_out (TheoryPP.pp_struct structthry) ostrm2;
         theory_out (TheoryPP.pp_thydata structthry) ostrm3;
+        Tracing.trace_theory name structthry;
         mesg "done.\n";
         if !report_times then
           (mesg ("Theory "^Lib.quote thyname^" took "^ tstr ^ " to build\n");

src/thm/Holmakefile

@@ -21,6 +21,14 @@ NET_UOD = $(dprot $(SIGOBJ)/Net.uo)
 all: $(patsubst %.sml,%.uo,$(wildcard *.sml)) Thm.uo
 
 ifeq ($(KERNELID),otknl)
+Thm.sml: otknl-thm.ML
+	$(CP) $< $@
+
+Thm-sig.sml: otknl-thmsig.ML
+	$(CP) $< $@
+
+else ifeq ($(KERNELID),trknl)
+
 Thm.sml: otknl-thm.ML
 	$(CP) $< $@
 

src/tracing/no/Tracing.sig

@@ -0,0 +1,6 @@
+signature Tracing =
+sig
+
+val trace_theory : string -> TheoryPP.struct_info_record -> unit
+
+end

src/tracing/no/Tracing.sml

@@ -0,0 +1,6 @@
+structure Tracing :> Tracing =
+struct
+
+fun trace_theory _ _ = ()
+
+end

src/tracing/yes/Tracing.sig

@@ -0,0 +1,6 @@
+signature Tracing =
+sig
+
+val trace_theory : string -> TheoryPP.struct_info_record -> unit
+
+end

src/tracing/yes/Tracing.sml

@@ -0,0 +1,21 @@
+structure Tracing :> Tracing =
+struct
+
+open TheoryPP
+
+fun export (file, x: 'a) = let
+  val _ = PolyML.shareCommonData x
+  val body = PolyML.exportSmall x
+  val ostream = BinIO.openOut file
+  val () = BinIO.output (ostream, body)
+  val () = BinIO.closeOut ostream
+in () end
+
+fun trace_theory name
+    ({theory,parents,types,constants,axioms,definitions,theorems,mldeps,...}: struct_info_record) = let
+  val file = concat[".holobjs/",name,".tr"]
+  val () = export(file, (theory,parents,types,constants,axioms,definitions,theorems,mldeps))
+  val _ = Unix.execute ("/usr/bin/gzip", ["-f", file])
+in () end
+
+end

tools/buildcline.sml

@@ -144,6 +144,8 @@ val cline_opt_descrs = [
    desc = mkBoolOpt #build_theory_graph false},
   {help = "build with logging kernel", long = ["otknl"], short = "",
    desc = setKname "--otknl"},
+  {help = "build with tracing kernel", long = ["trknl"], short = "",
+   desc = setKname "--trknl"},
   {help = "do relocation build (e.g., after a cleanForReloc)",
    long = ["relocbuild"], short = "",
    desc = mkBool #relocbuild true},

tools/buildutils.sml

@@ -104,6 +104,7 @@ fun read_buildsequence {kernelname} bseq_fname = let
         "stdknl" => "0"
       | "expk" => "experimental-kernel"
       | "otknl" => "0"
+      | "trknl" => "0"
       | _ => die ("Bad kernelname: "^kernelname)
     ]
   val readline = TextIO.inputLine
@@ -344,12 +345,12 @@ fun get_cline () = let
           SOME s => String.extract(s,2,NONE)
         | NONE =>
           (case
-              List.find (fn s => mem s ["--expk", "--otknl", "--stdknl"])oldopts
+              List.find (fn s => mem s ["--expk", "--otknl", "--stdknl", "--trknl"]) oldopts
              of
                 NONE => "stdknl"
               | SOME s =>
                 (warn ("Using kernel spec "^s^ " from earlier build command;\n\
-                       \    use one of --expk, --stdknl, --otknl to override");
+                       \    use one of --expk, --stdknl, --otknl, --trknl to override");
                  String.extract(s,2,NONE)))
   val _ = write_kernelid knlspec
   val buildgraph =
@@ -519,7 +520,7 @@ fun cleanForReloc0 HOLDIR =
 fun maybe_gmakeclean dirname owise () =
     if OS <> "winNT" then
       let
-        val gnumake = 
+        val gnumake =
             case List.rev (#arcs (OS.Path.fromString dirname)) of
               "minisat" :: "sat_solvers" :: "HolSat" :: "src" :: _ => true
             | "zc2hs" :: "sat_solvers" :: "HolSat" :: "src" :: _ => true
@@ -912,6 +913,7 @@ fun process_cline () =
                   Binaryset.empty cmp |> add "stdknl" dfltbuildseq
                                       |> add "expk" knlseq
                                       |> add "otknl" knlseq
+                                      |> add "trknl" dfltbuildseq
             in
               Binaryset.listItems alldirs
             end

tools/sequences/core-theories

@@ -26,6 +26,7 @@ src/num/theories/cv_compute
 # NOTE: otknl builds use the old Arithconv for proof constructions
 (stdknl)src/num/reduce/conv
 (expk)src/num/reduce/conv
+(trknl)src/num/reduce/conv
 (otknl)src/num/reduce/conv-old
 
 src/num/reduce/src

tools/sequences/kernel

@@ -18,6 +18,11 @@ src/portableML/monads
 src/prekernel
 **KERNEL**
 src/thm
+(stdknl)src/tracing/no
+(expk)src/tracing/no
+[poly](trknl)src/tracing/yes
+[mosml](trknl)src/tracing/no
+(otknl)src/tracing/no
 src/postkernel
 # these three directories are required to even run hol.bare.unquote
 src/parse