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.

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

Escaped go modules cannot be used properly when passed via --library #5729

Open
MikaelMayer opened this issue Aug 28, 2024 · 0 comments
Open
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done

Comments

@MikaelMayer
Copy link
Member

MikaelMayer commented Aug 28, 2024

Dafny version

latest-nightly

Code to produce this issue

// mathlib.dfy
module Math {
  const x := 1
}

First compile this file into a go module using something like
dafny translate go --go-module-name SomeGoModuleName

Then,

// mainfile.dfy
module P {
  import Math
  const x := Math.x;
}

Translate this file into a go module using --library mathlib.dfy and make sure to use the generated Go code of mathlib.dfy

The command should look like
dafny translate go --go-module-name SomeOtherGoModuleName --library mathlib.dfy --translation-record $(PATH_TO_MATHLIB.DTR)

What happened?

In the second project, it incorrectly imports Math "...Math" instead of _Math "....Math_", making Go unable to resolve the file

What type of operating system are you experiencing the problem on?

Windows

@MikaelMayer MikaelMayer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Aug 28, 2024
@MikaelMayer MikaelMayer self-assigned this Aug 28, 2024
@MikaelMayer MikaelMayer added the priority: next Will consider working on this after in progress work is done label Aug 28, 2024
@MikaelMayer MikaelMayer changed the title Escaped go modules should have matching DTR entries Escaped go modules cannot be used properly when passed via --library Aug 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done
Projects
None yet
Development

No branches or pull requests

1 participant