Job 1814

CakeML:26a8781cbc72e741e00c013f73ad90b079fd422d
  Merge pull request #863 from CakeML/repl [Mar 05 16:52:22]
HOL:db75935043ba3dba05bf90120123bf3ff89d2700
  Change Definition foo[notuserdef] to not store ind'n thms [Mar 02 23:34:40]
Machine:oven3+4.19.67.1.amd64-smp+

Mar 05 17:04:39 Claimed job
Mar 05 17:04:48 Building+HOL
Mar 05 17:24:48 Starting+developers
Mar 05 17:24:56 Finished+developers++++++++++++++++++++++++++++++++++++++++8.22+147404
Mar 05 17:24:56 Starting+developers/bin
Mar 05 17:25:10 Finished+developers/bin++++++++++++++++++++++++++++++++++++13.12+1255552
Mar 05 17:25:10 Starting+semantics/ffi
Mar 05 17:25:35 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++24.85+257964
Mar 05 17:25:35 Starting+semantics
Mar 05 17:30:08 Finished+semantics+++++++++++++++++++++++++++++++++++++++++272.86+1092956
Mar 05 17:30:08 Starting+semantics/proofs
Mar 05 17:38:03 Finished+semantics/proofs++++++++++++++++++++++++++++++++++474.64+1140912
Mar 05 17:38:04 Starting+semantics/alt_semantics
Mar 05 17:38:44 Finished+semantics/alt_semantics+++++++++++++++++++++++++++40.02+483144
Mar 05 17:38:44 Starting+semantics/alt_semantics/proofs
Mar 05 17:44:13 Finished+semantics/alt_semantics/proofs++++++++++++++++++++328.93+985692
Mar 05 17:44:13 Starting+basis/pure
Mar 05 17:50:55 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++401.10+983872
Mar 05 17:50:55 Starting+translator
Mar 05 17:57:11 Finished+translator++++++++++++++++++++++++++++++++++++++++376.07+1416404
Mar 05 17:57:11 Starting+compiler/parsing
Mar 05 18:00:08 Finished+compiler/parsing++++++++++++++++++++++++++++++++++176.80+3044764
Mar 05 18:00:08 Starting+characteristic
Mar 05 18:13:35 Finished+characteristic++++++++++++++++++++++++++++++++++++806.49+2123764
Mar 05 18:13:35 Starting+translator/monadic
Mar 05 18:17:32 Finished+translator/monadic++++++++++++++++++++++++++++++++236.72+1472780
Mar 05 18:17:33 Starting+basis
Mar 05 20:01:45 Finished+basis+++++++++++++++++++++++++++++++++++++++++++++6251.76+16882860
Mar 05 20:01:45 Starting+compiler/inference
Mar 05 20:04:49 Finished+compiler/inference++++++++++++++++++++++++++++++++183.69+1560248
Mar 05 20:04:49 Starting+compiler/backend/reg_alloc
Mar 05 20:08:00 Finished+compiler/backend/reg_alloc++++++++++++++++++++++++190.39+2271784
Mar 05 20:08:00 Starting+compiler/backend/gc
Mar 05 20:16:21 Finished+compiler/backend/gc+++++++++++++++++++++++++++++++500.32+2088984
Mar 05 20:16:21 Starting+compiler/backend
Mar 05 20:27:14 Finished+compiler/backend++++++++++++++++++++++++++++++++++653.28+2630356
Mar 05 20:27:15 Starting+compiler/encoders/asm
Mar 05 20:28:18 Finished+compiler/encoders/asm+++++++++++++++++++++++++++++63.16+779172
Mar 05 20:28:18 Starting+compiler/encoders/x64
Mar 05 20:30:54 Finished+compiler/encoders/x64+++++++++++++++++++++++++++++155.37+1044520
Mar 05 20:30:54 Starting+compiler/encoders/arm7
Mar 05 20:36:03 Finished+compiler/encoders/arm7++++++++++++++++++++++++++++309.25+1545188
Mar 05 20:36:04 Starting+compiler/encoders/arm8
Mar 05 20:37:41 Finished+compiler/encoders/arm8++++++++++++++++++++++++++++97.64+740484
Mar 05 20:37:42 Starting+compiler/encoders/arm8_asl
Mar 06 00:49:37 Finished+compiler/encoders/arm8_asl++++++++++++++++++++++++15115.03+40119916
Mar 06 00:49:37 Starting+compiler/encoders/mips
Mar 06 00:53:08 Finished+compiler/encoders/mips++++++++++++++++++++++++++++210.78+1099848
Mar 06 00:53:08 Starting+compiler/encoders/riscv
Mar 06 00:57:03 Finished+compiler/encoders/riscv+++++++++++++++++++++++++++234.87+1217308
Mar 06 00:57:04 Starting+compiler/encoders/ag32
Mar 06 00:57:55 Finished+compiler/encoders/ag32++++++++++++++++++++++++++++50.77+640892
Mar 06 00:57:55 Starting+compiler/backend/x64
Mar 06 00:58:44 Finished+compiler/backend/x64++++++++++++++++++++++++++++++48.60+1394372
Mar 06 00:58:44 Starting+compiler/backend/arm7
Mar 06 00:59:40 Finished+compiler/backend/arm7+++++++++++++++++++++++++++++56.11+1685832
Mar 06 00:59:40 Starting+compiler/backend/arm8
Mar 06 01:00:32 Finished+compiler/backend/arm8+++++++++++++++++++++++++++++51.37+1454804
Mar 06 01:00:32 Starting+compiler/backend/mips
Mar 06 01:01:30 Finished+compiler/backend/mips+++++++++++++++++++++++++++++57.45+1478024
Mar 06 01:01:30 Starting+compiler/backend/riscv
Mar 06 01:02:21 Finished+compiler/backend/riscv++++++++++++++++++++++++++++50.46+1493060
Mar 06 01:02:21 Starting+compiler/backend/ag32
Mar 06 01:05:18 Finished+compiler/backend/ag32+++++++++++++++++++++++++++++177.21+1422504
Mar 06 01:05:18 Starting+compiler/parsing/proofs
Mar 06 01:13:58 Finished+compiler/parsing/proofs+++++++++++++++++++++++++++519.72+1102748
Mar 06 01:13:59 Starting+compiler/inference/proofs
Mar 06 01:19:45 Finished+compiler/inference/proofs+++++++++++++++++++++++++346.01+1137512
Mar 06 01:19:45 Starting+compiler/backend/semantics
Mar 06 02:27:40 Finished+compiler/backend/semantics++++++++++++++++++++++++4073.86+2206624
Mar 06 02:27:40 Starting+compiler/backend/reg_alloc/proofs
Mar 06 02:35:43 Finished+compiler/backend/reg_alloc/proofs+++++++++++++++++482.82+1002908
Mar 06 02:35:43 Starting+compiler/backend/proofs
Mar 06 04:16:00 Finished+compiler/backend/proofs+++++++++++++++++++++++++++6016.34+11567228
Mar 06 04:16:00 Starting+compiler/backend/serialiser
Mar 06 04:19:22 Finished+compiler/backend/serialiser+++++++++++++++++++++++201.96+2519092
Mar 06 04:19:23 Starting+compiler/encoders/x64/proofs
Mar 06 04:40:59 Finished+compiler/encoders/x64/proofs++++++++++++++++++++++1295.93+4299956
Mar 06 04:40:59 Starting+compiler/encoders/arm7/proofs
Mar 06 05:10:46 Finished+compiler/encoders/arm7/proofs+++++++++++++++++++++1786.87+3831056
Mar 06 05:10:46 Starting+compiler/encoders/arm8/proofs
Mar 06 05:26:14 Finished+compiler/encoders/arm8/proofs+++++++++++++++++++++927.19+1499840
Mar 06 05:26:14 Starting+compiler/encoders/arm8_asl/proofs
Mar 06 07:19:48 Finished+compiler/encoders/arm8_asl/proofs+++++++++++++++++6813.27+5946560
Mar 06 07:19:48 Starting+compiler/encoders/mips/proofs
Mar 06 07:42:10 Finished+compiler/encoders/mips/proofs+++++++++++++++++++++1341.97+3970232
Mar 06 07:42:10 Starting+compiler/encoders/riscv/proofs
Mar 06 08:02:16 Finished+compiler/encoders/riscv/proofs++++++++++++++++++++1205.51+1296792
Mar 06 08:02:16 Starting+compiler/encoders/ag32/proofs
Mar 06 08:08:02 Finished+compiler/encoders/ag32/proofs+++++++++++++++++++++345.97+914184
Mar 06 08:08:03 Starting+compiler/backend/x64/proofs
Mar 06 08:09:04 Finished+compiler/backend/x64/proofs+++++++++++++++++++++++61.23+1721408
Mar 06 08:09:04 Starting+compiler/backend/arm7/proofs
Mar 06 08:10:05 Finished+compiler/backend/arm7/proofs++++++++++++++++++++++61.09+1440548
Mar 06 08:10:06 Starting+compiler/backend/arm8/proofs
Mar 06 08:11:08 Finished+compiler/backend/arm8/proofs++++++++++++++++++++++61.91+1674936
Mar 06 08:11:08 Starting+compiler/backend/arm8_asl
Mar 06 08:11:58 Finished+compiler/backend/arm8_asl+++++++++++++++++++++++++49.36+1160912
Mar 06 08:11:58 Starting+compiler/backend/mips/proofs
Mar 06 08:12:56 Finished+compiler/backend/mips/proofs++++++++++++++++++++++58.11+1478364
Mar 06 08:12:57 Starting+compiler/backend/riscv/proofs
Mar 06 08:13:59 Finished+compiler/backend/riscv/proofs+++++++++++++++++++++62.42+1658072
Mar 06 08:13:59 Starting+compiler/backend/ag32/proofs
Mar 06 08:41:39 Finished+compiler/backend/ag32/proofs++++++++++++++++++++++1658.81+3508888
Mar 06 08:41:39 Starting+compiler/proofs
Mar 06 08:46:54 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++315.39+3916720
Mar 06 08:46:55 Starting+candle/set-theory
Mar 06 08:48:05 Finished+candle/set-theory+++++++++++++++++++++++++++++++++70.22+987948
Mar 06 08:48:05 Starting+candle/syntax-lib
Mar 06 08:48:34 Finished+candle/syntax-lib+++++++++++++++++++++++++++++++++28.12+641440
Mar 06 08:48:34 Starting+candle/standard/syntax
Mar 06 08:53:00 Finished+candle/standard/syntax++++++++++++++++++++++++++++266.34+1343676
Mar 06 08:53:01 Starting+candle/standard/semantics
Mar 06 08:57:05 Finished+candle/standard/semantics+++++++++++++++++++++++++244.11+1700128
Mar 06 08:57:05 Starting+candle/standard/monadic
Mar 06 09:01:07 Finished+candle/standard/monadic+++++++++++++++++++++++++++241.77+1777512
Mar 06 09:01:07 Starting+candle/standard/ml_kernel
Mar 06 09:13:56 Finished+candle/standard/ml_kernel+++++++++++++++++++++++++768.10+3001836
Mar 06 09:13:56 Starting+candle/overloading/syntax
Mar 06 09:20:48 Finished+candle/overloading/syntax+++++++++++++++++++++++++411.88+1265264
Mar 06 09:20:48 Starting+candle/overloading/semantics
Mar 06 09:46:38 Finished+candle/overloading/semantics++++++++++++++++++++++1547.92+2959232
Mar 06 09:46:38 Starting+candle/overloading/monadic
Mar 06 09:52:03 Finished+candle/overloading/monadic++++++++++++++++++++++++324.08+1696064
Mar 06 09:52:03 Starting+candle/overloading/ml_kernel
Mar 06 10:06:46 Finished+candle/overloading/ml_kernel++++++++++++++++++++++883.13+3200348
Mar 06 10:06:46 Starting+candle/overloading/ml_checker
Mar 06 10:12:05 Finished+candle/overloading/ml_checker+++++++++++++++++++++318.71+3149392
Mar 06 10:12:05 Starting+candle/prover
Mar 06 10:30:07 Finished+candle/prover+++++++++++++++++++++++++++++++++++++1081.82+2755924
Mar 06 10:30:08 Starting+pancake
Mar 06 10:37:51 Finished+pancake+++++++++++++++++++++++++++++++++++++++++++463.40+4003324
Mar 06 10:37:51 Starting+pancake/ffi
Mar 06 10:37:52 Finished+pancake/ffi+++++++++++++++++++++++++++++++++++++++0.77+31684
Mar 06 10:37:53 Starting+pancake/semantics
Mar 06 10:43:16 Finished+pancake/semantics+++++++++++++++++++++++++++++++++322.91+1149632
Mar 06 10:43:16 Starting+pancake/proofs
Mar 06 11:09:56 Finished+pancake/proofs++++++++++++++++++++++++++++++++++++1600.08+7112916
Mar 06 11:09:57 Starting+characteristic/examples
Mar 06 11:12:48 Finished+characteristic/examples+++++++++++++++++++++++++++171.07+3403008
Mar 06 11:12:48 Starting+tutorial/solutions
Mar 06 11:49:35 Finished+tutorial/solutions++++++++++++++++++++++++++++++++2206.47+9558744
Mar 06 11:49:35 Starting+translator/monadic/examples
Mar 06 11:56:28 Finished+translator/monadic/examples+++++++++++++++++++++++412.70+3318724
Mar 06 11:56:28 Starting+examples
Mar 06 12:15:00 Finished+examples++++++++++++++++++++++++++++++++++++++++++1111.34+3600512
Mar 06 12:15:01 Starting+examples/compilation/x64
Mar 06 17:50:14 Finished+examples/compilation/x64++++++++++++++++++++++++++20113.08+25936860
Mar 06 17:50:14 Starting+examples/compilation/x64/proofs
Mar 06 17:54:42 Finished+examples/compilation/x64/proofs+++++++++++++++++++267.65+3246960
Mar 06 17:54:42 Starting+examples/compilation/ag32
Mar 06 19:12:18 Finished+examples/compilation/ag32+++++++++++++++++++++++++4655.33+9860432
Mar 06 19:12:18 Starting+examples/compilation/ag32/proofs
Mar 06 19:14:11 Finished+examples/compilation/ag32/proofs++++++++++++++++++113.25+3755708
Mar 06 19:14:12 Starting+examples/cost
Mar 06 21:12:37 Finished+examples/cost+++++++++++++++++++++++++++++++++++++7105.25+8718468
Mar 06 21:12:37 Starting+examples/lpr_checker
Mar 06 21:14:46 Finished+examples/lpr_checker++++++++++++++++++++++++++++++128.16+1035660
Mar 06 21:14:46 Starting+examples/lpr_checker/array
Mar 06 22:17:46 Finished+examples/lpr_checker/array++++++++++++++++++++++++3779.86+6897352
Mar 06 22:17:46 Starting+examples/lpr_checker/array/compilation
Mar 07 01:24:02 Finished+examples/lpr_checker/array/compilation++++++++++++11175.66+42726844
Mar 07 01:24:03 Starting+examples/lpr_checker/array/compilation/proofs
Mar 07 01:27:09 Finished+examples/lpr_checker/array/compilation/proofs+++++185.92+6784728
Mar 07 01:27:09 Starting+examples/opentheory
Mar 07 01:48:11 Finished+examples/opentheory+++++++++++++++++++++++++++++++1261.99+3854160
Mar 07 01:48:11 Starting+examples/opentheory
Mar 07 01:48:15 Finished+examples/opentheory+++++++++++++++++++++++++++++++2.89+32628
Mar 07 01:48:15 Starting+examples/opentheory/compilation
Mar 07 03:22:30 Finished+examples/opentheory/compilation+++++++++++++++++++5655.37+36480124
Mar 07 03:22:31 Starting+examples/opentheory/compilation/proofs
Mar 07 03:24:36 Finished+examples/opentheory/compilation/proofs++++++++++++125.42+4704792
Mar 07 03:24:36 Starting+examples/opentheory/compilation/ag32
Mar 07 04:54:02 Finished+examples/opentheory/compilation/ag32++++++++++++++5365.74+37652812
Mar 07 04:54:03 Starting+examples/opentheory/compilation/ag32/proofs
Mar 07 04:57:55 Finished+examples/opentheory/compilation/ag32/proofs+++++++231.61+6426192
Mar 07 04:57:55 Starting+examples/sat_encodings
Mar 07 05:02:15 Finished+examples/sat_encodings++++++++++++++++++++++++++++260.32+979536
Mar 07 05:02:16 Starting+examples/sat_encodings/case_studies
Mar 07 05:06:07 Finished+examples/sat_encodings/case_studies+++++++++++++++231.05+973324
Mar 07 05:06:07 Starting+examples/sat_encodings/translation
Mar 07 05:18:11 Finished+examples/sat_encodings/translation++++++++++++++++723.32+3691000
Mar 07 05:18:11 Starting+examples/sat_encodings/translation/compilation
Mar 07 06:45:51 Finished+examples/sat_encodings/translation/compilation++++5260.11+21464912
Mar 07 06:45:52 Starting+translator/okasaki-examples
Mar 07 06:55:27 Finished+translator/okasaki-examples+++++++++++++++++++++++575.52+2503828
Mar 07 06:55:28 Starting+translator/other-examples
Mar 07 06:59:18 Finished+translator/other-examples+++++++++++++++++++++++++230.07+1672384
Mar 07 06:59:18 Starting+compiler/parsing/tests
Mar 07 07:00:27 Finished+compiler/parsing/tests++++++++++++++++++++++++++++68.32+498860
Mar 07 07:00:27 Starting+compiler/inference/tests
Mar 07 07:16:12 Finished+compiler/inference/tests++++++++++++++++++++++++++944.47+4021468
Mar 07 07:16:12 Starting+compiler/printing/test
Mar 07 07:23:13 Finished+compiler/printing/test++++++++++++++++++++++++++++420.91+4974236
Mar 07 07:23:13 Starting+compiler/repl
Mar 07 07:49:24 Finished+compiler/repl+++++++++++++++++++++++++++++++++++++1570.14+4769168
Mar 07 07:49:24 Starting+compiler/bootstrap/translation
Mar 07 16:26:44 Finished+compiler/bootstrap/translation++++++++++++++++++++31039.81+39573620
Mar 07 16:26:44 Starting+unverified/sexpr-bootstrap/x64/64
Mar 07 16:49:04 Finished+unverified/sexpr-bootstrap/x64/64+++++++++++++++++1338.99+12724080
Mar 07 16:49:04 Starting+unverified/sexpr-bootstrap/x64/32
Mar 07 17:07:18 Finished+unverified/sexpr-bootstrap/x64/32+++++++++++++++++1092.67+9978276
Mar 07 17:07:18 Starting+compiler/benchmarks
Mar 07 17:07:23 Finished+compiler/benchmarks+++++++++++++++++++++++++++++++5.29+55156
Mar 07 17:07:24 Starting+compiler/bootstrap/compilation/x64/64
Mar 09 08:52:48 Finished+compiler/bootstrap/compilation/x64/64+++++++++++++143123.51+92784132
Mar 09 08:52:48 Starting+compiler/bootstrap/compilation/x64/64/proofs
Mar 09 09:32:49 Finished+compiler/bootstrap/compilation/x64/64/proofs++++++2400.53+34024920
Mar 09 09:32:49 Starting+compiler/bootstrap/compilation/x64/32
Mar 10 12:29:27 Finished+compiler/bootstrap/compilation/x64/32+++++++++++++96996.67+109157580
Mar 10 12:29:27 Starting+compiler/bootstrap/compilation/x64/32/proofs
Mar 10 12:35:47 Finished+compiler/bootstrap/compilation/x64/32/proofs++++++379.24+22395524
Mar 10 12:35:47 Starting+compiler/bootstrap/compilation/ag32/32
Mar 11 16:39:28 Finished+compiler/bootstrap/compilation/ag32/32++++++++++++101019.91+109129960
Mar 11 16:39:28 Starting+compiler/bootstrap/compilation/ag32/32/proofs
Mar 11 17:03:19 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"}