search

rems-project / cn-tutorial

8 stars 8 forks source link

Integrate `cn-runtime-testing` branch into `main` #70

Open septract opened 3 months ago

septract commented 3 months ago

The cn-runtime-testing branch includes a lot of changes needed for applying the runtime spec testing capabilities on the tutorial examples. The current cerberus repo CI setup for RTT points to this branch, rather than main. We should integrate the branch.

@dc-mak

dc-mak commented 2 months ago

This branch was mostly a stop-gap for work-arounds (sometimes based on missing features, sometimes based on ignorance) in the run up to POPL deadline. Agreed the end goal is to make CN runtime testing CI on the main branch. @rbanerjee20 has agreed to decide and execute how that is achieved.

rbanerjee20 commented 2 months ago

I would prefer not to merge the cn-runtime-testing branch into main right now since a lot of the changes Dhruv made before the POPL deadline involved changing the CN tutorial example files themselves to adjust for the fact that certain features were not implemented yet. Morally those features should exist in CN runtime testing, and implementing them is (part of) what I am working on now. So merging cn-runtime-testing would lead to some unnecessary hacks existing on main - it would probably be counterintuitive to have examples that fall into this (somewhat arbitrarily) restricted subset of CN on main when that restriction isn't needed for proof.

As a result I would propose we don't converge the two branches, but I am happy to think about how the CI might be improved such that as I push each feature/fix, more real CN tutorial examples from main can be checked and moved out of the "buggy" list, over and above the regression testing that is taking place on each push to Cerberus currently.

rbanerjee20 commented 2 months ago

(I briefly thought about there being one directory of examples for proof and one for runtime testing on main but this also seems counterintuitive given our "CN testing and proof can be done using the same specs" story)

septract commented 2 months ago

That seems reasonable as a short-term measure @rbanerjee20, but there will be an annoying cost to maintaining the branch if it sticks around for more than a few weeks. I think if we're not careful, the branch will diverge significantly (eg I know @bcpierce00 is about to land a big refactor to align with his CN style recommendations).

What changes exactly are needed to support what you need? Eg. could we write 'test harness' files which wrap the files on main ? Or are the changes needed deep and pervasive in the files themselves?

rbanerjee20 commented 2 months ago

Yes, I agree - this is very much a short-term solution. I don't intend for this branch to need to exist for very long as I plan to implement the fixes for these over the next few weeks.

Peter, Neel and I also discussed writing test harness files - tiny files with only a main function that #include the relevant CN tutorial example they want to test, instead of having these main functions that @dc-mak wrote as part of the CN tutorial example files themselves. However, the other changes Dhruv made are indeed deep within the CN specs themselves, which is why I am suggesting we wait a bit. For example, I believe Dhruv had to change CN datatypes into CN records in certain files - these sorts of modifications shouldn't exist in the examples on main morally and also would need to be changed back at some later stage anyway.

septract commented 2 months ago

Understood, this sounds like a good plan. Thanks!