[SERVER-48045] NoSuchMethodError testing TLA+ Created: 08/May/20  Updated: 29/Oct/23  Resolved: 12/May/20

Status: Closed
Project: Core Server
Component/s: Replication
Affects Version/s: None
Fix Version/s: 4.7.0

Type: Bug Priority: Major - P3
Reporter: A. Jesse Jiryu Davis Assignee: A. Jesse Jiryu Davis
Resolution: Fixed Votes: 0
Labels: None
Remaining Estimate: Not Specified
Time Spent: Not Specified
Original Estimate: Not Specified

Issue Links:
Depends
Backwards Compatibility: Fully Compatible
Operating System: ALL
Sprint: Repl 2020-05-18
Participants:
Linked BF Score: 50

 Description   

The TLA+ model-check task in Evergreen has started failing with:

Exception in thread "main" java.lang.NoSuchMethodError: java.lang.String.strip()Ljava/lang/String;
  at tlc2.TLC.handleParameters(TLC.java:750)
  at tlc2.TLC.main(TLC.java:245)

This is because we use the default java on the command line, which is Java 8 on the Ubuntu 18.04 builder machines, and the TLC model-checking tool has begun to require Java 11. I'm not sure this is intentional, I've filed a bug: https://github.com/tlaplus/tlaplus/issues/462

In any case, use Java 11, which is installed in /opt.



 Comments   
Comment by Githook User [ 12/May/20 ]

Author:

{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com', 'username': 'ajdavis'}

Message: SERVER-48045 Set Java path tla_plus.yml suite config
Branch: master
https://github.com/mongodb/mongo/commit/4317089d3206e16a623bd38f68e950f6b276f65c

Comment by A. Jesse Jiryu Davis [ 12/May/20 ]

Old solution hard-coded path to java binary; new one will configure it in tla_plus.yml suite config.

Comment by Judah Schvimer [ 12/May/20 ]

What's wrong with the current solution and what's the proposal for the better way?

Comment by A. Jesse Jiryu Davis [ 11/May/20 ]

Reopening, I think there's a slightly better way to do this.

Comment by Githook User [ 08/May/20 ]

Author:

{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@mongodb.com', 'username': 'ajdavis'}

Message: SERVER-48045 Use Java 11 for TLA+ model-checking
Branch: master
https://github.com/mongodb/mongo/commit/dc47e87ce770fd14af1d781edc54b4723fe53802

Generated at Thu Feb 08 05:15:58 UTC 2024 using Jira 9.7.1#970001-sha1:2222b88b221c4928ef0de3161136cc90c8356a66.