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

coqide-server build error on Windows #18548

Closed
rtetley opened this issue Jan 24, 2024 · 0 comments · Fixed by #18550
Closed

coqide-server build error on Windows #18548

rtetley opened this issue Jan 24, 2024 · 0 comments · Fixed by #18550
Milestone

Comments

@rtetley
Copy link
Contributor

rtetley commented Jan 24, 2024

Description of the problem

There seems to be a problem with building coqide-server on Cygwin.
See https://github.com/coq-community/vscoq/actions/runs/7544033174/job/20536408452?pr=706

Error:  The compilation of coqide-server failed at "C:\\ci\\cygwin64\\opam\\CP.2023.11.0~dev\\bin\\dune.exe subst".

#=== ERROR while compiling coqide-server.dev ==================================#
# context              2.0.10 | win32/x86_64 | ocaml-variants.4.13.1+flambda+mingw64c | https://coq.inria.fr/opam/core-dev#2024-01-16 13:33
# path                 C:/ci/cygwin64/opam/CP.2023.11.0~dev/.opam-switch/build/coqide-server.dev
# command              C:\ci\cygwin64\opam\CP.2023.11.0~dev\bin\dune.exe subst
# exit-code            1
# env-file             C:/ci/cygwin64/opam/log/coqide-server-604-d8a4ae.env
# output-file          C:/ci/cygwin64/opam/log/coqide-server-604-d8a4ae.out
### output ###
# Error:
# stat(test-suite/prerequisite/library_attributes.v): No such file or directory

This is probably due to the fact that test-suite/prerequisite/library_attributes.v is a sym link ?

Coq Version

The CI runs use the dev pick of the coq platform so coq#master is used

SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 24, 2024
Fix coq#18548

No idea why that bug happens on coqide-server and not -core or -stdlib
but we have historically avoided symlinks in the git repo due to
similar issues.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jan 30, 2024
Fix coq#18548

No idea why that bug happens on coqide-server and not -core or -stdlib
but we have historically avoided symlinks in the git repo due to
similar issues.
@coqbot-app coqbot-app bot added this to the 8.19.1 milestone Feb 5, 2024
SkySkimmer added a commit that referenced this issue Feb 5, 2024
Fix #18548

No idea why that bug happens on coqide-server and not -core or -stdlib
but we have historically avoided symlinks in the git repo due to
similar issues.

(cherry picked from commit 76180e5)
louiseddp pushed a commit to louiseddp/coq that referenced this issue Feb 27, 2024
Fix coq#18548

No idea why that bug happens on coqide-server and not -core or -stdlib
but we have historically avoided symlinks in the git repo due to
similar issues.
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 a pull request may close this issue.

1 participant