Job 1920

CakeML:cdf14d8edadcb9c9f5de58c224a6995f4c89f050
  Fixes following incl of const in configs [Jun 11 07:35:00]
#889 (consts)
Merging into:f7195c3d29d6bd5f389a7ff307f998a45d56552f
  Merge pull request #888 from CakeML/deflate [Jun 09 07:20:45]
HOL:48bc6e3fcf4f5c1a81a122354d8838d83bbce3ef
  Re-organise Holmake code to isolate some "file-system" code [Jun 07 01:51:29]
Machine:oven3

Jun 11 07:46:54 Claimed job
Jun 11 07:47:12 Building HOL
Jun 11 08:07:42 Starting developers
Jun 11 08:07:52 Finished developers                                               9s  97MB
Jun 11 08:07:52 Starting developers/bin
Jun 11 08:08:05 Finished developers/bin                                          13s   1GB
Jun 11 08:08:05 Starting semantics/ffi
Jun 11 08:08:30 Finished semantics/ffi                                           24s 224MB
Jun 11 08:08:30 Starting semantics
Jun 11 08:13:47 Finished semantics                                             5m16s   1GB
Jun 11 08:13:47 Starting semantics/proofs
Jun 11 08:29:10 Finished semantics/proofs                                     15m22s   1GB
Jun 11 08:29:10 Starting semantics/alt_semantics
Jun 11 08:30:07 Finished semantics/alt_semantics                                 57s 576MB
Jun 11 08:30:08 Starting semantics/alt_semantics/proofs
Jun 11 08:55:39 Finished semantics/alt_semantics/proofs                       25m30s   2GB
Jun 11 08:55:39 Starting basis/pure
Jun 11 09:03:10 Finished basis/pure                                            7m30s 895MB
Jun 11 09:03:10 Starting translator
Jun 11 09:10:59 Finished translator                                            7m48s   1GB
Jun 11 09:10:59 Starting compiler/parsing
Jun 11 09:14:12 Finished compiler/parsing                                      3m12s   3GB
Jun 11 09:14:12 Starting characteristic
Jun 11 09:28:48 Finished characteristic                                       14m35s   2GB
Jun 11 09:28:49 Starting translator/monadic
Jun 11 09:33:02 Finished translator/monadic                                    4m13s   1GB
Jun 11 09:33:02 Starting basis
Jun 11 11:25:03 Finished basis                                              1h52m00s  11GB
Jun 11 11:25:03 Starting compiler/inference
Jun 11 11:28:35 Finished compiler/inference                                    3m31s   1GB
Jun 11 11:28:35 Starting compiler/backend/reg_alloc
Jun 11 11:31:49 Finished compiler/backend/reg_alloc                            3m13s   2GB
Jun 11 11:31:49 Starting compiler/backend/gc
Jun 11 11:40:18 Finished compiler/backend/gc                                   8m28s   2GB
Jun 11 11:40:18 Starting compiler/backend
Jun 11 11:51:56 Finished compiler/backend                                     11m37s   3GB
Jun 11 11:51:56 Starting compiler/encoders/asm
Jun 11 11:53:02 Finished compiler/encoders/asm                                 1m05s 837MB
Jun 11 11:53:02 Starting compiler/encoders/x64
Jun 11 11:55:38 Finished compiler/encoders/x64                                 2m35s   1GB
Jun 11 11:55:39 Starting compiler/encoders/arm7
Jun 11 12:00:22 Finished compiler/encoders/arm7                                4m42s   1GB
Jun 11 12:00:22 Starting compiler/encoders/arm8
Jun 11 12:01:56 Finished compiler/encoders/arm8                                1m33s 674MB
Jun 11 12:01:56 Starting compiler/encoders/arm8_asl
Jun 11 16:21:08 Finished compiler/encoders/arm8_asl                         4h19m11s  39GB
Jun 11 16:21:08 Starting compiler/encoders/mips
Jun 11 16:24:28 Finished compiler/encoders/mips                                3m19s   1GB
Jun 11 16:24:28 Starting compiler/encoders/riscv
Jun 11 16:28:14 Finished compiler/encoders/riscv                               3m45s 868MB
Jun 11 16:28:14 Starting compiler/encoders/ag32
Jun 11 16:29:02 Finished compiler/encoders/ag32                                  48s 869MB
Jun 11 16:29:03 Starting compiler/backend/x64
Jun 11 16:29:54 Finished compiler/backend/x64                                    50s   1GB
Jun 11 16:29:54 Starting compiler/backend/arm7
Jun 11 16:30:45 Finished compiler/backend/arm7                                   51s   1GB
Jun 11 16:30:45 Starting compiler/backend/arm8
Jun 11 16:31:32 Finished compiler/backend/arm8                                   46s   1GB
Jun 11 16:31:33 Starting compiler/backend/mips
Jun 11 16:32:23 Finished compiler/backend/mips                                   50s   1GB
Jun 11 16:32:23 Starting compiler/backend/riscv
Jun 11 16:33:14 Finished compiler/backend/riscv                                  50s   1GB
Jun 11 16:33:14 Starting compiler/backend/ag32
Jun 11 16:36:13 Finished compiler/backend/ag32                                 2m58s   1GB
Jun 11 16:36:13 Starting compiler/parsing/proofs
Jun 11 16:44:44 Finished compiler/parsing/proofs                               8m30s   1GB
Jun 11 16:44:44 Starting compiler/inference/proofs
Jun 11 16:50:43 Finished compiler/inference/proofs                             5m58s   1GB
Jun 11 16:50:43 Starting compiler/backend/semantics
Jun 11 17:46:43 Finished compiler/backend/semantics                           55m58s   2GB
Jun 11 17:46:43 Starting compiler/backend/reg_alloc/proofs
Jun 11 17:54:47 Finished compiler/backend/reg_alloc/proofs                     8m03s   1GB
Jun 11 17:54:47 Starting compiler/backend/proofs
Jun 11 19:47:25 Finished compiler/backend/proofs                            1h52m36s  21GB
Jun 11 19:47:25 Starting compiler/backend/serialiser
Jun 11 19:50:55 Finished compiler/backend/serialiser                           3m30s   2GB
Jun 11 19:50:56 Starting compiler/encoders/x64/proofs
Jun 11 20:12:15 Finished compiler/encoders/x64/proofs                         21m19s   5GB
Jun 11 20:12:16 Starting compiler/encoders/arm7/proofs
Jun 11 20:41:49 Finished compiler/encoders/arm7/proofs                        29m32s   3GB
Jun 11 20:41:49 Starting compiler/encoders/arm8/proofs
Jun 11 20:57:05 Finished compiler/encoders/arm8/proofs                        15m15s   1GB
Jun 11 20:57:05 Starting compiler/encoders/arm8_asl/proofs
Jun 11 22:52:57 Finished compiler/encoders/arm8_asl/proofs                  1h55m51s   5GB
Jun 11 22:52:57 Starting compiler/encoders/mips/proofs
Jun 11 23:15:47 Finished compiler/encoders/mips/proofs                        22m49s   2GB
Jun 11 23:15:47 Starting compiler/encoders/riscv/proofs
Jun 11 23:35:50 Finished compiler/encoders/riscv/proofs                       20m02s   1GB
Jun 11 23:35:51 Starting compiler/encoders/ag32/proofs
Jun 11 23:41:29 Finished compiler/encoders/ag32/proofs                         5m38s 886MB
Jun 11 23:41:29 Starting compiler/backend/x64/proofs
Jun 11 23:42:34 Finished compiler/backend/x64/proofs                           1m04s   1GB
Jun 11 23:42:34 Starting compiler/backend/arm7/proofs
Jun 11 23:43:37 Finished compiler/backend/arm7/proofs                          1m03s   1GB
Jun 11 23:43:38 Starting compiler/backend/arm8/proofs
Jun 11 23:44:41 Finished compiler/backend/arm8/proofs                          1m03s   1GB
Jun 11 23:44:41 Starting compiler/backend/arm8_asl
Jun 11 23:45:34 Finished compiler/backend/arm8_asl                               52s   1GB
Jun 11 23:45:34 Starting compiler/backend/mips/proofs
Jun 11 23:46:36 Finished compiler/backend/mips/proofs                          1m02s   1GB
Jun 11 23:46:37 Starting compiler/backend/riscv/proofs
Jun 11 23:47:39 Finished compiler/backend/riscv/proofs                         1m01s   1GB
Jun 11 23:47:39 Starting compiler/backend/ag32/proofs
Jun 12 00:17:33 Finished compiler/backend/ag32/proofs                         29m53s   2GB
Jun 12 00:17:33 Starting compiler/proofs
Jun 12 00:22:58 Finished compiler/proofs                                       5m24s   5GB
Jun 12 00:22:58 Starting candle/set-theory
Jun 12 00:24:08 Finished candle/set-theory                                     1m09s 945MB
Jun 12 00:24:08 Starting candle/syntax-lib
Jun 12 00:24:37 Finished candle/syntax-lib                                       29s 705MB
Jun 12 00:24:37 Starting candle/standard/syntax
Jun 12 00:29:07 Finished candle/standard/syntax                                4m28s   1GB
Jun 12 00:29:07 Starting candle/standard/semantics
Jun 12 00:33:06 Finished candle/standard/semantics                             3m59s   1GB
Jun 12 00:33:07 Starting candle/standard/monadic
Jun 12 00:37:06 Finished candle/standard/monadic                               3m59s   1GB
Jun 12 00:37:06 Starting candle/standard/ml_kernel
Jun 12 00:50:55 Finished candle/standard/ml_kernel                            13m48s   3GB
Jun 12 00:50:55 Starting candle/overloading/syntax
Jun 12 00:57:45 Finished candle/overloading/syntax                             6m49s   1GB
Jun 12 00:57:45 Starting candle/overloading/semantics
Jun 12 01:24:06 Finished candle/overloading/semantics                         26m20s   2GB
Jun 12 01:24:06 Starting candle/overloading/monadic
Jun 12 01:29:40 Finished candle/overloading/monadic                            5m33s   1GB
Jun 12 01:29:40 Starting candle/overloading/ml_kernel
Jun 12 01:45:20 Finished candle/overloading/ml_kernel                         15m39s   3GB
Jun 12 01:45:20 Starting candle/overloading/ml_checker
Jun 12 01:50:43 Finished candle/overloading/ml_checker                         5m22s   3GB
Jun 12 01:50:43 Starting candle/prover
Jun 12 02:15:08 Finished candle/prover                                        24m24s   2GB
Jun 12 02:15:08 Starting pancake
Jun 12 02:23:09 Finished pancake                                               8m01s   3GB
Jun 12 02:23:09 Starting pancake/ffi
Jun 12 02:23:10 Finished pancake/ffi                                              0s  31MB
Jun 12 02:23:11 Starting pancake/semantics
Jun 12 02:28:36 Finished pancake/semantics                                     5m25s   1GB
Jun 12 02:28:36 Starting pancake/proofs
Jun 12 02:54:56 Finished pancake/proofs                                       26m19s   5GB
Jun 12 02:54:57 Starting characteristic/examples
Jun 12 02:57:57 Finished characteristic/examples                               2m59s   3GB
Jun 12 02:57:57 Starting tutorial/solutions
Jun 12 03:33:24 Finished tutorial/solutions                                   35m27s  10GB
Jun 12 03:33:25 Starting translator/monadic/examples
Jun 12 03:40:33 Finished translator/monadic/examples                           7m08s   2GB
Jun 12 03:40:34 Starting examples
Jun 12 04:00:23 Finished examples                                             19m49s   3GB
Jun 12 04:00:24 Starting examples/compilation/x64
Jun 12 08:33:21 Finished examples/compilation/x64                           4h32m57s  17GB
Jun 12 08:33:21 Starting examples/compilation/x64/proofs
Jun 12 08:37:45 Finished examples/compilation/x64/proofs                       4m23s   3GB
Jun 12 08:37:45 Starting examples/compilation/ag32
Jun 12 09:51:50 Finished examples/compilation/ag32                          1h14m03s   8GB
Jun 12 09:51:50 Starting examples/compilation/ag32/proofs
Jun 12 09:53:49 Finished examples/compilation/ag32/proofs                      1m58s   3GB
Jun 12 09:53:49 Starting examples/lpr_checker
Jun 12 09:55:59 Finished examples/lpr_checker                                  2m10s   1GB
Jun 12 09:55:59 Starting examples/lpr_checker/array
Jun 12 11:10:40 Finished examples/lpr_checker/array                         1h14m39s   6GB
Jun 12 11:10:40 Starting examples/lpr_checker/array/compilation
Jun 12 12:29:42 Finished examples/lpr_checker/array/compilation             1h19m02s  34GB
Jun 12 12:29:43 Starting examples/lpr_checker/array/compilation/proofs
Jun 12 12:32:40 Finished examples/lpr_checker/array/compilation/proofs         2m57s   6GB
Jun 12 12:32:41 Starting examples/opentheory
Jun 12 12:55:40 Finished examples/opentheory                                  22m59s   5GB
Jun 12 12:55:41 Starting examples/opentheory
Jun 12 12:55:44 Finished examples/opentheory                                      2s  45MB
Jun 12 12:55:44 Starting examples/opentheory/compilation
Jun 12 14:25:23 Finished examples/opentheory/compilation                    1h29m38s  40GB
Jun 12 14:25:23 Starting examples/opentheory/compilation/proofs
Jun 12 14:27:52 Finished examples/opentheory/compilation/proofs                2m29s   3GB
Jun 12 14:27:52 Starting examples/opentheory/compilation/ag32
Jun 12 15:43:20 Finished examples/opentheory/compilation/ag32               1h15m26s  27GB
Jun 12 15:43:21 Starting examples/opentheory/compilation/ag32/proofs
Jun 12 15:47:10 Finished examples/opentheory/compilation/ag32/proofs           3m49s   4GB
Jun 12 15:47:10 Starting examples/sat_encodings
Jun 12 15:51:30 Finished examples/sat_encodings                                4m19s   1GB
Jun 12 15:51:30 Starting examples/sat_encodings/case_studies
Jun 12 15:55:05 Finished examples/sat_encodings/case_studies                   3m34s 949MB
Jun 12 15:55:05 Starting examples/sat_encodings/translation
Jun 12 16:07:04 Finished examples/sat_encodings/translation                   11m57s   4GB
Jun 12 16:07:04 Starting examples/sat_encodings/translation/compilation
Jun 12 17:32:01 Finished examples/sat_encodings/translation/compilation     1h24m56s  22GB
Jun 12 17:32:01 Starting examples/deflate
Jun 12 17:34:04 Finished examples/deflate                                      2m02s 887MB
Jun 12 17:34:04 Starting examples/deflate/translation
Jun 12 17:37:04 Finished examples/deflate/translation                          2m59s   3GB
Jun 12 17:37:05 Starting examples/deflate/translation/compilation
Jun 12 18:16:13 Finished examples/deflate/translation/compilation             39m08s  14GB
Jun 12 18:16:13 Starting translator/okasaki-examples
Jun 12 18:26:42 Finished translator/okasaki-examples                          10m29s   1GB
Jun 12 18:26:43 Starting translator/other-examples
Jun 12 18:30:29 Finished translator/other-examples                             3m46s   1GB
Jun 12 18:30:29 Starting compiler/parsing/tests
Jun 12 18:31:37 Finished compiler/parsing/tests                                1m07s 678MB
Jun 12 18:31:37 Starting compiler/inference/tests
Jun 12 18:48:03 Finished compiler/inference/tests                             16m25s   5GB
Jun 12 18:48:03 Starting compiler/printing/test
Jun 12 18:55:40 Finished compiler/printing/test                                7m35s   3GB
Jun 12 18:55:40 Starting icing/flover
Jun 12 19:23:26 Finished icing/flover                                         27m46s   1GB
Jun 12 19:23:27 Starting icing/
Jun 12 21:36:36 Finished icing/                                             2h13m08s   7GB
Jun 12 21:36:36 Starting icing/examples
Jun 12 21:39:37 Finished icing/examples                                        3m01s   5GB
Jun 12 21:39:38 Starting compiler/repl
Jun 12 22:06:10 Finished compiler/repl                                        26m31s   4GB
Jun 12 22:06:10 Starting compiler/bootstrap/translation
Jun 13 05:46:13 FAILED: compiler/bootstrap/translation
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/machine-code/hoare-triple[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/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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$(HOLDIR)/examples/machine-code/decompiler[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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/reg_alloc/proofs[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
Scanned 88 directories
Starting work on precparserTheory
Starting work on monadic_encTheory
Starting work on caml_lexTheory
Starting work on README.md
README.md                                                                                                                                                             compiler/bootstrap/translation  (0s)     OK
Starting work on decProgTheory
precparserTheory                                                                                                                                              examples/formal-languages/context-free  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1]                                                                                                                                 (2.262s) 
monadic_encTheory                                                                                                                                                      compiler/encoders/monadic_enc (28s)     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                                                                                                                                                    compiler/encoders/monadic_enc (34s)     OK
monadic_enc64Theory                                                                                                                                                    compiler/encoders/monadic_enc (35s)     OK
Finished $(CAKEMLDIR)/compiler/encoders/monadic_enc [#theories: 3]                                                                                                                                      (97.756s) 
decProgTheory                                                                                                                                                         compiler/bootstrap/translation(345s)     OK
Starting work on to_flatProgTheory
caml_lexTheory                                                                                                                                                                compiler/parsing/ocaml(462s)     OK
Starting work on camlPEGTheory
camlPEGTheory                                                                                                                                                                 compiler/parsing/ocaml(231s)     OK
Starting work on camlPtreeConversionTheory
camlPtreeConversionTheory                                                                                                                                                     compiler/parsing/ocaml(114s)     OK
Starting work on caml_parserTheory
caml_parserTheory                                                                                                                                                             compiler/parsing/ocaml (26s)     OK
Finished $(CAKEMLDIR)/compiler/parsing/ocaml [#theories: 4]                                                                                                                                            (834.665s) 
to_flatProgTheory                                                                                                                                                     compiler/bootstrap/translation(672s)     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                                                     compiler/bootstrap/translation (22m)     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                                                      compiler/bootstrap/translation (20m)     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                                                      compiler/bootstrap/translation(964s)     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                                                     compiler/bootstrap/translation(571s)     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                                                       compiler/bootstrap/translation(455s)     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                                                      compiler/bootstrap/translation (19m)     OK
Starting work on caml_lexProgTheory
caml_lexProgTheory                                                                                                                                                    compiler/bootstrap/translation (17m)     OK
Starting work on caml_parserProgTheory
caml_parserProgTheory                                                                                                                                                 compiler/bootstrap/translation (36m)     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                                                                                   compiler/bootstrap/translation (36m)     OK
Starting work on inferProgTheory
inferProgTheory                                                                                                                                                       compiler/bootstrap/translation (84m)     OK
Starting work on explorerProgTheory
explorerProgTheory                                                                                                                                                    compiler/bootstrap/translation (35m)     OK
Starting work on decodeProgTheory
decodeProgTheory                                                                                                                                                      compiler/bootstrap/translation(599s)     OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                                                                                                                 compiler/bootstrap/translation(528s)     OK
Starting work on to_word32ProgTheory
Starting work on printingProgTheory
printingProgTheory                                                                                                                                                    compiler/bootstrap/translation(346s)     OK
Starting work on to_word64ProgTheory
to_word32ProgTheory                                                                                                                                                   compiler/bootstrap/translation (52m)     OK
Starting work on to_target32ProgTheory
to_word64ProgTheory                                                                                                                                                   compiler/bootstrap/translation (53m)     OK
Starting work on to_target64ProgTheory
to_target32ProgTheory                                                                                                                                                 compiler/bootstrap/translation (25m)     OK
Starting work on arm7ProgTheory
to_target64ProgTheory                                                                                                                                                 compiler/bootstrap/translation (25m)     OK
Starting work on x64ProgTheory
arm7ProgTheory                                                                                                                                                        compiler/bootstrap/translation(704s)     OK
Starting work on ag32ProgTheory
x64ProgTheory                                                                                                                                                         compiler/bootstrap/translation(622s)     OK
Starting work on arm8ProgTheory
ag32ProgTheory                                                                                                                                                        compiler/bootstrap/translation(488s)     OK
Starting work on compiler32ProgTheory
compiler32ProgTheory                                                                                                                                                  compiler/bootstrap/translation(435s)FAIL<1>
 Translating backend_compile
 Adding nsLookup representation thms for [compiler32Prog_env_22]
 Saved theorem _______ "nsLookup_compiler32Prog_env_23_pfun_eqs"
 error in quse /root/regression/cakeml-1920/compiler/bootstrap/translation/compiler32ProgScript.sml : HOL_ERR {message = "Unproved side condition in the translation of backendTheory.compile_def.", origin_function = "failwith", origin_structure = "??"}
 error in load /root/regression/cakeml-1920/compiler/bootstrap/translation/compiler32ProgScript : HOL_ERR {message = "Unproved side condition in the translation of backendTheory.compile_def.", origin_function = "failwith", origin_structure = "??"}
 
 WARNING: backend_compile has a precondition.
 
 Saved theorem _______ "backend_compile_v_thm"
 Uncaught exception: HOL_ERR {message = "Unproved side condition in the translation of backendTheory.compile_def.", origin_function = "failwith", origin_structure = "??"}
arm8ProgTheory                                                                                                                                                        compiler/bootstrap/translation(571s)MKILLED