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

JSON regression test fails #145

Open
markrtuttle opened this issue Sep 29, 2023 · 2 comments · May be fixed by #146
Open

JSON regression test fails #145

markrtuttle opened this issue Sep 29, 2023 · 2 comments · May be fixed by #146

Comments

@markrtuttle
Copy link

I'm unable to run the JSON regression test in Tests.dfy with dafny 4.2.0 from Homebrew on MacOS.

Tests.dfy begins with

// RUN: %run "%s" --unicode-char:false --input ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
// RUN: %run "%s" --unicode-char:true --input ../Unicode/UnicodeStringsWithUnicodeChar.dfy

So I try

git clone https://github.com/dafny-lang/libraries
cd libraries/src/JSON
dafny run --target cs --unicode-char:false --input ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy  Tests.dfy 
dafny run --target js --unicode-char:false --input ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy  Tests.dfy 
dafny run --target java --unicode-char:false --input ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy  Tests.dfy

My results are

  • C# fails with "The type or namespace name 'Abs' does not exist in the namespace 'Math' (are you missing an assembly reference?)"
  • JavaScript fails with "Cannot find module 'bignumber.js'"
  • Java fails with can't find Math.__default
@markrtuttle
Copy link
Author

Tests.dfy includes API.dfy which includes Serializer.dfy which includes ../Math.dfy which defines Abs. So verification works but compilation fails.

@markrtuttle
Copy link
Author

I think the compiler is picking up the standard Math class and not the Math class defined in this library. Renaming Math to DMath in this library solves the problem for Java, and I think also for C# and JavaScript.

@markrtuttle markrtuttle linked a pull request Oct 4, 2023 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Rename module Math->MathLib, name conflicts with Java/C# Math class markrtuttle/dafny-libraries
1 participant
@markrtuttle