[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

Previous message (by thread): [CakeML-dev] translating i2w
Next message (by thread): [CakeML-dev] anyword commits in HOL break cakeml/semantics
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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

Previous message (by thread): [CakeML-dev] translating i2w
Next message (by thread): [CakeML-dev] anyword commits in HOL break cakeml/semantics
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the Developers mailing list