Skip to content

Adapt to https://github.com/coq/coq/pull/20027#543

Merged
xavierleroy merged 1 commit intoAbsInt:masterfrom
proux01:coq_20027
Jan 14, 2025
Merged

Adapt to https://github.com/coq/coq/pull/20027#543
xavierleroy merged 1 commit intoAbsInt:masterfrom
proux01:coq_20027

Conversation

@proux01
Copy link
Contributor

@proux01 proux01 commented Jan 13, 2025

Adapt to rocq-prover/rocq#20027 (part of the renaming from Coq to Rocq)

@ppedrot
Copy link
Contributor

ppedrot commented Jan 13, 2025

This is backwards compatible, please merge ASAP to ease the life of the Rocq 9.0. RM.

@xavierleroy xavierleroy merged commit 54d2e47 into AbsInt:master Jan 14, 2025
7 checks passed
@xavierleroy
Copy link
Contributor

Ça vient, ça vient :-)

@xavierleroy
Copy link
Contributor

Feature wish for Rocq: a command-line option that prints the version number (and nothing else) and exit. Like in OCaml:

$ ocamlc -v
The OCaml compiler, version 4.14.2
Standard library directory: /foo/bar/lib/ocaml
$ ocamlc -version
4.14.2
$ ocamlc -where
/foo/bar/lib/ocaml

@ppedrot
Copy link
Contributor

ppedrot commented Jan 14, 2025

Thanks for the fast merge! Indeed, a way to access version data without ad-hoc parsing would be way more robust...

@ppedrot
Copy link
Contributor

ppedrot commented Jan 14, 2025

@xavierleroy good news and bad news: the good one is that there is indeed already a command to do that, it's coqc --print-version, which is present since Coq 8.6. The bad news is that this PR is already outdated because the message is bound to change again, see rocq-prover/rocq#20053. I'm writing the final patch right now, but it will need from our side a backport to the Coq 9.0 branch, so ideally it should go in asap (again but that's the last one hopefully).

@xavierleroy
Copy link
Contributor

there is indeed already a command to do that, it's coqc --print-version, which is present since Coq 8.6

I could definitely use this in CompCert's configure script. The oldest supported Coq version is currently 8.13.

@ppedrot
Copy link
Contributor

ppedrot commented Jan 14, 2025

@xavierleroy it's already written in #544

@proux01 proux01 deleted the coq_20027 branch January 15, 2025 09:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants