Job 1095

CakeML:fa186f6cfb9bfb08eaa4b872c1fecb943868b227
  Merge pull request #698 from CakeML/cakeml-rat-proj [Nov 16 15:11:37]
HOL:ca71e46c32fd6a11162c9640ee7006dfe1c6fabd
  Remove unnecessary CLINE_OPTIONS in tests that break Moscow ML build [Nov 13 22:33:35]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Nov 16 15:30:44 Claimed job
Nov 16 15:30:50 Reusing HOL
Nov 16 15:30:57 Starting developers
Nov 16 15:30:59 Finished developers                                               2s 121MB
Nov 16 15:30:59 Starting developers/bin
Nov 16 15:31:03 Finished developers/bin                                           3s 164MB
Nov 16 15:31:04 Starting semantics/ffi
Nov 16 15:31:12 Finished semantics/ffi                                            8s 232MB
Nov 16 15:31:13 Starting semantics
Nov 16 15:32:44 Finished semantics                                             1m31s   1GB
Nov 16 15:32:44 Starting semantics/proofs
Nov 16 15:36:10 Finished semantics/proofs                                      3m26s   1GB
Nov 16 15:36:11 Starting semantics/alt_semantics
Nov 16 15:36:18 Finished semantics/alt_semantics                                  6s 299MB
Nov 16 15:36:18 Starting semantics/alt_semantics/proofs
Nov 16 15:38:19 Finished semantics/alt_semantics/proofs                        2m00s 961MB
Nov 16 15:38:19 Starting basis/pure
Nov 16 15:39:12 Finished basis/pure                                              53s 721MB
Nov 16 15:39:13 Starting translator
Nov 16 15:41:19 Finished translator                                            2m06s   1GB
Nov 16 15:41:19 Starting compiler/parsing
Nov 16 15:42:53 Finished compiler/parsing                                      1m33s   2GB
Nov 16 15:42:53 Starting characteristic
Nov 16 15:48:34 Finished characteristic                                        5m40s   1GB
Nov 16 15:48:34 Starting translator/monadic
Nov 16 15:50:06 Finished translator/monadic                                    1m31s   1GB
Nov 16 15:50:06 Starting basis
Nov 16 16:11:26 Finished basis                                                21m19s   2GB
Nov 16 16:11:26 Starting compiler/inference
Nov 16 16:13:10 Finished compiler/inference                                    1m43s   1GB
Nov 16 16:13:10 Starting compiler/backend/reg_alloc
Nov 16 16:14:14 Finished compiler/backend/reg_alloc                            1m04s   1GB
Nov 16 16:14:15 Starting compiler/backend/gc
Nov 16 16:17:35 Finished compiler/backend/gc                                   3m20s   1GB
Nov 16 16:17:35 Starting compiler/backend
Nov 16 16:21:52 Finished compiler/backend                                      4m16s   1GB
Nov 16 16:21:53 Starting compiler/encoders/asm
Nov 16 16:22:14 Finished compiler/encoders/asm                                   20s 671MB
Nov 16 16:22:14 Starting compiler/encoders/x64
Nov 16 16:22:38 Finished compiler/encoders/x64                                   23s 918MB
Nov 16 16:22:38 Starting compiler/encoders/arm7
Nov 16 16:23:25 Finished compiler/encoders/arm7                                  46s 700MB
Nov 16 16:23:25 Starting compiler/encoders/arm8
Nov 16 16:23:38 Finished compiler/encoders/arm8                                  11s 826MB
Nov 16 16:23:38 Starting compiler/encoders/mips
Nov 16 16:23:55 Finished compiler/encoders/mips                                  16s 922MB
Nov 16 16:23:55 Starting compiler/encoders/riscv
Nov 16 16:24:09 Finished compiler/encoders/riscv                                 13s 654MB
Nov 16 16:24:09 Starting compiler/encoders/ag32
Nov 16 16:24:26 Finished compiler/encoders/ag32                                  16s 813MB
Nov 16 16:24:26 Starting compiler/backend/x64
Nov 16 16:24:44 Finished compiler/backend/x64                                    17s   1GB
Nov 16 16:24:44 Starting compiler/backend/arm7
Nov 16 16:25:02 Finished compiler/backend/arm7                                   18s   1GB
Nov 16 16:25:03 Starting compiler/backend/arm8
Nov 16 16:25:20 Finished compiler/backend/arm8                                   17s   1GB
Nov 16 16:25:21 Starting compiler/backend/mips
Nov 16 16:25:39 Finished compiler/backend/mips                                   17s   1GB
Nov 16 16:25:39 Starting compiler/backend/riscv
Nov 16 16:25:57 Finished compiler/backend/riscv                                  17s   1GB
Nov 16 16:25:57 Starting compiler/backend/ag32
Nov 16 16:27:10 Finished compiler/backend/ag32                                 1m13s   1GB
Nov 16 16:27:10 Starting compiler/parsing/proofs
Nov 16 16:32:58 Finished compiler/parsing/proofs                               5m46s   1GB
Nov 16 16:32:58 Starting compiler/inference/proofs
Nov 16 16:35:54 Finished compiler/inference/proofs                             2m55s 984MB
Nov 16 16:35:54 Starting compiler/backend/semantics
Nov 16 16:43:07 Finished compiler/backend/semantics                            7m12s   2GB
Nov 16 16:43:07 Starting compiler/backend/reg_alloc/proofs
Nov 16 16:46:34 Finished compiler/backend/reg_alloc/proofs                     3m27s 816MB
Nov 16 16:46:35 Starting compiler/backend/proofs
Nov 16 17:35:14 Finished compiler/backend/proofs                              48m38s   4GB
Nov 16 17:35:14 Starting compiler/encoders/x64/proofs
Nov 16 17:45:01 Finished compiler/encoders/x64/proofs                          9m46s   5GB
Nov 16 17:45:01 Starting compiler/encoders/arm7/proofs
Nov 16 17:58:15 Finished compiler/encoders/arm7/proofs                        13m12s   6GB
Nov 16 17:58:15 Starting compiler/encoders/arm8/proofs
Nov 16 18:05:40 Finished compiler/encoders/arm8/proofs                         7m24s   1GB
Nov 16 18:05:40 Starting compiler/encoders/mips/proofs
Nov 16 18:16:46 Finished compiler/encoders/mips/proofs                        11m05s   1GB
Nov 16 18:16:46 Starting compiler/encoders/riscv/proofs
Nov 16 18:26:08 Finished compiler/encoders/riscv/proofs                        9m21s 629MB
Nov 16 18:26:08 Starting compiler/encoders/ag32/proofs
Nov 16 18:28:43 Finished compiler/encoders/ag32/proofs                         2m34s 871MB
Nov 16 18:28:43 Starting compiler/backend/x64/proofs
Nov 16 18:29:02 Finished compiler/backend/x64/proofs                             18s   1GB
Nov 16 18:29:02 Starting compiler/backend/arm7/proofs
Nov 16 18:29:21 Finished compiler/backend/arm7/proofs                            18s   1GB
Nov 16 18:29:21 Starting compiler/backend/arm8/proofs
Nov 16 18:29:39 Finished compiler/backend/arm8/proofs                            17s   1GB
Nov 16 18:29:39 Starting compiler/backend/mips/proofs
Nov 16 18:29:57 Finished compiler/backend/mips/proofs                            17s 903MB
Nov 16 18:29:57 Starting compiler/backend/riscv/proofs
Nov 16 18:30:15 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 16 18:30:15 Starting compiler/backend/ag32/proofs
Nov 16 18:40:15 Finished compiler/backend/ag32/proofs                          9m58s   2GB
Nov 16 18:40:15 Starting compiler/proofs
Nov 16 18:41:47 Finished compiler/proofs                                       1m31s   2GB
Nov 16 18:41:47 Starting candle/set-theory
Nov 16 18:42:17 Finished candle/set-theory                                       29s 732MB
Nov 16 18:42:17 Starting candle/syntax-lib
Nov 16 18:42:28 Finished candle/syntax-lib                                       10s 602MB
Nov 16 18:42:28 Starting candle/standard/syntax
Nov 16 18:44:24 Finished candle/standard/syntax                                1m55s   1GB
Nov 16 18:44:24 Starting candle/standard/semantics
Nov 16 18:46:14 Finished candle/standard/semantics                             1m49s 894MB
Nov 16 18:46:14 Starting candle/standard/monadic
Nov 16 18:47:56 Finished candle/standard/monadic                               1m41s   1GB
Nov 16 18:47:56 Starting candle/standard/ml_kernel
Nov 16 18:52:09 Finished candle/standard/ml_kernel                             4m12s   3GB
Nov 16 18:52:09 Starting candle/standard/opentheory
Nov 16 19:01:17 Finished candle/standard/opentheory                            9m07s   3GB
Nov 16 19:01:18 Starting candle/standard/opentheory/compilation
Nov 16 19:33:14 Finished candle/standard/opentheory/compilation               31m56s  21GB
Nov 16 19:33:14 Starting candle/standard/opentheory/compilation/proofs
Nov 16 19:34:04 Finished candle/standard/opentheory/compilation/proofs           49s   2GB
Nov 16 19:34:04 Starting characteristic/examples
Nov 16 19:35:43 Finished characteristic/examples                               1m38s   2GB
Nov 16 19:35:43 Starting tutorial/solutions
Nov 16 19:54:39 Finished tutorial/solutions                                   18m54s   7GB
Nov 16 19:54:39 Starting translator/monadic/examples
Nov 16 19:59:24 Finished translator/monadic/examples                           4m44s   2GB
Nov 16 19:59:25 Starting examples
Nov 16 20:15:43 Finished examples                                             16m18s   5GB
Nov 16 20:15:44 Starting examples/compilation/x64
Nov 16 23:29:03 Finished examples/compilation/x64                           3h13m18s  15GB
Nov 16 23:29:03 Starting examples/compilation/x64/proofs
Nov 16 23:31:09 Finished examples/compilation/x64/proofs                       2m06s   2GB
Nov 16 23:31:10 Starting examples/compilation/ag32
Nov 17 00:02:09 Finished examples/compilation/ag32                            30m59s   5GB
Nov 17 00:02:09 Starting examples/compilation/ag32/proofs
Nov 17 00:03:04 Finished examples/compilation/ag32/proofs                        54s   3GB
Nov 17 00:03:04 Starting translator/okasaki-examples
Nov 17 00:07:40 Finished translator/okasaki-examples                           4m35s   1GB
Nov 17 00:07:40 Starting translator/other-examples
Nov 17 00:08:25 Finished translator/other-examples                               44s   1GB
Nov 17 00:08:25 Starting compiler/parsing/tests
Nov 17 00:08:51 Finished compiler/parsing/tests                                  25s 619MB
Nov 17 00:08:51 Starting compiler/inference/tests
Nov 17 00:13:29 Finished compiler/inference/tests                              4m38s   3GB
Nov 17 00:13:29 Starting compiler/bootstrap/translation
Nov 17 03:23:17 Finished compiler/bootstrap/translation                     3h09m46s  20GB
Nov 17 03:23:17 Starting unverified/sexpr-bootstrap/x64/64
Nov 17 03:41:02 Finished unverified/sexpr-bootstrap/x64/64                    17m43s   6GB
Nov 17 03:41:02 Starting unverified/sexpr-bootstrap/x64/32
Nov 17 03:51:55 Finished unverified/sexpr-bootstrap/x64/32                    10m52s   5GB
Nov 17 03:51:55 Starting compiler/benchmarks
Nov 17 04:31:22 Finished compiler/benchmarks                                  39m25s   2GB
Nov 17 04:31:22 Starting compiler/bootstrap/compilation/x64/64
Nov 17 18:12:22 Finished compiler/bootstrap/compilation/x64/64             13h40m59s  59GB
Nov 17 18:12:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 17 18:16:17 Finished compiler/bootstrap/compilation/x64/64/proofs          3m54s   5GB
Nov 17 18:16:17 Starting compiler/bootstrap/compilation/x64/32
Nov 18 05:47:14 Finished compiler/bootstrap/compilation/x64/32             11h30m55s  63GB
Nov 18 05:47:14 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 18 05:50:28 Finished compiler/bootstrap/compilation/x64/32/proofs          3m13s   4GB
Nov 18 05:50:28 Starting compiler/bootstrap/compilation/ag32/32
Nov 18 19:47:32 Finished compiler/bootstrap/compilation/ag32/32            13h57m03s  64GB
Nov 18 19:47:33 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 18 20:14:39 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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/machine-code/multiword[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$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32/proofs[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[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/model[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/model[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/model[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/model[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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32[0m
Starting work on README.md
Starting work on ag32BootstrapProofTheory
README.md                                                                       real:    0s  user:    0s     OK
ag32BootstrapProofTheory                                                        real: 1624s  user: 1604sFAIL<1>
         out = explode (concat (append cout))  err = explode cerr))
 
 failed.
 Failed to prove theorem cake_extract_writes.
 
 Exception raised at Tactical.FIRST_ASSUM:
  (THEN1 on line 319) (THEN1 on line 323) (THEN1 on line 327) (THEN1 on line 298) (THEN1 on line 337) (THEN1 on line 395) (THEN1 on line 412) (THEN1 on line 424)
 error in quse /home/myreen/regression/cakeml-1095/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml : HOL_ERR {message = " (THEN1 on line 319) (THEN1 on line 323) (THEN1 on line 327) (THEN1 on line 298) (THEN1 on line 337) (THEN1 on line 395) (THEN1 on line 412) (THEN1 on line 424)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1095/compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript : HOL_ERR {message = " (THEN1 on line 319) (THEN1 on line 323) (THEN1 on line 327) (THEN1 on line 298) (THEN1 on line 337) (THEN1 on line 395) (THEN1 on line 412) (THEN1 on line 424)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 319) (THEN1 on line 323) (THEN1 on line 327) (THEN1 on line 298) (THEN1 on line 337) (THEN1 on line 395) (THEN1 on line 412) (THEN1 on line 424)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}