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.

Sign up for GitHub

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

Jump to bottom

Quote more findlib paths #15707

Merged
merged 3 commits into from
Mar 8, 2022
Merged

Quote more findlib paths #15707

merged 3 commits into from
Mar 8, 2022

Conversation

JasonGross
Copy link
Member

This should fix the fact failing opam install on Windows, hopefully.

Followup to #15665

Fixes #15664 (hopefully for real this time)

@JasonGross
Quote more findlib paths
12b44fa 
This should fix the fact failing opam install on Windows, hopefully.
@JasonGross JasonGross added kind: fix This fixes a bug or incorrect documentation. kind: infrastructure CI, build tools, development tools. part: tools Coqdoc, coq_makefile, etc. kind: regression Problems that were not present in previous versions. priority: blocker The next release should be delayed if this is not fixed. kind: bug An error, flaw, fault or unintended behaviour. part: coq_makefile The coq_makefile binary for generating makefiles. labels Feb 17, 2022
@JasonGross JasonGross added this to the 8.16+rc1 milestone Feb 17, 2022
@JasonGross JasonGross requested a review from a team as a code owner February 17, 2022 22:23
@JasonGross
Copy link
Member Author

Another question (possibly not for this PR): Why use addprefix here rather than just doing -m "$(METAFILE)"?

coq/tools/CoqMakefile.in

Line 883 in dc5e355

$(HIDE)$(COQDEP) $(addprefix -m ,$(METAFILE)) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)

@JasonGross
Copy link
Member Author

Is ci-gappa failing everywhere, or is this broken?

File "./src/Gappa_tactic_loader.v", line 1, characters 0-37:
Error:
Dynlink error: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure("/builds/coq/coq/_build_ci/gappa/src/././gappatac.cmxs: cannot open shared object file: No such file or directory")")
Findlib paths:
/builds/coq/coq/_install_ci/lib
/builds/coq/coq/_install_ci/lib/coq/../coq-core/..
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Ltac2
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Flocq
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Flocq/IEEE754
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Flocq/Prop
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Flocq/Pff
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Flocq/Calc
/builds/coq/coq/_install_ci/lib/coq/user-contrib/Flocq/Core
src
/root/.opamcache/4.13.0+flambda/lib

Wait, is ci-gappa even using coq_makefile? It seems to be remake based...

@JasonGross
Copy link
Member Author

cc @gares?

@silene
Copy link
Contributor

silene commented Feb 18, 2022

Is ci-gappa failing everywhere, or is this broken?

It is failing everywhere, but only if you are especially unlucky. Indeed, the findlib pull request introduced a race condition. I will fix it.

silene
silene reviewed Feb 18, 2022
View reviewed changes
tools/CoqMakefile.in Outdated Show resolved Hide resolved
@JasonGross @silene
Remove prerequisite quoting
548d04f 
As per code review, quotes don't work in prerequisite paths, we'd need to escape spaces if there are any.  Hopefully there won't be, and we're just quoting for backslashes on Windows.

Co-authored-by: Guillaume Melquiond <[email protected]>
@SkySkimmer SkySkimmer requested a review from a team February 24, 2022 15:50
@SkySkimmer SkySkimmer removed kind: infrastructure CI, build tools, development tools. kind: bug An error, flaw, fault or unintended behaviour. labels Feb 24, 2022
@MSoegtropIMC
Copy link
Contributor

@JasonGross : do you think I should enable a dev build on Windows and Mac on Coq Platform? The daily build of 8.15 works fine.

@SkySkimmer
Copy link
Contributor

If you could fix the platform test in Coq's CI that would be nice (see also #15535)

@MSoegtropIMC
Copy link
Contributor

@SkySkimmer : ah yes - I forgot about this. Will do until Monday.

@JasonGross
Copy link
Member Author

Bump. This is still breaking Fiat Crypto's CI

@silene
Copy link
Contributor

silene commented Mar 8, 2022

@coqbot merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Mar 8, 2022

@silene: You cannot merge this PR because:

  • You are not among the assignees.

@silene silene self-assigned this Mar 8, 2022
@silene
Copy link
Contributor

silene commented Mar 8, 2022

@coqbot merge now

@coqbot-app coqbot-app bot merged commit a0df849 into coq:master Mar 8, 2022
@JasonGross JasonGross deleted the more-quoting branch March 8, 2022 19:21
@JasonGross
Copy link
Member Author

Thanks!

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

@silene silene silene approved these changes

Assignees

@silene silene

Labels
kind: fix This fixes a bug or incorrect documentation. kind: regression Problems that were not present in previous versions. part: coq_makefile The coq_makefile binary for generating makefiles. part: tools Coqdoc, coq_makefile, etc. priority: blocker The next release should be delayed if this is not fixed.
Projects
None yet
Milestone
8.16+rc1
Development

Successfully merging this pull request may close these issues.

coq_makefile's findlib_remove does not work on Windows
4 participants
@JasonGross @silene @MSoegtropIMC @SkySkimmer