Improve build times by moving various things related to correctness from Strata to StrataTest

[keyboardDrummer]

Partial fix for #349

Changes

• Move several theorems so they only build in StrataTest, improving the development speed when working on Strata
• Move all tests, identifiable by calls to #guard or #guard_msg from Strata/ to StrataTest/

Before:

lake build Strata 311.71s user 103.99s system 175% cpu 3:56.88 total

After:

lake build Strata 166.28s user 70.21s system 210% cpu 1:52.31 total

Testing

Refactoring that does not need any tests

[aqjune-aws]

If we are to move the Correct files, I think they must not be placed in "StrataTest" because they are not tests. :) Instead we must place them at a new "StrataProof" project.
Re. eval + guard_msgs - did removing them significantly improve the lake build speed? I thought they were supposed to be lightweight.

[keyboardDrummer]

Re. eval + guard_msgs - did removing them significantly improve the lake build speed? I thought they were supposed to be lightweight.

Not much. It went from about ~120s to ~112s

[keyboardDrummer]

If we are to move the Correct files, I think they must not be placed in "StrataTest" because they are not tests. :) Instead we must place them at a new "StrataProof" project.

Could there be cases where adding a proof makes certain tests no longer necessary? If the answer is yes, wouldn't it make sense to keep the proofs and the tests physically close together, so such cases are more easily identified?

Are there cases where you want to verify all the proofs but not run all the tests? What are benefits of keeping the two separate?

[aqjune-aws]

Could there be cases where adding a proof makes certain tests no longer necessary? If the answer is yes, wouldn't it make sense to keep the proofs and the tests physically close together, so such cases are more easily identified?

I think tests can still be useful after proofs - when someone wants to make changes to the implementation existing tests are good sanity checks for confirming whether the changes make sense. Confirming it by rewriting proofs will take slightly more.
Indeed, having these two physically close will be quite useful for identifying the locations. If we are to put those at one StrataTest target, the target name seems somewhat misleading... StrataTest will give an impression that the proofs are not about full correctness but proofs for correctness in specific test cases.

I guess a real concern is that actually there aren't that many proofs at the moment, so the necessity of having a separate StrataProof target seems slightly faint. But on the other hand, the experimental result do show that it is the proofs rather than the #evals that reduce the time. So if the main concern is compilation time, I believe this justifies the separate 'StrataProof' target. In the case of CompCert, most of time build time is on proofs, and Strata will probably follow the same path.

[keyboardDrummer]

I think tests can still be useful after proofs - when someone wants to make changes to the implementation existing tests are good sanity checks for confirming whether the changes make sense. Confirming it by rewriting proofs will take slightly more. Indeed, having these two physically close will be quite useful for identifying the locations. If we are to put those at one StrataTest target, the target name seems somewhat misleading... StrataTest will give an impression that the proofs are not about full correctness but proofs for correctness in specific test cases.

I guess a real concern is that actually there aren't that many proofs at the moment, so the necessity of having a separate StrataProof target seems slightly faint. But on the other hand, the experimental result do show that it is the proofs rather than the #evals that reduce the time. So if the main concern is compilation time, I believe this justifies the separate 'StrataProof' target. In the case of CompCert, most of time build time is on proofs, and Strata will probably follow the same path.

Do you want me to change something still? I don't have a strong opinion on the folders, so I'm happy to do whatever you prefer. My preference right now is to have both proofs and tests in StrataTest. What I like about the name StrataTest is that it matches the lake test command, it helps make it clear that everything in this folder is run on lake test. If there was a lake check command then I'd prefer the name StrataCheck.

[aqjune-aws]

Yep, I am fine with putting the proofs in StrataTest since I could not figure out how to add a custom command, e.g., lake proof.

[joscoh]

I would also prefer in the long run a separate StrataProof folder and build process. Particularly when developing proofs, it would nice to not care about running the tests. But I think it is fine to combine them for this PR and change the build processes later if others agree.