Job 1766

CakeML:5525b2dc1da264a4ad4d5b5dd23599b8fe8bafe3
  Use Definition.new_definition [Feb 06 17:14:33]
HOL:3d9ce37db374287660618d9f1f93521e70a02bf3
  Fix dependency inaccuracies in separationLogic/src/holfoot [Feb 10 02:09:38]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 11 01:19:11 Claimed job
Feb 11 01:19:15 Reusing HOL
Feb 11 01:19:28 Starting developers
Feb 11 01:19:32 Finished developers                                               4s 122MB
Feb 11 01:19:32 Starting developers/bin
Feb 11 01:19:36 Finished developers/bin                                           4s 675MB
Feb 11 01:19:36 Starting semantics/ffi
Feb 11 01:19:46 Finished semantics/ffi                                            9s 245MB
Feb 11 01:19:46 Starting semantics
Feb 11 01:21:11 Finished semantics                                             1m24s   1GB
Feb 11 01:21:11 Starting semantics/proofs
Feb 11 01:24:43 Finished semantics/proofs                                      3m31s   1GB
Feb 11 01:24:43 Starting semantics/alt_semantics
Feb 11 01:24:55 Finished semantics/alt_semantics                                 11s 415MB
Feb 11 01:24:55 Starting semantics/alt_semantics/proofs
Feb 11 01:27:21 Finished semantics/alt_semantics/proofs                        2m26s   1GB
Feb 11 01:27:21 Starting basis/pure
Feb 11 01:28:13 Finished basis/pure                                              51s 893MB
Feb 11 01:28:13 Starting translator
Feb 11 01:31:06 Finished translator                                            2m52s   2GB
Feb 11 01:31:06 Starting compiler/parsing
Feb 11 01:32:19 Finished compiler/parsing                                      1m13s   1GB
Feb 11 01:32:19 Starting characteristic
Feb 11 01:38:16 Finished characteristic                                        5m56s   1GB
Feb 11 01:38:16 Starting translator/monadic
Feb 11 01:40:02 Finished translator/monadic                                    1m46s   1GB
Feb 11 01:40:03 Starting basis
Feb 11 02:25:29 Finished basis                                                45m22s  15GB
Feb 11 02:25:30 Starting compiler/inference
Feb 11 02:26:41 Finished compiler/inference                                    1m11s   1GB
Feb 11 02:26:41 Starting compiler/backend/reg_alloc
Feb 11 02:27:49 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 11 02:27:49 Starting compiler/backend/gc
Feb 11 02:31:16 Finished compiler/backend/gc                                   3m26s   1GB
Feb 11 02:31:16 Starting compiler/backend
Feb 11 02:36:24 Finished compiler/backend                                      5m07s   2GB
Feb 11 02:36:24 Starting compiler/encoders/asm
Feb 11 02:36:48 Finished compiler/encoders/asm                                   24s 719MB
Feb 11 02:36:48 Starting compiler/encoders/x64
Feb 11 02:37:15 Finished compiler/encoders/x64                                   27s 835MB
Feb 11 02:37:15 Starting compiler/encoders/arm7
Feb 11 02:38:09 Finished compiler/encoders/arm7                                  53s   1GB
Feb 11 02:38:09 Starting compiler/encoders/arm8
Feb 11 02:38:24 Finished compiler/encoders/arm8                                  14s 880MB
Feb 11 02:38:24 Starting compiler/encoders/mips
Feb 11 02:38:42 Finished compiler/encoders/mips                                  18s   1GB
Feb 11 02:38:42 Starting compiler/encoders/riscv
Feb 11 02:38:59 Finished compiler/encoders/riscv                                 16s 780MB
Feb 11 02:38:59 Starting compiler/encoders/ag32
Feb 11 02:39:19 Finished compiler/encoders/ag32                                  19s 690MB
Feb 11 02:39:19 Starting compiler/backend/x64
Feb 11 02:39:41 Finished compiler/backend/x64                                    22s   1GB
Feb 11 02:39:41 Starting compiler/backend/arm7
Feb 11 02:40:06 Finished compiler/backend/arm7                                   23s   1GB
Feb 11 02:40:06 Starting compiler/backend/arm8
Feb 11 02:40:28 Finished compiler/backend/arm8                                   22s   1GB
Feb 11 02:40:28 Starting compiler/backend/mips
Feb 11 02:40:50 Finished compiler/backend/mips                                   22s   1GB
Feb 11 02:40:50 Starting compiler/backend/riscv
Feb 11 02:41:12 Finished compiler/backend/riscv                                  21s   1GB
Feb 11 02:41:12 Starting compiler/backend/ag32
Feb 11 02:42:22 Finished compiler/backend/ag32                                 1m09s   1GB
Feb 11 02:42:22 Starting compiler/parsing/proofs
Feb 11 02:46:06 Finished compiler/parsing/proofs                               3m44s   1GB
Feb 11 02:46:06 Starting compiler/inference/proofs
Feb 11 02:48:32 Finished compiler/inference/proofs                             2m26s 960MB
Feb 11 02:48:33 Starting compiler/backend/semantics
Feb 11 03:16:35 Finished compiler/backend/semantics                           28m02s   2GB
Feb 11 03:16:35 Starting compiler/backend/reg_alloc/proofs
Feb 11 03:19:59 Finished compiler/backend/reg_alloc/proofs                     3m24s   1GB
Feb 11 03:19:59 Starting compiler/backend/proofs
Feb 11 04:11:35 Finished compiler/backend/proofs                              51m34s  15GB
Feb 11 04:11:35 Starting compiler/backend/serialiser
Feb 11 04:13:01 Finished compiler/backend/serialiser                           1m25s   1GB
Feb 11 04:13:01 Starting compiler/encoders/x64/proofs
Feb 11 04:22:38 Finished compiler/encoders/x64/proofs                          9m37s   4GB
Feb 11 04:22:38 Starting compiler/encoders/arm7/proofs
Feb 11 04:35:52 Finished compiler/encoders/arm7/proofs                        13m14s   3GB
Feb 11 04:35:53 Starting compiler/encoders/arm8/proofs
Feb 11 04:42:37 Finished compiler/encoders/arm8/proofs                         6m44s   1GB
Feb 11 04:42:37 Starting compiler/encoders/mips/proofs
Feb 11 04:52:39 Finished compiler/encoders/mips/proofs                        10m01s   3GB
Feb 11 04:52:39 Starting compiler/encoders/riscv/proofs
Feb 11 05:01:32 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Feb 11 05:01:33 Starting compiler/encoders/ag32/proofs
Feb 11 05:04:06 Finished compiler/encoders/ag32/proofs                         2m33s 698MB
Feb 11 05:04:06 Starting compiler/backend/x64/proofs
Feb 11 05:04:33 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 11 05:04:34 Starting compiler/backend/arm7/proofs
Feb 11 05:05:02 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 11 05:05:02 Starting compiler/backend/arm8/proofs
Feb 11 05:05:30 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 11 05:05:30 Starting compiler/backend/mips/proofs
Feb 11 05:05:57 Finished compiler/backend/mips/proofs                            26s   1GB
Feb 11 05:05:57 Starting compiler/backend/riscv/proofs
Feb 11 05:06:25 Finished compiler/backend/riscv/proofs                           27s   1GB
Feb 11 05:06:25 Starting compiler/backend/ag32/proofs
Feb 11 05:19:17 Finished compiler/backend/ag32/proofs                         12m51s   3GB
Feb 11 05:19:17 Starting compiler/proofs
Feb 11 05:21:12 Finished compiler/proofs                                       1m54s   3GB
Feb 11 05:21:12 Starting candle/set-theory
Feb 11 05:21:40 Finished candle/set-theory                                       27s 794MB
Feb 11 05:21:40 Starting candle/syntax-lib
Feb 11 05:21:51 Finished candle/syntax-lib                                       11s 461MB
Feb 11 05:21:51 Starting candle/standard/syntax
Feb 11 05:23:41 Finished candle/standard/syntax                                1m49s   1GB
Feb 11 05:23:41 Starting candle/standard/semantics
Feb 11 05:25:28 Finished candle/standard/semantics                             1m46s   1GB
Feb 11 05:25:28 Starting candle/standard/monadic
Feb 11 05:27:05 Finished candle/standard/monadic                               1m37s   1GB
Feb 11 05:27:05 Starting candle/standard/ml_kernel
Feb 11 05:33:53 Finished candle/standard/ml_kernel                             6m47s   3GB
Feb 11 05:33:53 Starting candle/overloading/syntax
Feb 11 05:36:57 Finished candle/overloading/syntax                             3m03s   1GB
Feb 11 05:36:57 Starting candle/overloading/semantics
Feb 11 05:48:33 Finished candle/overloading/semantics                         11m36s   2GB
Feb 11 05:48:33 Starting candle/prover
Feb 11 05:56:30 Finished candle/prover                                         7m56s   3GB
Feb 11 05:56:30 Starting pancake
Feb 11 05:59:11 Finished pancake                                               2m41s   3GB
Feb 11 05:59:11 Starting pancake/ffi
Feb 11 05:59:11 Finished pancake/ffi                                              0s  35MB
Feb 11 05:59:11 Starting pancake/semantics
Feb 11 06:01:38 Finished pancake/semantics                                     2m26s 996MB
Feb 11 06:01:38 Starting pancake/proofs
Feb 11 06:13:34 Finished pancake/proofs                                       11m56s   6GB
Feb 11 06:13:34 Starting characteristic/examples
Feb 11 06:14:59 Finished characteristic/examples                               1m24s   3GB
Feb 11 06:14:59 Starting tutorial/solutions
Feb 11 06:31:05 Finished tutorial/solutions                                   16m05s  10GB
Feb 11 06:31:05 Starting translator/monadic/examples
Feb 11 06:34:25 Finished translator/monadic/examples                           3m19s   2GB
Feb 11 06:34:25 Starting examples
Feb 11 06:43:32 Finished examples                                              9m06s   4GB
Feb 11 06:43:32 Starting examples/compilation/x64
Feb 11 09:11:28 Finished examples/compilation/x64                           2h27m55s  17GB
Feb 11 09:11:29 Starting examples/compilation/x64/proofs
Feb 11 09:13:44 Finished examples/compilation/x64/proofs                       2m15s   3GB
Feb 11 09:13:44 Starting examples/compilation/ag32
Feb 11 09:48:23 Finished examples/compilation/ag32                            34m38s   9GB
Feb 11 09:48:23 Starting examples/compilation/ag32/proofs
Feb 11 09:49:18 Finished examples/compilation/ag32/proofs                        54s   2GB
Feb 11 09:49:18 Starting examples/cost
Feb 11 10:44:21 Finished examples/cost                                        55m01s   7GB
Feb 11 10:44:21 Starting examples/lpr_checker
Feb 11 10:45:15 Finished examples/lpr_checker                                    53s   1GB
Feb 11 10:45:15 Starting examples/lpr_checker/array
Feb 11 11:13:22 Finished examples/lpr_checker/array                           28m07s   8GB
Feb 11 11:13:22 Starting examples/lpr_checker/array/compilation
Feb 11 12:35:32 Finished examples/lpr_checker/array/compilation             1h22m08s  26GB
Feb 11 12:35:32 Starting examples/lpr_checker/array/compilation/proofs
Feb 11 12:36:55 Finished examples/lpr_checker/array/compilation/proofs         1m23s   6GB
Feb 11 12:36:56 Starting examples/opentheory
Feb 11 12:42:20 FAILED: examples/opentheory
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/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)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[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)/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$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanned 35 directories
Starting work on README.md
Starting work on prettyTheory
README.md                                                                                                                                                                         (0s)     OK
prettyTheory                                                                                                                                                                     (19s)     OK
Starting work on readerTheory
readerTheory                                                                                                                                                                     (49s)     OK
Starting work on reader_initTheory
reader_initTheory                                                                                                                                                                (25s)     OK
Starting work on readerProofTheory
readerProofTheory                                                                                                                                                                (62s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                                                                                                                            (19s)     OK
reader_commonProgTheory                                                                                                                                                         (154s)FAIL<1>
 Translating obj_t
 Saved theorem _______ "nsLookup_reader_commonProg_env_79_pfun_eqs"
 Adding nsLookup representation thms for [reader_commonProg_env_78]
 Adding nsLookup representation thms for [reader_commonProg_env_79]
 Saved theorem _______ "obj_t_v_thm"
 /home/cug/hk324/cml-regression/cakeml-1766/examples/opentheory/reader_commonProgScript.sml:133: error: Value or constructor (lrnext_def) has not been declared in structure sptreeTheory
 Found near translate sptreeTheory.lrnext_def
 error in quse /home/cug/hk324/cml-regression/cakeml-1766/examples/opentheory/reader_commonProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-1766/examples/opentheory/reader_commonProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"