Skip to content

Conversation

@vscoqbot
Copy link
Contributor

This pull-request concerns:

  • vscoq-language-server.2.3.3: Compatibility meta package for the VsRocq language server after the Rocq renaming
  • vsrocq-language-server.2.3.3: VSRocq language server


🐫 Pull-request generated by opam-publish v2.5.0

@gares
Copy link
Contributor

gares commented Oct 28, 2025

Superseeds #28761

@raphael-proust
Copy link
Contributor

CI errors are for lower bounds. With downgrade conf-gmp 5 to 1 we get the GCC strictness issue:

#=== ERROR while compiling conf-gmp.1 =========================================#
# context              2.5.0~alpha1 | linux/x86_64 | ocaml-base-compiler.4.14.2 | file:///home/opam/opam-repository
# path                 ~/.opam/4.14/.opam-switch/build/conf-gmp.1
# command              ~/.opam/opam-init/hooks/sandbox.sh build sh -exc cc -c $CFLAGS -I/usr/local/include test.c
# exit-code            1
# env-file             ~/.opam/log/conf-gmp-7-7a04a8.env
# output-file          ~/.opam/log/conf-gmp-7-7a04a8.out
### output ###
# + cc -c -I/usr/local/include test.c
# test.c: In function 'test':
# test.c:7:9: error: implicit declaration of function '__gmp_init'; did you mean '__gmpf_init'? [-Wimplicit-function-declaration]
#     7 |         __gmp_init();
#       |         ^~~~~~~~~~
#       |         __gmpf_init

This is unrelated to the packages at hand. It's not a blocker. But we should try to fix the story with gmp, maybe mark some old versions as avoid. Anyway, separate concern.


The Windows build fail because coqc is not found (cygwin) and findlib is not found (msys). Anyone wants to take a stab at addressing those?

@jmid
Copy link
Member

jmid commented Oct 28, 2025

This is unrelated to the packages at hand. It's not a blocker. But we should try to fix the story with gmp, maybe mark some old versions as avoid.

conf-gmp.1 already contains flags: [conf avoid-version]. You added it in 74a2549 😃
The lower bound search apparently ignores it though.
A natural next step is thus to remove such old, broken conf- packages as #28775 proposes.

@jmid
Copy link
Member

jmid commented Oct 28, 2025

The Windows build fail because coqc is not found (cygwin) and

What's your take on this failure @gares?

and findlib is not found (msys).

This is #28636 with a fix in ocaml/ocamlfind#112

@jmid jmid added the question label Oct 28, 2025
@gares
Copy link
Contributor

gares commented Oct 28, 2025

I don't think the failure on windows is relevant, Rocq has its own windows platform where these kind of PATH issues are sorted out.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants