Skip to content

Prefix RefC internal names to disambiguate#3765

Merged
dunhamsteve merged 10 commits into
idris-lang:mainfrom
joelberkeley:prefix-refc
Apr 15, 2026
Merged

Prefix RefC internal names to disambiguate#3765
dunhamsteve merged 10 commits into
idris-lang:mainfrom
joelberkeley:prefix-refc

Conversation

@joelberkeley
Copy link
Copy Markdown
Contributor

@joelberkeley joelberkeley commented Apr 5, 2026

Description

Value is sufficiently vague that it can collide with names from other support libs, such as Value in my MLIR lib. I've prefixed everything with Idris2_.

c.f. zulip discussion #help > Rename `Value` in RefC?

Self-check

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md
  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

Copy link
Copy Markdown
Contributor Author

@joelberkeley joelberkeley Apr 6, 2026

Choose a reason for hiding this comment

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

should I have updated this and other autogenerated files?

Comment thread support/refc/_datatypes.h
uint8_t tag;
uint8_t reserved;
} Value_header;
} Idris2_header;
Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

not sure about this rename

@joelberkeley
Copy link
Copy Markdown
Contributor Author

Do I need to do anything else here? Looks like CI timed out

@dunhamsteve
Copy link
Copy Markdown
Collaborator

Should we be updating the bootstrap image? I'm not sure what the policy is here, I think at one point we liked to have it be the previous version of Idris.

It looks like bootstrap-ci is wedging waiting for an ubuntu-20 runner, probably because they're deprecated. The like says they'd be down on the 8th to "raise awareness".

Evaluating initialise.if
Evaluating: success()
Result: true
Requested labels: ubuntu-20.04
Job defined at: idris-lang/Idris2/.github/workflows/ci-bootstrap.yml@refs/pull/3765/merge
Waiting for a runner to pick up this job...

If updating bootstrap is ok, we probably need to move bootstrap-ci.yml to a newer ubuntu.

@joelberkeley
Copy link
Copy Markdown
Contributor Author

joelberkeley commented Apr 15, 2026

Should we be updating the bootstrap image?

I have absolutely no idea. I don't know how it works (I thought the bootstrap image would be built from whatever changes I make elsewhere), in which case the answer would be "no, we shouldn't update the bootstrap image". But I have extremely low confidence in my knowledge here.

I only updated it because it appeared in the find/replace.

@dunhamsteve
Copy link
Copy Markdown
Collaborator

Yeah, the bootstrap files are usually only updated for releases. I wouldn't update it unless something is broken and we're forced to update it. I believe it is only used to build a scheme target (either chez or racket), so it should be fine as-is with these changes, and we should revert those two files. That should fix the build.

Aside from that does anyone have objections to this change?

@joelberkeley
Copy link
Copy Markdown
Contributor Author

joelberkeley commented Apr 15, 2026

Reverted bootstrap

@dunhamsteve
Copy link
Copy Markdown
Collaborator

Looks good to me, and I don't see any objections.

@joelberkeley
Copy link
Copy Markdown
Contributor Author

p.s. bootstrap version handled in this PR #3729

@dunhamsteve dunhamsteve merged commit 29d925c into idris-lang:main Apr 15, 2026
22 checks passed
@joelberkeley joelberkeley deleted the prefix-refc branch April 15, 2026 14:47
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 this pull request may close these issues.

2 participants