Job 628

CakeML:827dcf8ad6bf46e87765deb14c5090fde41fc760
  Merge 'origin/master' into 'cleanup' [Dec 11 14:27:08]
#582 (cleanup)
Merging into:3c96978d87a03a4b4dcf3c85eb41453777b2f86f
  Merge pull request #574 from CakeML/data-cost [Dec 11 11:05:59]
HOL:53a2a87362930e08c64eb2e030a10c92c0b3b45e
  Implement Portable.mapfilter to evaluate from left to right [Dec 12 05:39:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 13 05:10:40 Claimed job
Dec 13 05:10:57 Building HOL
Dec 13 11:50:38 FAILED: building HOL