-
Notifications
You must be signed in to change notification settings - Fork 39
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Serialization and deserialization of kernel terms and their environments #119
Comments
What do you think of #111 ? Maybe we should just have a single binary with |
I think it's fine if we merge |
If I'm not mistaken, we are aiming to have four forms of input to
|
This commit adds preliminary support for kernel environments, mainly addressing the global maps; some comments: - We have to override the problem of private types using Obj.magic, this will imply another cut and paste when we upgrade Coq. - We don't support 2-way serialization yet due to `Environ.env` being a private type, we'll have to do as above. - We start to add some more interesting types w.r.t. serialization, including a `SerType` interface and a map functor. - We are still missing serialization of the universe map, and some other minor stuff. c.f. ejgallego#119 Co-authored-by: Kaiyu Yang <[email protected]>
#118 is ready, however there are still some parts missing; in particular:
Good news is that most of the missing stuff can be done in parallel now. Another problem is that |
This commit adds preliminary support for kernel environments, mainly addressing the global maps; some comments: - We have to override the problem of private types using Obj.magic, this will imply another cut and paste when we upgrade Coq. - We don't support 2-way serialization yet due to `Environ.env` being a private type, we'll have to do as above. - We start to add some more interesting types w.r.t. serialization, including a `SerType` interface and a map functor. - We are still missing serialization of the universe map, and some other minor stuff. c.f. ejgallego#119 Co-authored-by: Kaiyu Yang <[email protected]>
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 |
I am realizing that we have a bit of a problem with the current "round-trip" idea. The 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 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 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 |
CHANGES: * [serapi ] Add `Parse` command to parse a sentence; c.f. ejgallego/coq-serapi#117 (@ejgallego) (cc: @yangky11) * [sercomp] Add "print" `--mode` to print the input Coq document (@ejgallego) (cc: @Ptival) * [serlib ] Serialize `Universe.t` (@ejgallego, request by @yangky11) * [sercomp] Merge `sercomp` and `compser`, add `--input` parameter to `sercomp` (@palmskog) (cc: @ejgallego) * [serlib ] Much improved support for serialization of `Environ.env` (@yangky11 and @ejgallego c.f. ejgallego/coq-serapi#118) * [serapi ] Make sure every command ends with `Completed`, even if it produced an exception (@brando90 and @ejgallego c.f. ejgallego/coq-serapi#124) * [sercomp] Add `--mode=kexp` to output the final kernel environment. (@ejgallego c.f. ejgallego/coq-serapi#119) * [serlib ] Serialize more internal environment fields (@ejgallego c.f. ejgallego/coq-serapi#119) * [serlib ] Improvements in serialization org (@ejgallego) * [serlib ] Serialize kernel entries (@ejgallego @palmskog) * [serlib ] Fix critical bug on `Constr` deserialization; reported by @palmskog, fix by @SkySkimmer. * [sertop] Fix backtrace printing when using `--debug` (@ejgallego) * [serlib ] Don't serialize VM values (@ejgallego, bug report by @palmskog) * [serapi ] Output location on tokenization (@ejgallego , idea by @palmskog) * [serapi ] Add basic documentation of the protocol (@ejgallego cc ejgallego/coq-serapi#109)
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]The text was updated successfully, but these errors were encountered: