Overview

Job 1814

CakeML:26a8781cbc72e741e00c013f73ad90b079fd422d
  Merge pull request #863 from CakeML/repl
HOL:db75935043ba3dba05bf90120123bf3ff89d2700
  Change Definition foo[notuserdef] to not store ind'n thms
Machine:oven3+4.19.67.1.amd64-smp+

 Claimed job
 Building+HOL
 Starting+developers
 Finished+developers++++++++++++++++++++++++++++++++++++++++8.22+147404
 Starting+developers/bin
 Finished+developers/bin++++++++++++++++++++++++++++++++++++13.12+1255552
 Starting+semantics/ffi
 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++24.85+257964
 Starting+semantics
 Finished+semantics+++++++++++++++++++++++++++++++++++++++++272.86+1092956
 Starting+semantics/proofs
 Finished+semantics/proofs++++++++++++++++++++++++++++++++++474.64+1140912
 Starting+semantics/alt_semantics
 Finished+semantics/alt_semantics+++++++++++++++++++++++++++40.02+483144
 Starting+semantics/alt_semantics/proofs
 Finished+semantics/alt_semantics/proofs++++++++++++++++++++328.93+985692
 Starting+basis/pure
 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++401.10+983872
 Starting+translator
 Finished+translator++++++++++++++++++++++++++++++++++++++++376.07+1416404
 Starting+compiler/parsing
 Finished+compiler/parsing++++++++++++++++++++++++++++++++++176.80+3044764
 Starting+characteristic
 Finished+characteristic++++++++++++++++++++++++++++++++++++806.49+2123764
 Starting+translator/monadic
 Finished+translator/monadic++++++++++++++++++++++++++++++++236.72+1472780
 Starting+basis
 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6251.76+16882860
 Starting+compiler/inference
 Finished+compiler/inference++++++++++++++++++++++++++++++++183.69+1560248
 Starting+compiler/backend/reg_alloc
 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++190.39+2271784
 Starting+compiler/backend/gc
 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++500.32+2088984
 Starting+compiler/backend
 Finished+compiler/backend++++++++++++++++++++++++++++++++++653.28+2630356
 Starting+compiler/encoders/asm
 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++63.16+779172
 Starting+compiler/encoders/x64
 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++155.37+1044520
 Starting+compiler/encoders/arm7
 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++309.25+1545188
 Starting+compiler/encoders/arm8
 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++97.64+740484
 Starting+compiler/encoders/arm8_asl
 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++15115.03+40119916
 Starting+compiler/encoders/mips
 Finished+compiler/encoders/mips++++++++++++++++++++++++++++210.78+1099848
 Starting+compiler/encoders/riscv
 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++234.87+1217308
 Starting+compiler/encoders/ag32
 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++50.77+640892
 Starting+compiler/backend/x64
 Finished+compiler/backend/x64++++++++++++++++++++++++++++++48.60+1394372
 Starting+compiler/backend/arm7
 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++56.11+1685832
 Starting+compiler/backend/arm8
 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++51.37+1454804
 Starting+compiler/backend/mips
 Finished+compiler/backend/mips+++++++++++++++++++++++++++++57.45+1478024
 Starting+compiler/backend/riscv
 Finished+compiler/backend/riscv++++++++++++++++++++++++++++50.46+1493060
 Starting+compiler/backend/ag32
 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++177.21+1422504
 Starting+compiler/parsing/proofs
 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++519.72+1102748
 Starting+compiler/inference/proofs
 Finished+compiler/inference/proofs+++++++++++++++++++++++++346.01+1137512
 Starting+compiler/backend/semantics
 Finished+compiler/backend/semantics++++++++++++++++++++++++4073.86+2206624
 Starting+compiler/backend/reg_alloc/proofs
 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++482.82+1002908
 Starting+compiler/backend/proofs
 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6016.34+11567228
 Starting+compiler/backend/serialiser
 Finished+compiler/backend/serialiser+++++++++++++++++++++++201.96+2519092
 Starting+compiler/encoders/x64/proofs
 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1295.93+4299956
 Starting+compiler/encoders/arm7/proofs
 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1786.87+3831056
 Starting+compiler/encoders/arm8/proofs
 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++927.19+1499840
 Starting+compiler/encoders/arm8_asl/proofs
 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++6813.27+5946560
 Starting+compiler/encoders/mips/proofs
 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1341.97+3970232
 Starting+compiler/encoders/riscv/proofs
 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1205.51+1296792
 Starting+compiler/encoders/ag32/proofs
 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++345.97+914184
 Starting+compiler/backend/x64/proofs
 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++61.23+1721408
 Starting+compiler/backend/arm7/proofs
 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++61.09+1440548
 Starting+compiler/backend/arm8/proofs
 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++61.91+1674936
 Starting+compiler/backend/arm8_asl
 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++49.36+1160912
 Starting+compiler/backend/mips/proofs
 Finished+compiler/backend/mips/proofs++++++++++++++++++++++58.11+1478364
 Starting+compiler/backend/riscv/proofs
 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++62.42+1658072
 Starting+compiler/backend/ag32/proofs
 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1658.81+3508888
 Starting+compiler/proofs
 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++315.39+3916720
 Starting+candle/set-theory
 Finished+candle/set-theory+++++++++++++++++++++++++++++++++70.22+987948
 Starting+candle/syntax-lib
 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++28.12+641440
 Starting+candle/standard/syntax
 Finished+candle/standard/syntax++++++++++++++++++++++++++++266.34+1343676
 Starting+candle/standard/semantics
 Finished+candle/standard/semantics+++++++++++++++++++++++++244.11+1700128
 Starting+candle/standard/monadic
 Finished+candle/standard/monadic+++++++++++++++++++++++++++241.77+1777512
 Starting+candle/standard/ml_kernel
 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++768.10+3001836
 Starting+candle/overloading/syntax
 Finished+candle/overloading/syntax+++++++++++++++++++++++++411.88+1265264
 Starting+candle/overloading/semantics
 Finished+candle/overloading/semantics++++++++++++++++++++++1547.92+2959232
 Starting+candle/overloading/monadic
 Finished+candle/overloading/monadic++++++++++++++++++++++++324.08+1696064
 Starting+candle/overloading/ml_kernel
 Finished+candle/overloading/ml_kernel++++++++++++++++++++++883.13+3200348
 Starting+candle/overloading/ml_checker
 Finished+candle/overloading/ml_checker+++++++++++++++++++++318.71+3149392
 Starting+candle/prover
 Finished+candle/prover+++++++++++++++++++++++++++++++++++++1081.82+2755924
 Starting+pancake
 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++463.40+4003324
 Starting+pancake/ffi
 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.77+31684
 Starting+pancake/semantics
 Finished+pancake/semantics+++++++++++++++++++++++++++++++++322.91+1149632
 Starting+pancake/proofs
 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1600.08+7112916
 Starting+characteristic/examples
 Finished+characteristic/examples+++++++++++++++++++++++++++171.07+3403008
 Starting+tutorial/solutions
 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2206.47+9558744
 Starting+translator/monadic/examples
 Finished+translator/monadic/examples+++++++++++++++++++++++412.70+3318724
 Starting+examples
 Finished+examples++++++++++++++++++++++++++++++++++++++++++1111.34+3600512
 Starting+examples/compilation/x64
 Finished+examples/compilation/x64++++++++++++++++++++++++++20113.08+25936860
 Starting+examples/compilation/x64/proofs
 Finished+examples/compilation/x64/proofs+++++++++++++++++++267.65+3246960
 Starting+examples/compilation/ag32
 Finished+examples/compilation/ag32+++++++++++++++++++++++++4655.33+9860432
 Starting+examples/compilation/ag32/proofs
 Finished+examples/compilation/ag32/proofs++++++++++++++++++113.25+3755708
 Starting+examples/cost
 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7105.25+8718468
 Starting+examples/lpr_checker
 Finished+examples/lpr_checker++++++++++++++++++++++++++++++128.16+1035660
 Starting+examples/lpr_checker/array
 Finished+examples/lpr_checker/array++++++++++++++++++++++++3779.86+6897352
 Starting+examples/lpr_checker/array/compilation
 Finished+examples/lpr_checker/array/compilation++++++++++++11175.66+42726844
 Starting+examples/lpr_checker/array/compilation/proofs
 Finished+examples/lpr_checker/array/compilation/proofs+++++185.92+6784728
 Starting+examples/opentheory
 Finished+examples/opentheory+++++++++++++++++++++++++++++++1261.99+3854160
 Starting+examples/opentheory
 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.89+32628
 Starting+examples/opentheory/compilation
 Finished+examples/opentheory/compilation+++++++++++++++++++5655.37+36480124
 Starting+examples/opentheory/compilation/proofs
 Finished+examples/opentheory/compilation/proofs++++++++++++125.42+4704792
 Starting+examples/opentheory/compilation/ag32
 Finished+examples/opentheory/compilation/ag32++++++++++++++5365.74+37652812
 Starting+examples/opentheory/compilation/ag32/proofs
 Finished+examples/opentheory/compilation/ag32/proofs+++++++231.61+6426192
 Starting+examples/sat_encodings
 Finished+examples/sat_encodings++++++++++++++++++++++++++++260.32+979536
 Starting+examples/sat_encodings/case_studies
 Finished+examples/sat_encodings/case_studies+++++++++++++++231.05+973324
 Starting+examples/sat_encodings/translation
 Finished+examples/sat_encodings/translation++++++++++++++++723.32+3691000
 Starting+examples/sat_encodings/translation/compilation
 Finished+examples/sat_encodings/translation/compilation++++5260.11+21464912
 Starting+translator/okasaki-examples
 Finished+translator/okasaki-examples+++++++++++++++++++++++575.52+2503828
 Starting+translator/other-examples
 Finished+translator/other-examples+++++++++++++++++++++++++230.07+1672384
 Starting+compiler/parsing/tests
 Finished+compiler/parsing/tests++++++++++++++++++++++++++++68.32+498860
 Starting+compiler/inference/tests
 Finished+compiler/inference/tests++++++++++++++++++++++++++944.47+4021468
 Starting+compiler/printing/test
 Finished+compiler/printing/test++++++++++++++++++++++++++++420.91+4974236
 Starting+compiler/repl
 Finished+compiler/repl+++++++++++++++++++++++++++++++++++++1570.14+4769168
 Starting+compiler/bootstrap/translation
 Finished+compiler/bootstrap/translation++++++++++++++++++++31039.81+39573620
 Starting+unverified/sexpr-bootstrap/x64/64
 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1338.99+12724080
 Starting+unverified/sexpr-bootstrap/x64/32
 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1092.67+9978276
 Starting+compiler/benchmarks
 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++5.29+55156
 Starting+compiler/bootstrap/compilation/x64/64
 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++143123.51+92784132
 Starting+compiler/bootstrap/compilation/x64/64/proofs
 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++2400.53+34024920
 Starting+compiler/bootstrap/compilation/x64/32
 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++96996.67+109157580
 Starting+compiler/bootstrap/compilation/x64/32/proofs
 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++379.24+22395524
 Starting+compiler/bootstrap/compilation/ag32/32
 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++101019.91+109129960
 Starting+compiler/bootstrap/compilation/ag32/32/proofs
 FAILED:+compiler/bootstrap/compilation/ag32/32/proofs
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)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[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$(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$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[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
Scanning [1m$(CAKEMLDIR)/candle/prover[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32[0m
Scanned 95 directories
Starting work on README.md
Starting work on ag32BootstrapProofTheory
README.md                                                                                                                                                                                             (0s)     OK
ag32BootstrapProofTheory                                                                                                                                                                             (21m)FAIL<1>
 SUM (MAP strlen cl) + LENGTH cl  cline_size  STRLEN inp  stdin_size 
 is_ag32_init_state
   (init_memory code data (THE cake_config.lab_conf.ffi_names) (cl,inp)) ms0 
 installed code 0 data 0 cake_config.lab_conf.ffi_names (basis_ffi cl fs)
   (heap_regs ag32_backend_config.stack_conf.reg_names) cake_machine_config
   (FUNPOW Next (cake_startup_clock ms0 inp cl) ms0)
 
 failed.
 Failed to prove theorem cake_installed.
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}