Job 1181

CakeML:30780b5e487d5486f9570c3ed4a9b92bed92de1d
  Fixups for inference and compute lib [Feb 10 12:52:58]
#724 (constrain_op_case)
Merging into:658771300986c1238e414b06f1443f7f4f08424a
  Merge pull request #723 from talsewell/explorer-data [Feb 11 23:28:15]
HOL:bbc6f9a1dc624543ead89ce3c72e7a8d773e37db
  Added BOREL_INDUCT (was: Induct_on_Borel_functions) [Feb 09 23:16:11]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 12 16:00:02 Claimed job
Feb 12 16:00:08 Building HOL
Feb 12 16:12:21 Starting developers
Feb 12 16:12:25 Finished developers                                               3s  91MB
Feb 12 16:12:25 Starting developers/bin
Feb 12 16:14:10 Finished developers/bin                                        1m44s   1GB
Feb 12 16:14:10 Starting semantics/ffi
Feb 12 16:14:20 Finished semantics/ffi                                           10s 243MB
Feb 12 16:14:21 Starting semantics
Feb 12 16:15:53 Finished semantics                                             1m31s   1GB
Feb 12 16:15:53 Starting semantics/proofs
Feb 12 16:19:21 Finished semantics/proofs                                      3m27s   1GB
Feb 12 16:19:21 Starting semantics/alt_semantics
Feb 12 16:19:30 Finished semantics/alt_semantics                                  8s 271MB
Feb 12 16:19:30 Starting semantics/alt_semantics/proofs
Feb 12 16:21:40 Finished semantics/alt_semantics/proofs                        2m09s   1GB
Feb 12 16:21:40 Starting basis/pure
Feb 12 16:24:47 Finished basis/pure                                            3m06s 718MB
Feb 12 16:24:47 Starting translator
Feb 12 16:27:25 Finished translator                                            2m38s   1GB
Feb 12 16:27:26 Starting compiler/parsing
Feb 12 16:28:39 Finished compiler/parsing                                      1m12s   1GB
Feb 12 16:28:39 Starting characteristic
Feb 12 16:34:36 Finished characteristic                                        5m56s   1GB
Feb 12 16:34:36 Starting translator/monadic
Feb 12 16:36:13 Finished translator/monadic                                    1m36s   1GB
Feb 12 16:36:14 Starting basis
Feb 12 17:11:19 Finished basis                                                35m05s  18GB
Feb 12 17:11:20 Starting compiler/inference
Feb 12 17:12:29 Finished compiler/inference                                    1m09s   1GB
Feb 12 17:12:30 Starting compiler/backend/reg_alloc
Feb 12 17:13:32 Finished compiler/backend/reg_alloc                            1m01s   1GB
Feb 12 17:13:32 Starting compiler/backend/gc
Feb 12 17:17:02 Finished compiler/backend/gc                                   3m29s   2GB
Feb 12 17:17:02 Starting compiler/backend
Feb 12 17:21:34 Finished compiler/backend                                      4m31s   2GB
Feb 12 17:21:35 Starting compiler/encoders/asm
Feb 12 17:21:57 Finished compiler/encoders/asm                                   21s 810MB
Feb 12 17:21:57 Starting compiler/encoders/x64
Feb 12 17:22:56 Finished compiler/encoders/x64                                   58s 950MB
Feb 12 17:22:56 Starting compiler/encoders/arm7
Feb 12 17:24:43 Finished compiler/encoders/arm7                                1m46s   1GB
Feb 12 17:24:43 Starting compiler/encoders/arm8
Feb 12 17:25:17 Finished compiler/encoders/arm8                                  34s 810MB
Feb 12 17:25:17 Starting compiler/encoders/mips
Feb 12 17:26:29 Finished compiler/encoders/mips                                1m11s   1GB
Feb 12 17:26:30 Starting compiler/encoders/riscv
Feb 12 17:27:57 Finished compiler/encoders/riscv                               1m26s   1GB
Feb 12 17:27:57 Starting compiler/encoders/ag32
Feb 12 17:28:15 Finished compiler/encoders/ag32                                  17s 796MB
Feb 12 17:28:15 Starting compiler/backend/x64
Feb 12 17:28:33 Finished compiler/backend/x64                                    18s   1GB
Feb 12 17:28:34 Starting compiler/backend/arm7
Feb 12 17:28:53 Finished compiler/backend/arm7                                   19s   1GB
Feb 12 17:28:53 Starting compiler/backend/arm8
Feb 12 17:29:12 Finished compiler/backend/arm8                                   18s   1GB
Feb 12 17:29:12 Starting compiler/backend/mips
Feb 12 17:29:30 Finished compiler/backend/mips                                   17s 863MB
Feb 12 17:29:30 Starting compiler/backend/riscv
Feb 12 17:29:50 Finished compiler/backend/riscv                                  19s   1GB
Feb 12 17:29:50 Starting compiler/backend/ag32
Feb 12 17:31:02 Finished compiler/backend/ag32                                 1m11s   1GB
Feb 12 17:31:02 Starting compiler/parsing/proofs
Feb 12 17:36:58 Finished compiler/parsing/proofs                               5m55s 822MB
Feb 12 17:36:58 Starting compiler/inference/proofs
Feb 12 17:39:30 Finished compiler/inference/proofs                             2m31s   1GB
Feb 12 17:39:30 Starting compiler/backend/semantics
Feb 12 18:10:07 Finished compiler/backend/semantics                           30m36s   2GB
Feb 12 18:10:07 Starting compiler/backend/reg_alloc/proofs
Feb 12 18:13:48 Finished compiler/backend/reg_alloc/proofs                     3m40s 899MB
Feb 12 18:13:49 Starting compiler/backend/proofs
Feb 12 19:20:50 Finished compiler/backend/proofs                            1h07m01s  15GB
Feb 12 19:20:51 Starting compiler/encoders/x64/proofs
Feb 12 19:30:47 Finished compiler/encoders/x64/proofs                          9m56s   4GB
Feb 12 19:30:47 Starting compiler/encoders/arm7/proofs
Feb 12 19:44:05 Finished compiler/encoders/arm7/proofs                        13m17s   3GB
Feb 12 19:44:05 Starting compiler/encoders/arm8/proofs
Feb 12 19:50:47 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Feb 12 19:50:47 Starting compiler/encoders/mips/proofs
Feb 12 20:00:39 Finished compiler/encoders/mips/proofs                         9m51s   2GB
Feb 12 20:00:39 Starting compiler/encoders/riscv/proofs
Feb 12 20:09:36 Finished compiler/encoders/riscv/proofs                        8m56s   1GB
Feb 12 20:09:37 Starting compiler/encoders/ag32/proofs
Feb 12 20:12:17 Finished compiler/encoders/ag32/proofs                         2m40s 635MB
Feb 12 20:12:17 Starting compiler/backend/x64/proofs
Feb 12 20:12:39 Finished compiler/backend/x64/proofs                             21s 800MB
Feb 12 20:12:40 Starting compiler/backend/arm7/proofs
Feb 12 20:13:01 Finished compiler/backend/arm7/proofs                            21s   1GB
Feb 12 20:13:01 Starting compiler/backend/arm8/proofs
Feb 12 20:13:21 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 12 20:13:22 Starting compiler/backend/mips/proofs
Feb 12 20:13:43 Finished compiler/backend/mips/proofs                            20s   1GB
Feb 12 20:13:43 Starting compiler/backend/riscv/proofs
Feb 12 20:14:04 Finished compiler/backend/riscv/proofs                           20s   1GB
Feb 12 20:14:04 Starting compiler/backend/ag32/proofs
Feb 12 20:27:19 Finished compiler/backend/ag32/proofs                         13m14s   3GB
Feb 12 20:27:19 Starting compiler/proofs
Feb 13 14:51:03 Resuming compiler/proofs
Feb 13 14:52:36 Finished compiler/proofs                                       1m33s   3GB
Feb 13 14:52:37 Starting candle/set-theory
Feb 13 14:53:06 Finished candle/set-theory                                       28s 807MB
Feb 13 14:53:06 Starting candle/syntax-lib
Feb 13 14:53:16 Finished candle/syntax-lib                                       10s 645MB
Feb 13 14:53:16 Starting candle/standard/syntax
Feb 13 14:55:06 Finished candle/standard/syntax                                1m49s 841MB
Feb 13 14:55:06 Starting candle/standard/semantics
Feb 13 14:56:52 Finished candle/standard/semantics                             1m45s 961MB
Feb 13 14:56:52 Starting candle/standard/monadic
Feb 13 14:58:34 Finished candle/standard/monadic                               1m41s   1GB
Feb 13 14:58:34 Starting candle/standard/ml_kernel
Feb 13 15:03:57 Finished candle/standard/ml_kernel                             5m22s   5GB
Feb 13 15:03:58 Starting candle/standard/opentheory
Feb 13 15:13:52 Finished candle/standard/opentheory                            9m53s   4GB
Feb 13 15:13:52 Starting candle/standard/opentheory/compilation
Feb 13 15:45:11 Finished candle/standard/opentheory/compilation               31m18s  21GB
Feb 13 15:45:11 Starting candle/standard/opentheory/compilation/proofs
Feb 13 15:45:50 Finished candle/standard/opentheory/compilation/proofs           38s   2GB
Feb 13 15:45:50 Starting characteristic/examples
Feb 13 15:47:22 Finished characteristic/examples                               1m32s   2GB
Feb 13 15:47:22 Starting tutorial/solutions
Feb 13 16:02:13 Finished tutorial/solutions                                   14m49s   8GB
Feb 13 16:02:13 Starting translator/monadic/examples
Feb 13 16:05:14 Finished translator/monadic/examples                           3m00s   2GB
Feb 13 16:05:14 Starting examples
Feb 13 16:14:58 Finished examples                                              9m44s   4GB
Feb 13 16:14:59 Starting examples/compilation/x64
Feb 13 18:31:17 Finished examples/compilation/x64                           2h16m17s  14GB
Feb 13 18:31:17 Starting examples/compilation/x64/proofs
Feb 13 18:33:00 Finished examples/compilation/x64/proofs                       1m42s   2GB
Feb 13 18:33:00 Starting examples/compilation/ag32
Feb 13 19:04:33 Finished examples/compilation/ag32                            31m33s   6GB
Feb 13 19:04:33 Starting examples/compilation/ag32/proofs
Feb 13 19:05:19 Finished examples/compilation/ag32/proofs                        45s   3GB
Feb 13 19:05:20 Starting examples/cost
Feb 13 19:49:01 Finished examples/cost                                        43m39s   6GB
Feb 13 19:49:01 Starting examples/lpr_checker
Feb 13 19:52:56 Finished examples/lpr_checker                                  3m54s   2GB
Feb 13 19:52:57 Starting examples/lpr_checker/compilation
Feb 13 20:10:01 Finished examples/lpr_checker/compilation                     17m03s   7GB
Feb 13 20:10:01 Starting examples/lpr_checker/compilation/proofs
Feb 13 20:10:40 Finished examples/lpr_checker/compilation/proofs                 38s   2GB
Feb 13 20:10:40 Starting examples/lpr_checker/array
Feb 13 20:20:30 Finished examples/lpr_checker/array                            9m49s   2GB
Feb 13 20:20:30 Starting examples/lpr_checker/array/compilation
Feb 13 20:36:20 Finished examples/lpr_checker/array/compilation               15m49s   9GB
Feb 13 20:36:20 Starting examples/lpr_checker/array/compilation/proofs
Feb 13 20:37:03 Finished examples/lpr_checker/array/compilation/proofs           43s   3GB
Feb 13 20:37:04 Starting translator/okasaki-examples
Feb 13 20:41:27 Finished translator/okasaki-examples                           4m23s   1GB
Feb 13 20:41:27 Starting translator/other-examples
Feb 13 20:43:31 Finished translator/other-examples                             2m02s   1GB
Feb 13 20:43:31 Starting compiler/parsing/tests
Feb 13 20:43:57 Finished compiler/parsing/tests                                  25s 655MB
Feb 13 20:43:57 Starting compiler/inference/tests
Feb 13 20:48:32 Finished compiler/inference/tests                              4m34s   4GB
Feb 13 20:48:33 Starting compiler/bootstrap/translation
Feb 13 22:02:03 FAILED: compiler/bootstrap/translation
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[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/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[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/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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$(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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Starting work on monadic_encTheory
Starting work on README.md
Starting work on to_flatProgTheory
README.md                                       real:    0s  user:    0s     OK
monadic_encTheory                               real:    9s  user:    9s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                             real:   14s  user:   13s     OK
monadic_enc64Theory                             real:   14s  user:   13s     OK
to_flatProgTheory                               real:  449s  user:  441s     OK
Starting work on to_closProgTheory
to_closProgTheory                               real:  466s  user:  459s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                real:  383s  user:  375s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                real:  323s  user:  315s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                               real:  170s  user:  167s     OK
Starting work on lexerProgTheory
lexerProgTheory                                 real:  279s  user:  275s     OK
Starting work on parserProgTheory
parserProgTheory                                real:  514s  user:  503s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                             real:  955s  user:  943s     OK
Starting work on inferProgTheory
inferProgTheory                                 real:  866s  user:  856sFAIL<1>
 Saved theorem _____ "check_ctor_tenv_v_thm"
 Translating is_value
 Saved theorem _____ "nsLookup_inferProg_env_84_pfun_eqs"
 Adding nsLookup representation thms for [inferProg_env_84]
 Saved theorem _____ "is_value_v_thm"
 error in quse /home/cake/oven/regression/cakeml-1181/compiler/bootstrap/translation/inferProgScript.sml : HOL_ERR {message = "at line 560, character 4:\nDon't expect to find a of in this position after a (\non line 561, characters 16-17 and at line 560, character 4.\n", origin_function = "Absyn", origin_structure = "Absyn"}
 error in load /home/cake/oven/regression/cakeml-1181/compiler/bootstrap/translation/inferProgScript : HOL_ERR {message = "at line 560, character 4:\nDon't expect to find a of in this position after a (\non line 561, characters 16-17 and at line 560, character 4.\n", origin_function = "Absyn", origin_structure = "Absyn"}
 Don't expect to find a of in this position after a (
 on line 561, characters 16-17 and at line 560, character 4.
 Uncaught exception: HOL_ERR {message = "at line 560, character 4:\nDon't expect to find a of in this position after a (\non line 561, characters 16-17 and at line 560, character 4.\n", origin_function = "Absyn", origin_structure = "Absyn"}