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

Separate package for extraction modules #16294

Open
liyishuai opened this issue Jul 6, 2022 · 1 comment
Open

Separate package for extraction modules #16294

liyishuai opened this issue Jul 6, 2022 · 1 comment
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: extraction The extraction mechanism.
Projects
Dune

Comments

@liyishuai
Copy link
Member

Description of the problem

As mentioned in QuickChick/QuickChick#294, QuickChick extracts Z to either integer or big integer based on the underlying Coq version, because the ideal extraction module only ships with Coq >= 8.15.

Consider splitting extraction modules into a separate library so that older versions of Coq can use the new extractions?

Furthermore: Should we version the entire standard library asynchronously from the core?

Coq Version

Version-generic.
@ejgallego ejgallego added this to Ready to address in Dune Jul 7, 2022
@anton-trunov
Copy link
Member

This would be great to have! It's kind of a blocker for a project I'm working on to support Coq 8.15.

@anton-trunov anton-trunov added part: extraction The extraction mechanism. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Jul 7, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: extraction The extraction mechanism.
Projects
Dune
  
Ready to address
Milestone
No milestone
Development

No branches or pull requests
2 participants
@anton-trunov @liyishuai