[CakeML-dev] Recent CF regression

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Tue Feb 28 23:59:29 UTC 2017


You can use the fix suggested in the commits I linked to. I.e., turn
xapp into xapp_spec eq_num_v_thm.

If someone is extra ambitious, they could instead try to make xapp
create eq_XXX_v_thm from eq_v_thm on the fly and do the correct
instantiation.

On 1 March 2017 at 10:55, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> It definitely has to do with xapp on equality of numbers. It produces a existentially quantified goal where the things to be compared are not of type int or num, but of type ‘a. It’s the sort of goal, where if you could instantiate ‘a to num or int, then you could prove it, but of course that’s not how things work. Possibly xapp is internally failing to specialise some theorem before doing something like an irule.
>
> Scott
>
>> On 2017/02/28, at 23:46, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>>
>> 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
>



More information about the Developers mailing list