JSON regression test fails

[markrtuttle]

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]

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

[markrtuttle]

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.