Wrc20 balance fixes

[hjorthjort]

Misc fixes, mostly necessary for verifying $do-balance in KEwasm

[ehildenb]

Some of these lemmas appear to make the term bigger, which always makes me skeptical. But I don't want to hold this up.

[hjorthjort]

Some of these lemmas appear to make the term bigger, which always makes me skeptical. But I don't want to hold this up.

I agree in general, but I think it's alright as long as they are only in a specialized module, like WRC20-LEMMAS. Because they are aimed at that specific program and they work well there.

[ehildenb]

@hjorthjort FYI, once automerge is applied, and it's approved, and tests are passing, you don't need to manually merge it into master. In some cases it will make it merge sooner to do so, but on the average doing so will just increase the build pressure on our servers.

[hjorthjort]

Thanks for letting me know, that's a time saver ehildenb <[email protected]> schrieb am Di., 21. Apr. 2020, 8:18 PM:

…

@hjorthjort <https://github.com/hjorthjort> FYI, once automerge is applied, and it's approved, and tests are passing, you don't need to manually merge it into master. In some cases it will make it merge sooner to do so, but on the average doing so will just increase the build pressure on our servers. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#310 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACBGJJ72F6CEGG2Q23QVHLDRNXPQHANCNFSM4MIVWHZQ> .

[hjorthjort]

Can you make sense of this error? Seems all the tests ran into it:

Cannot contact rvwork-2: java.lang.InterruptedException

[hjorthjort]

Also, the conformance tests all got this error, but it seems it didn't stop them:

error: object directory /home/jenkins-slave/devops.git/objects does not exist; check .git/objects/info/alternates.

[ehildenb]

@hjorthjort the first error just means rvwork-2 went offline for a bit, so you just need to force rebuild.

The second error usually shows up if the Jenkinsfile or Makefile does any git operations. It usually is harmless. It's because we have a server-wide git-cache running, but the cache is not available once you've finished the checkout scm step which actually checks out the code on Jenkins. So any use of git commands in the repo itself will have problems with that step.

[hjorthjort]

Not sure automerge is getting the hint here.