[CakeML-dev] Recent CF regression

[Scott Owens]

Recently I’ve been using CF to verify some sorting algorithms. Insertion sort was pretty easy. Quicksort is harder, but I’m making progress. (The annoyances, and nicenesses of CF are the same between the two, but the quicksort algorithm (in particular Hoare’s original partitioning algorithm) has much more intricate invariants.)

I’ve just merged my branch back to the basis branch. My branch had been off of the basis branch, and as of last week sometime, both my insertion sort and quicksort files should have built. Now they don’t as xapp is generating some unprovable goals in what before were trivial cases. This is due to a change on the basis branch in the last few days, possibly in CF itself, or with the array basis library, since my sorting algorithms use arrays. I don’t know how to track down the regression (there’s a lot mysterious to me about how the CF tactics work), can someone help, hopefully whomever has been editing this part of the basis branch recently.

Scott