Skip to content

Conversation

@robin-aws
Copy link
Member

@robin-aws robin-aws commented Sep 12, 2024

Description

See test for what this fixes: without this fix we end up with an import on the consumer side that says import Math ".../Math" when the correct name is Math_.

How has this been tested?

Augmented the timesTwo.dfy separate compilation test.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

@MikaelMayer
Copy link
Member

The issue in the generated code of this one is that it used to be

	if _System.Companion_Nat_.Is_(_3_x) {

but now it is

	if Companion_Nat_.Is_(_3_x) {

I see other change slike:

func (*NT) String() string {
	return "_module.NT"
}

into

func (*NT) String() string {
	return "_System.NT"
}

@MikaelMayer
Copy link
Member

I fixed the issue with the CI. I'm not sure why the original PR was doing both the escaping and setting ModuleName globally. I'm not sure as well what test to write?

@robin-aws robin-aws marked this pull request as ready for review October 3, 2024 22:39
@robin-aws robin-aws enabled auto-merge (squash) October 3, 2024 22:49
Copy link
Member

@MikaelMayer MikaelMayer left a comment

Choose a reason for hiding this comment

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

Nice test !

@robin-aws robin-aws merged commit b5f57e0 into dafny-lang:master Oct 4, 2024
22 checks passed
@robin-aws robin-aws deleted the escaped-names-in-libraries-on-go branch October 11, 2024 18:26
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.

3 participants