Target Java 11 in all builds

[ahelwer]

Closes #921

[ahelwer]

@lemmy @Calvin-L there's a unit test failure and unfortunately I cannot reproduce it locally on linux nor macOS. Any idea what could be causing it? Looks like some kind of module override function signature matching issue?

Failures:

TEST CLASS: tlc2.TraceExpressionSpecSafetyBFSTest
TEST NAME: testSpec
ERROR:
util.Assert$TLCRuntimeException: Parsing or semantic analysis failed.
	at util.Assert.fail(Assert.java:54)
	at tlc2.tool.impl.SpecProcessor.processSpec(SpecProcessor.java:408)
	at tlc2.tool.impl.SpecProcessor.<init>(SpecProcessor.java:176)
	at tlc2.tool.impl.Spec.<init>(Spec.java:110)
	at tlc2.tool.impl.Tool.<init>(Tool.java:211)
	at tlc2.tool.impl.Tool.<init>(Tool.java:206)
	at tlc2.tool.impl.Tool.<init>(Tool.java:196)
	at tlc2.tool.impl.Tool.<init>(Tool.java:182)
	at tlc2.tool.impl.FastTool.<init>(FastTool.java:50)
	at tlc2.TraceExpressionSpecTest.testSpec(TraceExpressionSpecTest.java:80)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at util.IsolatedTestCaseRunner.run(IsolatedTestCaseRunner.java:71)
SYSTEM.OUT:
TLC2 Version 2.18 of Day Month 20??
Running breadth-first search Model-Checking with fp 0 and seed 1 with 1 worker on 4 cores with 3552MB heap and 0MB offheap memory [pid: 5490] (Linux 6.5.0-1021-azure amd64, Eclipse Adoptium 11.0.23 x86_64, OffHeapDiskFPSet, DiskStateQueue).
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/test-model/TESpecTest/TESpecTest.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/_TLAPlusDebugger.tla
Semantic processing of module Naturals
Semantic processing of module _TLAPlusDebugger
Semantic processing of module TESpecTest
Starting... (2024-05-15 22:25:16)
Failed to match EvaluatingValueTest!A operator override from file:/home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/test-class/tlc2/tool/EvaluatingValueTest.class with signature: <Java Method: public static synchronized tlc2.value.impl.Value tlc2.tool.EvaluatingValueTest.action(tlc2.tool.impl.Tool,tla2sany.semantic.ExprOrOpArgNode[],tlc2.util.Context,tlc2.tool.TLCState,tlc2.tool.TLCState,int,tlc2.tool.coverage.CostModel)> (no such module).
Warning: Failed to match Get operator override from UserModuleOverrideAnnotation with signature: public static tlc2.value.impl.Value tlc2.overrides.UserModuleOverrideAnnotationImpl.getNumberOne() (no such module).
(Use the -nowarning option to disable this warning.)
Warning: Failed to match Get2 operator override from UserModuleOverrideAnnotation with signature: public static tlc2.value.impl.Value tlc2.overrides.UserModuleOverrideAnnotationImpl.Get2() (no such module).
Warning: Failed to match Get2 operator override from UserModuleOverrideAnnotation with signature: public static tlc2.value.impl.Value tlc2.overrides.UserModuleOverrideAnnotationImpl.Get2(tlc2.value.impl.Value) (no such module).
Warning: Failed to match NoSuchIdentifier operator override from UserModuleOverrideAnnotation with signature: public static tlc2.value.impl.Value tlc2.overrides.UserModuleOverrideAnnotationImpl.noSuchIdentifier() (no such module).
Warning: Failed to match Get operator override from NoSuchModule with signature: public static tlc2.value.impl.Value tlc2.overrides.UserModuleOverrideAnnotationImpl.noSuchModule() (no such module).
Debugger is listening on 0.0.0.0/0.0.0.0:54633
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2024-05-15 22:25:16.
Error: Invariant Safety is violated.
Error: The behavior up to this point is:
State 1: <Init line 18, col 5 to line 19, col 16 of module TESpecTest>
/\ x = 0
/\ y = FALSE

State 2: <Increment line 22, col 5 to line 23, col 14 of module TESpecTest>
/\ x = 1
/\ y = TRUE

State 3: <Increment line 22, col 5 to line 23, col 14 of module TESpecTest>
/\ x = 2
/\ y = FALSE

State 4: <Increment line 22, col 5 to line 23, col 14 of module TESpecTest>
/\ x = 3
/\ y = TRUE

5 states generated, 4 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
Finished in 01s at (2024-05-15 22:25:16)
Trace exploration spec path: states/TESpecTest_TTrace_1715811915.tla
Parsing file /home/runner/work/tlaplus/tlaplus/states/TESpecTest_TTrace_1715811915.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Sequences.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLCExt.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/test-model/TESpecTest/TESpecTest.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Toolbox.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/Naturals.tla
Parsing file /home/runner/work/tlaplus/tlaplus/tlatools/org.lamport.tlatools/class/tla2sany/StandardModules/TLC.tla
Parsing file /home/runner/work/tlaplus/tlaplus/states/tlc2.TraceExpressionSpecSafetyBFSTest/6227334027674783102/TESpecTest_TEExpression.tla (/home/runner/work/tlaplus/tlaplus/states/TESpecTest_TTrace_1715811915.tla)

Fatal errors while parsing TLA+ spec in file TESpecTest_TTrace_1715811915

tla2sany.semantic.AbortException
*** Abort messages: 1

Unknown location

Cannot find source file for module TESpecTest_TETrace imported in module TESpecTest_TTrace_1715811915.


Starting... (2024-05-15 22:25:17)
SYSTEM.ERR:
None

[lemmy]

No idea, perhaps bisect switching to Java 11 and the ant plugin change first?

[ahelwer]

The ant plugin change isn't involved in the UT failure, it's 100% ant; maven isn't used.

[ahelwer]

Turns out it was transient. @lemmy @Calvin-L this is good to merge, as is the compiler warning PR: #915

[Calvin-L]

Turns out it was transient.

That means it's probably unrelated to this PR. But it may still indicate a race or or other bug in the test suite, and we should be on the lookout if it ever happens again.