Job 1815

CakeML:88d8c85caea5ee40c5b25f5691b6b101ea939a80
  Update a README.md [Mar 09 10:54:58]
#864 (tidy-up)
Merging into:26a8781cbc72e741e00c013f73ad90b079fd422d
  Merge pull request #863 from CakeML/repl [Mar 05 16:52:22]
HOL:9ef02c741e59da2e5b90512fc92aa8194c043623
  Fix Holmakefiles for Tamarack example; further modernise port-full [Mar 07 23:09:46]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 09 11:01:56 Claimed job
Mar 09 11:02:03 Building HOL
Mar 09 11:13:43 Starting developers
Mar 09 11:13:48 Finished developers                                               4s  85MB
Mar 09 11:13:48 Starting developers/bin
Mar 09 11:13:56 Finished developers/bin                                           8s   1GB
Mar 09 11:13:57 Starting semantics/ffi
Mar 09 11:14:08 Finished semantics/ffi                                           11s 209MB
Mar 09 11:14:08 Starting semantics
Mar 09 11:16:39 Finished semantics                                             2m30s   1GB
Mar 09 11:16:39 Starting semantics/proofs
Mar 09 11:20:50 Finished semantics/proofs                                      4m09s   1GB
Mar 09 11:20:50 Starting semantics/alt_semantics
Mar 09 11:21:09 Finished semantics/alt_semantics                                 18s 460MB
Mar 09 11:21:09 Starting semantics/alt_semantics/proofs
Mar 09 11:24:18 Finished semantics/alt_semantics/proofs                        3m08s 739MB
Mar 09 11:24:18 Starting basis/pure
Mar 09 13:33:02 Resuming basis/pure
Mar 09 13:33:07 Finished basis/pure                                               4s  15MB
Mar 09 13:33:07 Starting translator
Mar 09 13:37:13 Finished translator                                            4m05s 661MB
Mar 09 13:37:14 Starting compiler/parsing
Mar 09 13:39:11 Finished compiler/parsing                                      1m57s 675MB
Mar 09 13:39:12 Starting characteristic
Mar 09 13:47:04 Finished characteristic                                        7m51s   1GB
Mar 09 13:47:04 Starting translator/monadic
Mar 09 13:49:28 Finished translator/monadic                                    2m23s   1GB
Mar 09 13:49:28 Starting basis
Mar 09 14:50:03 Finished basis                                              1h00m34s   3GB
Mar 09 14:50:03 Starting compiler/inference
Mar 09 14:52:05 Finished compiler/inference                                    2m01s 296MB
Mar 09 14:52:05 Starting compiler/backend/reg_alloc
Mar 09 14:54:23 Finished compiler/backend/reg_alloc                            2m17s 438MB
Mar 09 14:54:23 Starting compiler/backend/gc
Mar 09 15:00:01 Finished compiler/backend/gc                                   5m38s   1GB
Mar 09 15:00:01 Starting compiler/backend
Mar 09 15:07:40 Finished compiler/backend                                      7m38s   2GB
Mar 09 15:07:41 Starting compiler/encoders/asm
Mar 09 15:08:13 Finished compiler/encoders/asm                                   32s 670MB
Mar 09 15:08:14 Starting compiler/encoders/x64
Mar 09 15:09:39 Finished compiler/encoders/x64                                 1m25s 745MB
Mar 09 15:09:39 Starting compiler/encoders/arm7
Mar 09 15:12:21 Finished compiler/encoders/arm7                                2m41s 863MB
Mar 09 15:12:22 Starting compiler/encoders/arm8
Mar 09 15:13:15 Finished compiler/encoders/arm8                                  53s 765MB
Mar 09 15:13:15 Starting compiler/encoders/arm8_asl
Mar 09 17:55:24 Finished compiler/encoders/arm8_asl                         2h42m08s   7GB
Mar 09 17:55:24 Starting compiler/encoders/mips
Mar 09 17:57:14 Finished compiler/encoders/mips                                1m49s   1GB
Mar 09 17:57:14 Starting compiler/encoders/riscv
Mar 09 17:59:20 Finished compiler/encoders/riscv                               2m05s   1GB
Mar 09 17:59:20 Starting compiler/encoders/ag32
Mar 09 17:59:45 Finished compiler/encoders/ag32                                  24s 713MB
Mar 09 17:59:45 Starting compiler/backend/x64
Mar 09 18:00:09 Finished compiler/backend/x64                                    24s   1GB
Mar 09 18:00:09 Starting compiler/backend/arm7
Mar 09 18:00:35 Finished compiler/backend/arm7                                   25s   1GB
Mar 09 18:00:35 Starting compiler/backend/arm8
Mar 09 18:01:01 Finished compiler/backend/arm8                                   25s   1GB
Mar 09 18:01:01 Starting compiler/backend/mips
Mar 09 18:01:25 Finished compiler/backend/mips                                   24s   1GB
Mar 09 18:01:25 Starting compiler/backend/riscv
Mar 09 18:01:51 Finished compiler/backend/riscv                                  25s   1GB
Mar 09 18:01:51 Starting compiler/backend/ag32
Mar 09 18:03:28 Finished compiler/backend/ag32                                 1m36s   1GB
Mar 09 18:03:28 Starting compiler/parsing/proofs
Mar 09 18:07:40 Finished compiler/parsing/proofs                               4m11s   1GB
Mar 09 18:07:40 Starting compiler/inference/proofs
Mar 09 18:10:35 Finished compiler/inference/proofs                             2m54s   1GB
Mar 09 18:10:35 Starting compiler/backend/semantics
Mar 09 18:49:16 Finished compiler/backend/semantics                           38m40s   1GB
Mar 09 18:49:16 Starting compiler/backend/reg_alloc/proofs
Mar 09 18:53:33 Finished compiler/backend/reg_alloc/proofs                     4m16s 622MB
Mar 09 18:53:33 Starting compiler/backend/proofs
Mar 09 20:02:41 Finished compiler/backend/proofs                            1h09m07s   7GB
Mar 09 20:02:41 Starting compiler/backend/serialiser
Mar 09 20:04:44 Finished compiler/backend/serialiser                           2m02s   1GB
Mar 09 20:04:44 Starting compiler/encoders/x64/proofs
Mar 09 20:16:55 Finished compiler/encoders/x64/proofs                         12m10s   1GB
Mar 09 20:16:55 Starting compiler/encoders/arm7/proofs
Mar 09 20:33:45 Finished compiler/encoders/arm7/proofs                        16m49s   1GB
Mar 09 20:33:45 Starting compiler/encoders/arm8/proofs
Mar 09 20:41:47 Finished compiler/encoders/arm8/proofs                         8m02s   1GB
Mar 09 20:41:48 Starting compiler/encoders/arm8_asl/proofs
Mar 09 21:44:00 Finished compiler/encoders/arm8_asl/proofs                  1h02m11s   3GB
Mar 09 21:44:00 Starting compiler/encoders/mips/proofs
Mar 09 21:55:53 Finished compiler/encoders/mips/proofs                        11m52s   1GB
Mar 09 21:55:53 Starting compiler/encoders/riscv/proofs
Mar 09 22:05:28 Finished compiler/encoders/riscv/proofs                        9m35s   1GB
Mar 09 22:05:28 Starting compiler/encoders/ag32/proofs
Mar 09 22:08:25 Finished compiler/encoders/ag32/proofs                         2m56s 705MB
Mar 09 22:08:25 Starting compiler/backend/x64/proofs
Mar 09 22:08:55 Finished compiler/backend/x64/proofs                             30s   1GB
Mar 09 22:08:56 Starting compiler/backend/arm7/proofs
Mar 09 22:09:26 Finished compiler/backend/arm7/proofs                            30s   1GB
Mar 09 22:09:26 Starting compiler/backend/arm8/proofs
Mar 09 22:09:56 Finished compiler/backend/arm8/proofs                            29s   1GB
Mar 09 22:09:56 Starting compiler/backend/arm8_asl
Mar 09 22:10:20 Finished compiler/backend/arm8_asl                               24s   1GB
Mar 09 22:10:20 Starting compiler/backend/mips/proofs
Mar 09 22:10:51 Finished compiler/backend/mips/proofs                            29s   1GB
Mar 09 22:10:51 Starting compiler/backend/riscv/proofs
Mar 09 22:11:21 Finished compiler/backend/riscv/proofs                           29s   1GB
Mar 09 22:11:21 Starting compiler/backend/ag32/proofs
Mar 09 22:26:28 Finished compiler/backend/ag32/proofs                         15m07s   2GB
Mar 09 22:26:29 Starting compiler/proofs
Mar 09 22:29:15 Finished compiler/proofs                                       2m45s   4GB
Mar 09 22:29:15 Starting candle/set-theory
Mar 09 22:29:56 Finished candle/set-theory                                       40s 623MB
Mar 09 22:29:56 Starting candle/syntax-lib
Mar 09 22:30:15 Finished candle/syntax-lib                                       18s 629MB
Mar 09 22:30:15 Starting candle/standard/syntax
Mar 09 22:32:35 Finished candle/standard/syntax                                2m19s 972MB
Mar 09 22:32:35 Starting candle/standard/semantics
Mar 09 22:34:45 Finished candle/standard/semantics                             2m09s   1GB
Mar 09 22:34:45 Starting candle/standard/monadic
Mar 09 22:37:00 Finished candle/standard/monadic                               2m14s   1GB
Mar 09 22:37:01 Starting candle/standard/ml_kernel
Mar 09 22:44:25 Finished candle/standard/ml_kernel                             7m23s   3GB
Mar 09 22:44:25 Starting candle/overloading/syntax
Mar 09 22:48:00 Finished candle/overloading/syntax                             3m35s   1GB
Mar 09 22:48:01 Starting candle/overloading/semantics
Mar 09 23:01:00 Finished candle/overloading/semantics                         12m59s   2GB
Mar 09 23:01:00 Starting candle/overloading/monadic
Mar 09 23:03:53 Finished candle/overloading/monadic                            2m52s   1GB
Mar 09 23:03:53 Starting candle/overloading/ml_kernel
Mar 09 23:12:25 Finished candle/overloading/ml_kernel                          8m31s   3GB
Mar 09 23:12:25 Starting candle/overloading/ml_checker
Mar 09 23:15:02 Finished candle/overloading/ml_checker                         2m37s   3GB
Mar 09 23:15:02 Starting candle/prover
Mar 09 23:24:00 Finished candle/prover                                         8m57s   3GB
Mar 09 23:24:01 Starting pancake
Mar 09 23:28:20 Finished pancake                                               4m18s   2GB
Mar 09 23:28:20 Starting pancake/ffi
Mar 09 23:28:21 Finished pancake/ffi                                              0s  17MB
Mar 09 23:28:21 Starting pancake/semantics
Mar 09 23:31:16 Finished pancake/semantics                                     2m55s   1GB
Mar 09 23:31:17 Starting pancake/proofs
Mar 09 23:45:24 Finished pancake/proofs                                       14m06s   6GB
Mar 09 23:45:24 Starting characteristic/examples
Mar 09 23:47:25 Finished characteristic/examples                               2m01s   1GB
Mar 09 23:47:25 Starting tutorial/solutions
Mar 10 00:05:59 Finished tutorial/solutions                                   18m33s   7GB
Mar 10 00:05:59 Starting translator/monadic/examples
Mar 10 00:11:08 Finished translator/monadic/examples                           5m08s   3GB
Mar 10 00:11:08 Starting examples
Mar 10 00:25:35 Finished examples                                             14m26s   3GB
Mar 10 00:25:35 Starting examples/compilation/x64
Mar 10 03:34:25 Finished examples/compilation/x64                           3h08m49s   7GB
Mar 10 03:34:26 Starting examples/compilation/x64/proofs
Mar 10 03:38:17 Finished examples/compilation/x64/proofs                       3m51s   2GB
Mar 10 03:38:18 Starting examples/compilation/ag32
Mar 10 04:22:05 Finished examples/compilation/ag32                            43m47s   6GB
Mar 10 04:22:05 Starting examples/compilation/ag32/proofs
Mar 10 04:23:38 Finished examples/compilation/ag32/proofs                      1m32s   2GB
Mar 10 04:23:38 Starting examples/cost
Mar 10 05:41:33 Finished examples/cost                                      1h17m52s   3GB
Mar 10 05:41:33 Starting examples/lpr_checker
Mar 10 05:42:46 Finished examples/lpr_checker                                  1m13s   1GB
Mar 10 05:42:47 Starting examples/lpr_checker/array
Mar 10 06:17:24 Finished examples/lpr_checker/array                           34m36s   3GB
Mar 10 06:17:24 Starting examples/lpr_checker/array/compilation
Mar 10 08:07:05 Finished examples/lpr_checker/array/compilation             1h49m40s   7GB
Mar 10 08:07:06 Starting examples/lpr_checker/array/compilation/proofs
Mar 10 08:09:50 Finished examples/lpr_checker/array/compilation/proofs         2m44s   2GB
Mar 10 08:09:51 Starting examples/opentheory
Mar 10 08:21:52 Finished examples/opentheory                                  12m01s   3GB
Mar 10 08:21:52 Starting examples/opentheory
Mar 10 08:21:54 Finished examples/opentheory                                      1s  18MB
Mar 10 08:21:55 Starting examples/opentheory/compilation
Mar 10 09:22:51 Finished examples/opentheory/compilation                    1h00m56s   8GB
Mar 10 09:22:51 Starting examples/opentheory/compilation/proofs
Mar 10 09:24:12 Finished examples/opentheory/compilation/proofs                1m20s   3GB
Mar 10 09:24:12 Starting examples/opentheory/compilation/ag32
Mar 10 10:15:02 Finished examples/opentheory/compilation/ag32                 50m49s   7GB
Mar 10 10:15:02 Starting examples/opentheory/compilation/ag32/proofs
Mar 10 10:17:48 Finished examples/opentheory/compilation/ag32/proofs           2m45s   2GB
Mar 10 10:17:48 Starting examples/sat_encodings
Mar 10 10:20:01 Finished examples/sat_encodings                                2m12s 843MB
Mar 10 10:20:01 Starting examples/sat_encodings/case_studies
Mar 10 10:22:01 Finished examples/sat_encodings/case_studies                   1m59s 768MB
Mar 10 10:22:02 Starting examples/sat_encodings/translation
Mar 10 10:29:22 Finished examples/sat_encodings/translation                    7m18s   3GB
Mar 10 10:29:22 Starting examples/sat_encodings/translation/compilation
Mar 10 11:38:54 Finished examples/sat_encodings/translation/compilation     1h09m31s   5GB
Mar 10 11:38:54 Starting translator/okasaki-examples
Mar 10 11:44:57 Finished translator/okasaki-examples                           6m02s   1GB
Mar 10 11:44:57 Starting translator/other-examples
Mar 10 11:47:37 Finished translator/other-examples                             2m39s   1GB
Mar 10 11:47:37 Starting compiler/parsing/tests
Mar 10 11:48:11 Finished compiler/parsing/tests                                  33s 559MB
Mar 10 11:48:12 Starting compiler/inference/tests
Mar 10 11:57:23 Finished compiler/inference/tests                              9m11s   4GB
Mar 10 11:57:23 Starting compiler/printing/test
Mar 10 12:02:16 Finished compiler/printing/test                                4m52s   1GB
Mar 10 12:02:16 Starting compiler/repl
Mar 10 12:19:02 Finished compiler/repl                                        16m45s   4GB
Mar 10 12:19:02 Starting compiler/bootstrap/translation
Mar 10 17:25:11 Finished compiler/bootstrap/translation                     5h06m08s  11GB
Mar 10 17:25:11 Starting unverified/sexpr-bootstrap/x64/64
Mar 10 17:37:22 Finished unverified/sexpr-bootstrap/x64/64                    12m10s   8GB
Mar 10 17:37:22 Starting unverified/sexpr-bootstrap/x64/32
Mar 10 17:47:11 Finished unverified/sexpr-bootstrap/x64/32                     9m48s   8GB
Mar 10 17:47:11 Starting compiler/benchmarks
Mar 10 17:47:16 Finished compiler/benchmarks                                      4s  30MB
Mar 10 17:47:16 Starting compiler/bootstrap/compilation/x64/64
Mar 13 05:43:50 FAILED: compiler/bootstrap/compilation/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/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/model
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/model
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/model
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/model
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/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanned 90 directories
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                                           (0s)     OK
cake-sexpr-32                                                     (220s)     OK
cake-sexpr-64                                                     (309s)     OK
to_dataBootstrapTheory                                            (149m)     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                          (40h)     OK
Starting work on cake.S
cake.S                                                             (17h)FAIL<Signal 9>
   val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "x64Bootstrap">>
           lab_to_target eval: runtime: 16h05m32s,    gctime: 13h21m09s,     systime: 10m12s.
           lab_to_target real: 18h57m24s
           lab_to_target size: 143851050