[CakeML-dev] Recent CF regression

[Scott Owens]

Thanks for fixing this.

However, this is going to be a disaster if we want to include CF in the tutorials. "Mostly you should use xapp, except that sometimes it silently fails and produces unprovable goals that look provable unless you turn on printing with types."

Scott

> On 2017/03/01, at 04:48, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 
> I'm going to apply the eq_num_v_thm fix to get these examples working
> again. (Let me know if you're in the middle of doing stuff to them...)
> 
> I think the basis branch may currently be in a stable state - if so,
> I'm also going to merge it to master. But I won't delete it, so we can
> continue working with breaking changes there.
> 
> On 1 March 2017 at 10:59, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>> 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
>>>