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

Missing conversion functions for types for the extraction plugin? #371

Closed
toku-sa-n opened this issue Nov 21, 2023 · 3 comments · Fixed by #375 or ocaml/opam-repository#25310
Closed

Missing conversion functions for types for the extraction plugin? #371

toku-sa-n opened this issue Nov 21, 2023 · 3 comments · Fixed by #375 or ocaml/opam-repository#25310

Comments

@toku-sa-n
Copy link
Contributor

toku-sa-n commented Nov 21, 2023 •
edited
Loading

Hi. While I was viewing serlib's document, I noticed that functions for converting between types for the extraction plugin (e.g., lang) and SExp were missing.

Is it okay to send a PR to implement them?
@ejgallego
Copy link
Owner

ejgallego commented Nov 21, 2023 •
edited
Loading

Hi @toku-sa-n !

Absolutely, a PR to fix this problem would be much welcome! I'd recommend you also add a test to the test suite.

Unfortunately we cannot do this automatically yet, see ejgallego/coq-lsp#761 for a discussion

@toku-sa-n
Copy link
Contributor Author

I may be missing something, but it seems that we need to modify the upstream Coq code to implement the functions because there are neither wit_* functions defined in Extraction_plugin nor types of 'a Genarg.genarg_type defined there. The G_extraction module where I think such functions are to be defined is empty.

Is it correct?

@ejgallego
Copy link
Owner

This is because the extraction.mli file was added. Because of that, it is now not possible to access the AST of extraction commands.

cc @SkySkimmer (coq/coq@99eae36)

ejgallego added a commit to ejgallego/coq that referenced this issue Nov 27, 2023
@ejgallego
[extraction] (re)-export AST witnesses.
0821be5 
Fix downfall of coq#17293 :/

cc: ejgallego/coq-serapi#371
@ejgallego ejgallego mentioned this issue Nov 27, 2023
Merged
@toku-sa-n toku-sa-n mentioned this issue Nov 29, 2023
Merged
SkySkimmer pushed a commit to SkySkimmer/coq that referenced this issue Dec 7, 2023
@ejgallego @SkySkimmer
[extraction] (re)-export AST witnesses.
5cdb24f 
Fix downfall of coq#17293 :/

cc: ejgallego/coq-serapi#371
(cherry picked from commit 0821be5)
@ejgallego ejgallego mentioned this issue Feb 21, 2024
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 21, 2024
@ejgallego
[new release] coq-serapi (8.19.0+0.19.1)
2c085e7 
CHANGES:

 - [serlib] Support `btauto` Coq plugin (@ejgallego, ejgallego/coq-serapi#362)
 - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n,
            ejgallego/coq-serapi#375, fixes ejgallego/coq-serapi#371)
 - [general] Make licensing clearer (@ejgallego, @palmskog,
             @SnarkBoojum, ejgallego/coq-serapi#361, closes ejgallego/coq-serapi#266)
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 21, 2024
@ejgallego
[new release] coq-serapi (8.19.0+0.19.1)
366e5e7 
CHANGES:

 - [serlib] Support `btauto` Coq plugin (@ejgallego, ejgallego/coq-serapi#362)
 - [serlib] Support `extraction` Coq plugin (@ejgallego, @toku-sa-n,
            ejgallego/coq-serapi#375, fixes ejgallego/coq-serapi#371)
 - [general] Make licensing clearer (@ejgallego, @palmskog,
             @SnarkBoojum, ejgallego/coq-serapi#361, closes ejgallego/coq-serapi#266)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
2 participants
@ejgallego @toku-sa-n