Overview

Job 3246

CakeML:43da32e8ee787b66070059120da38890d0c92725
  mllist: use heap-list-sort
#1349 (talsewell:array-heap-sort-cleanup)
Merging into:48ce8d3f3d18621a5da67f004dfd21efbc459a6b
  Merge pull request #1344 from CakeML/mcandidate-fix
HOL:e6d0417424f6e780d9ef01ffce6d7f69f789a706
  Mention change in remove_user_printer's type in release notes
Machine:pavlova

 Claimed job
 Reusing HOL
 Starting developers
 FAILED: developers
Starting work on lint_build_dirs
lint_build_dirs                                                     (0s)     OK
Starting work on lint
lint                                                                (0s)     OK
readme_gen                                                          (0s)     OK
Starting work on README.md
README.md                                                           (0s)FAIL<1>
 Checking: /scratch/cakeml/regression/cakeml-3246
 Checking: /scratch/cakeml/regression/cakeml-3246/basis
 Checking: /scratch/cakeml/regression/cakeml-3246/basis/pure
 ERROR! readme_gen.sml failed due to:
 mllistScript.sml: Triviality has been deprecated. Please use Theorem with a local tag instead.
 These errors were in: /scratch/cakeml/regression/cakeml-3246/basis/pure
 
 Full log: /scratch/cakeml/regression/cakeml-3246/developers/.hol/logs/README.md