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.

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

Condition code blocks over Coq/OCaml versions #15109

Open
liyishuai opened this issue Nov 3, 2021 · 0 comments
Open

Condition code blocks over Coq/OCaml versions #15109

liyishuai opened this issue Nov 3, 2021 · 0 comments
Labels
kind: design discussion Discussion about the design of a feature. kind: feature New user-facing feature request or implementation.

Comments

@liyishuai
Copy link
Member

Description of the problem

Some code works with certain versions of Coq and OCaml. To write Coq code that work with multiple versions, current solutions use cppo:

SimpleIO

#if OCAML_VERSION >= (4, 8, 0)
Extract Inlined Constant int_of_ascii => "Stdlib.int_of_char".
Extract Inlined Constant ascii_of_int => "Stdlib.char_of_int".
#else
Extract Inlined Constant int_of_ascii => "Pervasives.int_of_char".
Extract Inlined Constant ascii_of_int => "Pervasives.char_of_int".
#endif

QuickChick

#if COQ_VERSION >= (8, 15, 0)
Require Import ExtrOcamlZBigInt.
#else
Require Import ExtrOcamlZInt.
#endif

These code work fine in non-interactive scenarios (edit-save-preprocess-compile). Is it worth having similar functionality in Coqtop, so that these code can work with CoqIDE/ProofGeneral?

@Alizter Alizter added kind: feature request kind: design discussion Discussion about the design of a feature. kind: feature New user-facing feature request or implementation. and removed kind: feature request labels Nov 10, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: design discussion Discussion about the design of a feature. kind: feature New user-facing feature request or implementation.
Projects
None yet
Development

No branches or pull requests

2 participants