CakeML Regression Test

Job 930

CakeML:599312a00978fbf1202927b225d059f2fc99bc95
  Fix scripts for MEM_DROP change in HOL [Jul 02 00:10:35]
HOL:b2c522cc4feed537711f40aa24b104bb98940c08
  Update comment on DPLL function's speed in TUTORIAL's tools chapter [Jul 02 00:29:31]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 02 04:22:49 Claimed job
Jul 02 04:22:52 Building HOL
Jul 02 04:30:38 Starting developers
Jul 02 04:30:38 Finished developers                                               0s  20MB
Jul 02 04:30:39 Starting developers/bin
Jul 02 04:30:42 Finished developers/bin                                           3s 144MB
Jul 02 04:30:42 Starting semantics/ffi
Jul 02 04:31:15 Finished semantics/ffi                                           32s 499MB
Jul 02 04:31:15 Starting semantics
Jul 02 04:32:45 Finished semantics                                             1m29s 981MB
Jul 02 04:32:46 Starting semantics/proofs
Jul 02 04:35:44 Finished semantics/proofs                                      2m58s   1GB
Jul 02 04:35:44 Starting semantics/alt_semantics
Jul 02 04:35:50 Finished semantics/alt_semantics                                  5s 304MB
Jul 02 04:35:51 Starting semantics/alt_semantics/proofs
Jul 02 04:37:36 Finished semantics/alt_semantics/proofs                        1m45s 801MB
Jul 02 04:37:37 Starting basis/pure
Jul 02 04:41:10 Finished basis/pure                                            3m33s 630MB
Jul 02 04:41:11 Starting translator
Jul 02 04:42:49 Finished translator                                            1m38s   1GB
Jul 02 04:42:50 Starting compiler/parsing
Jul 02 04:43:47 Finished compiler/parsing                                        56s   2GB
Jul 02 04:43:47 Starting characteristic
Jul 02 04:48:53 Finished characteristic                                        5m05s   1GB
Jul 02 04:48:54 Starting translator/monadic
Jul 02 04:50:18 Finished translator/monadic                                    1m23s   1GB
Jul 02 04:50:18 Starting basis
Jul 02 05:07:19 Finished basis                                                17m00s   2GB
Jul 02 05:07:20 Starting compiler/inference
Jul 02 05:09:07 Finished compiler/inference                                    1m47s   1GB
Jul 02 05:09:07 Starting compiler/backend/reg_alloc
Jul 02 05:10:04 Finished compiler/backend/reg_alloc                              56s   1GB
Jul 02 05:10:04 Starting compiler/backend/gc
Jul 02 05:18:58 Finished compiler/backend/gc                                   8m53s   1GB
Jul 02 05:18:58 Starting compiler/backend
Jul 02 05:18:59 Finished compiler/backend                                         0s  43MB
Jul 02 05:19:00 Starting compiler/encoders/asm
Jul 02 05:19:00 Finished compiler/encoders/asm                                    0s  37MB
Jul 02 05:19:00 Starting compiler/encoders/x64
Jul 02 05:19:56 Finished compiler/encoders/x64                                   55s 911MB
Jul 02 05:19:56 Starting compiler/encoders/arm7
Jul 02 05:21:32 Finished compiler/encoders/arm7                                1m35s   1GB
Jul 02 05:21:32 Starting compiler/encoders/arm8
Jul 02 05:22:01 Finished compiler/encoders/arm8                                  28s 866MB
Jul 02 05:22:01 Starting compiler/encoders/mips
Jul 02 05:23:04 Finished compiler/encoders/mips                                1m02s 998MB
Jul 02 05:23:04 Starting compiler/encoders/riscv
Jul 02 05:24:22 Finished compiler/encoders/riscv                               1m16s 804MB
Jul 02 05:24:22 Starting compiler/encoders/ag32
Jul 02 05:24:37 Finished compiler/encoders/ag32                                  14s 750MB
Jul 02 05:24:37 Starting compiler/backend/x64
Jul 02 05:24:53 Finished compiler/backend/x64                                    15s   1GB
Jul 02 05:24:53 Starting compiler/backend/arm7
Jul 02 05:25:10 Finished compiler/backend/arm7                                   16s   1GB
Jul 02 05:25:10 Starting compiler/backend/arm8
Jul 02 05:25:26 Finished compiler/backend/arm8                                   15s   1GB
Jul 02 05:25:26 Starting compiler/backend/mips
Jul 02 05:25:41 Finished compiler/backend/mips                                   15s 897MB
Jul 02 05:25:42 Starting compiler/backend/riscv
Jul 02 05:25:58 Finished compiler/backend/riscv                                  15s   1GB
Jul 02 05:25:58 Starting compiler/backend/ag32
Jul 02 05:27:03 Finished compiler/backend/ag32                                 1m05s 975MB
Jul 02 05:27:04 Starting compiler/parsing/proofs
Jul 02 05:32:30 Finished compiler/parsing/proofs                               5m25s   1GB
Jul 02 05:32:30 Starting compiler/inference/proofs
Jul 02 05:35:10 Finished compiler/inference/proofs                             2m39s   1GB
Jul 02 05:35:10 Starting compiler/backend/semantics
Jul 02 05:42:11 Finished compiler/backend/semantics                            7m00s   2GB
Jul 02 05:42:11 Starting compiler/backend/reg_alloc/proofs
Jul 02 05:45:20 Finished compiler/backend/reg_alloc/proofs                     3m08s   1GB
Jul 02 05:45:21 Starting compiler/backend/proofs
Jul 02 06:23:37 Finished compiler/backend/proofs                              38m15s   4GB
Jul 02 06:23:37 Starting compiler/encoders/x64/proofs
Jul 02 06:33:34 Finished compiler/encoders/x64/proofs                          9m56s   5GB
Jul 02 06:33:34 Starting compiler/encoders/arm7/proofs
Jul 02 06:47:16 Finished compiler/encoders/arm7/proofs                        13m42s   3GB
Jul 02 06:47:17 Starting compiler/encoders/arm8/proofs
Jul 02 06:54:00 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Jul 02 06:54:00 Starting compiler/encoders/mips/proofs
Jul 02 07:03:55 Finished compiler/encoders/mips/proofs                         9m54s   2GB
Jul 02 07:03:55 Starting compiler/encoders/riscv/proofs
Jul 02 07:12:19 Finished compiler/encoders/riscv/proofs                        8m23s 971MB
Jul 02 07:12:19 Starting compiler/encoders/ag32/proofs
Jul 02 07:14:47 Finished compiler/encoders/ag32/proofs                         2m27s 616MB
Jul 02 07:14:47 Starting compiler/backend/x64/proofs
Jul 02 07:15:03 Finished compiler/backend/x64/proofs                             15s 969MB
Jul 02 07:15:03 Starting compiler/backend/arm7/proofs
Jul 02 07:15:21 Finished compiler/backend/arm7/proofs                            17s   1GB
Jul 02 07:15:21 Starting compiler/backend/arm8/proofs
Jul 02 07:15:37 Finished compiler/backend/arm8/proofs                            15s   1GB
Jul 02 07:15:37 Starting compiler/backend/mips/proofs
Jul 02 07:15:54 Finished compiler/backend/mips/proofs                            16s   1GB
Jul 02 07:15:54 Starting compiler/backend/riscv/proofs
Jul 02 07:16:10 Finished compiler/backend/riscv/proofs                           15s   1GB
Jul 02 07:16:11 Starting compiler/backend/ag32/proofs
Jul 02 07:24:55 Finished compiler/backend/ag32/proofs                          8m42s   2GB
Jul 02 07:24:55 Starting compiler/proofs
Jul 02 07:26:08 Finished compiler/proofs                                       1m12s   3GB
Jul 02 07:26:08 Starting candle/set-theory
Jul 02 07:26:32 Finished candle/set-theory                                       24s 678MB
Jul 02 07:26:33 Starting candle/syntax-lib
Jul 02 07:26:42 Finished candle/syntax-lib                                        9s 601MB
Jul 02 07:26:42 Starting candle/standard/syntax
Jul 02 07:27:30 FAILED: candle/standard/syntax
]0;Holmake: ~/regression/cakeml-930/basis/pure]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-930/basis/pure]0;Holmake: ~/regression/cakeml-930/misc]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-930/misc]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-b2c522cc4feed537711f40aa24b104bb98940c08/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-930/misc]0;Holmake: ~/regression/cakeml-930/developers]0;Holmake: ~/regression/cakeml-930/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-930/misc]0;Holmake: ~/regression/cakeml-930/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-930/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-930/misc]0;Holmake: ~/regression/cakeml-930/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-930/basis/pure]0;Holmake: ~/regression/cakeml-930/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-lib[1mWorking in $(CAKEMLDIR)/candle/syntax-lib[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/candle/standard/syntax[0m
Starting work on holSyntaxTheory
Starting work on README.md
README.md                                                                                                                                                                         OK
holSyntaxTheory                                                                                                                                                                   OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                                                                                                                                     FAILED! <1>
      "rename_bvars_RACONV",
      [
         QUOTE
         " (*#loc 2538 29*)\n   \226\136\128names env tm.\n    LENGTH (bv_names tm) \226\137\164 LENGTH names \226\136\167\n    DISJOINT (set (MAP FST env ++ names)) (set (MAP (FST o SND) env ++ bv_names tm)) \226\136\167\n    DISJOINT (set (MAP FST env ++ names)) {x | \226\136\131ty. VFREE_IN (Var x ty) tm} \226\136\167\n    ALL_DISTINCT (MAP FST env ++ names) \226\136\167\n    welltyped tm\n    \226\135\146 RACONV (MAP (\206\187(s',(s,ty)). (Var s ty, Var s' ty)) env) (tm, SND (rename_bvars names env tm))"
         ],
      ... >> ... >> ... ...
      )
 error in quse /home/myreen/regression/cakeml-930/candle/standard/syntax/holSyntaxExtraScript.sml : Fail "Static Errors"
 error in load holSyntaxExtraScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"