Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[feature request] Ability to save .vo file from coqtop/sertop #14117

Closed
JasonGross opened this issue Apr 15, 2021 · 3 comments
Closed

[feature request] Ability to save .vo file from coqtop/sertop #14117

JasonGross opened this issue Apr 15, 2021 · 3 comments
Labels
kind: feature New user-facing feature request or implementation.

Comments

@JasonGross
Copy link
Member

It seems that saving .vo files is done from

coq/vernac/library.mli

Lines 49 to 52 in 00391bd

val save_library_to :
'document todo_proofs ->
output_native_objects:bool ->
DirPath.t -> string -> Opaqueproof.opaquetab -> unit

which is called only from ccompile and

coq/stm/stm.mli

Lines 140 to 147 in 110921a

(* Saves on the disk a .vio corresponding to the current status:
- if the worker pool is empty, all tasks are saved
- if the worker proof is not empty, then it waits until all workers
are done with their current jobs and then dumps (or fails if one
of the completed tasks is a failure).
Note: the create_vos argument is used in the "-vos" mode, where the
proof tasks are not dumped into the output file. *)
val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc

which itself is called only from ccompile. So it seems there is not a way to save the .vo file at the end of a long coqtop session / from sertop.

This would be quite useful, for example, in HoTT/Coq-HoTT#1455 (comment), where being able to replace coqc by a script using serapi under the hood would cut the time spent on the CI job by 33% (because we'd no longer need to compile each file both with coqc to get the .vo file for files depending on it and also with alectryon to record the playback).

cc @cpitclaudel @ejgallego
@JasonGross JasonGross added the kind: feature New user-facing feature request or implementation. label Apr 15, 2021
@ejgallego
Copy link
Member

SerAPI does certainly support this but I am unsure if interactively in the main branch yet, as the plan was to include it in the fix for ejgallego/coq-serapi#49 ; adding such support is trivial so please open an issue in the coq-serapi repos and I will push the fix for #49 including the save command.

@ejgallego
Copy link
Member

Note that sercomp & friends do already have the ability to generate .vo files.

@JasonGross JasonGross mentioned this issue Apr 15, 2021
Closed
@ejgallego
Copy link
Member

Indeed this is supported in both coq-lsp and sertop, so closing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: feature New user-facing feature request or implementation.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JasonGross @ejgallego