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