OverviewCakeML:472e8a3848db6facbce05d42a5bd13544d05e308
Add ALOOKUP to rewrites of nsLookup_conv
#856 (printing)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
Merge pull request #852 from CakeML/tidy-up
HOL:6b1dbc7559064a70fabbe71836947411103b499e
Fix INCLUDES for src/coalgebras
Machine:oven3+4.19.67.1.amd64-smp+
Claimed job
Building+HOL
Starting+developers
Finished+developers++++++++++++++++++++++++++++++++++++++++7.75+135852
Starting+developers/bin
Finished+developers/bin++++++++++++++++++++++++++++++++++++9.58+677940
Starting+semantics/ffi
Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++19.74+244036
Starting+semantics
Finished+semantics+++++++++++++++++++++++++++++++++++++++++191.63+1193884
Starting+semantics/proofs
Finished+semantics/proofs++++++++++++++++++++++++++++++++++480.43+1336404
Starting+semantics/alt_semantics
Finished+semantics/alt_semantics+++++++++++++++++++++++++++25.20+434712
Starting+semantics/alt_semantics/proofs
Finished+semantics/alt_semantics/proofs++++++++++++++++++++323.13+923116
Starting+basis/pure
Finished+basis/pure++++++++++++++++++++++++++++++++++++++++380.74+840240
Starting+translator
Finished+translator++++++++++++++++++++++++++++++++++++++++352.93+1656744
Starting+compiler/parsing
Finished+compiler/parsing++++++++++++++++++++++++++++++++++159.84+1884692
Starting+characteristic
Finished+characteristic++++++++++++++++++++++++++++++++++++715.01+2158108
Starting+translator/monadic
Finished+translator/monadic++++++++++++++++++++++++++++++++205.36+1559332
Starting+basis
Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6067.04+15474204
Starting+compiler/inference
Finished+compiler/inference++++++++++++++++++++++++++++++++161.90+1030980
Starting+compiler/backend/reg_alloc
Finished+compiler/backend/reg_alloc++++++++++++++++++++++++124.24+1324616
Starting+compiler/backend/gc
Finished+compiler/backend/gc+++++++++++++++++++++++++++++++406.32+1777188
Starting+compiler/backend
Finished+compiler/backend++++++++++++++++++++++++++++++++++531.08+2465600
Starting+compiler/encoders/asm
Finished+compiler/encoders/asm+++++++++++++++++++++++++++++50.18+858116
Starting+compiler/encoders/x64
Finished+compiler/encoders/x64+++++++++++++++++++++++++++++134.14+1061436
Starting+compiler/encoders/arm7
Finished+compiler/encoders/arm7++++++++++++++++++++++++++++282.16+1721468
Starting+compiler/encoders/arm8
Finished+compiler/encoders/arm8++++++++++++++++++++++++++++83.92+700836
Starting+compiler/encoders/mips
Finished+compiler/encoders/mips++++++++++++++++++++++++++++191.11+1244192
Starting+compiler/encoders/riscv
Finished+compiler/encoders/riscv+++++++++++++++++++++++++++227.16+1147768
Starting+compiler/encoders/ag32
Finished+compiler/encoders/ag32++++++++++++++++++++++++++++41.23+703252
Starting+compiler/backend/x64
Finished+compiler/backend/x64++++++++++++++++++++++++++++++44.35+1422408
Starting+compiler/backend/arm7
Finished+compiler/backend/arm7+++++++++++++++++++++++++++++44.23+1653776
Starting+compiler/backend/arm8
Finished+compiler/backend/arm8+++++++++++++++++++++++++++++44.01+1397968
Starting+compiler/backend/mips
Finished+compiler/backend/mips+++++++++++++++++++++++++++++40.29+1546512
Starting+compiler/backend/riscv
Finished+compiler/backend/riscv++++++++++++++++++++++++++++43.12+1388364
Starting+compiler/backend/ag32
Finished+compiler/backend/ag32+++++++++++++++++++++++++++++144.08+1346796
Starting+compiler/parsing/proofs
Finished+compiler/parsing/proofs+++++++++++++++++++++++++++507.34+1218452
Starting+compiler/inference/proofs
Finished+compiler/inference/proofs+++++++++++++++++++++++++314.54+978724
Starting+compiler/backend/semantics
Finished+compiler/backend/semantics++++++++++++++++++++++++3766.78+2161084
Starting+compiler/backend/reg_alloc/proofs
Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++457.67+866800
Starting+compiler/backend/proofs
Finished+compiler/backend/proofs+++++++++++++++++++++++++++6091.54+22980092
Starting+compiler/backend/serialiser
Finished+compiler/backend/serialiser+++++++++++++++++++++++150.01+2308716
Starting+compiler/encoders/x64/proofs
Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1285.31+5025848
Starting+compiler/encoders/arm7/proofs
Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1751.09+3728540
Starting+compiler/encoders/arm8/proofs
Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++927.39+1536904
Starting+compiler/encoders/mips/proofs
Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1370.43+2559068
Starting+compiler/encoders/riscv/proofs
Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1166.60+1456868
Starting+compiler/encoders/ag32/proofs
Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++348.36+854840
Starting+compiler/backend/x64/proofs
Finished+compiler/backend/x64/proofs+++++++++++++++++++++++49.33+1349152
Starting+compiler/backend/arm7/proofs
Finished+compiler/backend/arm7/proofs++++++++++++++++++++++51.51+1666220
Starting+compiler/backend/arm8/proofs
Finished+compiler/backend/arm8/proofs++++++++++++++++++++++51.70+1689472
Starting+compiler/backend/mips/proofs
Finished+compiler/backend/mips/proofs++++++++++++++++++++++52.46+1442688
Starting+compiler/backend/riscv/proofs
Finished+compiler/backend/riscv/proofs+++++++++++++++++++++51.94+1580008
Starting+compiler/backend/ag32/proofs
Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1656.75+2384252
Starting+compiler/proofs
Finished+compiler/proofs+++++++++++++++++++++++++++++++++++264.12+3332492
Starting+candle/set-theory
Finished+candle/set-theory+++++++++++++++++++++++++++++++++55.67+789328
Starting+candle/syntax-lib
Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++24.19+485980
Starting+candle/standard/syntax
Finished+candle/standard/syntax++++++++++++++++++++++++++++232.32+1340120
Starting+candle/standard/semantics
Finished+candle/standard/semantics+++++++++++++++++++++++++221.76+1229696
Starting+candle/standard/monadic
Finished+candle/standard/monadic+++++++++++++++++++++++++++207.15+1412836
Starting+candle/standard/ml_kernel
Finished+candle/standard/ml_kernel+++++++++++++++++++++++++847.99+3559728
Starting+candle/overloading/syntax
Finished+candle/overloading/syntax+++++++++++++++++++++++++392.61+1642668
Starting+candle/overloading/semantics
Finished+candle/overloading/semantics++++++++++++++++++++++1525.77+2890840
Starting+candle/prover
FAILED:+candle/prover
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Starting work on README.md
Starting work on ast_extrasTheory
README.md (0s) OK
ast_extrasTheory (18s) OK
Starting work on permsTheory
permsTheory (81s) OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory (204s) OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_prover_invTheory (54s) OK
candle_kernel_permsTheory (190s) OK
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory (156s) OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory (93s) OK
Starting work on candle_basis_evaluateTheory
candle_basis_evaluateTheory (61s) OK
Starting work on candle_prover_semanticsTheory
candle_prover_semanticsTheory (80s)FAIL<1>
no assum
error in quse /root/regression/cakeml-1710/candle/prover/candle_prover_semanticsScript.sml : HOL_ERR {message = "no assum", origin_function = "POP_ASSUM", origin_structure = "Tactical"}
error in load /root/regression/cakeml-1710/candle/prover/candle_prover_semanticsScript : HOL_ERR {message = "no assum", origin_function = "POP_ASSUM", origin_structure = "Tactical"}
Proof of
EVERY simple_dec basis EVERY safe_dec basis
failed.
Failed to prove theorem basis_decs_ok.
Uncaught exception: HOL_ERR {message = "no assum", origin_function = "POP_ASSUM", origin_structure = "Tactical"}