Serialization and deserialization of kernel terms and their environments

[palmskog]

We want to be able to serialize and deserialize environments with elaborated and fully typed kernel terms (Constr.t). More specifically, we want to be able to serialize (relevant data from) .vo files via the command line, and then be able to separately check the results.

Tasks:

• add all the necessary annotations to enable kernel term serialization, following 454815f and #118
• introduce a new "format" .kenv that drops many unnecessary parts of .vo files, but can still be sent to the checker
• extend sercomp with a new option --mode=env that takes a .vo or (even .v?) file as input and outputs sexps according to .kenv [for producing serialized kernel terms]
• extend sercomp to support the .kenv format with the --mode=check option [for checking serialized kernel terms]
• construct a small example with non-trivial terms that doesn't require the Coq prelude

[ejgallego]

What do you think of #111 ? Maybe we should just have a single binary with --input and --output modes?

[palmskog]

I think it's fine if we merge sercomp/compser, as long as we can provide a simple mapping, e.g., compser --mode=check f.sexp is equivalent to sercomp --input=sexp --output=check f.sexp. Maybe we keep --mode and just add --input?

[palmskog]

If I'm not mistaken, we are aiming to have four forms of input to sercomp:

• regular vernacular (.v files): vernac(?)
• sexp-serialized vernacular: sexp(?)
• OCaml-serialized kernel terms + data (.vo files): vo
• sexp-serialized kernel environments: kenv

[ejgallego]

#118 is ready, however there are still some parts missing; in particular:

• UGraph.t: essential
• Conv_oracle.oracle: I am not sure how important this is for type-checking / roundtrip
• Declarations.module_retroknowledge: shouldn't matter a lot [I hope]
• Mod_subst.delta_resolver: this seems important
• Univ.ContextSet.t: Pretty important too,
• Cemitcodes.to_patch_substituted: VM stuff, can be ignored for now,
• Mod_subst.substituted: No idea,

Good news is that most of the missing stuff can be done in parallel now.

Another problem is that Environ.environ is a private type, but Object.magic plus some cut and paste should save us like in the case for globals.

[ejgallego]

We also need to add the dumping option, but indeed I am thinking if it wouldn't make more sense a fine env-manipulation API. The whole env is really big I'm afraid.

For now we can see it using the (Query () Env) command.

[ejgallego]

I am realizing that we have a bit of a problem with the current "round-trip" idea.

The env type in Coq is private, so indeed it means that it is not meant to be fed to the type checker. We could do a roundtrip, but the kernel doesn't have the ability to check and env back; the env is supposed to be already checked.

So indeed they only way we can make the kernel check something is using a function such as:

val add_constant
  :  in_section:bool
  -> Label.t
  -> global_declaration
  -> env
  -> Constant.t * env

which basically extends env with the corresponding Declarations.constant_body. The input data is a bit different, in particular, it is of type Entries.definition_entry, which is the "unchecked" constant data.

Ummm, maybe this would be a good moment to schedule a call and discuss a bit more.

[palmskog]

No matter how the roundtrip will work in the end, I think we can at least go ahead and add an option to sercomp to serialize environments, so our side can understand a bit better what's going on. For example, in sercomp.ml, does it make sense to serialize the "final" environment:

let close_document ~mode ~doc ~in_file =
  let open Sertop_arg in
  match mode with
  | C_parse -> ()
  | C_sexp  -> ()
  | C_print -> ()
  | C_stats ->
    Sercomp_stats.print_stats ()
  | C_env ->
   (* ??? *)
  | C_check ->
    let _doc = Stm.join ~doc in
    check_pending_proofs ()
  | C_vo ->
    let _doc = Stm.join ~doc in
    check_pending_proofs ();
    let ldir = Stm.get_ldir ~doc in
    let out_vo = Filename.(remove_extension in_file) ^ ".vo" in
    Library.save_library_to ldir out_vo (Global.opaque_tables ())

[ejgallego]

Sure, done in #126