OverviewCakeML: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