Job 374

CakeML:28524d1940731133f83b3439292571a42258723c
  Remove TAC_PROOF and prove from ml_translatorLib [Jul 21 17:10:47]
#500 (type+module-update)
Merging into:910722143cb157b627cd6d21db74c26607142fdf
  Make xlet_auto less likely to generate extra assumptions [Jul 19 13:34:47]
HOL:741148f614f5435da2a53e84dedd0c7a5e33d6d4
  Merge pull request #565 from AndreasLoow/holkernel-sort_vars-doc [Jul 21 09:28:01]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Jul 21 22:18:03 Claimed job
Jul 21 22:18:17 Building HOL
Jul 21 22:30:44 Starting developers/bin
Jul 21 22:30:54 Finished developers/bin                                           8s 224MB
Jul 21 22:30:56 Starting semantics/ffi
Jul 21 22:31:57 Finished semantics/ffi                                           59s 509MB
Jul 21 22:31:59 Starting semantics
Jul 21 22:34:25 Finished semantics                                             2m23s 748MB
Jul 21 22:34:27 Starting semantics/proofs
Jul 21 22:39:51 Finished semantics/proofs                                      5m21s   1GB
Jul 21 22:39:53 Starting basis/pure
Jul 21 22:45:35 Finished basis/pure                                            5m40s 784MB
Jul 21 22:45:37 Starting translator
Jul 21 22:48:26 Finished translator                                            2m46s 947MB
Jul 21 22:48:28 Starting compiler/parsing
Jul 21 22:50:35 Finished compiler/parsing                                      2m04s   2GB
Jul 21 22:50:37 Starting characteristic
Jul 21 22:54:59 Finished characteristic                                        4m20s   1GB
Jul 21 22:55:01 Starting basis
Jul 21 23:23:58 Finished basis                                                28m55s   2GB
Jul 21 23:24:00 Starting translator/monadic
Jul 21 23:24:04 Finished translator/monadic                                       1s  15MB
Jul 21 23:24:06 Starting compiler/inference
Jul 21 23:26:31 Finished compiler/inference                                    2m23s 785MB
Jul 21 23:26:33 Starting compiler/backend/reg_alloc
Jul 21 23:27:32 Finished compiler/backend/reg_alloc                              56s   1GB
Jul 21 23:27:34 Starting compiler/backend/gc
Jul 21 23:42:46 Finished compiler/backend/gc                                  15m10s   5GB
Jul 21 23:42:48 Starting compiler/backend
Jul 21 23:42:53 Finished compiler/backend                                         3s  14MB
Jul 21 23:42:55 Starting compiler/encoders/asm
Jul 21 23:42:58 Finished compiler/encoders/asm                                    0s  11MB
Jul 21 23:43:00 Starting compiler/encoders/x64
Jul 21 23:44:28 Finished compiler/encoders/x64                                 1m26s 742MB
Jul 21 23:44:30 Starting compiler/encoders/arm6
Jul 21 23:47:32 Finished compiler/encoders/arm6                                3m00s   1GB
Jul 21 23:47:34 Starting compiler/encoders/arm8
Jul 21 23:48:21 Finished compiler/encoders/arm8                                  44s 406MB
Jul 21 23:48:23 Starting compiler/encoders/mips
Jul 21 23:49:58 Finished compiler/encoders/mips                                1m33s 705MB
Jul 21 23:50:01 Starting compiler/encoders/riscv
Jul 21 23:51:34 Finished compiler/encoders/riscv                               1m31s 592MB
Jul 21 23:51:36 Starting compiler/backend/x64
Jul 21 23:52:06 Finished compiler/backend/x64                                    28s 883MB
Jul 21 23:52:08 Starting compiler/backend/arm6
Jul 21 23:52:45 Finished compiler/backend/arm6                                   34s   1GB
Jul 21 23:52:47 Starting compiler/backend/arm8
Jul 21 23:53:21 Finished compiler/backend/arm8                                   31s   1GB
Jul 21 23:53:23 Starting compiler/backend/mips
Jul 21 23:53:56 Finished compiler/backend/mips                                   31s   1GB
Jul 21 23:53:58 Starting compiler/backend/riscv
Jul 21 23:54:32 Finished compiler/backend/riscv                                  31s   1GB
Jul 21 23:54:34 Starting compiler/parsing/proofs
Jul 21 23:58:36 Finished compiler/parsing/proofs                               3m59s 813MB
Jul 21 23:58:38 Starting compiler/inference/proofs
Jul 22 00:02:51 Finished compiler/inference/proofs                             4m11s   1GB
Jul 22 00:02:53 Starting compiler/backend/semantics
Jul 22 00:17:01 Finished compiler/backend/semantics                           14m05s   2GB
Jul 22 00:17:03 Starting compiler/backend/reg_alloc/proofs
Jul 22 00:18:29 Finished compiler/backend/reg_alloc/proofs                     1m23s 662MB
Jul 22 00:18:31 Starting compiler/backend/proofs
Jul 22 01:13:25 Finished compiler/backend/proofs                              54m52s   2GB
Jul 22 01:13:27 Starting compiler/encoders/x64/proofs
Jul 22 01:24:52 Finished compiler/encoders/x64/proofs                         11m23s   1GB
Jul 22 01:24:54 Starting compiler/encoders/arm6/proofs
Jul 22 01:37:25 Finished compiler/encoders/arm6/proofs                        12m29s   2GB
Jul 22 01:37:27 Starting compiler/encoders/arm8/proofs
Jul 22 01:45:44 Finished compiler/encoders/arm8/proofs                         8m14s   1GB
Jul 22 01:45:46 Starting compiler/encoders/mips/proofs
Jul 22 01:57:06 Finished compiler/encoders/mips/proofs                        11m17s   2GB
Jul 22 01:57:08 Starting compiler/encoders/riscv/proofs
Jul 22 02:09:42 Finished compiler/encoders/riscv/proofs                       12m32s 867MB
Jul 22 02:09:44 Starting compiler/backend/x64/proofs
Jul 22 02:10:21 Finished compiler/backend/x64/proofs                             34s   1GB
Jul 22 02:10:23 Starting compiler/backend/arm6/proofs
Jul 22 02:11:03 Finished compiler/backend/arm6/proofs                            38s   1GB
Jul 22 02:11:05 Starting compiler/backend/arm8/proofs
Jul 22 02:11:38 Finished compiler/backend/arm8/proofs                            31s   1GB
Jul 22 02:11:40 Starting compiler/backend/mips/proofs
Jul 22 02:12:17 Finished compiler/backend/mips/proofs                            34s   1GB
Jul 22 02:12:19 Starting compiler/backend/riscv/proofs
Jul 22 02:12:54 Finished compiler/backend/riscv/proofs                           33s   1GB
Jul 22 02:12:56 Starting compiler/proofs
Jul 22 02:15:13 Finished compiler/proofs                                       2m15s   2GB
Jul 22 02:15:15 Starting candle/set-theory
Jul 22 02:16:11 Finished candle/set-theory                                       54s 588MB
Jul 22 02:16:13 Starting candle/syntax-lib
Jul 22 02:16:32 Finished candle/syntax-lib                                       17s 587MB
Jul 22 02:16:34 Starting candle/standard/syntax
Jul 22 02:19:19 Finished candle/standard/syntax                                2m42s 943MB
Jul 22 02:19:21 Starting candle/standard/semantics
Jul 22 02:21:38 Finished candle/standard/semantics                             2m14s 808MB
Jul 22 02:21:40 Starting candle/standard/monadic
Jul 22 02:24:08 Finished candle/standard/monadic                               2m26s 873MB
Jul 22 02:24:10 Starting candle/standard/ml_kernel
Jul 22 02:30:01 Finished candle/standard/ml_kernel                             5m48s   1GB
Jul 22 02:30:03 Starting candle/standard/opentheory
Jul 22 02:30:29 Finished candle/standard/opentheory                              24s 617MB
Jul 22 02:30:31 Starting characteristic/examples
Jul 22 02:33:06 Finished characteristic/examples                               2m32s   1GB
Jul 22 02:33:08 Starting tutorial/solutions
Jul 22 02:54:14 Finished tutorial/solutions                                   21m04s   6GB
Jul 22 02:54:16 Starting translator/monadic/examples
Jul 22 02:57:06 Finished translator/monadic/examples                           2m47s   2GB
Jul 22 02:57:08 Starting examples
Jul 22 03:05:03 Finished examples                                              7m53s   3GB
Jul 22 03:05:05 Starting examples/compilation
Jul 22 06:00:44 Finished examples/compilation                               2h55m37s   8GB
Jul 22 06:00:46 Starting examples/compilation/proofs
Jul 22 06:04:13 Finished examples/compilation/proofs                           3m24s   3GB
Jul 22 06:04:15 Starting compiler/benchmarks
Jul 22 06:04:17 Finished compiler/benchmarks                                      0s   4MB
Jul 22 06:04:21 Starting translator/okasaki-examples
Jul 22 06:10:50 Finished translator/okasaki-examples                           6m26s   1GB
Jul 22 06:10:52 Starting translator/other-examples
Jul 22 06:17:24 Finished translator/other-examples                             6m29s 984MB
Jul 22 06:17:26 Starting compiler/parsing/tests
Jul 22 06:17:36 FAILED: compiler/parsing/tests
]0;Holmake: ..]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-741148f614f5435da2a53e84dedd0c7a5e33d6d4/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-741148f614f5435da2a53e84dedd0c7a5e33d6d4/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-741148f614f5435da2a53e84dedd0c7a5e33d6d4/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-741148f614f5435da2a53e84dedd0c7a5e33d6d4/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ..]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/parsing/tests
Starting work on cmlTestsTheory
Starting work on lexerTestsTheory
lexerTestsTheory                                                                                                                                          OK
cmlTestsTheory                                                                                                                                   FAILED! <1>
                                               [Nd (mkNT nEliteral,L)
                                                  [Lf (TK (WordT 3),L)]]]]]]]]]]]]]]]]
 fringe =  [TK ValT; TK (AlphaT "w"); TK EqualsT; TK (WordT 3)]
 runtime: 0.01600s,    gctime: 0.00000s,     systime: 0.00000s.
 error in quse /scratch/cakeml/regression/cakeml-374/compiler/parsing/tests/cmlTestsScript.sml : Fail "Failed Semantics fails; is not the required "
 error in load cmlTestsScript : Fail "Failed Semantics fails; is not the required "
 Semantics (ptree_TopLevelDec) to  Dlet L (Pvar "w") (Lit (Word64 3w))
 Semantics fails; is not the required 
   Tdec (Dlet locs (Pvar "w") (Lit (Word64 3w)))
 Uncaught exception: Fail "Failed Semantics fails; is not the required "