Job 1383

CakeML:d979dab193020d8e4687a630b6aabd6de4a20cbd
  Fix build failure caused by HOL API change in ThmSetData [Oct 27 06:19:52]
HOL:6c0c2409ecdbd7195911f674a77bfdd39c83816e
  Fix printing of boolean negation after numeric types are loaded [Oct 26 03:48:20]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Oct 27 06:35:02 Claimed job
Oct 27 06:35:05 Reusing HOL
Oct 27 06:35:52 Starting developers
Oct 27 06:35:56 Finished developers                                               4s  69MB
Oct 27 06:35:57 Starting developers/bin
Oct 27 06:36:03 Finished developers/bin                                           6s   1GB
Oct 27 06:36:04 Starting semantics/ffi
Oct 27 06:36:15 Finished semantics/ffi                                           10s 234MB
Oct 27 06:36:15 Starting semantics
Oct 27 06:37:40 Finished semantics                                             1m25s   1GB
Oct 27 06:37:40 Starting semantics/proofs
Oct 27 06:41:12 Finished semantics/proofs                                      3m31s 833MB
Oct 27 06:41:13 Starting semantics/alt_semantics
Oct 27 06:41:22 Finished semantics/alt_semantics                                  8s 279MB
Oct 27 06:41:22 Starting semantics/alt_semantics/proofs
Oct 27 06:43:39 Finished semantics/alt_semantics/proofs                        2m17s 813MB
Oct 27 06:43:39 Starting basis/pure
Oct 27 06:44:30 Finished basis/pure                                              50s 770MB
Oct 27 06:44:30 Starting translator
Oct 27 06:47:18 Finished translator                                            2m47s   1GB
Oct 27 06:47:19 Starting compiler/parsing
Oct 27 06:48:32 Finished compiler/parsing                                      1m12s   2GB
Oct 27 06:48:32 Starting characteristic
Oct 27 06:54:43 Finished characteristic                                        6m11s   1GB
Oct 27 06:54:44 Starting translator/monadic
Oct 27 06:56:25 Finished translator/monadic                                    1m41s   1GB
Oct 27 06:56:25 Starting basis
Oct 27 07:32:37 Finished basis                                                36m11s  10GB
Oct 27 07:32:37 Starting compiler/inference
Oct 27 07:33:49 Finished compiler/inference                                    1m11s   1GB
Oct 27 07:33:49 Starting compiler/backend/reg_alloc
Oct 27 07:34:57 Finished compiler/backend/reg_alloc                            1m07s   1GB
Oct 27 07:34:57 Starting compiler/backend/gc
Oct 27 07:38:38 Finished compiler/backend/gc                                   3m41s   2GB
Oct 27 07:38:38 Starting compiler/backend
Oct 27 07:43:20 Finished compiler/backend                                      4m41s   3GB
Oct 27 07:43:20 Starting compiler/encoders/asm
Oct 27 07:43:43 Finished compiler/encoders/asm                                   22s 649MB
Oct 27 07:43:43 Starting compiler/encoders/x64
Oct 27 07:44:47 Finished compiler/encoders/x64                                 1m03s 774MB
Oct 27 07:44:47 Starting compiler/encoders/arm7
Oct 27 07:46:47 Finished compiler/encoders/arm7                                1m59s   1GB
Oct 27 07:46:47 Starting compiler/encoders/arm8
Oct 27 07:47:24 Finished compiler/encoders/arm8                                  37s 910MB
Oct 27 07:47:25 Starting compiler/encoders/mips
Oct 27 07:48:49 Finished compiler/encoders/mips                                1m24s   1GB
Oct 27 07:48:49 Starting compiler/encoders/riscv
Oct 27 07:50:26 Finished compiler/encoders/riscv                               1m36s   1GB
Oct 27 07:50:26 Starting compiler/encoders/ag32
Oct 27 07:50:45 Finished compiler/encoders/ag32                                  18s 814MB
Oct 27 07:50:45 Starting compiler/backend/x64
Oct 27 07:51:04 Finished compiler/backend/x64                                    18s   1GB
Oct 27 07:51:04 Starting compiler/backend/arm7
Oct 27 07:51:24 Finished compiler/backend/arm7                                   20s   1GB
Oct 27 07:51:25 Starting compiler/backend/arm8
Oct 27 07:51:44 Finished compiler/backend/arm8                                   19s   1GB
Oct 27 07:51:44 Starting compiler/backend/mips
Oct 27 07:52:03 Finished compiler/backend/mips                                   19s   1GB
Oct 27 07:52:04 Starting compiler/backend/riscv
Oct 27 07:52:23 Finished compiler/backend/riscv                                  19s   1GB
Oct 27 07:52:23 Starting compiler/backend/ag32
Oct 27 07:53:35 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 27 07:53:35 Starting compiler/parsing/proofs
Oct 27 07:59:29 Finished compiler/parsing/proofs                               5m53s   1GB
Oct 27 07:59:29 Starting compiler/inference/proofs
Oct 27 08:02:06 Finished compiler/inference/proofs                             2m37s   1GB
Oct 27 08:02:06 Starting compiler/backend/semantics
Oct 27 08:33:46 Finished compiler/backend/semantics                           31m39s   1GB
Oct 27 08:33:46 Starting compiler/backend/reg_alloc/proofs
Oct 27 08:37:34 Finished compiler/backend/reg_alloc/proofs                     3m47s 714MB
Oct 27 08:37:34 Starting compiler/backend/proofs
Oct 27 09:35:07 Finished compiler/backend/proofs                              57m32s  16GB
Oct 27 09:35:07 Starting compiler/encoders/x64/proofs
Oct 27 09:45:25 Finished compiler/encoders/x64/proofs                         10m17s   3GB
Oct 27 09:45:25 Starting compiler/encoders/arm7/proofs
Oct 27 09:59:31 Finished compiler/encoders/arm7/proofs                        14m05s   3GB
Oct 27 09:59:31 Starting compiler/encoders/arm8/proofs
Oct 27 10:06:35 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Oct 27 10:06:35 Starting compiler/encoders/mips/proofs
Oct 27 10:17:25 Finished compiler/encoders/mips/proofs                        10m49s   2GB
Oct 27 10:17:25 Starting compiler/encoders/riscv/proofs
Oct 27 10:26:56 Finished compiler/encoders/riscv/proofs                        9m31s   1GB
Oct 27 10:26:57 Starting compiler/encoders/ag32/proofs
Oct 27 10:29:47 Finished compiler/encoders/ag32/proofs                         2m49s 662MB
Oct 27 10:29:47 Starting compiler/backend/x64/proofs
Oct 27 10:30:07 Finished compiler/backend/x64/proofs                             20s   1GB
Oct 27 10:30:07 Starting compiler/backend/arm7/proofs
Oct 27 10:30:29 Finished compiler/backend/arm7/proofs                            21s   1GB
Oct 27 10:30:30 Starting compiler/backend/arm8/proofs
Oct 27 10:30:49 Finished compiler/backend/arm8/proofs                            19s   1GB
Oct 27 10:30:49 Starting compiler/backend/mips/proofs
Oct 27 10:31:11 Finished compiler/backend/mips/proofs                            21s   1GB
Oct 27 10:31:11 Starting compiler/backend/riscv/proofs
Oct 27 10:31:32 Finished compiler/backend/riscv/proofs                           20s   1GB
Oct 27 10:31:32 Starting compiler/backend/ag32/proofs
Oct 27 10:45:17 Finished compiler/backend/ag32/proofs                         13m44s   2GB
Oct 27 10:45:17 Starting compiler/proofs
Oct 27 10:47:07 Finished compiler/proofs                                       1m49s   3GB
Oct 27 10:47:07 Starting candle/set-theory
Oct 27 10:47:37 Finished candle/set-theory                                       29s 764MB
Oct 27 10:47:37 Starting candle/syntax-lib
Oct 27 10:47:48 Finished candle/syntax-lib                                       10s 619MB
Oct 27 10:47:48 Starting candle/standard/syntax
Oct 27 10:49:42 Finished candle/standard/syntax                                1m53s   1GB
Oct 27 10:49:42 Starting candle/standard/semantics
Oct 27 10:51:30 Finished candle/standard/semantics                             1m47s   1GB
Oct 27 10:51:30 Starting candle/standard/monadic
Oct 27 10:53:18 Finished candle/standard/monadic                               1m47s   1GB
Oct 27 10:53:18 Starting candle/standard/ml_kernel
Oct 27 10:59:04 Finished candle/standard/ml_kernel                             5m45s   4GB
Oct 27 10:59:04 Starting candle/overloading/syntax
Oct 27 11:02:22 Finished candle/overloading/syntax                             3m17s   1GB
Oct 27 11:02:22 Starting candle/overloading/semantics
Oct 27 11:15:27 Finished candle/overloading/semantics                         13m04s   2GB
Oct 27 11:15:27 Starting characteristic/examples
Oct 27 11:16:48 Finished characteristic/examples                               1m20s   4GB
Oct 27 11:16:48 Starting tutorial/solutions
Oct 27 11:31:58 Finished tutorial/solutions                                   15m09s   8GB
Oct 27 11:31:58 Starting translator/monadic/examples
Oct 27 11:35:14 Finished translator/monadic/examples                           3m15s   3GB
Oct 27 11:35:14 Starting examples
Oct 27 11:43:58 Finished examples                                              8m43s   3GB
Oct 27 11:43:58 Starting examples/compilation/x64
Oct 27 14:05:13 Finished examples/compilation/x64                           2h21m14s  19GB
Oct 27 14:05:13 Starting examples/compilation/x64/proofs
Oct 27 14:06:47 Finished examples/compilation/x64/proofs                       1m34s   2GB
Oct 27 14:06:48 Starting examples/compilation/ag32
Oct 27 14:39:15 Finished examples/compilation/ag32                            32m27s   6GB
Oct 27 14:39:15 Starting examples/compilation/ag32/proofs
Oct 27 14:39:58 Finished examples/compilation/ag32/proofs                        42s   2GB
Oct 27 14:39:59 Starting examples/cost
Oct 27 15:29:04 Finished examples/cost                                        49m04s   7GB
Oct 27 15:29:04 Starting examples/lpr_checker
Oct 27 15:33:06 Finished examples/lpr_checker                                  4m01s   2GB
Oct 27 15:33:06 Starting examples/lpr_checker/compilation
Oct 27 15:50:28 Finished examples/lpr_checker/compilation                     17m22s  13GB
Oct 27 15:50:28 Starting examples/lpr_checker/compilation/proofs
Oct 27 15:51:05 Finished examples/lpr_checker/compilation/proofs                 36s   3GB
Oct 27 15:51:05 Starting examples/lpr_checker/array
Oct 27 16:06:32 Finished examples/lpr_checker/array                           15m26s   3GB
Oct 27 16:06:32 Starting examples/lpr_checker/array/compilation
Oct 27 16:25:20 Finished examples/lpr_checker/array/compilation               18m47s  13GB
Oct 27 16:25:20 Starting examples/lpr_checker/array/compilation/proofs
Oct 27 16:26:05 Finished examples/lpr_checker/array/compilation/proofs           44s   3GB
Oct 27 16:26:05 Starting examples/opentheory
Oct 27 16:36:06 Finished examples/opentheory                                  10m00s   4GB
Oct 27 16:36:06 Starting examples/opentheory
Oct 27 16:36:07 Finished examples/opentheory                                      1s  21MB
Oct 27 16:36:07 Starting examples/opentheory/compilation
Oct 27 17:10:27 Finished examples/opentheory/compilation                      34m19s  20GB
Oct 27 17:10:27 Starting examples/opentheory/compilation/proofs
Oct 27 17:11:05 Finished examples/opentheory/compilation/proofs                  38s   3GB
Oct 27 17:11:06 Starting examples/opentheory/compilation/ag32
Oct 27 17:45:44 Finished examples/opentheory/compilation/ag32                 34m38s  15GB
Oct 27 17:45:45 Starting examples/opentheory/compilation/ag32/proofs
Oct 27 17:47:28 Finished examples/opentheory/compilation/ag32/proofs           1m43s   5GB
Oct 27 17:47:28 Starting translator/okasaki-examples
Oct 27 17:51:56 Finished translator/okasaki-examples                           4m27s   1GB
Oct 27 17:51:56 Starting translator/other-examples
Oct 27 17:53:57 Finished translator/other-examples                             2m00s   1GB
Oct 27 17:53:58 Starting compiler/parsing/tests
Oct 27 17:54:24 Finished compiler/parsing/tests                                  26s 538MB
Oct 27 17:54:24 Starting compiler/inference/tests
Oct 27 17:59:08 Finished compiler/inference/tests                              4m43s   3GB
Oct 27 17:59:08 Starting compiler/bootstrap/translation
Oct 27 20:53:37 Finished compiler/bootstrap/translation                     2h54m28s  44GB
Oct 27 20:53:37 Starting unverified/sexpr-bootstrap/x64/64
Oct 27 21:03:09 Finished unverified/sexpr-bootstrap/x64/64                     9m23s   8GB
Oct 27 21:03:09 Starting unverified/sexpr-bootstrap/x64/32
Oct 27 21:10:43 Finished unverified/sexpr-bootstrap/x64/32                     7m27s   8GB
Oct 27 21:10:44 Starting compiler/benchmarks
Oct 27 21:10:46 Finished compiler/benchmarks                                      1s  23MB
Oct 27 21:10:46 Starting compiler/bootstrap/compilation/x64/64
Oct 28 10:00:19 Finished compiler/bootstrap/compilation/x64/64             12h49m29s  64GB
Oct 28 10:00:19 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 28 10:03:27 Finished compiler/bootstrap/compilation/x64/64/proofs          3m08s  12GB
Oct 28 10:03:28 Starting compiler/bootstrap/compilation/x64/32
Oct 28 21:05:45 Finished compiler/bootstrap/compilation/x64/32             11h02m15s  64GB
Oct 28 21:05:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 28 21:08:33 Finished compiler/bootstrap/compilation/x64/32/proofs          2m47s  10GB
Oct 28 21:08:33 Starting compiler/bootstrap/compilation/ag32/32
Oct 29 05:08:11 FAILED: compiler/bootstrap/compilation/ag32/32
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
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/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
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/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                       real:    0s  user:    0s     OK
to_dataBootstrapTheory                          real: 3565s  user: 3546s     OK
Starting work on to_lab_ag32BootstrapTheory
to_lab_ag32BootstrapTheory                      real:  419m  user:  964m     OK
Starting work on ag32BootstrapTheory
ag32BootstrapTheory                             real:   49s  user:   46sFAIL<1>
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/sexp_parserProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/to_word32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/to_target32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/arm7ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/ag32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/translation/compiler32ProgTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/to_dataBootstrapTheory : Interrupt
 error in load $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/to_lab_ag32BootstrapTheory : Interrupt
 error in load /home/cake/oven/regression/cakeml-1383/compiler/bootstrap/compilation/ag32/32/ag32BootstrapScript : Interrupt
 Uncaught exception: Interrupt