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

Error message for a failed extraction to Scheme / JSON mentions Ocaml #17817

Closed
ana-borges opened this issue Jul 5, 2023 · 2 comments · Fixed by #17889
Closed

Error message for a failed extraction to Scheme / JSON mentions Ocaml #17817

ana-borges opened this issue Jul 5, 2023 · 2 comments · Fixed by #17889
Labels
kind: user messages Improvement of error messages, new warnings, etc. part: extraction The extraction mechanism.
Milestone
8.19+rc1

Comments

@ana-borges
Copy link
Contributor

ana-borges commented Jul 5, 2023 •
edited

The error message when trying to extract informative inductive types with a Prop instance to Scheme or JSON mentions OCaml instead of Scheme or JSON. This was already noted in another issue:

[C]hanging the extraction language to JSON or Scheme produces the same message ("The Ocaml extraction cannot handle this situation yet.").

Originally posted by @cpitclaudel in #10749 (comment)

Coq version: 8.17
@ana-borges ana-borges added kind: user messages Improvement of error messages, new warnings, etc. part: extraction The extraction mechanism. labels Jul 5, 2023
@ana-borges ana-borges mentioned this issue Jul 5, 2023
Open
herbelin added a commit to herbelin/github-coq that referenced this issue Jul 26, 2023
@herbelin
Extraction: Moving code around in preparation of fixing coq#17817.
3f5c851
herbelin added a commit to herbelin/github-coq that referenced this issue Jul 26, 2023
@herbelin
Fixes coq#17817: extraction error message refers to actual language o…
fc76ccb 
…f extraction.
@herbelin herbelin mentioned this issue Jul 26, 2023
Merged
1 task
@herbelin
Copy link
Member

herbelin commented Jul 26, 2023 •
edited

Fixed in #17889 [edited].

@ana-borges
Copy link
Contributor Author

Great! I guess you mean #17889, though.

herbelin added a commit to herbelin/github-coq that referenced this issue Jul 31, 2023
@herbelin
Fixes coq#17817: extraction error message refers to actual language o…
8c113b5 
…f extraction.
@coqbot-app coqbot-app bot added this to the 8.18.0 milestone Aug 1, 2023
coqbot-app bot added a commit that referenced this issue Aug 1, 2023
@coqbot-app @ppedrot
Merge PR #17889: Fixes #17817: refer to actual chosen extraction lang…
3974f34 
…uage in extraction error messages

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
@Zimmi48 Zimmi48 modified the milestones: 8.18.0, 8.19+rc1 Oct 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: user messages Improvement of error messages, new warnings, etc. part: extraction The extraction mechanism.
Projects
None yet
Milestone
8.19+rc1
3 participants
@herbelin @Zimmi48 @ana-borges