[CakeML-dev] Recent CF regression

[Ramana Kumar]

One possible change that comes to mind is xapp on equality of numbers.

The relevant commits are:
https://github.com/CakeML/cakeml/commit/ba5b533f23f12c07969d33cf643a9cc50575092a
https://github.com/CakeML/cakeml/commit/3fa00165bfbe52445b2c5fcd595e257f054f9e99

If it's not that, could you say which function xapp is failing on? (I
am building it though in the meantime.)

On 1 March 2017 at 10:43, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 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
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers