search

rocq-archive / coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Other
128 stars 39 forks source link

[feature request] Ability to save .vo file from interactive session #238

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

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 https://github.com/HoTT/HoTT/pull/1455#issuecomment-820528119, 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

Originally posted by @JasonGross in https://github.com/coq/coq/issues/14117

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 https://github.com/ejgallego/coq-serapi/issues/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.

Originally posted by @ejgallego in https://github.com/coq/coq/issues/14117#issuecomment-820631442

ejgallego commented 3 years ago

Was a bit tricky indeed as the current architecture needed some changes to handle initialization state, and not surprisingly the Coq usptream code path for saving a .vo from an interactive session had never been tested and was buggy.

PR implementing this here https://github.com/ejgallego/coq-serapi/pull/239

ejgallego commented 3 years ago

Duplicate of #128

ejgallego commented 3 years ago

Closed by #239