Job 1930

CakeML:77c2995e9367631ea166d26c234519d53609c723
  Rename source_to_sourceScript.sml to avoid clashing name [Jun 16 20:49:58]
#884 (let-lift)
Merging into:f7195c3d29d6bd5f389a7ff307f998a45d56552f
  Merge pull request #888 from CakeML/deflate [Jun 09 07:20:45]
HOL:55691be292491aef452ee5e7c56e67b02601f669
  Holmake: fix mlton build [Jun 10 00:41:25]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 16 20:51:28 Claimed job
Jun 16 20:51:30 Reusing HOL
Jun 16 20:51:48 Starting developers
Jun 16 20:51:52 Finished developers                                               4s 133MB
Jun 16 20:51:53 Starting developers/bin
Jun 16 20:52:04 Finished developers/bin                                          11s   1GB
Jun 16 20:52:04 Starting semantics/ffi
Jun 16 20:52:23 Finished semantics/ffi                                           18s 304MB
Jun 16 20:52:23 Starting semantics
Jun 16 20:57:28 Finished semantics                                             5m04s   2GB
Jun 16 20:57:28 Starting semantics/proofs
Jun 16 21:12:49 Finished semantics/proofs                                     15m20s   2GB
Jun 16 21:12:49 Starting semantics/alt_semantics
Jun 16 21:13:22 Finished semantics/alt_semantics                                 32s 603MB
Jun 16 21:13:22 Starting semantics/alt_semantics/proofs
Jun 16 21:24:35 Finished semantics/alt_semantics/proofs                       11m12s   2GB
Jun 16 21:24:35 Starting basis/pure
Jun 16 21:25:44 Finished basis/pure                                            1m08s   1GB
Jun 16 21:25:44 Starting translator
Jun 16 21:29:27 Finished translator                                            3m42s   3GB
Jun 16 21:29:28 Starting compiler/parsing
Jun 16 21:30:56 Finished compiler/parsing                                      1m28s   6GB
Jun 16 21:30:56 Starting characteristic
Jun 16 21:37:46 Finished characteristic                                        6m49s   3GB
Jun 16 21:37:46 Starting translator/monadic
Jun 16 21:39:50 Finished translator/monadic                                    2m04s   2GB
Jun 16 21:39:51 Starting basis
Jun 16 22:31:05 Finished basis                                                51m13s  36GB
Jun 16 22:31:05 Starting compiler/inference
Jun 16 22:32:36 Finished compiler/inference                                    1m30s   1GB
Jun 16 22:32:36 Starting compiler/backend/reg_alloc
Jun 16 22:34:18 Finished compiler/backend/reg_alloc                            1m41s   2GB
Jun 16 22:34:18 Starting compiler/backend/gc
Jun 16 22:38:45 Finished compiler/backend/gc                                   4m26s   2GB
Jun 16 22:38:45 Starting compiler/backend
Jun 16 22:45:08 Finished compiler/backend                                      6m22s   3GB
Jun 16 22:45:08 Starting compiler/encoders/asm
Jun 16 22:45:39 Finished compiler/encoders/asm                                   31s   1GB
Jun 16 22:45:40 Starting compiler/encoders/x64
Jun 16 22:46:12 Finished compiler/encoders/x64                                   31s   1GB
Jun 16 22:46:12 Starting compiler/encoders/arm7
Jun 16 22:47:07 Finished compiler/encoders/arm7                                  54s   1GB
Jun 16 22:47:07 Starting compiler/encoders/arm8
Jun 16 22:47:25 Finished compiler/encoders/arm8                                  17s   1GB
Jun 16 22:47:25 Starting compiler/encoders/arm8_asl
Jun 16 22:50:02 Finished compiler/encoders/arm8_asl                            2m37s   1GB
Jun 16 22:50:02 Starting compiler/encoders/mips
Jun 16 22:50:25 Finished compiler/encoders/mips                                  22s   1GB
Jun 16 22:50:25 Starting compiler/encoders/riscv
Jun 16 22:50:46 Finished compiler/encoders/riscv                                 20s   1GB
Jun 16 22:50:46 Starting compiler/encoders/ag32
Jun 16 22:51:10 Finished compiler/encoders/ag32                                  23s   1GB
Jun 16 22:51:10 Starting compiler/backend/x64
Jun 16 22:51:33 Finished compiler/backend/x64                                    22s   1GB
Jun 16 22:51:33 Starting compiler/backend/arm7
Jun 16 22:51:56 Finished compiler/backend/arm7                                   23s   1GB
Jun 16 22:51:57 Starting compiler/backend/arm8
Jun 16 22:52:20 Finished compiler/backend/arm8                                   23s   1GB
Jun 16 22:52:20 Starting compiler/backend/mips
Jun 16 22:52:45 Finished compiler/backend/mips                                   24s   1GB
Jun 16 22:52:45 Starting compiler/backend/riscv
Jun 16 22:53:10 Finished compiler/backend/riscv                                  24s   1GB
Jun 16 22:53:10 Starting compiler/backend/ag32
Jun 16 22:54:35 Finished compiler/backend/ag32                                 1m25s   2GB
Jun 16 22:54:35 Starting compiler/parsing/proofs
Jun 16 22:57:15 Finished compiler/parsing/proofs                               2m39s   1GB
Jun 16 22:57:15 Starting compiler/inference/proofs
Jun 16 22:59:54 Finished compiler/inference/proofs                             2m38s   1GB
Jun 16 22:59:54 Starting compiler/backend/semantics
Jun 16 23:55:21 Finished compiler/backend/semantics                           55m26s   4GB
Jun 16 23:55:21 Starting compiler/backend/reg_alloc/proofs
Jun 17 00:01:33 Finished compiler/backend/reg_alloc/proofs                     6m11s   1GB
Jun 17 00:01:33 Starting compiler/backend/proofs
Jun 17 01:19:13 Finished compiler/backend/proofs                            1h17m37s  16GB
Jun 17 01:19:13 Starting compiler/backend/serialiser
Jun 17 01:20:51 Finished compiler/backend/serialiser                           1m37s   1GB
Jun 17 01:20:51 Starting compiler/encoders/x64/proofs
Jun 17 01:30:44 Finished compiler/encoders/x64/proofs                          9m53s   4GB
Jun 17 01:30:45 Starting compiler/encoders/arm7/proofs
Jun 17 01:44:15 Finished compiler/encoders/arm7/proofs                        13m29s  11GB
Jun 17 01:44:15 Starting compiler/encoders/arm8/proofs
Jun 17 01:51:09 Finished compiler/encoders/arm8/proofs                         6m54s   3GB
Jun 17 01:51:09 Starting compiler/encoders/arm8_asl/proofs
Jun 17 02:06:04 Finished compiler/encoders/arm8_asl/proofs                    14m54s   3GB
Jun 17 02:06:04 Starting compiler/encoders/mips/proofs
Jun 17 02:15:59 Finished compiler/encoders/mips/proofs                         9m54s   7GB
Jun 17 02:15:59 Starting compiler/encoders/riscv/proofs
Jun 17 02:24:38 Finished compiler/encoders/riscv/proofs                        8m38s   4GB
Jun 17 02:24:39 Starting compiler/encoders/ag32/proofs
Jun 17 02:27:02 Finished compiler/encoders/ag32/proofs                         2m23s   1GB
Jun 17 02:27:02 Starting compiler/backend/x64/proofs
Jun 17 02:27:31 Finished compiler/backend/x64/proofs                             28s   2GB
Jun 17 02:27:31 Starting compiler/backend/arm7/proofs
Jun 17 02:28:01 Finished compiler/backend/arm7/proofs                            29s   2GB
Jun 17 02:28:01 Starting compiler/backend/arm8/proofs
Jun 17 02:28:28 Finished compiler/backend/arm8/proofs                            26s   1GB
Jun 17 02:28:28 Starting compiler/backend/arm8_asl
Jun 17 02:28:51 Finished compiler/backend/arm8_asl                               22s   1GB
Jun 17 02:28:52 Starting compiler/backend/mips/proofs
Jun 17 02:29:20 Finished compiler/backend/mips/proofs                            28s   1GB
Jun 17 02:29:21 Starting compiler/backend/riscv/proofs
Jun 17 02:29:50 Finished compiler/backend/riscv/proofs                           29s   2GB
Jun 17 02:29:51 Starting compiler/backend/ag32/proofs
Jun 17 02:42:34 Finished compiler/backend/ag32/proofs                         12m42s   4GB
Jun 17 02:42:34 Starting compiler/proofs
Jun 17 02:44:44 Finished compiler/proofs                                       2m10s   3GB
Jun 17 02:44:45 Starting candle/set-theory
Jun 17 02:45:21 Finished candle/set-theory                                       36s   1GB
Jun 17 02:45:21 Starting candle/syntax-lib
Jun 17 02:45:35 Finished candle/syntax-lib                                       13s 923MB
Jun 17 02:45:35 Starting candle/standard/syntax
Jun 17 02:47:39 Finished candle/standard/syntax                                2m03s   1GB
Jun 17 02:47:39 Starting candle/standard/semantics
Jun 17 02:49:31 Finished candle/standard/semantics                             1m52s   1GB
Jun 17 02:49:32 Starting candle/standard/monadic
Jun 17 02:51:26 Finished candle/standard/monadic                               1m54s   2GB
Jun 17 02:51:26 Starting candle/standard/ml_kernel
Jun 17 02:57:45 Finished candle/standard/ml_kernel                             6m18s   5GB
Jun 17 02:57:45 Starting candle/overloading/syntax
Jun 17 03:00:57 Finished candle/overloading/syntax                             3m11s   2GB
Jun 17 03:00:57 Starting candle/overloading/semantics
Jun 17 03:11:50 Finished candle/overloading/semantics                         10m52s   6GB
Jun 17 03:11:50 Starting candle/overloading/monadic
Jun 17 03:14:15 Finished candle/overloading/monadic                            2m24s   2GB
Jun 17 03:14:15 Starting candle/overloading/ml_kernel
Jun 17 03:21:21 Finished candle/overloading/ml_kernel                          7m05s   5GB
Jun 17 03:21:21 Starting candle/overloading/ml_checker
Jun 17 03:23:45 Finished candle/overloading/ml_checker                         2m23s   5GB
Jun 17 03:23:45 Starting candle/prover
Jun 17 03:33:40 Finished candle/prover                                         9m54s   4GB
Jun 17 03:33:40 Starting pancake
Jun 17 03:37:32 Finished pancake                                               3m51s   5GB
Jun 17 03:37:32 Starting pancake/ffi
Jun 17 03:37:32 Finished pancake/ffi                                              0s  35MB
Jun 17 03:37:32 Starting pancake/semantics
Jun 17 03:40:02 Finished pancake/semantics                                     2m29s   2GB
Jun 17 03:40:02 Starting pancake/proofs
Jun 17 03:51:39 Finished pancake/proofs                                       11m36s   7GB
Jun 17 03:51:39 Starting characteristic/examples
Jun 17 03:53:06 Finished characteristic/examples                               1m26s   4GB
Jun 17 03:53:06 Starting tutorial/solutions
Jun 17 04:09:52 Finished tutorial/solutions                                   16m45s  12GB
Jun 17 04:09:52 Starting translator/monadic/examples
Jun 17 04:13:59 Finished translator/monadic/examples                           4m06s   3GB
Jun 17 04:14:00 Starting examples
Jun 17 04:24:43 Finished examples                                             10m43s   7GB
Jun 17 04:24:44 Starting examples/compilation/x64
Jun 17 06:57:01 Finished examples/compilation/x64                           2h32m16s  31GB
Jun 17 06:57:01 Starting examples/compilation/x64/proofs
Jun 17 06:59:26 Finished examples/compilation/x64/proofs                       2m25s   4GB
Jun 17 06:59:27 Starting examples/compilation/ag32
Jun 17 07:37:13 Finished examples/compilation/ag32                            37m45s  13GB
Jun 17 07:37:13 Starting examples/compilation/ag32/proofs
Jun 17 07:39:12 Finished examples/compilation/ag32/proofs                      1m59s   5GB
Jun 17 07:39:12 Starting examples/lpr_checker
Jun 17 07:40:47 Finished examples/lpr_checker                                  1m34s   2GB
Jun 17 07:40:47 Starting examples/lpr_checker/array
Jun 17 08:22:33 Finished examples/lpr_checker/array                           41m44s  12GB
Jun 17 08:22:33 Starting examples/lpr_checker/array/compilation
Jun 17 10:00:51 Finished examples/lpr_checker/array/compilation             1h38m17s  34GB
Jun 17 10:00:51 Starting examples/lpr_checker/array/compilation/proofs
Jun 17 10:02:39 Finished examples/lpr_checker/array/compilation/proofs         1m47s   6GB
Jun 17 10:02:39 Starting examples/opentheory
Jun 17 10:13:41 Finished examples/opentheory                                  11m01s   4GB
Jun 17 10:13:41 Starting examples/opentheory
Jun 17 10:13:42 Finished examples/opentheory                                      1s 136MB
Jun 17 10:13:43 Starting examples/opentheory/compilation
Jun 17 11:00:21 Finished examples/opentheory/compilation                      46m38s  49GB
Jun 17 11:00:21 Starting examples/opentheory/compilation/proofs
Jun 17 11:01:28 Finished examples/opentheory/compilation/proofs                1m06s   4GB
Jun 17 11:01:28 Starting examples/opentheory/compilation/ag32
Jun 17 11:43:11 Finished examples/opentheory/compilation/ag32                 41m42s  36GB
Jun 17 11:43:11 Starting examples/opentheory/compilation/ag32/proofs
Jun 17 11:45:08 Finished examples/opentheory/compilation/ag32/proofs           1m57s   8GB
Jun 17 11:45:08 Starting examples/sat_encodings
Jun 17 11:47:19 Finished examples/sat_encodings                                2m10s   1GB
Jun 17 11:47:19 Starting examples/sat_encodings/case_studies
Jun 17 11:49:08 Finished examples/sat_encodings/case_studies                   1m49s   1GB
Jun 17 11:49:09 Starting examples/sat_encodings/translation
Jun 17 11:55:22 Finished examples/sat_encodings/translation                    6m13s   5GB
Jun 17 11:55:22 Starting examples/sat_encodings/translation/compilation
Jun 17 12:56:40 Finished examples/sat_encodings/translation/compilation     1h01m17s  23GB
Jun 17 12:56:40 Starting examples/deflate
Jun 17 12:57:46 Finished examples/deflate                                      1m05s   1GB
Jun 17 12:57:47 Starting examples/deflate/translation
Jun 17 12:59:45 Finished examples/deflate/translation                          1m58s   4GB
Jun 17 12:59:45 Starting examples/deflate/translation/compilation
Jun 17 13:33:21 Finished examples/deflate/translation/compilation             33m33s  20GB
Jun 17 13:33:21 Starting translator/okasaki-examples
Jun 17 13:39:40 Finished translator/okasaki-examples                           6m18s   3GB
Jun 17 13:39:40 Starting translator/other-examples
Jun 17 13:40:57 Finished translator/other-examples                             1m16s   1GB
Jun 17 13:40:57 Starting compiler/parsing/tests
Jun 17 13:41:31 Finished compiler/parsing/tests                                  33s 680MB
Jun 17 13:41:31 Starting compiler/inference/tests
Jun 17 13:50:51 Finished compiler/inference/tests                              9m19s   6GB
Jun 17 13:50:51 Starting compiler/printing/test
Jun 17 13:54:56 Finished compiler/printing/test                                4m04s   4GB
Jun 17 13:54:56 Starting icing/flover
Jun 17 14:08:07 Finished icing/flover                                         13m11s   1GB
Jun 17 14:08:08 Starting icing/
Jun 17 15:15:38 Finished icing/                                             1h07m29s  18GB
Jun 17 15:15:38 Starting icing/examples
Jun 17 15:16:38 FAILED: icing/examples
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)/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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[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$(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$(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/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/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/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)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/icing/flover/Infra[0m
Scanning [1m$(CAKEMLDIR)/icing/flover/semantics[0m
Scanning [1m$(CAKEMLDIR)/icing/flover[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanning [1m$(CAKEMLDIR)/icing[0m
Scanned 84 directories
Starting work on README.md
Starting work on dirs
Starting work on dopplerProgCompTheory
dirs                                                                                                                                                                     (0s)     OK
README.md                                                                                                                                                                (0s)     OK
dopplerProgCompTheory                                                                                                                                                   (53s)FAIL<1>
 /home/myreen/regression/cakeml-1930/icing/icing_optimisationsLib.sml:135: error: Value or constructor (is_optimise_with_plan_correct_lift) has not been declared
 Found near
   MP (Q.SPEC [... ..., ...] is_optimise_with_plan_correct_lift)
   plan_correct_perform_rewrites
 error in quse /home/myreen/regression/cakeml-1930/icing/icing_optimisationsLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/icing/icing_optimisationsLib : Fail "Static Errors"
 error in load $(CAKEMLDIR)/icing/supportLib : Fail "Static Errors"
 error in load $(CAKEMLDIR)/icing/examples/exampleLib : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1930/icing/examples/dopplerProgCompScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"