Job 1725

CakeML:ebbc94cbdb27eb948840b51f2cbb79e585b1a260
  fix for renamed constructor [Jan 17 00:14:08]
#857 (eval-bitmaps)
Merging into:fd3e72e7afc931fb4f4945cae710715da37ea03c
  Merge pull request #852 from CakeML/tidy-up [Jan 05 17:40:32]
HOL:0e74a42a431c508b13c303f1ef44290a2ba31e2c
  Fix typo in documentation of SRULE [Jan 17 23:32:45]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 19 01:13:02 Claimed job
Jan 19 01:13:05 Reusing HOL
Jan 19 01:13:18 Starting developers
Jan 19 01:13:22 Finished developers                                               4s 144MB
Jan 19 01:13:22 Starting developers/bin
Jan 19 01:13:26 Finished developers/bin                                           4s 675MB
Jan 19 01:13:26 Starting semantics/ffi
Jan 19 01:13:35 Finished semantics/ffi                                            8s 235MB
Jan 19 01:13:35 Starting semantics
Jan 19 01:14:59 Finished semantics                                             1m23s   1GB
Jan 19 01:14:59 Starting semantics/proofs
Jan 19 01:18:24 Finished semantics/proofs                                      3m25s   1GB
Jan 19 01:18:25 Starting semantics/alt_semantics
Jan 19 01:18:35 Finished semantics/alt_semantics                                 10s 355MB
Jan 19 01:18:36 Starting semantics/alt_semantics/proofs
Jan 19 01:21:00 Finished semantics/alt_semantics/proofs                        2m24s 835MB
Jan 19 01:21:00 Starting basis/pure
Jan 19 01:21:50 Finished basis/pure                                              50s 861MB
Jan 19 01:21:50 Starting translator
Jan 19 01:24:32 Finished translator                                            2m41s   1GB
Jan 19 01:24:32 Starting compiler/parsing
Jan 19 01:25:45 Finished compiler/parsing                                      1m12s   2GB
Jan 19 01:25:45 Starting characteristic
Jan 19 01:31:28 Finished characteristic                                        5m43s   1GB
Jan 19 01:31:28 Starting translator/monadic
Jan 19 01:33:08 Finished translator/monadic                                    1m39s   1GB
Jan 19 01:33:08 Starting basis
Jan 19 02:17:04 Finished basis                                                43m54s  14GB
Jan 19 02:17:04 Starting compiler/inference
Jan 19 02:18:11 Finished compiler/inference                                    1m06s   1GB
Jan 19 02:18:11 Starting compiler/backend/reg_alloc
Jan 19 02:19:15 Finished compiler/backend/reg_alloc                            1m04s   1GB
Jan 19 02:19:15 Starting compiler/backend/gc
Jan 19 02:22:31 Finished compiler/backend/gc                                   3m15s   1GB
Jan 19 02:22:31 Starting compiler/backend
Jan 19 02:27:02 Finished compiler/backend                                      4m31s   2GB
Jan 19 02:27:03 Starting compiler/encoders/asm
Jan 19 02:27:25 Finished compiler/encoders/asm                                   22s 734MB
Jan 19 02:27:25 Starting compiler/encoders/x64
Jan 19 02:27:51 Finished compiler/encoders/x64                                   25s 990MB
Jan 19 02:27:51 Starting compiler/encoders/arm7
Jan 19 02:28:44 Finished compiler/encoders/arm7                                  52s 730MB
Jan 19 02:28:44 Starting compiler/encoders/arm8
Jan 19 02:28:57 Finished compiler/encoders/arm8                                  13s 934MB
Jan 19 02:28:57 Starting compiler/encoders/mips
Jan 19 02:29:14 Finished compiler/encoders/mips                                  17s   1GB
Jan 19 02:29:14 Starting compiler/encoders/riscv
Jan 19 02:29:30 Finished compiler/encoders/riscv                                 15s 975MB
Jan 19 02:29:30 Starting compiler/encoders/ag32
Jan 19 02:29:48 Finished compiler/encoders/ag32                                  18s 845MB
Jan 19 02:29:48 Starting compiler/backend/x64
Jan 19 02:30:07 Finished compiler/backend/x64                                    18s   1GB
Jan 19 02:30:07 Starting compiler/backend/arm7
Jan 19 02:30:29 Finished compiler/backend/arm7                                   22s   1GB
Jan 19 02:30:29 Starting compiler/backend/arm8
Jan 19 02:30:49 Finished compiler/backend/arm8                                   19s   1GB
Jan 19 02:30:49 Starting compiler/backend/mips
Jan 19 02:31:09 Finished compiler/backend/mips                                   20s   1GB
Jan 19 02:31:09 Starting compiler/backend/riscv
Jan 19 02:31:29 Finished compiler/backend/riscv                                  19s   1GB
Jan 19 02:31:29 Starting compiler/backend/ag32
Jan 19 02:32:38 Finished compiler/backend/ag32                                 1m08s   1GB
Jan 19 02:32:38 Starting compiler/parsing/proofs
Jan 19 02:36:18 Finished compiler/parsing/proofs                               3m39s   1GB
Jan 19 02:36:18 Starting compiler/inference/proofs
Jan 19 02:38:41 Finished compiler/inference/proofs                             2m22s 889MB
Jan 19 02:38:41 Starting compiler/backend/semantics
Jan 19 03:06:28 Finished compiler/backend/semantics                           27m46s   2GB
Jan 19 03:06:28 Starting compiler/backend/reg_alloc/proofs
Jan 19 03:09:53 Finished compiler/backend/reg_alloc/proofs                     3m24s 797MB
Jan 19 03:09:53 Starting compiler/backend/proofs
Jan 19 03:58:20 Finished compiler/backend/proofs                              48m26s  13GB
Jan 19 03:58:20 Starting compiler/backend/serialiser
Jan 19 03:59:31 Finished compiler/backend/serialiser                           1m11s   1GB
Jan 19 03:59:31 Starting compiler/encoders/x64/proofs
Jan 19 04:09:03 Finished compiler/encoders/x64/proofs                          9m31s   4GB
Jan 19 04:09:03 Starting compiler/encoders/arm7/proofs
Jan 19 04:22:20 Finished compiler/encoders/arm7/proofs                        13m16s   3GB
Jan 19 04:22:20 Starting compiler/encoders/arm8/proofs
Jan 19 04:29:08 Finished compiler/encoders/arm8/proofs                         6m48s   1GB
Jan 19 04:29:08 Starting compiler/encoders/mips/proofs
Jan 19 04:39:03 Finished compiler/encoders/mips/proofs                         9m54s   2GB
Jan 19 04:39:03 Starting compiler/encoders/riscv/proofs
Jan 19 04:47:53 Finished compiler/encoders/riscv/proofs                        8m50s   1GB
Jan 19 04:47:53 Starting compiler/encoders/ag32/proofs
Jan 19 04:50:28 Finished compiler/encoders/ag32/proofs                         2m34s 707MB
Jan 19 04:50:28 Starting compiler/backend/x64/proofs
Jan 19 04:50:50 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 19 04:50:50 Starting compiler/backend/arm7/proofs
Jan 19 04:51:15 Finished compiler/backend/arm7/proofs                            24s   1GB
Jan 19 04:51:15 Starting compiler/backend/arm8/proofs
Jan 19 04:51:39 Finished compiler/backend/arm8/proofs                            23s   1GB
Jan 19 04:51:39 Starting compiler/backend/mips/proofs
Jan 19 04:52:02 Finished compiler/backend/mips/proofs                            22s   1GB
Jan 19 04:52:03 Starting compiler/backend/riscv/proofs
Jan 19 04:52:26 Finished compiler/backend/riscv/proofs                           22s   1GB
Jan 19 04:52:26 Starting compiler/backend/ag32/proofs
Jan 19 05:04:50 Finished compiler/backend/ag32/proofs                         12m22s   2GB
Jan 19 05:04:50 Starting compiler/proofs
Jan 19 05:06:28 Finished compiler/proofs                                       1m38s   3GB
Jan 19 05:06:28 Starting candle/set-theory
Jan 19 05:06:56 Finished candle/set-theory                                       27s 742MB
Jan 19 05:06:56 Starting candle/syntax-lib
Jan 19 05:07:06 Finished candle/syntax-lib                                       10s 612MB
Jan 19 05:07:06 Starting candle/standard/syntax
Jan 19 05:08:54 Finished candle/standard/syntax                                1m47s   1GB
Jan 19 05:08:54 Starting candle/standard/semantics
Jan 19 05:10:37 Finished candle/standard/semantics                             1m42s   1GB
Jan 19 05:10:37 Starting candle/standard/monadic
Jan 19 05:12:10 Finished candle/standard/monadic                               1m32s   1GB
Jan 19 05:12:10 Starting candle/standard/ml_kernel
Jan 19 05:18:43 Finished candle/standard/ml_kernel                             6m33s   4GB
Jan 19 05:18:43 Starting candle/overloading/syntax
Jan 19 05:21:43 Finished candle/overloading/syntax                             2m59s   1GB
Jan 19 05:21:43 Starting candle/overloading/semantics
Jan 19 05:33:16 Finished candle/overloading/semantics                         11m32s   2GB
Jan 19 05:33:16 Starting candle/prover
Jan 19 05:40:20 Finished candle/prover                                         7m03s   3GB
Jan 19 05:40:20 Starting pancake
Jan 19 05:42:12 Finished pancake                                               1m52s   2GB
Jan 19 05:42:12 Starting pancake/ffi
Jan 19 05:42:12 Finished pancake/ffi                                              0s   6MB
Jan 19 05:42:12 Starting pancake/semantics
Jan 19 05:44:27 Finished pancake/semantics                                     2m14s   1GB
Jan 19 05:44:27 Starting pancake/proofs
Jan 19 05:56:11 Finished pancake/proofs                                       11m43s   5GB
Jan 19 05:56:11 Starting characteristic/examples
Jan 19 05:57:27 Finished characteristic/examples                               1m16s   2GB
Jan 19 05:57:27 Starting tutorial/solutions
Jan 19 06:13:43 Finished tutorial/solutions                                   16m14s   9GB
Jan 19 06:13:43 Starting translator/monadic/examples
Jan 19 06:16:59 Finished translator/monadic/examples                           3m15s   2GB
Jan 19 06:16:59 Starting examples
Jan 19 06:25:35 Finished examples                                              8m36s   4GB
Jan 19 06:25:35 Starting examples/compilation/x64
Jan 19 08:52:33 Finished examples/compilation/x64                           2h26m55s  19GB
Jan 19 08:52:35 Starting examples/compilation/x64/proofs
Jan 19 08:54:22 Finished examples/compilation/x64/proofs                       1m47s   3GB
Jan 19 08:54:23 Starting examples/compilation/ag32
Jan 19 09:28:40 Finished examples/compilation/ag32                            34m16s   9GB
Jan 19 09:28:40 Starting examples/compilation/ag32/proofs
Jan 19 09:29:26 Finished examples/compilation/ag32/proofs                        46s   2GB
Jan 19 09:29:26 Starting examples/cost
Jan 19 10:24:16 Finished examples/cost                                        54m49s   8GB
Jan 19 10:24:16 Starting examples/lpr_checker
Jan 19 10:25:05 Finished examples/lpr_checker                                    48s   1GB
Jan 19 10:25:05 Starting examples/lpr_checker/array
Jan 19 10:53:12 Finished examples/lpr_checker/array                           28m07s   7GB
Jan 19 10:53:12 Starting examples/lpr_checker/array/compilation
Jan 19 12:14:59 Finished examples/lpr_checker/array/compilation             1h21m45s  24GB
Jan 19 12:14:59 Starting examples/lpr_checker/array/compilation/proofs
Jan 19 12:16:12 Finished examples/lpr_checker/array/compilation/proofs         1m13s   6GB
Jan 19 12:16:12 Starting examples/opentheory
Jan 19 12:25:50 Finished examples/opentheory                                   9m37s   6GB
Jan 19 12:25:50 Starting examples/opentheory
Jan 19 12:25:51 Finished examples/opentheory                                      1s 138MB
Jan 19 12:25:51 Starting examples/opentheory/compilation
Jan 19 13:05:10 Finished examples/opentheory/compilation                      39m19s  27GB
Jan 19 13:05:11 Starting examples/opentheory/compilation/proofs
Jan 19 13:05:51 Finished examples/opentheory/compilation/proofs                  40s   3GB
Jan 19 13:05:52 Starting examples/opentheory/compilation/ag32
Jan 19 13:44:11 Finished examples/opentheory/compilation/ag32                 38m18s  27GB
Jan 19 13:44:11 Starting examples/opentheory/compilation/ag32/proofs
Jan 19 13:45:45 Finished examples/opentheory/compilation/ag32/proofs           1m34s   5GB
Jan 19 13:45:45 Starting examples/sat_encodings
Jan 19 13:47:34 Finished examples/sat_encodings                                1m48s 901MB
Jan 19 13:47:34 Starting examples/sat_encodings/case_studies
Jan 19 13:49:09 Finished examples/sat_encodings/case_studies                   1m34s 745MB
Jan 19 13:49:09 Starting examples/sat_encodings/translation
Jan 19 13:54:38 Finished examples/sat_encodings/translation                    5m29s   2GB
Jan 19 13:54:38 Starting examples/sat_encodings/translation/compilation
Jan 19 14:42:57 Finished examples/sat_encodings/translation/compilation       48m18s  22GB
Jan 19 14:42:57 Starting translator/okasaki-examples
Jan 19 14:47:21 Finished translator/okasaki-examples                           4m22s   1GB
Jan 19 14:47:21 Starting translator/other-examples
Jan 19 14:49:06 Finished translator/other-examples                             1m44s   1GB
Jan 19 14:49:06 Starting compiler/parsing/tests
Jan 19 14:49:34 Finished compiler/parsing/tests                                  28s 603MB
Jan 19 14:49:34 Starting compiler/inference/tests
Jan 19 14:57:26 Finished compiler/inference/tests                              7m51s   4GB
Jan 19 14:57:26 Starting compiler/repl
Jan 19 15:06:39 Finished compiler/repl                                         9m12s   6GB
Jan 19 15:06:39 Starting compiler/bootstrap/translation
Jan 19 17:45:51 Finished compiler/bootstrap/translation                     2h39m10s  38GB
Jan 19 17:45:51 Starting unverified/sexpr-bootstrap/x64/64
Jan 19 17:56:27 FAILED: unverified/sexpr-bootstrap/x64/64
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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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)/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/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/developers/bin[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
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(108s)     OK
Starting work on cake.S
cake.S                                         unverified/sexpr-bootstrap/x64/64(477s)     OK
Starting work on cake
cake                                           unverified/sexpr-bootstrap/x64/64  (7s)FAIL<2>
 cc    -c -o cake.o cake.S
 cc    -c -o basis_ffi.o basis_ffi.c
 cc  cake.o basis_ffi.o   -o cake
 /usr/bin/ld: basis_ffi.o: in function `main':
 basis_ffi.c:(.text+0xacc): undefined reference to `cake_codebuffer_end'
 /usr/bin/ld: basis_ffi.c:(.text+0xad3): undefined reference to `cake_text_begin'
 /usr/bin/ld: basis_ffi.c:(.text+0xae8): undefined reference to `cake_text_begin'
 collect2: error: ld returned 1 exit status
 make: *** [Makefile:35: cake] Error 1