Job 1500

CakeML:a37eb54205c6e4b652a2b9da806582a92d8b2375
  Don't translate definition that doesn't exist [Mar 23 10:26:43]
#821 (opentheory-improve)
Merging into:9c2de3ee5f524d70e727448b250ce0f8f085ee53
  Merge pull request #820 from CakeML/fix-export-x64-macos [Mar 22 20:43:15]
HOL:ab03cec5200c8b23f9ba60c5cea958cfcd0cd158
  Make all string overloads "inferior" [Mar 23 06:14:09]
Machine:oven3 4.19.67.1.amd64-smp

Mar 25 10:32:40 Claimed job
Mar 25 10:32:51 Building HOL
Mar 25 11:06:06 Starting developers
Mar 25 11:06:14 Finished developers                                               7s 128MB
Mar 25 11:06:14 Starting developers/bin
Mar 25 11:06:27 Finished developers/bin                                          12s   1GB
Mar 25 11:06:27 Starting semantics/ffi
Mar 25 11:06:52 Finished semantics/ffi                                           24s 281MB
Mar 25 11:06:52 Starting semantics
Mar 25 11:10:01 Finished semantics                                             3m08s 944MB
Mar 25 11:10:01 Starting semantics/proofs
Mar 25 11:17:41 Finished semantics/proofs                                      7m39s   1GB
Mar 25 11:17:41 Starting semantics/alt_semantics
Mar 25 11:18:02 Finished semantics/alt_semantics                                 21s 328MB
Mar 25 11:18:03 Starting semantics/alt_semantics/proofs
Mar 25 11:22:38 Finished semantics/alt_semantics/proofs                        4m35s 876MB
Mar 25 11:22:38 Starting basis/pure
Mar 25 11:28:42 Finished basis/pure                                            6m03s 883MB
Mar 25 11:28:42 Starting translator
Mar 25 11:34:18 Finished translator                                            5m35s   1GB
Mar 25 11:34:18 Starting compiler/parsing
Mar 25 11:36:46 Finished compiler/parsing                                      2m27s   2GB
Mar 25 11:36:46 Starting characteristic
Mar 25 11:49:21 Finished characteristic                                       12m34s   1GB
Mar 25 11:49:21 Starting translator/monadic
Mar 25 11:52:47 Finished translator/monadic                                    3m26s   1GB
Mar 25 11:52:48 Starting basis
Mar 25 13:25:44 Finished basis                                              1h32m56s  17GB
Mar 25 13:25:45 Starting compiler/inference
Mar 25 13:28:14 Finished compiler/inference                                    2m28s   1GB
Mar 25 13:28:14 Starting compiler/backend/reg_alloc
Mar 25 13:30:15 Finished compiler/backend/reg_alloc                            2m00s   1GB
Mar 25 13:30:15 Starting compiler/backend/gc
Mar 25 13:37:06 Finished compiler/backend/gc                                   6m50s   3GB
Mar 25 13:37:06 Starting compiler/backend
Mar 25 13:46:37 Finished compiler/backend                                      9m30s   3GB
Mar 25 13:46:37 Starting compiler/encoders/asm
Mar 25 13:47:25 Finished compiler/encoders/asm                                   48s 797MB
Mar 25 13:47:26 Starting compiler/encoders/x64
Mar 25 13:49:42 Finished compiler/encoders/x64                                 2m16s 854MB
Mar 25 13:49:42 Starting compiler/encoders/arm7
Mar 25 13:54:11 Finished compiler/encoders/arm7                                4m28s   1GB
Mar 25 13:54:11 Starting compiler/encoders/arm8
Mar 25 13:55:35 Finished compiler/encoders/arm8                                1m23s 604MB
Mar 25 13:55:35 Starting compiler/encoders/mips
Mar 25 13:58:50 Finished compiler/encoders/mips                                3m14s 986MB
Mar 25 13:58:50 Starting compiler/encoders/riscv
Mar 25 14:02:28 Finished compiler/encoders/riscv                               3m38s 900MB
Mar 25 14:02:29 Starting compiler/encoders/ag32
Mar 25 14:03:07 Finished compiler/encoders/ag32                                  37s 631MB
Mar 25 14:03:07 Starting compiler/backend/x64
Mar 25 14:03:48 Finished compiler/backend/x64                                    40s   1GB
Mar 25 14:03:48 Starting compiler/backend/arm7
Mar 25 14:04:33 Finished compiler/backend/arm7                                   45s   1GB
Mar 25 14:04:33 Starting compiler/backend/arm8
Mar 25 14:05:15 Finished compiler/backend/arm8                                   41s   1GB
Mar 25 14:05:15 Starting compiler/backend/mips
Mar 25 14:05:56 Finished compiler/backend/mips                                   40s   1GB
Mar 25 14:05:56 Starting compiler/backend/riscv
Mar 25 14:06:40 Finished compiler/backend/riscv                                  43s   1GB
Mar 25 14:06:40 Starting compiler/backend/ag32
Mar 25 14:09:05 Finished compiler/backend/ag32                                 2m24s   1GB
Mar 25 14:09:05 Starting compiler/parsing/proofs
Mar 25 14:21:10 Finished compiler/parsing/proofs                              12m04s 953MB
Mar 25 14:21:10 Starting compiler/inference/proofs
Mar 25 14:26:36 Finished compiler/inference/proofs                             5m25s   1GB
Mar 25 14:26:37 Starting compiler/backend/semantics
Mar 25 15:28:45 Finished compiler/backend/semantics                         1h02m06s   2GB
Mar 25 15:28:45 Starting compiler/backend/reg_alloc/proofs
Mar 25 15:36:22 Finished compiler/backend/reg_alloc/proofs                     7m36s 923MB
Mar 25 15:36:23 Starting compiler/backend/proofs
Mar 25 17:16:55 Finished compiler/backend/proofs                            1h40m30s  16GB
Mar 25 17:16:56 Starting compiler/encoders/x64/proofs
Mar 25 17:38:27 Finished compiler/encoders/x64/proofs                         21m31s   4GB
Mar 25 17:38:27 Starting compiler/encoders/arm7/proofs
Mar 25 18:08:30 Finished compiler/encoders/arm7/proofs                        30m02s   3GB
Mar 25 18:08:30 Starting compiler/encoders/arm8/proofs
Mar 25 18:23:31 Finished compiler/encoders/arm8/proofs                        15m00s   1GB
Mar 25 18:23:32 Starting compiler/encoders/mips/proofs
Mar 25 18:46:13 Finished compiler/encoders/mips/proofs                        22m40s   2GB
Mar 25 18:46:13 Starting compiler/encoders/riscv/proofs
Mar 25 19:06:50 Finished compiler/encoders/riscv/proofs                       20m36s   1GB
Mar 25 19:06:50 Starting compiler/encoders/ag32/proofs
Mar 25 19:12:34 Finished compiler/encoders/ag32/proofs                         5m43s 836MB
Mar 25 19:12:34 Starting compiler/backend/x64/proofs
Mar 25 19:13:21 Finished compiler/backend/x64/proofs                             46s   1GB
Mar 25 19:13:21 Starting compiler/backend/arm7/proofs
Mar 25 19:14:08 Finished compiler/backend/arm7/proofs                            47s   1GB
Mar 25 19:14:09 Starting compiler/backend/arm8/proofs
Mar 25 19:14:54 Finished compiler/backend/arm8/proofs                            44s   1GB
Mar 25 19:14:54 Starting compiler/backend/mips/proofs
Mar 25 19:15:41 Finished compiler/backend/mips/proofs                            46s   1GB
Mar 25 19:15:41 Starting compiler/backend/riscv/proofs
Mar 25 19:16:27 Finished compiler/backend/riscv/proofs                           45s   1GB
Mar 25 19:16:27 Starting compiler/backend/ag32/proofs
Mar 25 19:44:50 Finished compiler/backend/ag32/proofs                         28m22s   2GB
Mar 25 19:44:51 Starting compiler/proofs
Mar 25 19:48:49 Finished compiler/proofs                                       3m57s   3GB
Mar 25 19:48:49 Starting candle/set-theory
Mar 25 19:49:48 Finished candle/set-theory                                       58s 845MB
Mar 25 19:49:48 Starting candle/syntax-lib
Mar 25 19:50:12 Finished candle/syntax-lib                                       23s 662MB
Mar 25 19:50:12 Starting candle/standard/syntax
Mar 25 19:54:05 Finished candle/standard/syntax                                3m52s   1GB
Mar 25 19:54:05 Starting candle/standard/semantics
Mar 25 19:57:56 Finished candle/standard/semantics                             3m50s   1GB
Mar 25 19:57:56 Starting candle/standard/monadic
Mar 25 20:01:34 Finished candle/standard/monadic                               3m37s   1GB
Mar 25 20:01:35 Starting candle/standard/ml_kernel
Mar 25 20:13:15 Finished candle/standard/ml_kernel                            11m39s   3GB
Mar 25 20:13:15 Starting candle/overloading/syntax
Mar 25 20:19:53 Finished candle/overloading/syntax                             6m37s   1GB
Mar 25 20:19:53 Starting candle/overloading/semantics
Mar 25 20:46:17 Finished candle/overloading/semantics                         26m23s   4GB
Mar 25 20:46:18 Starting characteristic/examples
Mar 25 20:49:02 Finished characteristic/examples                               2m44s   3GB
Mar 25 20:49:03 Starting tutorial/solutions
Mar 25 21:22:57 Finished tutorial/solutions                                   33m53s   8GB
Mar 25 21:22:57 Starting translator/monadic/examples
Mar 25 21:28:32 Finished translator/monadic/examples                           5m34s   2GB
Mar 25 21:28:32 Starting examples
Mar 25 21:43:50 Finished examples                                             15m17s   3GB
Mar 25 21:43:50 Starting examples/compilation/x64
Mar 26 02:56:28 Finished examples/compilation/x64                           5h12m37s  17GB
Mar 26 02:56:29 Starting examples/compilation/x64/proofs
Mar 26 02:59:51 Finished examples/compilation/x64/proofs                       3m21s   3GB
Mar 26 02:59:51 Starting examples/compilation/ag32
Mar 26 04:13:37 Finished examples/compilation/ag32                          1h13m45s   7GB
Mar 26 04:13:38 Starting examples/compilation/ag32/proofs
Mar 26 04:15:18 Finished examples/compilation/ag32/proofs                      1m39s   3GB
Mar 26 04:15:18 Starting examples/cost
Mar 26 06:04:26 Finished examples/cost                                      1h49m04s   7GB
Mar 26 06:04:26 Starting examples/lpr_checker
Mar 26 06:12:50 Finished examples/lpr_checker                                  8m24s   4GB
Mar 26 06:12:51 Starting examples/lpr_checker/compilation
Mar 26 06:47:27 Finished examples/lpr_checker/compilation                     34m36s  16GB
Mar 26 06:47:27 Starting examples/lpr_checker/compilation/proofs
Mar 26 06:48:53 Finished examples/lpr_checker/compilation/proofs               1m25s   2GB
Mar 26 06:48:54 Starting examples/lpr_checker/array
Mar 26 07:21:07 Finished examples/lpr_checker/array                           32m13s   4GB
Mar 26 07:21:08 Starting examples/lpr_checker/array/compilation
Mar 26 08:02:59 Finished examples/lpr_checker/array/compilation               41m50s  14GB
Mar 26 08:02:59 Starting examples/lpr_checker/array/compilation/proofs
Mar 26 08:04:42 Finished examples/lpr_checker/array/compilation/proofs         1m42s   4GB
Mar 26 08:04:42 Starting examples/opentheory
Mar 26 08:24:54 Finished examples/opentheory                                  20m11s   5GB
Mar 26 08:24:55 Starting examples/opentheory
Mar 26 08:24:57 Finished examples/opentheory                                      2s  33MB
Mar 26 08:24:57 Starting examples/opentheory/compilation
Mar 26 09:32:18 Finished examples/opentheory/compilation                    1h07m20s  17GB
Mar 26 09:32:18 Starting examples/opentheory/compilation/proofs
Mar 26 09:33:44 Finished examples/opentheory/compilation/proofs                1m25s   4GB
Mar 26 09:33:44 Starting examples/opentheory/compilation/ag32
Mar 26 10:44:12 Finished examples/opentheory/compilation/ag32               1h10m27s  17GB
Mar 26 10:44:13 Starting examples/opentheory/compilation/ag32/proofs
Mar 26 10:46:11 FAILED: examples/opentheory/compilation/ag32/proofs
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$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32/proofs[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
Scanning [1m$(CAKEMLDIR)/examples/opentheory[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples/opentheory/compilation/ag32[0m
Starting work on README.md
Starting work on readerProgProofTheory
README.md                                                                                                                                                    real:    0s  user:    0s     OK
readerProgProofTheory                                                                                                                                        real:  114s  user:  108sFAIL<1>
 <<HOL message: Created theory "readerProgProof">>
 Saved theorem _____ "target_state_rel_reader_start_asm_state"
 Saved theorem _____ "reader_installed"
 Saved theorem _____ "reader_machine_sem"
 error in quse /root/regression/cakeml-1500/examples/opentheory/compilation/ag32/proofs/readerProgProofScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load /root/regression/cakeml-1500/examples/opentheory/compilation/ag32/proofs/readerProgProofScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}