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

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Mon Dec 5 00:21:51 UTC 2016

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.


More information about the Developers mailing list