CakeML Regression Test

Job 929

CakeML:599312a00978fbf1202927b225d059f2fc99bc95
  Fix scripts for MEM_DROP change in HOL [Jul 02 00:10:35]
HOL:8877f97ec124591c9fb742b443b7ef86e99ae2d6
  Clean up MEM_DROP situation [Jul 01 02:16:30]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 02 00:37:38 Claimed job
Jul 02 00:37:45 Building HOL
Jul 02 00:45:28 Starting developers
Jul 02 00:45:29 Finished developers                                               0s  29MB
Jul 02 00:45:29 Starting developers/bin
Jul 02 00:45:33 Finished developers/bin                                           3s 144MB
Jul 02 00:45:33 Starting semantics/ffi
Jul 02 00:46:06 Finished semantics/ffi                                           32s 484MB
Jul 02 00:46:06 Starting semantics
Jul 02 00:47:35 Finished semantics                                             1m28s 889MB
Jul 02 00:47:35 Starting semantics/proofs
Jul 02 00:50:34 Finished semantics/proofs                                      2m58s   1GB
Jul 02 00:50:34 Starting semantics/alt_semantics
Jul 02 00:50:40 Finished semantics/alt_semantics                                  5s 324MB
Jul 02 00:50:40 Starting semantics/alt_semantics/proofs
Jul 02 00:52:27 Finished semantics/alt_semantics/proofs                        1m46s 735MB
Jul 02 00:52:27 Starting basis/pure
Jul 02 00:56:01 Finished basis/pure                                            3m33s 645MB
Jul 02 00:56:01 Starting translator
Jul 02 00:57:40 Finished translator                                            1m38s   1GB
Jul 02 00:57:41 Starting compiler/parsing
Jul 02 00:58:38 Finished compiler/parsing                                        56s   2GB
Jul 02 00:58:38 Starting characteristic
Jul 02 01:03:42 Finished characteristic                                        5m03s   1GB
Jul 02 01:03:42 Starting translator/monadic
Jul 02 01:05:08 Finished translator/monadic                                    1m26s   1GB
Jul 02 01:05:09 Starting basis
Jul 02 01:22:06 Finished basis                                                16m57s   2GB
Jul 02 01:22:07 Starting compiler/inference
Jul 02 01:23:56 Finished compiler/inference                                    1m48s   1GB
Jul 02 01:23:56 Starting compiler/backend/reg_alloc
Jul 02 01:24:54 Finished compiler/backend/reg_alloc                              57s   1GB
Jul 02 01:24:54 Starting compiler/backend/gc
Jul 02 01:33:46 Finished compiler/backend/gc                                   8m51s   1GB
Jul 02 01:33:46 Starting compiler/backend
Jul 02 01:33:47 Finished compiler/backend                                         0s  43MB
Jul 02 01:33:47 Starting compiler/encoders/asm
Jul 02 01:33:48 Finished compiler/encoders/asm                                    0s  37MB
Jul 02 01:33:48 Starting compiler/encoders/x64
Jul 02 01:34:44 Finished compiler/encoders/x64                                   55s 965MB
Jul 02 01:34:44 Starting compiler/encoders/arm7
Jul 02 01:36:19 Finished compiler/encoders/arm7                                1m34s   1GB
Jul 02 01:36:19 Starting compiler/encoders/arm8
Jul 02 01:36:47 Finished compiler/encoders/arm8                                  28s 874MB
Jul 02 01:36:48 Starting compiler/encoders/mips
Jul 02 01:37:50 Finished compiler/encoders/mips                                1m02s 994MB
Jul 02 01:37:51 Starting compiler/encoders/riscv
Jul 02 01:39:05 Finished compiler/encoders/riscv                               1m14s 863MB
Jul 02 01:39:06 Starting compiler/encoders/ag32
Jul 02 01:39:21 Finished compiler/encoders/ag32                                  14s 610MB
Jul 02 01:39:21 Starting compiler/backend/x64
Jul 02 01:39:37 Finished compiler/backend/x64                                    15s   1GB
Jul 02 01:39:37 Starting compiler/backend/arm7
Jul 02 01:39:53 Finished compiler/backend/arm7                                   15s   1GB
Jul 02 01:39:54 Starting compiler/backend/arm8
Jul 02 01:40:10 Finished compiler/backend/arm8                                   16s   1GB
Jul 02 01:40:10 Starting compiler/backend/mips
Jul 02 01:40:26 Finished compiler/backend/mips                                   15s   1GB
Jul 02 01:40:26 Starting compiler/backend/riscv
Jul 02 01:40:42 Finished compiler/backend/riscv                                  15s   1GB
Jul 02 01:40:43 Starting compiler/backend/ag32
Jul 02 01:41:49 Finished compiler/backend/ag32                                 1m05s 928MB
Jul 02 01:41:49 Starting compiler/parsing/proofs
Jul 02 01:47:25 Finished compiler/parsing/proofs                               5m35s   1GB
Jul 02 01:47:26 Starting compiler/inference/proofs
Jul 02 01:50:04 Finished compiler/inference/proofs                             2m38s   1GB
Jul 02 01:50:05 Starting compiler/backend/semantics
Jul 02 01:57:05 Finished compiler/backend/semantics                            7m00s   2GB
Jul 02 01:57:05 Starting compiler/backend/reg_alloc/proofs
Jul 02 02:00:21 Finished compiler/backend/reg_alloc/proofs                     3m14s 677MB
Jul 02 02:00:21 Starting compiler/backend/proofs
Jul 02 02:38:29 Finished compiler/backend/proofs                              38m07s   3GB
Jul 02 02:38:29 Starting compiler/encoders/x64/proofs
Jul 02 02:48:23 Finished compiler/encoders/x64/proofs                          9m53s   7GB
Jul 02 02:48:23 Starting compiler/encoders/arm7/proofs
Jul 02 03:02:09 Finished compiler/encoders/arm7/proofs                        13m45s   3GB
Jul 02 03:02:10 Starting compiler/encoders/arm8/proofs
Jul 02 03:08:47 Finished compiler/encoders/arm8/proofs                         6m36s   1GB
Jul 02 03:08:47 Starting compiler/encoders/mips/proofs
Jul 02 03:18:54 Finished compiler/encoders/mips/proofs                        10m06s   2GB
Jul 02 03:18:54 Starting compiler/encoders/riscv/proofs
Jul 02 03:27:12 Finished compiler/encoders/riscv/proofs                        8m17s   1GB
Jul 02 03:27:12 Starting compiler/encoders/ag32/proofs
Jul 02 03:29:39 Finished compiler/encoders/ag32/proofs                         2m27s 880MB
Jul 02 03:29:40 Starting compiler/backend/x64/proofs
Jul 02 03:29:56 Finished compiler/backend/x64/proofs                             16s   1GB
Jul 02 03:29:57 Starting compiler/backend/arm7/proofs
Jul 02 03:30:13 Finished compiler/backend/arm7/proofs                            16s   1GB
Jul 02 03:30:14 Starting compiler/backend/arm8/proofs
Jul 02 03:30:29 Finished compiler/backend/arm8/proofs                            15s   1GB
Jul 02 03:30:29 Starting compiler/backend/mips/proofs
Jul 02 03:30:46 Finished compiler/backend/mips/proofs                            16s   1GB
Jul 02 03:30:47 Starting compiler/backend/riscv/proofs
Jul 02 03:31:03 Finished compiler/backend/riscv/proofs                           16s 964MB
Jul 02 03:31:04 Starting compiler/backend/ag32/proofs
Jul 02 03:39:59 Finished compiler/backend/ag32/proofs                          8m54s   1GB
Jul 02 03:39:59 Starting compiler/proofs
Jul 02 03:41:24 Finished compiler/proofs                                       1m24s   2GB
Jul 02 03:41:24 Starting candle/set-theory
Jul 02 03:41:49 Finished candle/set-theory                                       24s 832MB
Jul 02 03:41:49 Starting candle/syntax-lib
Jul 02 03:41:58 Finished candle/syntax-lib                                        8s 653MB
Jul 02 03:41:58 Starting candle/standard/syntax
Jul 02 03:42:46 FAILED: candle/standard/syntax
]0;Holmake: ~/regression/cakeml-929/basis/pure]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-929/basis/pure]0;Holmake: ~/regression/cakeml-929/misc]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-929/misc]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-8877f97ec124591c9fb742b443b7ef86e99ae2d6/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-929/misc]0;Holmake: ~/regression/cakeml-929/developers]0;Holmake: ~/regression/cakeml-929/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-929/misc]0;Holmake: ~/regression/cakeml-929/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-929/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-929/misc]0;Holmake: ~/regression/cakeml-929/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-929/basis/pure]0;Holmake: ~/regression/cakeml-929/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-929/candle/standard/syntax/holSyntaxExtraScript.sml : Fail "Static Errors"
 error in load holSyntaxExtraScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"