search

Whiley / WhileyTheoremProver

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
Apache License 2.0
8 stars 2 forks source link

wyal CompileTask.java #150

Open OlaFosheimGrostad opened 4 years ago

OlaFosheimGrostad commented 4 years ago

Line 98: lambda needs a parameter `return (Build.Meter dummy) -> execute(src);`` Line 101: remove throws IOException (lambda fails to type check, and execute does not throw anyway)

DavePearce commented 4 years ago

Hey,

I think you're suggesting it could be improved by including build metering. Yes, that makes sense. Keep in mind, however, that I'm just keeping this theorem prover alive for now. In fact, I'm going to rebuild it soon ... hopefully early in the new year. As such, I'm not maintaining it really other than what is absolutely necessary!

OlaFosheimGrostad commented 4 years ago

It was more that the compiler complained and refused to let it pass type checking. This could be because of my setup. SDK 13.

DavePearce commented 4 years ago

Hey Ola, did you manage to fix this? I'm back from holiday now and getting back onto doing stuff ...