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

coqdev.el: use install layout coqtop when in _build_ci #17282

Merged
merged 1 commit into from
Apr 3, 2023
Merged

coqdev.el: use install layout coqtop when in _build_ci #17282

merged 1 commit into from
Apr 3, 2023

Conversation

SkySkimmer
Copy link
Contributor

the shims don't look in the right place to find installed dependencies

@SkySkimmer
coqdev.el: use install layout coqtop when in _build_ci
e9c23b6 
the shims don't look in the right place to find installed dependencies
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 23, 2023 10:50
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 23, 2023
@andres-erbsen
Copy link
Contributor

andres-erbsen commented Feb 23, 2023 •
edited
Loading

https://github.com/coq/coq/blob/c4587fa780c885fda25a38a2f16e84dc9011f9bd/dev/doc/build-system.dune.md#running-binaries-coqtop--coqide does not sound like this is required. Is it really? Having to switch PATH based on whether the .v file I am editing is in stdlib seems like just extra hassle. If the distinction is required, it would be nice to have the documentation be very up-front about it.

@SkySkimmer
Copy link
Contributor Author

The shims are only intended for the stdlib, you should build with the install target and use the binaries in the install layout for anything else.

@SkySkimmer SkySkimmer removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Feb 23, 2023
@SkySkimmer
Copy link
Contributor Author

@coq/dev-tools-maintainers ping

@ppedrot ppedrot self-assigned this Apr 3, 2023
@ppedrot ppedrot added this to the 8.18+rc1 milestone Apr 3, 2023
@ppedrot ppedrot added the kind: infrastructure CI, build tools, development tools. label Apr 3, 2023
@ppedrot
Copy link
Member

ppedrot commented Apr 3, 2023

I have no idea about this but since nobody wants to assign and it's a pretty much well-delimited dev-targeted change, I'm merging it. Worst case we can revert. @coqbot merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Apr 3, 2023

@ppedrot: You can't merge the PR because it hasn't been approved yet.

@ppedrot
Copy link
Member

ppedrot commented Apr 3, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 7c4e8b7 into coq:master Apr 3, 2023
@SkySkimmer SkySkimmer deleted the coqdev branch April 4, 2023 11:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@SkySkimmer @andres-erbsen @ppedrot