Overview

Job 2940

CakeML:3a1a76714bef559e7c06f95c50f4466a3fe13991
  Pancake 16bit ShMem: update Pancake top-level proof
#1212 (16bit)
Merging into:b68e46f49bc81902b1785c5861e13b9385818aa4
  Merge pull request #1218 from CakeML/build-tweaks
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses
Machine:lammmington

 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                                                           (1s)FAIL<1>
 Checking: /scratch/cakeml/regression3/cakeml-2940
 Checking: /scratch/cakeml/regression3/cakeml-2940/basis
 Checking: /scratch/cakeml/regression3/cakeml-2940/basis/pure
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/overloading
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/overloading/ml_checker
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/overloading/ml_kernel
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/overloading/monadic
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/overloading/semantics
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/overloading/syntax
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/prover
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/prover/compute
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/set-theory
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/standard
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/standard/ml_kernel
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/standard/ml_kernel/lisp
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/standard/monadic
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/standard/semantics
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/standard/syntax
 Checking: /scratch/cakeml/regression3/cakeml-2940/candle/syntax-lib
 Checking: /scratch/cakeml/regression3/cakeml-2940/characteristic
 Checking: /scratch/cakeml/regression3/cakeml-2940/characteristic/examples
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/San
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/ag32
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/ag32/proofs
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/arm7
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/arm7/proofs
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/arm8
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/arm8/proofs
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/arm8_asl
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/cv_compute
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/gc
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/mips
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/mips/proofs
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/pattern_matching
 Checking: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/proofs
 ERROR! readme_gen.sml failed due to:
 data_to_wordProofScript.sml: Use Theory sytnax instead of old export_theory
 These errors were in: /scratch/cakeml/regression3/cakeml-2940/compiler/backend/proofs
 
 Full log: /scratch/cakeml/regression3/cakeml-2940/developers/.hol/logs/README.md