Overview

Job 1845

CakeML:5874d51fd2ff96d1dc4edccc0e43aebfc3c5c06e
  Make readme_gen a bit happier
#865 (Iced_cake)
Merging into:82bbc7aaff75d6af713057a1095be95f322a08fd
  Merge pull request #870 from CakeML/itree-semantics
HOL:9808526b233f88ea0a3b91583172af86bafc46ab
  Fix broken proofs after changing several extreal lemmas into [simp]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 FAILED: developers
readme_gen                                                          (0s)     OK
Starting work on README.md
README.md                                                           (0s)FAIL<1>
 RealIntervalInferenceScript.sml: The Type syntax is to be used instead of type_abbrev.
 RealRangeArithScript.sml: The Theorem syntax is to be used instead of store_thm.
 TypeValidatorScript.sml: The Theorem syntax is to be used instead of store_thm.
 floverParserScript.sml: The Theorem syntax is to be used instead of store_thm.
 output: unable to open file: /home/cake/oven/regression/cakeml-1845/icing/flover/output/readmePrefix
 semantics: unable to open file: /home/cake/oven/regression/cakeml-1845/icing/flover/semantics/readmePrefix
 sqrtApproxScript.sml: file must start with (*
 ssaPrgsScript.sml: The Theorem syntax is to be used instead of store_thm.
 These errors were in: /home/cake/oven/regression/cakeml-1845/icing/flover