[CakeML-dev] anyword commits in HOL break cakeml/semantics

[Ramana Kumar]

I failed to reproduce this with HOL at f8ba39d and CakeML at 5271d06.
I.e., my build worked fine on those commits.

On 5 December 2016 at 11:21,  <Michael.Norrish at data61.csiro.au> wrote:
> For reasons I can’t fathom, if HOL is at 8200352, then CakeML at 5271d06 builds in semantics fine.
>
> If HOL is at f8ba39d (origin/multiword and origin/master as I write), then the same CakeML fails to build in semantics, with the terminationScript failing to make on the attempt to prove termination for evaluate.
>
> Michael
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers