Stream: Coq devs & plugin devs

Topic: Conditional compilation with version number

Pierre Rousselin (Sep 13 2023 at 17:28):

Is there any way to obtain the version of Coq inside Coq?
Is it possible to have some form of "Conditional compilation" which would look like

If Version > 8.5 then
    Require A
else
    Require Compat_8_5
end.

Pierre Roux (Sep 13 2023 at 17:30):

Not that I know. Honestly, Coq offers compatibility with at least two consecutive versions and I'm usually happy with that. Looking for more compatibility (if it doesn't come for free) is often asking for troubles IMHO.

Karl Palmskog (Sep 13 2023 at 17:36):

I think Dune is supposed to provide Coq version access at some point, if not now. So one can set up conditional compilation on Coq version with Dune. That's probably better than doing it inside Coq

Jason Gross (Sep 13 2023 at 18:02):

If you do go the inside-coq route, I think you can do this with coq-elpi. Some projects use gcc in preprocessor-only mode to use C-style conditional macros. If you're looking for compatibility naming things, you can pull the trick where if you do Module Coq. Module Foo. Module Bar. Definition baz := ... End Bar. End Foo. End Coq., then Coq.Foo.Bar.baz will refer to the thing in the standard library if it exists (assuming its been Require'd), and otherwise will refer to your compatibility constant.

If you just want the version of Coq inside of Coq, you can add something to your makefile that does `printf 'From Coq Require Import String.\nLocal Open Scope string_scope.\nDefinition coq_version := "%s".\n' "$(coqc --print-version | cut -d " " -f 1) > coq_version.v" or whatever.

Emilio Jesús Gallego Arias (Sep 14 2023 at 15:13):

Dune does provide the %{coq:version} variable since a few releases.

Last updated: Nov 29 2023 at 22:01 UTC