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

Fixes #17817: refer to actual chosen extraction language in extraction error messages #17889

Merged
merged 2 commits into from Aug 1, 2023
Merged

Fixes #17817: refer to actual chosen extraction language in extraction error messages #17889

merged 2 commits into from Aug 1, 2023

Conversation

herbelin
Copy link
Member

Fixes / closes #17817

  • Added changelog.

@herbelin herbelin added kind: fix This fixes a bug or incorrect documentation. kind: user messages Improvement of error messages, new warnings, etc. part: extraction The extraction mechanism. labels Jul 26, 2023
@herbelin herbelin added this to the 8.18.0 milestone Jul 26, 2023
@herbelin herbelin requested a review from a team as a code owner July 26, 2023 14:14
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 26, 2023
@ana-borges ana-borges mentioned this pull request Jul 28, 2023
Closed
@ppedrot
Copy link
Member

ppedrot commented Jul 28, 2023

While this fix is correct, I think it would have been even simpler to just remove the mention to any language and just say "extraction" rather than "OCaml extraction". The problem is not in the backend, but in the frontend of CIC erasure.

@herbelin
Copy link
Member Author

I was hesitating to do so actually. The problem does not show up with Haskell, is that correct? At least, it is under this assumption that I kept the name of the language, but that would indeed be as understandable (and a simpler implementation) without the name.

@herbelin herbelin force-pushed the master+fix17817-extraction-prop-elim-error-not-ocaml-specific branch from 4d3970f to 5389409 Compare July 31, 2023 17:51
@herbelin
Copy link
Member Author

I renounced to mentioning a language name in the message.

Looks also like a full CI is not needed (assuming that no development checks the error message).

@herbelin herbelin removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 31, 2023
@ppedrot ppedrot self-assigned this Aug 1, 2023
@ppedrot
Copy link
Member

ppedrot commented Aug 1, 2023

This is trivial, no need to wait more. @coqbot merge now

@coqbot-app coqbot-app bot merged commit 3974f34 into coq:master Aug 1, 2023
6 checks passed
@Zimmi48 Zimmi48 added this to Request 8.18.0 inclusion in Coq 8.18 Aug 13, 2023
@gares gares modified the milestones: 8.18.0, 8.19+rc1 Aug 31, 2023
@Zimmi48 Zimmi48 removed this from Request 8.18.0 inclusion in Coq 8.18 Oct 12, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: fix This fixes a bug or incorrect documentation. kind: user messages Improvement of error messages, new warnings, etc. part: extraction The extraction mechanism.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

Error message for a failed extraction to Scheme / JSON mentions Ocaml
3 participants
@herbelin @ppedrot @gares