l4v icon indicating copy to clipboard operation
l4v copied to clipboard

MCS: synchronise proof directories with master

Open corlewis opened this issue 2 years ago • 2 comments

Several proof directories on the rt branch had diverged from master in unexpected ways. This commit manually brings them back in sync.

The specific directories are access-control, bisim, dpolicy, drefine, and infoflow.

corlewis avatar Oct 13 '22 02:10 corlewis

Good to bring them in sync again. A lot of these look like wrong indentation got fixed on the MCS side. No problem reverting this here, but we should probably add a todo to fix it in master instead, so it gets carried over in the next merge.

I actually thought it was the other way around, the indentation was fixed on master and had been previously accidentally reverted on MCS.

corlewis avatar Oct 13 '22 07:10 corlewis

Good to bring them in sync again. A lot of these look like wrong indentation got fixed on the MCS side. No problem reverting this here, but we should probably add a todo to fix it in master instead, so it gets carried over in the next merge.

I actually thought it was the other way around, the indentation was fixed on master and had been previously accidentally reverted on MCS.

Entirely possible :-) I thought I saw an example where the indent is now wrong, but I might just have been wrong about that or it's mixed. In any case, the flow should be from master to rt, so no point trying to fix indent in the rt branch.

lsf37 avatar Oct 14 '22 06:10 lsf37