[feature request] Ability to save .vo file from interactive session #238
Milestone
Comments
ejgallego
added a commit
that referenced
this issue
Apr 17, 2021
We introduce a new commmand: ```lisp (SaveDoc opts) ``` to save .vo files from an interactive session. `opts` are optional, and can be - `(sid s)`: save the document at a specific sentence - `(prefix_output_dir dir)` add a prefix to the `file.vo` to be saved. Note that Coq requires that the module name and the filename do match, thus in order to use this command `sertop` must be called with the `--topfile file.v` flag, otherwise `CannotSaveVo` will be raised. Closes #238
|
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 #239 |
ejgallego
added a commit
that referenced
this issue
Apr 17, 2021
We introduce a new commmand: ```lisp (SaveDoc opts) ``` to save .vo files from an interactive session. `opts` are optional, and can be - `(sid s)`: save the document at a specific sentence - `(prefix_output_dir dir)` add a prefix to the `file.vo` to be saved. Note that Coq requires that the module name and the filename do match, thus in order to use this command `sertop` must be called with the `--topfile file.v` flag, otherwise `CannotSaveVo` will be raised. Closes #238
ejgallego
added a commit
that referenced
this issue
Apr 17, 2021
We introduce a new commmand: ```lisp (SaveDoc opts) ``` to save .vo files from an interactive session. `opts` are optional, and can be - `(sid s)`: save the document at a specific sentence - `(prefix_output_dir dir)` add a prefix to the `file.vo` to be saved. Note that Coq requires that the module name and the filename do match, thus in order to use this command `sertop` must be called with the `--topfile file.v` flag, otherwise `CannotSaveVo` will be raised. Closes #238
|
Duplicate of #128 |
ejgallego
added a commit
that referenced
this issue
Apr 17, 2021
We introduce a new commmand: ```lisp (SaveDoc opts) ``` to save .vo files from an interactive session. `opts` are optional, and can be - `(sid s)`: save the document at a specific sentence - `(prefix_output_dir dir)` add a prefix to the `file.vo` to be saved. Note that Coq requires that the module name and the filename do match, thus in order to use this command `sertop` must be called with the `--topfile file.v` flag, otherwise `CannotSaveVo` will be raised. Closes #128 #238
|
Closed by #239 |
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jun 15, 2022
CHANGES:
- [serapi] New query `(Query () (LogicalPath file))` which will
return the logical path for a particular `.v` file
(@ejgallego, see also
cpitclaudel/alectryon#25)
- [serapi] new `(SaveDoc opts)` command supporting saving of .vo
files even when from interactive mode; note that using
`--topfile` is required (fixes rocq-archive/coq-serapi#238, @ejgallego, reported
by Jason Gross)
- [sertop] we don't link the OCaml `num` library anymore, this could
have some impact on plugins (@ejgallego)
- [nix] Added Nix support (rocq-archive/coq-serapi#249, fixes rocq-archive/coq-serapi#248, @Zimmi48, reported
by @nyraghu)
- [serapi] Fix COQPATH support: interpret paths as absolute (rocq-archive/coq-serapi#249, @Zimmi48)
- [serlib] Ignore `env` parameter in certain exceptions (rocq-archive/coq-serapi#254, fixes rocq-archive/coq-serapi#250,
@ejgallego, reported by @cpitclaudel)
- [sertop] New option `--omit_env` that will disable the serialization of
Coq's super heavy global environments (rocq-archive/coq-serapi#254 @ejgallego)
- [build] Test OCaml 4.12 (ejgallego/coq-serapi#257 @ejgallego)
- [sertop] Async mode was not working due to passing `-no-glob` to workers
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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
coqcby 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 withcoqcto get the.vofile for files depending on it and also with alectryon to record the playback).cc @cpitclaudel @ejgallego
Originally posted by @JasonGross in coq/coq#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 #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 coq/coq#14117 (comment)
The text was updated successfully, but these errors were encountered: