OverviewCakeML:502d6861eadcf3ed5a3048c4e0b25f9c52810b4c
Remove TL which hinders translator's no_change_refs
#857 (eval-bitmaps)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
Merge pull request #852 from CakeML/tidy-up
HOL:6b1dbc7559064a70fabbe71836947411103b499e
Fix INCLUDES for src/coalgebras
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 147MB
Starting developers/bin
Finished developers/bin 4s 675MB
Starting semantics/ffi
Finished semantics/ffi 8s 217MB
Starting semantics
Finished semantics 1m22s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m27s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 10s 347MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m24s 958MB
Starting basis/pure
Finished basis/pure 49s 863MB
Starting translator
Finished translator 2m42s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m11s 1GB
Starting characteristic
Finished characteristic 5m38s 2GB
Starting translator/monadic
Finished translator/monadic 1m41s 1GB
Starting basis
Finished basis 43m46s 17GB
Starting compiler/inference
Finished compiler/inference 1m06s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m06s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m14s 1GB
Starting compiler/backend
Finished compiler/backend 4m33s 2GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 22s 725MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 25s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 56s 862MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 13s 900MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 16s 855MB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 15s 835MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 774MB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 21s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 20s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 19s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m06s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 3m36s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m23s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 28m27s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m24s 798MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 48m12s 11GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1m12s 1GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m27s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 12m59s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m34s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m57s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m50s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m33s 683MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 23s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 23s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 24s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 22s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 22s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m38s 2GB
Starting compiler/proofs
Finished compiler/proofs 1m42s 3GB
Starting candle/set-theory
Finished candle/set-theory 27s 858MB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 643MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m46s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m40s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m32s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 6m20s 3GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m02s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 11m35s 2GB
Starting candle/prover
Finished candle/prover 7m05s 3GB
Starting pancake
Finished pancake 1m55s 2GB
Starting pancake/ffi
Finished pancake/ffi 0s 8MB
Starting pancake/semantics
Finished pancake/semantics 2m15s 1GB
Starting pancake/proofs
Finished pancake/proofs 11m51s 5GB
Starting characteristic/examples
Finished characteristic/examples 1m16s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 15m44s 9GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m10s 2GB
Starting examples
Finished examples 8m42s 4GB
Starting examples/compilation/x64
Finished examples/compilation/x64 2h29m12s 19GB
Starting examples/compilation/x64/proofs
Finished examples/compilation/x64/proofs 1m38s 3GB
Starting examples/compilation/ag32
Finished examples/compilation/ag32 33m41s 8GB
Starting examples/compilation/ag32/proofs
Finished examples/compilation/ag32/proofs 45s 3GB
Starting examples/cost
Finished examples/cost 54m19s 8GB
Starting examples/lpr_checker
Finished examples/lpr_checker 47s 1GB
Starting examples/lpr_checker/array
FAILED: examples/lpr_checker/array
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker[0m
Starting work on README.md
Starting work on lpr_composeProgTheory
Starting work on lpr_listTheory
README.md (0s) OK
lpr_listTheory (69s) OK
lpr_composeProgTheory (154s) OK
Starting work on lpr_arrayProgTheory
lpr_arrayProgTheory (701s)FAIL<1>
NONE => INL err
| SOME lpr =>
case ... ... ls (... ... w8z) earliest of
NONE => INL err
| SOME (fml',inds') => INR (... ... inds' cls))
else INL err) v)
failed.
Failed to prove theorem check_unsat'_spec.
Uncaught exception: HOL_ERR {message = " (THEN1 on line 2715) (THEN1 on line 2782) (THEN1 on line 2712) (THEN1 on line 2826) (THEN1 on line 2847) (THEN1 on line 2852)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}