Skip to content

[rocq makefile] Don't erase ROCQPATH - #22246

Merged
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
proux01:fix-rocqmakefile
Jul 9, 2026
Merged

[rocq makefile] Don't erase ROCQPATH#22246
coqbot-app[bot] merged 1 commit into
rocq-prover:masterfrom
proux01:fix-rocqmakefile

Conversation

@proux01

@proux01 proux01 commented Jul 9, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@proux01 proux01 added this to the 9.3+rc1 milestone Jul 9, 2026
@proux01
proux01 requested a review from a team as a code owner July 9, 2026 07:33
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 9, 2026
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 9, 2026
@proux01

proux01 commented Jul 9, 2026

Copy link
Copy Markdown
Contributor Author

Cc @rlepigre-skylabs-ai linked to #21564 (comment)

@SkySkimmer

SkySkimmer commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

I think rather this should be renamed

@rlepigre-skylabs-ai

rlepigre-skylabs-ai commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

I agree, the naming of that variable is unfortunate.

@rlepigre-skylabs-ai rlepigre-skylabs-ai mentioned this pull request Jul 9, 2026
Merged
@SkySkimmer

SkySkimmer commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

probably to something like ROCQ_FINDLIB_INSTALL_PATH

@rlepigre-skylabs-ai

rlepigre-skylabs-ai commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

This is meant to hold the logical path for the package, so I would call it PACKAGE_LOGPATH or something like that, and I would similarly rename HASROCQPATH into HAS_PACKAGE_LOGPATH maybe?

@Janno

Janno commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

I want to advocate for LOGICAL_PATH because LOGPATH sounds like it's related to logging.

@proux01 proux01 added kind: fix This fixes a bug or incorrect documentation. part: coq_makefile The coq_makefile binary for generating makefiles. request: full CI Use this label when you want your next push to trigger a full CI. labels Jul 9, 2026
@proux01
proux01 force-pushed the fix-rocqmakefile branch from 48f9d49 to c1c8628 Compare July 9, 2026 08:12
@proux01
proux01 requested a review from a team as a code owner July 9, 2026 08:12
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 9, 2026
@proux01
[rocq makefile] Don't erase ROCQPATH
e964f5c 
Fixing an unfortunate variable overlap from
rocq-prover#21564
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 9, 2026
@proux01
proux01 force-pushed the fix-rocqmakefile branch from c1c8628 to e964f5c Compare July 9, 2026 08:14
@coqbot-app coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 9, 2026
@proux01

proux01 commented Jul 9, 2026

Copy link
Copy Markdown
Contributor Author

BTW, it may look like I'm complaining about that unfortunate bug, but I'm very happy to see progress made in this direction. Thanks for all your work!

@rlepigre-skylabs-ai

rlepigre-skylabs-ai commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

The changes look good to me, I'll run a few tests to make sure everything still works.

rlepigre-skylabs-ai
rlepigre-skylabs-ai approved these changes Jul 9, 2026
View reviewed changes

@rlepigre-skylabs-ai rlepigre-skylabs-ai left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything seems fine after some extra local testing, so this is good to go as far as I'm concerned.

@SkySkimmer

SkySkimmer commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

@coqbot run full ci

@SkySkimmer SkySkimmer self-assigned this Jul 9, 2026
@SkySkimmer

SkySkimmer commented Jul 9, 2026

Copy link
Copy Markdown
Contributor

@coqbot merge now

@coqbot-app
coqbot-app Bot merged commit b8e4101 into rocq-prover:master Jul 9, 2026
8 checks passed
@proux01
proux01 deleted the fix-rocqmakefile branch July 9, 2026 11:21
gares added a commit that referenced this pull request Jul 22, 2026
@gares
Backport PR #22246: [rocq makefile] Don't erase ROCQPATH
1c6c8ba
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@rlepigre-skylabs-ai rlepigre-skylabs-ai rlepigre-skylabs-ai approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels

kind: fix This fixes a bug or incorrect documentation. part: coq_makefile The coq_makefile binary for generating makefiles.

Projects

Release management
Status: ...

Milestone

9.3+rc1

Development

Successfully merging this pull request may close these issues.

4 participants

@proux01 @SkySkimmer @rlepigre-skylabs-ai @Janno