Job 1765

CakeML:62355d1569fbecf5ed8d03eb7c503322622c95aa
  adds README for `candle/overloading` [Feb 07 06:51:45]
#860 (cyclicity-check-rebase)
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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 10 19:30:02 Claimed job
Feb 10 19:30:04 Reusing HOL
Feb 10 19:30:44 Starting developers
Feb 10 19:30:49 Finished developers                                               4s 102MB
Feb 10 19:30:49 Starting developers/bin
Feb 10 19:30:55 Finished developers/bin                                           5s 670MB
Feb 10 19:30:55 Starting semantics/ffi
Feb 10 19:31:05 Finished semantics/ffi                                           10s 205MB
Feb 10 19:31:05 Starting semantics
Feb 10 19:32:36 Finished semantics                                             1m30s   1GB
Feb 10 19:32:36 Starting semantics/proofs
Feb 10 19:36:26 Finished semantics/proofs                                      3m49s   1GB
Feb 10 19:36:26 Starting semantics/alt_semantics
Feb 10 19:36:40 Finished semantics/alt_semantics                                 13s 369MB
Feb 10 19:36:40 Starting semantics/alt_semantics/proofs
Feb 10 19:39:23 Finished semantics/alt_semantics/proofs                        2m42s 697MB
Feb 10 19:39:23 Starting basis/pure
Feb 10 19:40:17 Finished basis/pure                                              53s 896MB
Feb 10 19:40:17 Starting translator
Feb 10 19:43:23 Finished translator                                            3m05s   2GB
Feb 10 19:43:23 Starting compiler/parsing
Feb 10 19:44:44 Finished compiler/parsing                                      1m20s   2GB
Feb 10 19:44:44 Starting characteristic
Feb 10 19:50:59 Finished characteristic                                        6m14s   1GB
Feb 10 19:50:59 Starting translator/monadic
Feb 10 19:52:50 Finished translator/monadic                                    1m50s   1GB
Feb 10 19:52:50 Starting basis
Feb 10 20:42:57 Finished basis                                                50m06s  10GB
Feb 10 20:42:58 Starting compiler/inference
Feb 10 20:44:11 Finished compiler/inference                                    1m13s   1GB
Feb 10 20:44:11 Starting compiler/backend/reg_alloc
Feb 10 20:45:23 Finished compiler/backend/reg_alloc                            1m11s   1GB
Feb 10 20:45:23 Starting compiler/backend/gc
Feb 10 20:49:13 Finished compiler/backend/gc                                   3m49s   2GB
Feb 10 20:49:13 Starting compiler/backend
Feb 10 20:54:48 Finished compiler/backend                                      5m34s   2GB
Feb 10 20:54:48 Starting compiler/encoders/asm
Feb 10 20:55:14 Finished compiler/encoders/asm                                   25s 672MB
Feb 10 20:55:14 Starting compiler/encoders/x64
Feb 10 20:55:42 Finished compiler/encoders/x64                                   28s 594MB
Feb 10 20:55:43 Starting compiler/encoders/arm7
Feb 10 20:56:37 Finished compiler/encoders/arm7                                  53s 662MB
Feb 10 20:56:37 Starting compiler/encoders/arm8
Feb 10 20:56:52 Finished compiler/encoders/arm8                                  15s 779MB
Feb 10 20:56:52 Starting compiler/encoders/mips
Feb 10 20:57:12 Finished compiler/encoders/mips                                  19s   1GB
Feb 10 20:57:12 Starting compiler/encoders/riscv
Feb 10 20:57:30 Finished compiler/encoders/riscv                                 17s 784MB
Feb 10 20:57:30 Starting compiler/encoders/ag32
Feb 10 20:57:51 Finished compiler/encoders/ag32                                  21s 588MB
Feb 10 20:57:51 Starting compiler/backend/x64
Feb 10 20:58:14 Finished compiler/backend/x64                                    22s   1GB
Feb 10 20:58:14 Starting compiler/backend/arm7
Feb 10 20:58:38 Finished compiler/backend/arm7                                   23s   1GB
Feb 10 20:58:38 Starting compiler/backend/arm8
Feb 10 20:59:01 Finished compiler/backend/arm8                                   22s   1GB
Feb 10 20:59:01 Starting compiler/backend/mips
Feb 10 20:59:24 Finished compiler/backend/mips                                   22s   1GB
Feb 10 20:59:24 Starting compiler/backend/riscv
Feb 10 20:59:48 Finished compiler/backend/riscv                                  23s   1GB
Feb 10 20:59:48 Starting compiler/backend/ag32
Feb 10 21:01:03 Finished compiler/backend/ag32                                 1m15s   1GB
Feb 10 21:01:03 Starting compiler/parsing/proofs
Feb 10 21:05:10 Finished compiler/parsing/proofs                               4m06s   1GB
Feb 10 21:05:11 Starting compiler/inference/proofs
Feb 10 21:07:50 Finished compiler/inference/proofs                             2m39s 970MB
Feb 10 21:07:51 Starting compiler/backend/semantics
Feb 10 21:40:57 Finished compiler/backend/semantics                           33m06s   2GB
Feb 10 21:40:57 Starting compiler/backend/reg_alloc/proofs
Feb 10 21:44:52 Finished compiler/backend/reg_alloc/proofs                     3m53s 744MB
Feb 10 21:44:53 Starting compiler/backend/proofs
Feb 10 22:44:20 Finished compiler/backend/proofs                              59m26s  13GB
Feb 10 22:44:20 Starting compiler/backend/serialiser
Feb 10 22:45:53 Finished compiler/backend/serialiser                           1m32s   2GB
Feb 10 22:45:53 Starting compiler/encoders/x64/proofs
Feb 10 22:56:12 Finished compiler/encoders/x64/proofs                         10m19s   4GB
Feb 10 22:56:12 Starting compiler/encoders/arm7/proofs
Feb 10 23:10:45 Finished compiler/encoders/arm7/proofs                        14m32s   5GB
Feb 10 23:10:45 Starting compiler/encoders/arm8/proofs
Feb 10 23:18:03 Finished compiler/encoders/arm8/proofs                         7m17s   1GB
Feb 10 23:18:03 Starting compiler/encoders/mips/proofs
Feb 10 23:28:46 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Feb 10 23:28:46 Starting compiler/encoders/riscv/proofs
Feb 10 23:38:07 Finished compiler/encoders/riscv/proofs                        9m20s   1GB
Feb 10 23:38:07 Starting compiler/encoders/ag32/proofs
Feb 10 23:40:56 Finished compiler/encoders/ag32/proofs                         2m48s 634MB
Feb 10 23:40:56 Starting compiler/backend/x64/proofs
Feb 10 23:41:25 Finished compiler/backend/x64/proofs                             28s   1GB
Feb 10 23:41:25 Starting compiler/backend/arm7/proofs
Feb 10 23:41:55 Finished compiler/backend/arm7/proofs                            29s   1GB
Feb 10 23:41:55 Starting compiler/backend/arm8/proofs
Feb 10 23:42:24 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 10 23:42:24 Starting compiler/backend/mips/proofs
Feb 10 23:42:54 Finished compiler/backend/mips/proofs                            29s   1GB
Feb 10 23:42:54 Starting compiler/backend/riscv/proofs
Feb 10 23:43:23 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 10 23:43:23 Starting compiler/backend/ag32/proofs
Feb 10 23:57:12 Finished compiler/backend/ag32/proofs                         13m46s   2GB
Feb 10 23:57:12 Starting compiler/proofs
Feb 10 23:59:12 Finished compiler/proofs                                       2m00s   3GB
Feb 10 23:59:12 Starting candle/set-theory
Feb 10 23:59:43 Finished candle/set-theory                                       29s 829MB
Feb 10 23:59:43 Starting candle/syntax-lib
Feb 10 23:59:55 Finished candle/syntax-lib                                       12s 469MB
Feb 10 23:59:55 Starting candle/standard/syntax
Feb 11 00:01:53 Finished candle/standard/syntax                                1m57s   1GB
Feb 11 00:01:53 Starting candle/standard/semantics
Feb 11 00:03:46 Finished candle/standard/semantics                             1m53s   1GB
Feb 11 00:03:47 Starting candle/standard/monadic
Feb 11 00:05:31 Finished candle/standard/monadic                               1m44s   1GB
Feb 11 00:05:31 Starting candle/standard/ml_kernel
Feb 11 00:12:47 Finished candle/standard/ml_kernel                             7m15s   3GB
Feb 11 00:12:47 Starting candle/overloading/syntax
Feb 11 00:16:07 Finished candle/overloading/syntax                             3m19s   1GB
Feb 11 00:16:07 Starting candle/overloading/semantics
Feb 11 00:28:41 Finished candle/overloading/semantics                         12m33s   2GB
Feb 11 00:28:41 Starting candle/overloading/monadic
Feb 11 00:31:08 Finished candle/overloading/monadic                            2m26s   1GB
Feb 11 00:31:08 Starting candle/overloading/ml_kernel
Feb 11 00:39:24 Finished candle/overloading/ml_kernel                          8m15s   3GB
Feb 11 00:39:25 Starting candle/overloading/ml_checker
Feb 11 00:41:55 Finished candle/overloading/ml_checker                         2m29s   3GB
Feb 11 00:41:55 Starting candle/prover
Feb 11 00:49:58 Finished candle/prover                                         8m02s   3GB
Feb 11 00:49:58 Starting pancake
Feb 11 00:52:51 Finished pancake                                               2m53s   2GB
Feb 11 00:52:52 Starting pancake/ffi
Feb 11 00:52:52 Finished pancake/ffi                                              0s  18MB
Feb 11 00:52:52 Starting pancake/semantics
Feb 11 00:55:37 Finished pancake/semantics                                     2m44s   1GB
Feb 11 00:55:37 Starting pancake/proofs
Feb 11 01:08:48 Finished pancake/proofs                                       13m09s   6GB
Feb 11 01:08:48 Starting characteristic/examples
Feb 11 01:10:14 Finished characteristic/examples                               1m25s   1GB
Feb 11 01:10:14 Starting tutorial/solutions
Feb 11 01:27:16 Finished tutorial/solutions                                   17m01s   8GB
Feb 11 01:27:16 Starting translator/monadic/examples
Feb 11 01:30:58 Finished translator/monadic/examples                           3m41s   3GB
Feb 11 01:30:58 Starting examples
Feb 11 01:41:18 Finished examples                                             10m19s   4GB
Feb 11 01:41:18 Starting examples/compilation/x64
Feb 11 04:16:08 Finished examples/compilation/x64                           2h34m49s  14GB
Feb 11 04:16:08 Starting examples/compilation/x64/proofs
Feb 11 04:18:41 Finished examples/compilation/x64/proofs                       2m33s   3GB
Feb 11 04:18:41 Starting examples/compilation/ag32
Feb 11 04:55:03 Finished examples/compilation/ag32                            36m21s  12GB
Feb 11 04:55:03 Starting examples/compilation/ag32/proofs
Feb 11 04:56:01 Finished examples/compilation/ag32/proofs                        57s   2GB
Feb 11 04:56:01 Starting examples/cost
Feb 11 05:58:08 Finished examples/cost                                      1h02m06s   7GB
Feb 11 05:58:08 Starting examples/lpr_checker
Feb 11 05:59:04 Finished examples/lpr_checker                                    55s 987MB
Feb 11 05:59:05 Starting examples/lpr_checker/array
Feb 11 06:30:35 Finished examples/lpr_checker/array                           31m29s   5GB
Feb 11 06:30:35 Starting examples/lpr_checker/array/compilation
Feb 11 07:57:56 Finished examples/lpr_checker/array/compilation             1h27m19s  26GB
Feb 11 07:57:56 Starting examples/lpr_checker/array/compilation/proofs
Feb 11 07:59:25 Finished examples/lpr_checker/array/compilation/proofs         1m28s   7GB
Feb 11 07:59:25 Starting examples/opentheory
Feb 11 08:05:15 FAILED: examples/opentheory
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanned 35 directories
Starting work on README.md
Starting work on prettyTheory
README.md                                                           (0s)     OK
prettyTheory                                                       (21s)     OK
Starting work on readerTheory
readerTheory                                                       (56s)     OK
Starting work on reader_initTheory
reader_initTheory                                                  (26s)     OK
Starting work on readerProofTheory
readerProofTheory                                                  (66s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                              (20s)     OK
reader_commonProgTheory                                           (165s)FAIL<1>
 Translating obj_t
 Saved theorem _______ "nsLookup_reader_commonProg_env_79_pfun_eqs"
 Adding nsLookup representation thms for [reader_commonProg_env_78]
 error in quse /home/cake/oven/regression/cakeml-1765/examples/opentheory/reader_commonProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1765/examples/opentheory/reader_commonProgScript : Fail "Static Errors"
 Adding nsLookup representation thms for [reader_commonProg_env_79]
 Saved theorem _______ "obj_t_v_thm"
 /home/cake/oven/regression/cakeml-1765/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
 Uncaught exception: Fail "Static Errors"