Text encoding issues

[danielgrahl]

-- name of this issue has been updated 15.02.

The example program (now with acceptable syntax) cannot be run or proven. WW says "there are errors in the source file." But I cannot see any. That message disappears if the _axiom statement is removed.

//At first there may be axioms:
_axiom(∀Integer x: ∀Integer y : (x+y)*(x+y) = x*x + 2*x*y + y*y)

//Before the main block there may be function declarations like this: 
function Integer pow(Integer base, Integer exponent) {
    Integer result := base
    Integer tmp := exponent

    if(exponent = 0) {
            return 1
    }

    while( tmp > 1) {
            result := result * base
            tmp := tmp - 1
    }

    return base
}  

//After the function declarations follows the main block:
Integer a := 5
Integer b := 3
Integer c := 0

c := pow(a, b)

[jspam]

I cannot reproduce this; the program can be run and proven without problems here.

Could you please post the full file name under which you saved the example program, along with the full error message that appears?

E.g. for me that would be Test/syntax.ww and

'Launching _Test_syntax.ww' has encountered a problem.

There are errors in the source file.

The goal is to make sure that you tried to launch the right file.

[jspam]

As of 3ba4b2c, the syntax error messages are displayed in the error dialog. Could you please paste the error messages here?

[danielgrahl]

Saved it under test/bla.ww, the full error message is: 'Launching _test_bla.ww' has encountered a problem. There are errors in the source file.

[danielgrahl]

It seems to be related with quantifiers. Here is a MWE: function Boolean foo() _requires ∀ Integer i : true { return true }

[jspam]

I still cannot reproduce this here ...

Could you please try it out with the current version I just uploaded to the build server? It displays the syntax error messages in the error dialog which appears when launching. Then we'll see which error message is causing the problem.

[danielgrahl]

It's an encoding problem, even though the file is in UTF-8, it's parsed as something else: There are syntax errors in the source file: Line 2: no viable alternative at input '�'

[jspam]

Is this the same machine you experienced #33 on?

Anyways, in 695db65 I tried to specify UTF8 as default JVM encoding in the startup options. I uploaded a build of that revision; maybe you could try that one?

[jspam]

@danielbruns Have you already tried it out?

[danielgrahl]

sorry for the delay; it works fine