Job 1764

CakeML:874bb72cf49d4a806eb88215b31da518ea5352f8
  Delay building of L3 equivalence proofs until needed [Jan 25 23:29:04]
#858 (asl-equiv)
Merging into: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 10 11:22:50 Claimed job
Feb 10 11:22:57 Building HOL
Feb 10 11:32:03 Starting developers
Feb 10 11:32:08 Finished developers                                               4s 189MB
Feb 10 11:32:08 Starting developers/bin
Feb 10 11:32:12 Finished developers/bin                                           4s 674MB
Feb 10 11:32:12 Starting semantics/ffi
Feb 10 11:32:21 Finished semantics/ffi                                            9s 222MB
Feb 10 11:32:22 Starting semantics
Feb 10 11:33:56 Finished semantics                                             1m34s   1GB
Feb 10 11:33:56 Starting semantics/proofs
Feb 10 11:37:33 Finished semantics/proofs                                      3m36s   1GB
Feb 10 11:37:33 Starting semantics/alt_semantics
Feb 10 11:37:45 Finished semantics/alt_semantics                                 11s 399MB
Feb 10 11:37:45 Starting semantics/alt_semantics/proofs
Feb 10 11:40:12 Finished semantics/alt_semantics/proofs                        2m26s 918MB
Feb 10 11:40:12 Starting basis/pure
Feb 10 11:43:01 Finished basis/pure                                            2m49s 802MB
Feb 10 11:43:01 Starting translator
Feb 10 11:45:53 Finished translator                                            2m51s   1GB
Feb 10 11:45:53 Starting compiler/parsing
Feb 10 11:47:06 Finished compiler/parsing                                      1m13s   3GB
Feb 10 11:47:06 Starting characteristic
Feb 10 11:52:55 Finished characteristic                                        5m48s   2GB
Feb 10 11:52:55 Starting translator/monadic
Feb 10 11:54:39 Finished translator/monadic                                    1m44s   1GB
Feb 10 11:54:39 Starting basis
Feb 10 12:40:07 Finished basis                                                45m26s  15GB
Feb 10 12:40:08 Starting compiler/inference
Feb 10 12:41:23 Finished compiler/inference                                    1m15s   1GB
Feb 10 12:41:23 Starting compiler/backend/reg_alloc
Feb 10 12:42:31 Finished compiler/backend/reg_alloc                            1m07s   1GB
Feb 10 12:42:31 Starting compiler/backend/gc
Feb 10 12:46:09 Finished compiler/backend/gc                                   3m37s   2GB
Feb 10 12:46:09 Starting compiler/backend
Feb 10 12:51:17 Finished compiler/backend                                      5m08s   2GB
Feb 10 12:51:17 Starting compiler/encoders/asm
Feb 10 12:51:42 Finished compiler/encoders/asm                                   24s 583MB
Feb 10 12:51:42 Starting compiler/encoders/x64
Feb 10 12:52:45 Finished compiler/encoders/x64                                 1m02s 810MB
Feb 10 12:52:45 Starting compiler/encoders/arm7
Feb 10 12:54:47 Finished compiler/encoders/arm7                                2m02s   1GB
Feb 10 12:54:48 Starting compiler/encoders/arm8
Feb 10 12:55:26 Finished compiler/encoders/arm8                                  38s 920MB
Feb 10 12:55:26 Starting compiler/encoders/arm8_asl
Feb 10 14:20:46 Finished compiler/encoders/arm8_asl                         1h25m18s  20GB
Feb 10 14:20:46 Starting compiler/encoders/mips
Feb 10 14:22:13 Finished compiler/encoders/mips                                1m27s   1GB
Feb 10 14:22:14 Starting compiler/encoders/riscv
Feb 10 14:23:58 Finished compiler/encoders/riscv                               1m44s   1GB
Feb 10 14:23:58 Starting compiler/encoders/ag32
Feb 10 14:24:18 Finished compiler/encoders/ag32                                  19s 891MB
Feb 10 14:24:18 Starting compiler/backend/x64
Feb 10 14:24:39 Finished compiler/backend/x64                                    20s   1GB
Feb 10 14:24:39 Starting compiler/backend/arm7
Feb 10 14:25:02 Finished compiler/backend/arm7                                   22s   1GB
Feb 10 14:25:02 Starting compiler/backend/arm8
Feb 10 14:25:23 Finished compiler/backend/arm8                                   21s   1GB
Feb 10 14:25:24 Starting compiler/backend/mips
Feb 10 14:25:46 Finished compiler/backend/mips                                   22s   1GB
Feb 10 14:25:46 Starting compiler/backend/riscv
Feb 10 14:26:07 Finished compiler/backend/riscv                                  21s   1GB
Feb 10 14:26:08 Starting compiler/backend/ag32
Feb 10 14:27:18 Finished compiler/backend/ag32                                 1m10s   1GB
Feb 10 14:27:19 Starting compiler/parsing/proofs
Feb 10 14:31:04 Finished compiler/parsing/proofs                               3m45s   1GB
Feb 10 14:31:05 Starting compiler/inference/proofs
Feb 10 14:33:33 Finished compiler/inference/proofs                             2m28s   1GB
Feb 10 14:33:33 Starting compiler/backend/semantics
Feb 10 15:01:32 Finished compiler/backend/semantics                           27m59s   2GB
Feb 10 15:01:32 Starting compiler/backend/reg_alloc/proofs
Feb 10 15:04:58 Finished compiler/backend/reg_alloc/proofs                     3m25s 903MB
Feb 10 15:04:58 Starting compiler/backend/proofs
Feb 10 15:56:20 Finished compiler/backend/proofs                              51m21s  15GB
Feb 10 15:56:21 Starting compiler/backend/serialiser
Feb 10 15:57:47 Finished compiler/backend/serialiser                           1m26s   1GB
Feb 10 15:57:48 Starting compiler/encoders/x64/proofs
Feb 10 16:07:26 Finished compiler/encoders/x64/proofs                          9m38s   4GB
Feb 10 16:07:26 Starting compiler/encoders/arm7/proofs
Feb 10 16:20:32 Finished compiler/encoders/arm7/proofs                        13m05s   3GB
Feb 10 16:20:32 Starting compiler/encoders/arm8/proofs
Feb 10 16:27:20 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
Feb 10 16:27:20 Starting compiler/encoders/arm8_asl/proofs
Feb 10 17:17:34 Finished compiler/encoders/arm8_asl/proofs                    50m11s   5GB
Feb 10 17:17:34 Starting compiler/encoders/mips/proofs
Feb 10 17:27:28 Finished compiler/encoders/mips/proofs                         9m53s   2GB
Feb 10 17:27:28 Starting compiler/encoders/riscv/proofs
Feb 10 17:36:21 Finished compiler/encoders/riscv/proofs                        8m52s   1GB
Feb 10 17:36:21 Starting compiler/encoders/ag32/proofs
Feb 10 17:38:54 Finished compiler/encoders/ag32/proofs                         2m32s 703MB
Feb 10 17:38:54 Starting compiler/backend/x64/proofs
Feb 10 17:39:21 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 10 17:39:21 Starting compiler/backend/arm7/proofs
Feb 10 17:39:50 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 10 17:39:50 Starting compiler/backend/arm8/proofs
Feb 10 17:40:18 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 10 17:40:19 Starting compiler/backend/arm8_asl
Feb 10 17:40:41 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 10 17:40:41 Starting compiler/backend/mips/proofs
Feb 10 17:41:09 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 10 17:41:09 Starting compiler/backend/riscv/proofs
Feb 10 17:41:36 Finished compiler/backend/riscv/proofs                           27s   1GB
Feb 10 17:41:36 Starting compiler/backend/ag32/proofs
Feb 10 17:54:16 Finished compiler/backend/ag32/proofs                         12m39s   2GB
Feb 10 17:54:16 Starting compiler/proofs
Feb 10 17:56:26 Finished compiler/proofs                                       2m09s   3GB
Feb 10 17:56:26 Starting candle/set-theory
Feb 10 17:56:54 Finished candle/set-theory                                       28s 850MB
Feb 10 17:56:54 Starting candle/syntax-lib
Feb 10 17:57:06 Finished candle/syntax-lib                                       11s 639MB
Feb 10 17:57:06 Starting candle/standard/syntax
Feb 10 17:58:55 Finished candle/standard/syntax                                1m48s   1GB
Feb 10 17:58:55 Starting candle/standard/semantics
Feb 10 18:00:43 Finished candle/standard/semantics                             1m47s   1GB
Feb 10 18:00:43 Starting candle/standard/monadic
Feb 10 18:02:20 Finished candle/standard/monadic                               1m36s   1GB
Feb 10 18:02:20 Starting candle/standard/ml_kernel
Feb 10 18:09:00 Finished candle/standard/ml_kernel                             6m40s   4GB
Feb 10 18:09:01 Starting candle/overloading/syntax
Feb 10 18:12:04 Finished candle/overloading/syntax                             3m03s   1GB
Feb 10 18:12:05 Starting candle/overloading/semantics
Feb 10 18:23:50 Finished candle/overloading/semantics                         11m42s   2GB
Feb 10 18:23:51 Starting candle/prover
Feb 10 18:31:26 Finished candle/prover                                         7m35s   3GB
Feb 10 18:31:26 Starting pancake
Feb 10 18:34:11 Finished pancake                                               2m44s   2GB
Feb 10 18:34:11 Starting pancake/ffi
Feb 10 18:34:11 Finished pancake/ffi                                              0s  35MB
Feb 10 18:34:11 Starting pancake/semantics
Feb 10 18:36:40 Finished pancake/semantics                                     2m28s   1GB
Feb 10 18:36:41 Starting pancake/proofs
Feb 10 18:48:43 Finished pancake/proofs                                       12m02s   4GB
Feb 10 18:48:43 Starting characteristic/examples
Feb 10 18:50:09 Finished characteristic/examples                               1m25s   3GB
Feb 10 18:50:09 Starting tutorial/solutions
Feb 10 19:06:26 Finished tutorial/solutions                                   16m16s  10GB
Feb 10 19:06:26 Starting translator/monadic/examples
Feb 10 19:09:47 Finished translator/monadic/examples                           3m20s   2GB
Feb 10 19:09:47 Starting examples
Feb 10 19:19:04 Finished examples                                              9m17s   4GB
Feb 10 19:19:05 Starting examples/compilation/x64
Feb 10 21:47:43 Finished examples/compilation/x64                           2h28m37s  23GB
Feb 10 21:47:43 Starting examples/compilation/x64/proofs
Feb 10 21:49:57 Finished examples/compilation/x64/proofs                       2m13s   3GB
Feb 10 21:49:57 Starting examples/compilation/ag32
Feb 10 22:24:30 Finished examples/compilation/ag32                            34m32s  10GB
Feb 10 22:24:30 Starting examples/compilation/ag32/proofs
Feb 10 22:25:25 Finished examples/compilation/ag32/proofs                        54s   2GB
Feb 10 22:25:25 Starting examples/cost
Feb 10 23:21:02 Finished examples/cost                                        55m35s  10GB
Feb 10 23:21:02 Starting examples/lpr_checker
Feb 10 23:21:54 Finished examples/lpr_checker                                    52s 743MB
Feb 10 23:21:54 Starting examples/lpr_checker/array
Feb 10 23:49:53 Finished examples/lpr_checker/array                           27m58s   7GB
Feb 10 23:49:53 Starting examples/lpr_checker/array/compilation
Feb 11 01:12:16 Finished examples/lpr_checker/array/compilation             1h22m20s  31GB
Feb 11 01:12:18 Starting examples/lpr_checker/array/compilation/proofs
Feb 11 01:13:47 Finished examples/lpr_checker/array/compilation/proofs         1m28s   7GB
Feb 11 01:13:47 Starting examples/opentheory
Feb 11 01:19:11 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                                                       (20s)     OK
Starting work on readerTheory
readerTheory                                                       (51s)     OK
Starting work on reader_initTheory
reader_initTheory                                                  (24s)     OK
Starting work on readerProofTheory
readerProofTheory                                                  (64s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                              (20s)     OK
reader_commonProgTheory                                           (151s)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-1764/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-1764/examples/opentheory/reader_commonProgScript.sml : Fail "Static Errors"
 error in load /home/cug/hk324/cml-regression/cakeml-1764/examples/opentheory/reader_commonProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"