Job 1763

CakeML:b6ce1417ef4a3913736824d1853fa54db032c681
  Merge branch 'master' into minor-reheapification [Jan 21 05:38:01]
#855 (minor-reheapification)
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 06:40:05 Claimed job
Feb 10 06:40:08 Building HOL
Feb 10 06:50:09 Starting developers
Feb 10 06:50:14 Finished developers                                               4s  81MB
Feb 10 06:50:15 Starting developers/bin
Feb 10 06:50:20 Finished developers/bin                                           5s 670MB
Feb 10 06:50:20 Starting semantics/ffi
Feb 10 06:50:31 Finished semantics/ffi                                           10s 203MB
Feb 10 06:50:31 Starting semantics
Feb 10 06:52:29 Finished semantics                                             1m58s   1GB
Feb 10 06:52:29 Starting semantics/proofs
Feb 10 06:56:20 Finished semantics/proofs                                      3m50s   1GB
Feb 10 06:56:20 Starting semantics/alt_semantics
Feb 10 06:56:34 Finished semantics/alt_semantics                                 14s 371MB
Feb 10 06:56:35 Starting semantics/alt_semantics/proofs
Feb 10 06:59:15 Finished semantics/alt_semantics/proofs                        2m40s 836MB
Feb 10 06:59:16 Starting basis/pure
Feb 10 07:02:21 Finished basis/pure                                            3m04s 628MB
Feb 10 07:02:21 Starting translator
Feb 10 07:05:26 Finished translator                                            3m04s   1GB
Feb 10 07:05:26 Starting compiler/parsing
Feb 10 07:06:47 Finished compiler/parsing                                      1m21s   2GB
Feb 10 07:06:48 Starting characteristic
Feb 10 07:12:57 Finished characteristic                                        6m08s   1GB
Feb 10 07:12:57 Starting translator/monadic
Feb 10 07:14:47 Finished translator/monadic                                    1m50s   1GB
Feb 10 07:14:47 Starting basis
Feb 10 08:04:48 Finished basis                                                49m58s  13GB
Feb 10 08:04:48 Starting compiler/inference
Feb 10 08:06:09 Finished compiler/inference                                    1m20s   1GB
Feb 10 08:06:09 Starting compiler/backend/reg_alloc
Feb 10 08:07:20 Finished compiler/backend/reg_alloc                            1m10s   1GB
Feb 10 08:07:20 Starting compiler/backend/gc
Feb 10 08:11:23 Finished compiler/backend/gc                                   4m01s   1GB
Feb 10 08:11:23 Starting compiler/backend
Feb 10 08:16:56 Finished compiler/backend                                      5m33s   2GB
Feb 10 08:16:56 Starting compiler/encoders/asm
Feb 10 08:17:22 Finished compiler/encoders/asm                                   25s 918MB
Feb 10 08:17:23 Starting compiler/encoders/x64
Feb 10 08:18:30 Finished compiler/encoders/x64                                 1m07s 766MB
Feb 10 08:18:30 Starting compiler/encoders/arm7
Feb 10 08:20:44 Finished compiler/encoders/arm7                                2m13s   1GB
Feb 10 08:20:44 Starting compiler/encoders/arm8
Feb 10 08:21:25 Finished compiler/encoders/arm8                                  40s 871MB
Feb 10 08:21:25 Starting compiler/encoders/mips
Feb 10 08:23:04 Finished compiler/encoders/mips                                1m38s   1GB
Feb 10 08:23:05 Starting compiler/encoders/riscv
Feb 10 08:25:01 Finished compiler/encoders/riscv                               1m56s   1GB
Feb 10 08:25:02 Starting compiler/encoders/ag32
Feb 10 08:25:22 Finished compiler/encoders/ag32                                  20s 799MB
Feb 10 08:25:22 Starting compiler/backend/x64
Feb 10 08:25:45 Finished compiler/backend/x64                                    21s   1GB
Feb 10 08:25:45 Starting compiler/backend/arm7
Feb 10 08:26:10 Finished compiler/backend/arm7                                   24s   1GB
Feb 10 08:26:10 Starting compiler/backend/arm8
Feb 10 08:26:32 Finished compiler/backend/arm8                                   22s   1GB
Feb 10 08:26:33 Starting compiler/backend/mips
Feb 10 08:26:54 Finished compiler/backend/mips                                   21s   1GB
Feb 10 08:26:55 Starting compiler/backend/riscv
Feb 10 08:27:19 Finished compiler/backend/riscv                                  23s   1GB
Feb 10 08:27:19 Starting compiler/backend/ag32
Feb 10 08:28:34 Finished compiler/backend/ag32                                 1m14s   1GB
Feb 10 08:28:34 Starting compiler/parsing/proofs
Feb 10 08:32:38 Finished compiler/parsing/proofs                               4m04s   1GB
Feb 10 08:32:39 Starting compiler/inference/proofs
Feb 10 08:35:17 Finished compiler/inference/proofs                             2m38s   1GB
Feb 10 08:35:18 Starting compiler/backend/semantics
Feb 10 09:08:20 Finished compiler/backend/semantics                           33m01s   2GB
Feb 10 09:08:20 Starting compiler/backend/reg_alloc/proofs
Feb 10 09:12:17 Finished compiler/backend/reg_alloc/proofs                     3m56s 769MB
Feb 10 09:12:17 Starting compiler/backend/proofs
Feb 10 10:11:27 Finished compiler/backend/proofs                              59m09s  23GB
Feb 10 10:11:27 Starting compiler/backend/serialiser
Feb 10 10:12:57 Finished compiler/backend/serialiser                           1m30s   1GB
Feb 10 10:12:58 Starting compiler/encoders/x64/proofs
Feb 10 10:23:15 Finished compiler/encoders/x64/proofs                         10m17s   5GB
Feb 10 10:23:15 Starting compiler/encoders/arm7/proofs
Feb 10 10:37:25 Finished compiler/encoders/arm7/proofs                        14m09s   4GB
Feb 10 10:37:25 Starting compiler/encoders/arm8/proofs
Feb 10 10:44:46 Finished compiler/encoders/arm8/proofs                         7m20s   1GB
Feb 10 10:44:46 Starting compiler/encoders/mips/proofs
Feb 10 10:55:42 Finished compiler/encoders/mips/proofs                        10m55s   2GB
Feb 10 10:55:42 Starting compiler/encoders/riscv/proofs
Feb 10 11:05:13 Finished compiler/encoders/riscv/proofs                        9m31s   1GB
Feb 10 11:05:14 Starting compiler/encoders/ag32/proofs
Feb 10 11:08:02 Finished compiler/encoders/ag32/proofs                         2m48s 722MB
Feb 10 11:08:02 Starting compiler/backend/x64/proofs
Feb 10 11:08:31 Finished compiler/backend/x64/proofs                             28s   1GB
Feb 10 11:08:31 Starting compiler/backend/arm7/proofs
Feb 10 11:09:01 Finished compiler/backend/arm7/proofs                            29s   1GB
Feb 10 11:09:01 Starting compiler/backend/arm8/proofs
Feb 10 11:09:30 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 10 11:09:30 Starting compiler/backend/mips/proofs
Feb 10 11:09:59 Finished compiler/backend/mips/proofs                            28s   1GB
Feb 10 11:09:59 Starting compiler/backend/riscv/proofs
Feb 10 11:10:27 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 10 11:10:27 Starting compiler/backend/ag32/proofs
Feb 10 11:24:18 Finished compiler/backend/ag32/proofs                         13m50s   2GB
Feb 10 11:24:18 Starting compiler/proofs
Feb 10 11:26:39 Finished compiler/proofs                                       2m20s   4GB
Feb 10 11:26:39 Starting candle/set-theory
Feb 10 11:27:09 Finished candle/set-theory                                       29s 865MB
Feb 10 11:27:09 Starting candle/syntax-lib
Feb 10 11:27:21 Finished candle/syntax-lib                                       11s 743MB
Feb 10 11:27:21 Starting candle/standard/syntax
Feb 10 11:29:16 Finished candle/standard/syntax                                1m55s 961MB
Feb 10 11:29:16 Starting candle/standard/semantics
Feb 10 11:31:09 Finished candle/standard/semantics                             1m52s   1GB
Feb 10 11:31:09 Starting candle/standard/monadic
Feb 10 11:32:54 Finished candle/standard/monadic                               1m44s   1GB
Feb 10 11:32:54 Starting candle/standard/ml_kernel
Feb 10 11:40:08 Finished candle/standard/ml_kernel                             7m14s   3GB
Feb 10 11:40:08 Starting candle/overloading/syntax
Feb 10 11:43:28 Finished candle/overloading/syntax                             3m19s   1GB
Feb 10 11:43:28 Starting candle/overloading/semantics
Feb 10 11:55:54 Finished candle/overloading/semantics                         12m25s   2GB
Feb 10 11:55:54 Starting candle/prover
Feb 10 12:03:56 Finished candle/prover                                         8m01s   2GB
Feb 10 12:03:56 Starting pancake
Feb 10 12:06:47 Finished pancake                                               2m50s   2GB
Feb 10 12:06:47 Starting pancake/ffi
Feb 10 12:06:48 Finished pancake/ffi                                              0s  21MB
Feb 10 12:06:48 Starting pancake/semantics
Feb 10 12:09:31 Finished pancake/semantics                                     2m42s   1GB
Feb 10 12:09:31 Starting pancake/proofs
Feb 10 12:22:33 Finished pancake/proofs                                       13m01s   5GB
Feb 10 12:22:33 Starting characteristic/examples
Feb 10 12:24:01 Finished characteristic/examples                               1m27s   3GB
Feb 10 12:24:01 Starting tutorial/solutions
Feb 10 12:41:06 Finished tutorial/solutions                                   17m04s  10GB
Feb 10 12:41:06 Starting translator/monadic/examples
Feb 10 12:44:45 Finished translator/monadic/examples                           3m38s   2GB
Feb 10 12:44:46 Starting examples
Feb 10 12:55:22 Finished examples                                             10m36s   4GB
Feb 10 12:55:23 Starting examples/compilation/x64
Feb 10 15:30:34 Finished examples/compilation/x64                           2h35m10s  18GB
Feb 10 15:30:34 Starting examples/compilation/x64/proofs
Feb 10 15:33:11 Finished examples/compilation/x64/proofs                       2m36s   3GB
Feb 10 15:33:11 Starting examples/compilation/ag32
Feb 10 16:08:56 Finished examples/compilation/ag32                            35m44s   9GB
Feb 10 16:08:56 Starting examples/compilation/ag32/proofs
Feb 10 16:09:54 Finished examples/compilation/ag32/proofs                        57s   2GB
Feb 10 16:09:54 Starting examples/cost
Feb 10 17:11:51 Finished examples/cost                                      1h01m56s   8GB
Feb 10 17:11:51 Starting examples/lpr_checker
Feb 10 17:12:46 Finished examples/lpr_checker                                    54s 664MB
Feb 10 17:12:46 Starting examples/lpr_checker/array
Feb 10 17:44:03 Finished examples/lpr_checker/array                           31m16s   5GB
Feb 10 17:44:03 Starting examples/lpr_checker/array/compilation
Feb 10 19:12:18 Finished examples/lpr_checker/array/compilation             1h28m12s  37GB
Feb 10 19:12:18 Starting examples/lpr_checker/array/compilation/proofs
Feb 10 19:14:18 Finished examples/lpr_checker/array/compilation/proofs         2m00s   4GB
Feb 10 19:14:18 Starting examples/opentheory
Feb 10 19:20:06 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                                                       (20s)     OK
Starting work on readerTheory
readerTheory                                                       (54s)     OK
Starting work on reader_initTheory
reader_initTheory                                                  (25s)     OK
Starting work on readerProofTheory
readerProofTheory                                                  (67s)     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]
 Adding nsLookup representation thms for [reader_commonProg_env_79]
 error in quse /home/cake/oven/regression/cakeml-1763/examples/opentheory/reader_commonProgScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1763/examples/opentheory/reader_commonProgScript : Fail "Static Errors"
 Saved theorem _______ "obj_t_v_thm"
 /home/cake/oven/regression/cakeml-1763/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"