Open palmskog opened 5 years ago
What do you think of #111 ? Maybe we should just have a single binary with --input
and --output
modes?
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
?
If I'm not mistaken, we are aiming to have four forms of input to sercomp
:
.v
files): vernac
(?)sexp
(?).vo
files): vo
kenv
UGraph.t
: essentialConv_oracle.oracle
: I am not sure how important this is for type-checking / roundtripDeclarations.module_retroknowledge
: shouldn't matter a lot [I hope]Mod_subst.delta_resolver
: this seems importantUniv.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.
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.
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.
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 ())
Sure, done in #126
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:
.kenv
that drops many unnecessary parts of.vo
files, but can still be sent to the checkersercomp
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]sercomp
to support the.kenv
format with the--mode=check
option [for checking serialized kernel terms]