Job 1497

CakeML:dc4cad21d9c06f65824bd7807d0a5e6c2447e406
  Hash input strings in reader [Mar 20 12:35:12]
#821 (opentheory-improve)
Merging into:9c2de3ee5f524d70e727448b250ce0f8f085ee53
  Merge pull request #820 from CakeML/fix-export-x64-macos [Mar 22 20:43:15]
HOL:2ab294231cc2a57bf1ffcea47cb232709fa51797
  Remove old debugging code that is not used anymore [Mar 18 22:56:26]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Mar 22 20:57:25 Claimed job
Mar 22 20:57:29 Building HOL
Mar 22 21:12:00 Starting developers
Mar 22 21:12:01 Finished developers                                               0s  35MB
Mar 22 21:12:01 Starting developers/bin
Mar 22 21:12:07 Finished developers/bin                                           5s   1GB
Mar 22 21:12:07 Starting semantics/ffi
Mar 22 21:12:17 Finished semantics/ffi                                           10s 298MB
Mar 22 21:12:17 Starting semantics
Mar 22 21:13:49 Finished semantics                                             1m31s   1GB
Mar 22 21:13:49 Starting semantics/proofs
Mar 22 21:17:09 Finished semantics/proofs                                      3m19s   2GB
Mar 22 21:17:09 Starting semantics/alt_semantics
Mar 22 21:17:17 Finished semantics/alt_semantics                                  7s 413MB
Mar 22 21:17:18 Starting semantics/alt_semantics/proofs
Mar 22 21:19:25 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Mar 22 21:19:25 Starting basis/pure
Mar 22 21:22:09 Finished basis/pure                                            2m44s   1GB
Mar 22 21:22:10 Starting translator
Mar 22 21:24:45 Finished translator                                            2m35s   2GB
Mar 22 21:24:45 Starting compiler/parsing
Mar 22 21:25:50 Finished compiler/parsing                                      1m05s   3GB
Mar 22 21:25:51 Starting characteristic
Mar 22 21:31:51 Finished characteristic                                        6m00s   3GB
Mar 22 21:31:51 Starting translator/monadic
Mar 22 21:33:39 Finished translator/monadic                                    1m47s   3GB
Mar 22 21:33:39 Starting basis
Mar 22 22:17:10 Finished basis                                                43m30s  24GB
Mar 22 22:17:10 Starting compiler/inference
Mar 22 22:18:17 Finished compiler/inference                                    1m06s   2GB
Mar 22 22:18:17 Starting compiler/backend/reg_alloc
Mar 22 22:19:24 Finished compiler/backend/reg_alloc                            1m06s   1GB
Mar 22 22:19:24 Starting compiler/backend/gc
Mar 22 22:22:57 Finished compiler/backend/gc                                   3m32s   3GB
Mar 22 22:22:57 Starting compiler/backend
Mar 22 22:27:56 Finished compiler/backend                                      4m58s   5GB
Mar 22 22:27:56 Starting compiler/encoders/asm
Mar 22 22:28:18 Finished compiler/encoders/asm                                   21s 967MB
Mar 22 22:28:18 Starting compiler/encoders/x64
Mar 22 22:29:21 Finished compiler/encoders/x64                                 1m02s   1GB
Mar 22 22:29:21 Starting compiler/encoders/arm7
Mar 22 22:31:22 Finished compiler/encoders/arm7                                2m00s   1GB
Mar 22 22:31:23 Starting compiler/encoders/arm8
Mar 22 22:32:01 Finished compiler/encoders/arm8                                  38s   1GB
Mar 22 22:32:01 Starting compiler/encoders/mips
Mar 22 22:33:26 Finished compiler/encoders/mips                                1m24s   1GB
Mar 22 22:33:26 Starting compiler/encoders/riscv
Mar 22 22:35:02 Finished compiler/encoders/riscv                               1m36s   1GB
Mar 22 22:35:02 Starting compiler/encoders/ag32
Mar 22 22:35:22 Finished compiler/encoders/ag32                                  18s 922MB
Mar 22 22:35:22 Starting compiler/backend/x64
Mar 22 22:35:41 Finished compiler/backend/x64                                    18s   1GB
Mar 22 22:35:41 Starting compiler/backend/arm7
Mar 22 22:36:03 Finished compiler/backend/arm7                                   21s   1GB
Mar 22 22:36:03 Starting compiler/backend/arm8
Mar 22 22:36:23 Finished compiler/backend/arm8                                   19s   1GB
Mar 22 22:36:23 Starting compiler/backend/mips
Mar 22 22:36:43 Finished compiler/backend/mips                                   19s   1GB
Mar 22 22:36:43 Starting compiler/backend/riscv
Mar 22 22:37:03 Finished compiler/backend/riscv                                  20s   1GB
Mar 22 22:37:03 Starting compiler/backend/ag32
Mar 22 22:38:14 Finished compiler/backend/ag32                                 1m10s   2GB
Mar 22 22:38:14 Starting compiler/parsing/proofs
Mar 22 22:43:41 Finished compiler/parsing/proofs                               5m27s   2GB
Mar 22 22:43:41 Starting compiler/inference/proofs
Mar 22 22:46:11 Finished compiler/inference/proofs                             2m29s   2GB
Mar 22 22:46:11 Starting compiler/backend/semantics
Mar 22 23:13:03 Finished compiler/backend/semantics                           26m51s   5GB
Mar 22 23:13:03 Starting compiler/backend/reg_alloc/proofs
Mar 22 23:16:20 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Mar 22 23:16:20 Starting compiler/backend/proofs
Mar 23 00:09:44 Finished compiler/backend/proofs                              53m23s  31GB
Mar 23 00:09:45 Starting compiler/encoders/x64/proofs
Mar 23 00:19:17 Finished compiler/encoders/x64/proofs                          9m32s   5GB
Mar 23 00:19:17 Starting compiler/encoders/arm7/proofs
Mar 23 00:31:59 Finished compiler/encoders/arm7/proofs                        12m41s   7GB
Mar 23 00:31:59 Starting compiler/encoders/arm8/proofs
Mar 23 00:38:20 Finished compiler/encoders/arm8/proofs                         6m21s   2GB
Mar 23 00:38:20 Starting compiler/encoders/mips/proofs
Mar 23 00:48:00 Finished compiler/encoders/mips/proofs                         9m39s   5GB
Mar 23 00:48:00 Starting compiler/encoders/riscv/proofs
Mar 23 00:56:13 Finished compiler/encoders/riscv/proofs                        8m12s   3GB
Mar 23 00:56:14 Starting compiler/encoders/ag32/proofs
Mar 23 00:58:34 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 23 00:58:34 Starting compiler/backend/x64/proofs
Mar 23 00:58:57 Finished compiler/backend/x64/proofs                             22s   1GB
Mar 23 00:58:58 Starting compiler/backend/arm7/proofs
Mar 23 00:59:21 Finished compiler/backend/arm7/proofs                            22s   1GB
Mar 23 00:59:21 Starting compiler/backend/arm8/proofs
Mar 23 00:59:41 Finished compiler/backend/arm8/proofs                            20s   1GB
Mar 23 00:59:41 Starting compiler/backend/mips/proofs
Mar 23 01:00:02 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 23 01:00:03 Starting compiler/backend/riscv/proofs
Mar 23 01:00:26 Finished compiler/backend/riscv/proofs                           23s   2GB
Mar 23 01:00:26 Starting compiler/backend/ag32/proofs
Mar 23 01:12:38 Finished compiler/backend/ag32/proofs                         12m10s   4GB
Mar 23 01:12:38 Starting compiler/proofs
Mar 23 01:14:34 Finished compiler/proofs                                       1m55s   6GB
Mar 23 01:14:34 Starting candle/set-theory
Mar 23 01:15:04 Finished candle/set-theory                                       29s   1GB
Mar 23 01:15:04 Starting candle/syntax-lib
Mar 23 01:15:15 Finished candle/syntax-lib                                       10s 792MB
Mar 23 01:15:15 Starting candle/standard/syntax
Mar 23 01:17:05 Finished candle/standard/syntax                                1m50s   1GB
Mar 23 01:17:06 Starting candle/standard/semantics
Mar 23 01:18:52 Finished candle/standard/semantics                             1m46s   2GB
Mar 23 01:18:52 Starting candle/standard/monadic
Mar 23 01:20:32 Finished candle/standard/monadic                               1m39s   1GB
Mar 23 01:20:32 Starting candle/standard/ml_kernel
Mar 23 01:25:45 Finished candle/standard/ml_kernel                             5m12s   5GB
Mar 23 01:25:45 Starting candle/overloading/syntax
Mar 23 01:28:57 Finished candle/overloading/syntax                             3m11s   1GB
Mar 23 01:28:57 Starting candle/overloading/semantics
Mar 23 01:41:01 Finished candle/overloading/semantics                         12m03s   7GB
Mar 23 01:41:01 Starting characteristic/examples
Mar 23 01:42:18 Finished characteristic/examples                               1m16s   4GB
Mar 23 01:42:18 Starting tutorial/solutions
Mar 23 01:57:26 Finished tutorial/solutions                                   15m08s  16GB
Mar 23 01:57:27 Starting translator/monadic/examples
Mar 23 02:00:47 Finished translator/monadic/examples                           3m20s   3GB
Mar 23 02:00:47 Starting examples
Mar 23 02:09:12 Finished examples                                              8m25s   6GB
Mar 23 02:09:12 Starting examples/compilation/x64
Mar 23 04:29:23 Finished examples/compilation/x64                           2h20m10s  38GB
Mar 23 04:29:23 Starting examples/compilation/x64/proofs
Mar 23 04:31:17 Finished examples/compilation/x64/proofs                       1m53s   3GB
Mar 23 04:31:17 Starting examples/compilation/ag32
Mar 23 05:04:29 Finished examples/compilation/ag32                            33m11s  13GB
Mar 23 05:04:29 Starting examples/compilation/ag32/proofs
Mar 23 05:05:22 Finished examples/compilation/ag32/proofs                        52s   4GB
Mar 23 05:05:22 Starting examples/cost
Mar 23 05:59:07 Finished examples/cost                                        53m41s  12GB
Mar 23 05:59:08 Starting examples/lpr_checker
Mar 23 06:02:53 Finished examples/lpr_checker                                  3m44s   3GB
Mar 23 06:02:53 Starting examples/lpr_checker/compilation
Mar 23 06:21:10 Finished examples/lpr_checker/compilation                     18m16s  21GB
Mar 23 06:21:10 Starting examples/lpr_checker/compilation/proofs
Mar 23 06:21:53 Finished examples/lpr_checker/compilation/proofs                 42s   4GB
Mar 23 06:21:53 Starting examples/lpr_checker/array
Mar 23 06:35:38 Finished examples/lpr_checker/array                           13m44s   5GB
Mar 23 06:35:38 Starting examples/lpr_checker/array/compilation
Mar 23 06:54:45 Finished examples/lpr_checker/array/compilation               19m06s  16GB
Mar 23 06:54:45 Starting examples/lpr_checker/array/compilation/proofs
Mar 23 06:55:35 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Mar 23 06:55:36 Starting examples/opentheory
Mar 23 06:59:10 FAILED: examples/opentheory
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)/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/lem_lib_stub[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
Starting work on prettyTheory
prettyTheory           real:   20s  user:   19s     OK
Starting work on readerTheory
readerTheory           real:   53s  user:   50s     OK
Starting work on reader_initTheory
reader_initTheory      real:   22s  user:   21s     OK
Starting work on readerProofTheory
readerProofTheory      real:   60s  user:   59s     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory  real:   17s  user:   16s     OK
...er_commonProgTheory real:   56s  user:   53sFAIL<1>
 Translating pp_tyop_aux
 Saved theorem _____ "nsLookup_reader_commonProg_env_12_pfun_eqs"
 Adding nsLookup representation thms for [reader_commonProg_env_11, reader_commonProg_env_10]
 Adding nsLookup representation thms for [reader_commonProg_env_12]
 Saved theorem _____ "pp_tyop_aux_v_thm"
 /home/myreen/regression/cakeml-1497/examples/opentheory/reader_commonProgScript.sml:41: error: Value or constructor (pp_tyop_def) has not been declared
 Found near translate pp_tyop_def
 error in quse /home/myreen/regression/cakeml-1497/examples/opentheory/reader_commonProgScript.sml : Fail "Static Errors"
 error in load /home/myreen/regression/cakeml-1497/examples/opentheory/reader_commonProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"