[CakeML-dev] anyword commits in HOL break cakeml/semantics
Ramana.Kumar at cl.cam.ac.uk
Mon Dec 5 04:41:43 UTC 2016
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.
> Developers mailing list
> Developers at cakeml.org
More information about the Developers