Job 1694

CakeML:20eed03c8fddc76a811637635fe8ce67835de8af
  Restore string_dec_thm to get bootstrap translation to work [Dec 19 13:44:33]
#850 (eval)
Merging into:761b33d5c59b62a50a3543bc67362744ff2f598a
  Move a forgotten Lem file and update README.md files [Dec 18 17:13:53]
HOL:9511d2021f824ef967db312f1d1a41c58dbf7acb
  Fix a proof in face of automatic simp change in affbde85bd8 [Dec 16 05:35:31]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 19 13:55:06 Claimed job
Dec 19 13:55:13 Reusing HOL
Dec 19 13:55:51 Starting developers
Dec 19 13:55:56 Finished developers                                               4s  88MB
Dec 19 13:55:56 Starting developers/bin
Dec 19 13:56:02 Finished developers/bin                                           5s 670MB
Dec 19 13:56:02 Starting semantics/ffi
Dec 19 13:56:11 Finished semantics/ffi                                            8s 216MB
Dec 19 13:56:11 Starting semantics
Dec 19 13:57:39 Finished semantics                                             1m27s   1GB
Dec 19 13:57:39 Starting semantics/proofs
Dec 19 14:01:28 Finished semantics/proofs                                      3m48s   1GB
Dec 19 14:01:28 Starting semantics/alt_semantics
Dec 19 14:01:40 Finished semantics/alt_semantics                                 11s 364MB
Dec 19 14:01:40 Starting semantics/alt_semantics/proofs
Dec 19 14:04:17 Finished semantics/alt_semantics/proofs                        2m36s 749MB
Dec 19 14:04:17 Starting basis/pure
Dec 19 14:05:08 Finished basis/pure                                              50s 627MB
Dec 19 14:05:09 Starting translator
Dec 19 14:08:08 Finished translator                                            2m59s   1GB
Dec 19 14:08:08 Starting compiler/parsing
Dec 19 14:09:29 Finished compiler/parsing                                      1m20s   3GB
Dec 19 14:09:30 Starting characteristic
Dec 19 14:15:20 Finished characteristic                                        5m50s   2GB
Dec 19 14:15:20 Starting translator/monadic
Dec 19 14:17:00 Finished translator/monadic                                    1m39s   1GB
Dec 19 14:17:00 Starting basis
Dec 19 15:05:47 Finished basis                                                48m45s  14GB
Dec 19 15:05:47 Starting compiler/inference
Dec 19 15:06:57 Finished compiler/inference                                    1m09s   1GB
Dec 19 15:06:57 Starting compiler/backend/reg_alloc
Dec 19 15:08:06 Finished compiler/backend/reg_alloc                            1m08s   1GB
Dec 19 15:08:06 Starting compiler/backend/gc
Dec 19 15:11:40 Finished compiler/backend/gc                                   3m33s   2GB
Dec 19 15:11:40 Starting compiler/backend
Dec 19 15:16:28 Finished compiler/backend                                      4m46s   2GB
Dec 19 15:16:28 Starting compiler/encoders/asm
Dec 19 15:16:51 Finished compiler/encoders/asm                                   23s 720MB
Dec 19 15:16:51 Starting compiler/encoders/x64
Dec 19 15:17:18 Finished compiler/encoders/x64                                   26s 969MB
Dec 19 15:17:18 Starting compiler/encoders/arm7
Dec 19 15:18:11 Finished compiler/encoders/arm7                                  52s 694MB
Dec 19 15:18:12 Starting compiler/encoders/arm8
Dec 19 15:18:26 Finished compiler/encoders/arm8                                  13s 930MB
Dec 19 15:18:26 Starting compiler/encoders/mips
Dec 19 15:18:44 Finished compiler/encoders/mips                                  18s   1GB
Dec 19 15:18:45 Starting compiler/encoders/riscv
Dec 19 15:19:01 Finished compiler/encoders/riscv                                 16s 780MB
Dec 19 15:19:01 Starting compiler/encoders/ag32
Dec 19 15:19:20 Finished compiler/encoders/ag32                                  18s 665MB
Dec 19 15:19:20 Starting compiler/backend/x64
Dec 19 15:19:40 Finished compiler/backend/x64                                    19s   1GB
Dec 19 15:19:40 Starting compiler/backend/arm7
Dec 19 15:20:01 Finished compiler/backend/arm7                                   20s   1GB
Dec 19 15:20:02 Starting compiler/backend/arm8
Dec 19 15:20:22 Finished compiler/backend/arm8                                   20s   1GB
Dec 19 15:20:22 Starting compiler/backend/mips
Dec 19 15:20:42 Finished compiler/backend/mips                                   19s   1GB
Dec 19 15:20:42 Starting compiler/backend/riscv
Dec 19 15:21:02 Finished compiler/backend/riscv                                  20s   1GB
Dec 19 15:21:02 Starting compiler/backend/ag32
Dec 19 15:22:15 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 19 15:22:16 Starting compiler/parsing/proofs
Dec 19 15:26:17 Finished compiler/parsing/proofs                               4m01s   1GB
Dec 19 15:26:18 Starting compiler/inference/proofs
Dec 19 15:28:48 Finished compiler/inference/proofs                             2m30s 948MB
Dec 19 15:28:48 Starting compiler/backend/semantics
Dec 19 16:01:38 Finished compiler/backend/semantics                           32m49s   2GB
Dec 19 16:01:38 Starting compiler/backend/reg_alloc/proofs
Dec 19 16:05:24 Finished compiler/backend/reg_alloc/proofs                     3m45s   1GB
Dec 19 16:05:24 Starting compiler/backend/proofs
Dec 19 17:02:59 Finished compiler/backend/proofs                              57m33s  16GB
Dec 19 17:02:59 Starting compiler/backend/serialiser
Dec 19 17:04:12 Finished compiler/backend/serialiser                           1m12s   1GB
Dec 19 17:04:12 Starting compiler/encoders/x64/proofs
Dec 19 17:14:36 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Dec 19 17:14:36 Starting compiler/encoders/arm7/proofs
Dec 19 17:28:53 Finished compiler/encoders/arm7/proofs                        14m16s   3GB
Dec 19 17:28:53 Starting compiler/encoders/arm8/proofs
Dec 19 17:36:07 Finished compiler/encoders/arm8/proofs                         7m13s   1GB
Dec 19 17:36:07 Starting compiler/encoders/mips/proofs
Dec 19 17:46:39 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Dec 19 17:46:40 Starting compiler/encoders/riscv/proofs
Dec 19 17:56:08 Finished compiler/encoders/riscv/proofs                        9m28s   1GB
Dec 19 17:56:09 Starting compiler/encoders/ag32/proofs
Dec 19 17:58:56 Finished compiler/encoders/ag32/proofs                         2m46s 900MB
Dec 19 17:58:56 Starting compiler/backend/x64/proofs
Dec 19 17:59:20 Finished compiler/backend/x64/proofs                             24s   1GB
Dec 19 17:59:20 Starting compiler/backend/arm7/proofs
Dec 19 17:59:46 Finished compiler/backend/arm7/proofs                            25s   1GB
Dec 19 17:59:46 Starting compiler/backend/arm8/proofs
Dec 19 18:00:10 Finished compiler/backend/arm8/proofs                            24s   1GB
Dec 19 18:00:11 Starting compiler/backend/mips/proofs
Dec 19 18:00:36 Finished compiler/backend/mips/proofs                            24s   1GB
Dec 19 18:00:36 Starting compiler/backend/riscv/proofs
Dec 19 18:01:00 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 19 18:01:00 Starting compiler/backend/ag32/proofs
Dec 19 18:14:27 Finished compiler/backend/ag32/proofs                         13m26s   2GB
Dec 19 18:14:27 Starting compiler/proofs
Dec 19 18:16:14 Finished compiler/proofs                                       1m46s   3GB
Dec 19 18:16:14 Starting candle/set-theory
Dec 19 18:16:42 Finished candle/set-theory                                       27s 820MB
Dec 19 18:16:42 Starting candle/syntax-lib
Dec 19 18:16:53 Finished candle/syntax-lib                                       10s 617MB
Dec 19 18:16:53 Starting candle/standard/syntax
Dec 19 18:18:46 Finished candle/standard/syntax                                1m52s 852MB
Dec 19 18:18:47 Starting candle/standard/semantics
Dec 19 18:20:32 Finished candle/standard/semantics                             1m45s   1GB
Dec 19 18:20:33 Starting candle/standard/monadic
Dec 19 18:22:20 Finished candle/standard/monadic                               1m47s   1GB
Dec 19 18:22:21 Starting candle/standard/ml_kernel
Dec 19 18:28:14 Finished candle/standard/ml_kernel                             5m52s   3GB
Dec 19 18:28:14 Starting candle/overloading/syntax
Dec 19 18:31:25 Finished candle/overloading/syntax                             3m11s   1GB
Dec 19 18:31:26 Starting candle/overloading/semantics
Dec 19 18:43:30 Finished candle/overloading/semantics                         12m03s   2GB
Dec 19 18:43:30 Starting pancake
Dec 19 18:45:27 Finished pancake                                               1m57s   2GB
Dec 19 18:45:27 Starting pancake/ffi
Dec 19 18:45:28 Finished pancake/ffi                                              0s   4MB
Dec 19 18:45:28 Starting pancake/semantics
Dec 19 18:47:57 Finished pancake/semantics                                     2m28s   1GB
Dec 19 18:47:57 Starting pancake/proofs
Dec 19 19:00:43 Finished pancake/proofs                                       12m45s   6GB
Dec 19 19:00:43 Starting characteristic/examples
Dec 19 19:02:09 Finished characteristic/examples                               1m25s   3GB
Dec 19 19:02:09 Starting tutorial/solutions
Dec 19 19:18:49 Finished tutorial/solutions                                   16m39s   9GB
Dec 19 19:18:49 Starting translator/monadic/examples
Dec 19 19:22:19 Finished translator/monadic/examples                           3m29s   2GB
Dec 19 19:22:19 Starting examples
Dec 19 19:32:19 Finished examples                                             10m00s   4GB
Dec 19 19:32:19 Starting examples/compilation/x64
Dec 19 22:07:23 Finished examples/compilation/x64                           2h35m01s  16GB
Dec 19 22:07:23 Starting examples/compilation/x64/proofs
Dec 19 22:09:16 Finished examples/compilation/x64/proofs                       1m52s   3GB
Dec 19 22:09:16 Starting examples/compilation/ag32
Dec 19 22:44:53 Finished examples/compilation/ag32                            35m36s  10GB
Dec 19 22:44:53 Starting examples/compilation/ag32/proofs
Dec 19 22:45:48 Finished examples/compilation/ag32/proofs                        54s   3GB
Dec 19 22:45:48 Starting examples/cost
Dec 19 23:46:52 Finished examples/cost                                      1h01m03s   7GB
Dec 19 23:46:52 Starting examples/lpr_checker
Dec 19 23:47:41 Finished examples/lpr_checker                                    48s   2GB
Dec 19 23:47:41 Starting examples/lpr_checker/array
Dec 20 00:18:29 Finished examples/lpr_checker/array                           30m47s   6GB
Dec 20 00:18:29 Starting examples/lpr_checker/array/compilation
Dec 20 01:45:19 Finished examples/lpr_checker/array/compilation             1h26m47s  29GB
Dec 20 01:45:19 Starting examples/lpr_checker/array/compilation/proofs
Dec 20 01:46:35 Finished examples/lpr_checker/array/compilation/proofs         1m15s   6GB
Dec 20 01:46:35 Starting examples/opentheory
Dec 20 01:56:45 Finished examples/opentheory                                  10m09s   5GB
Dec 20 01:56:45 Starting examples/opentheory
Dec 20 01:56:46 Finished examples/opentheory                                      1s  21MB
Dec 20 01:56:47 Starting examples/opentheory/compilation
Dec 20 02:34:16 Finished examples/opentheory/compilation                      37m29s  26GB
Dec 20 02:34:17 Starting examples/opentheory/compilation/proofs
Dec 20 02:35:02 Finished examples/opentheory/compilation/proofs                  45s   4GB
Dec 20 02:35:02 Starting examples/opentheory/compilation/ag32
Dec 20 03:15:47 Finished examples/opentheory/compilation/ag32                 40m42s  28GB
Dec 20 03:15:47 Starting examples/opentheory/compilation/ag32/proofs
Dec 20 03:17:29 Finished examples/opentheory/compilation/ag32/proofs           1m41s   6GB
Dec 20 03:17:29 Starting examples/sat_encodings
Dec 20 03:19:19 Finished examples/sat_encodings                                1m49s 877MB
Dec 20 03:19:19 Starting examples/sat_encodings/case_studies
Dec 20 03:21:02 Finished examples/sat_encodings/case_studies                   1m42s   1GB
Dec 20 03:21:02 Starting examples/sat_encodings/translation
Dec 20 03:27:03 Finished examples/sat_encodings/translation                    6m01s   3GB
Dec 20 03:27:03 Starting examples/sat_encodings/translation/compilation
Dec 20 04:22:14 Finished examples/sat_encodings/translation/compilation       55m10s  20GB
Dec 20 04:22:14 Starting translator/okasaki-examples
Dec 20 04:27:05 Finished translator/okasaki-examples                           4m49s   1GB
Dec 20 04:27:05 Starting translator/other-examples
Dec 20 04:27:51 Finished translator/other-examples                               45s   1GB
Dec 20 04:27:51 Starting compiler/parsing/tests
Dec 20 04:28:22 Finished compiler/parsing/tests                                  30s 546MB
Dec 20 04:28:22 Starting compiler/inference/tests
Dec 20 04:36:53 Finished compiler/inference/tests                              8m15s   5GB
Dec 20 04:36:53 Starting compiler/bootstrap/translation
Dec 20 07:25:07 Finished compiler/bootstrap/translation                     2h48m12s  26GB
Dec 20 07:25:07 Starting unverified/sexpr-bootstrap/x64/64
Dec 20 07:26:37 FAILED: unverified/sexpr-bootstrap/x64/64
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Starting work on cake.S
Finished $(CAKEMLDIR)/unverified/sexpr-bootstrap                       (0.000s) 
Starting work on README.md
Starting work on cake-sexpr-x64-64
cake.S                                              developers/bin  (0s)     OK
README.md                        unverified/sexpr-bootstrap/x64/64  (0s)     OK
cake-sexpr-x64-64                unverified/sexpr-bootstrap/x64/64 (74s)     OK
Starting work on cake.S
cake.S                           unverified/sexpr-bootstrap/x64/64  (5s)FAIL<1>
 ### ERROR: parse error
 Parsing of sexp syntax failed
 Program exited with nonzero exit code.