Job 1184

CakeML:30780b5e487d5486f9570c3ed4a9b92bed92de1d
  Fixups for inference and compute lib [Feb 10 12:52:58]
#724 (constrain_op_case)
Merging into:ed66b67fb3e2faf1ea517dff415c277cad73c8dc
  Merge pull request #714 from CakeML/nopacklib [Feb 16 18:25:28]
HOL:bbc6f9a1dc624543ead89ce3c72e7a8d773e37db
  Added BOREL_INDUCT (was: Induct_on_Borel_functions) [Feb 09 23:16:11]
Machine:oven3 4.19.67.1.amd64-smp

Feb 16 18:27:51 Claimed job
Feb 16 18:28:00 Building HOL
Feb 16 18:52:42 Starting developers
Feb 16 18:52:49 Finished developers                                               7s 130MB
Feb 16 18:52:50 Starting developers/bin
Feb 16 18:53:05 Finished developers/bin                                          15s   1GB
Feb 16 18:53:05 Starting semantics/ffi
Feb 16 18:53:28 Finished semantics/ffi                                           22s 251MB
Feb 16 18:53:29 Starting semantics
Feb 16 18:56:31 Finished semantics                                             3m01s   1GB
Feb 16 18:56:31 Starting semantics/proofs
Feb 16 19:03:31 Finished semantics/proofs                                      6m59s   1GB
Feb 16 19:03:31 Starting semantics/alt_semantics
Feb 16 19:03:50 Finished semantics/alt_semantics                                 18s 309MB
Feb 16 19:03:50 Starting semantics/alt_semantics/proofs
Feb 16 19:08:09 Finished semantics/alt_semantics/proofs                        4m18s   1GB
Feb 16 19:08:09 Starting basis/pure
Feb 16 19:14:10 Finished basis/pure                                            6m00s 867MB
Feb 16 19:14:10 Starting translator
Feb 16 19:19:28 Finished translator                                            5m18s   1GB
Feb 16 19:19:29 Starting compiler/parsing
Feb 16 19:21:52 Finished compiler/parsing                                      2m23s   3GB
Feb 16 19:21:52 Starting characteristic
Feb 16 19:33:59 Finished characteristic                                       12m06s   1GB
Feb 16 19:33:59 Starting translator/monadic
Feb 16 19:37:17 Finished translator/monadic                                    3m17s   1GB
Feb 16 19:37:17 Starting basis
Feb 16 20:42:32 Finished basis                                              1h05m12s  21GB
Feb 16 20:42:32 Starting compiler/inference
Feb 16 20:44:55 Finished compiler/inference                                    2m22s   1GB
Feb 16 20:44:55 Starting compiler/backend/reg_alloc
Feb 16 20:46:48 Finished compiler/backend/reg_alloc                            1m53s   1GB
Feb 16 20:46:49 Starting compiler/backend/gc
Feb 16 20:53:16 Finished compiler/backend/gc                                   6m27s   2GB
Feb 16 20:53:16 Starting compiler/backend
Feb 16 21:01:31 Finished compiler/backend                                      8m14s   2GB
Feb 16 21:01:31 Starting compiler/encoders/asm
Feb 16 21:02:16 Finished compiler/encoders/asm                                   44s 763MB
Feb 16 21:02:16 Starting compiler/encoders/x64
Feb 16 21:04:19 Finished compiler/encoders/x64                                 2m03s 984MB
Feb 16 21:04:19 Starting compiler/encoders/arm7
Feb 16 21:08:03 Finished compiler/encoders/arm7                                3m43s   1GB
Feb 16 21:08:03 Starting compiler/encoders/arm8
Feb 16 21:09:15 Finished compiler/encoders/arm8                                1m11s 636MB
Feb 16 21:09:15 Starting compiler/encoders/mips
Feb 16 21:11:45 Finished compiler/encoders/mips                                2m29s 927MB
Feb 16 21:11:45 Starting compiler/encoders/riscv
Feb 16 21:14:42 Finished compiler/encoders/riscv                               2m57s 880MB
Feb 16 21:14:42 Starting compiler/encoders/ag32
Feb 16 21:15:19 Finished compiler/encoders/ag32                                  36s 656MB
Feb 16 21:15:19 Starting compiler/backend/x64
Feb 16 21:15:58 Finished compiler/backend/x64                                    39s   1GB
Feb 16 21:15:58 Starting compiler/backend/arm7
Feb 16 21:16:40 Finished compiler/backend/arm7                                   41s   1GB
Feb 16 21:16:41 Starting compiler/backend/arm8
Feb 16 21:17:20 Finished compiler/backend/arm8                                   39s   1GB
Feb 16 21:17:21 Starting compiler/backend/mips
Feb 16 21:17:58 Finished compiler/backend/mips                                   37s   1GB
Feb 16 21:17:59 Starting compiler/backend/riscv
Feb 16 21:18:39 Finished compiler/backend/riscv                                  39s   1GB
Feb 16 21:18:39 Starting compiler/backend/ag32
Feb 16 21:20:57 Finished compiler/backend/ag32                                 2m17s   1GB
Feb 16 21:20:57 Starting compiler/parsing/proofs
Feb 16 21:33:06 Finished compiler/parsing/proofs                              12m08s   1GB
Feb 16 21:33:06 Starting compiler/inference/proofs
Feb 16 21:38:16 Finished compiler/inference/proofs                             5m09s   1GB
Feb 16 21:38:16 Starting compiler/backend/semantics
Feb 16 22:34:49 Finished compiler/backend/semantics                           56m31s   2GB
Feb 16 22:34:49 Starting compiler/backend/reg_alloc/proofs
Feb 16 22:42:04 Finished compiler/backend/reg_alloc/proofs                     7m14s 950MB
Feb 16 22:42:04 Starting compiler/backend/proofs
Feb 17 00:43:12 Finished compiler/backend/proofs                            2h01m07s  25GB
Feb 17 00:43:12 Starting compiler/encoders/x64/proofs
Feb 17 01:03:13 Finished compiler/encoders/x64/proofs                         20m01s   4GB
Feb 17 01:03:13 Starting compiler/encoders/arm7/proofs
Feb 17 01:32:00 Finished compiler/encoders/arm7/proofs                        28m46s   3GB
Feb 17 01:32:01 Starting compiler/encoders/arm8/proofs
Feb 17 01:46:10 Finished compiler/encoders/arm8/proofs                        14m09s   1GB
Feb 17 01:46:10 Starting compiler/encoders/mips/proofs
Feb 17 02:07:37 Finished compiler/encoders/mips/proofs                        21m26s   2GB
Feb 17 02:07:38 Starting compiler/encoders/riscv/proofs
Feb 17 02:26:08 Finished compiler/encoders/riscv/proofs                       18m30s   1GB
Feb 17 02:26:08 Starting compiler/encoders/ag32/proofs
Feb 17 02:31:30 Finished compiler/encoders/ag32/proofs                         5m21s 807MB
Feb 17 02:31:30 Starting compiler/backend/x64/proofs
Feb 17 02:32:12 Finished compiler/backend/x64/proofs                             41s 866MB
Feb 17 02:32:12 Starting compiler/backend/arm7/proofs
Feb 17 02:32:57 Finished compiler/backend/arm7/proofs                            45s   1GB
Feb 17 02:32:58 Starting compiler/backend/arm8/proofs
Feb 17 02:33:36 Finished compiler/backend/arm8/proofs                            38s   1GB
Feb 17 02:33:37 Starting compiler/backend/mips/proofs
Feb 17 02:34:26 Finished compiler/backend/mips/proofs                            48s   1GB
Feb 17 02:34:26 Starting compiler/backend/riscv/proofs
Feb 17 02:35:09 Finished compiler/backend/riscv/proofs                           42s   1GB
Feb 17 02:35:09 Starting compiler/backend/ag32/proofs
Feb 17 03:02:24 Finished compiler/backend/ag32/proofs                         27m13s   2GB
Feb 17 03:02:24 Starting compiler/proofs
Feb 17 03:06:01 Finished compiler/proofs                                       3m37s   3GB
Feb 17 03:06:01 Starting candle/set-theory
Feb 17 03:06:57 Finished candle/set-theory                                       55s 973MB
Feb 17 03:06:57 Starting candle/syntax-lib
Feb 17 03:07:20 Finished candle/syntax-lib                                       22s 638MB
Feb 17 03:07:21 Starting candle/standard/syntax
Feb 17 03:11:03 Finished candle/standard/syntax                                3m42s   1GB
Feb 17 03:11:03 Starting candle/standard/semantics
Feb 17 03:14:44 Finished candle/standard/semantics                             3m40s   1GB
Feb 17 03:14:44 Starting candle/standard/monadic
Feb 17 03:18:09 Finished candle/standard/monadic                               3m24s   1GB
Feb 17 03:18:09 Starting candle/standard/ml_kernel
Feb 17 03:28:54 Finished candle/standard/ml_kernel                            10m45s   3GB
Feb 17 03:28:55 Starting candle/standard/opentheory
Feb 17 03:47:47 Finished candle/standard/opentheory                           18m51s   3GB
Feb 17 03:47:47 Starting candle/standard/opentheory/compilation
Feb 17 04:51:53 Finished candle/standard/opentheory/compilation             1h04m05s  16GB
Feb 17 04:51:53 Starting candle/standard/opentheory/compilation/proofs
Feb 17 04:53:09 Finished candle/standard/opentheory/compilation/proofs         1m15s   3GB
Feb 17 04:53:10 Starting characteristic/examples
Feb 17 04:55:45 Finished characteristic/examples                               2m34s   2GB
Feb 17 04:55:45 Starting tutorial/solutions
Feb 17 05:26:05 Finished tutorial/solutions                                   30m20s   7GB
Feb 17 05:26:05 Starting translator/monadic/examples
Feb 17 05:31:14 Finished translator/monadic/examples                           5m08s   2GB
Feb 17 05:31:15 Starting examples
Feb 17 05:45:36 Finished examples                                             14m20s   5GB
Feb 17 05:45:36 Starting examples/compilation/x64
Feb 17 10:34:02 Finished examples/compilation/x64                           4h48m26s  14GB
Feb 17 10:34:03 Starting examples/compilation/x64/proofs
Feb 17 10:36:52 Finished examples/compilation/x64/proofs                       2m49s   3GB
Feb 17 10:36:53 Starting examples/compilation/ag32
Feb 17 11:41:25 Finished examples/compilation/ag32                          1h04m31s   7GB
Feb 17 11:41:25 Starting examples/compilation/ag32/proofs
Feb 17 11:42:57 Finished examples/compilation/ag32/proofs                      1m31s   3GB
Feb 17 11:42:57 Starting examples/cost
Feb 17 13:07:52 Finished examples/cost                                      1h24m53s   7GB
Feb 17 13:07:52 Starting examples/lpr_checker
Feb 17 13:15:42 Finished examples/lpr_checker                                  7m49s   3GB
Feb 17 13:15:43 Starting examples/lpr_checker/compilation
Feb 17 13:47:10 Finished examples/lpr_checker/compilation                     31m27s  12GB
Feb 17 13:47:10 Starting examples/lpr_checker/compilation/proofs
Feb 17 13:48:18 Finished examples/lpr_checker/compilation/proofs               1m07s   2GB
Feb 17 13:48:19 Starting examples/lpr_checker/array
Feb 17 14:05:02 Finished examples/lpr_checker/array                           16m42s   3GB
Feb 17 14:05:02 Starting examples/lpr_checker/array/compilation
Feb 17 14:37:44 Finished examples/lpr_checker/array/compilation               32m39s   9GB
Feb 17 14:37:44 Starting examples/lpr_checker/array/compilation/proofs
Feb 17 14:39:06 Finished examples/lpr_checker/array/compilation/proofs         1m21s   3GB
Feb 17 14:39:06 Starting translator/okasaki-examples
Feb 17 14:47:38 Finished translator/okasaki-examples                           8m31s   1GB
Feb 17 14:47:38 Starting translator/other-examples
Feb 17 14:51:07 Finished translator/other-examples                             3m28s   1GB
Feb 17 14:51:07 Starting compiler/parsing/tests
Feb 17 14:52:06 Finished compiler/parsing/tests                                  58s 681MB
Feb 17 14:52:06 Starting compiler/inference/tests
Feb 17 15:00:42 Finished compiler/inference/tests                              8m35s   3GB
Feb 17 15:00:42 Starting compiler/bootstrap/translation
Feb 17 17:24:05 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:   22s  user:   20s     OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                                                                                                                                          real:   26s  user:   24s     OK
monadic_enc64Theory                                                                                                                                          real:   26s  user:   25s     OK
to_flatProgTheory                                                                                                                                            real:  840s  user:  823s     OK
Starting work on to_closProgTheory
to_closProgTheory                                                                                                                                            real:  849s  user:  833s     OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                                                                                                                             real:  769s  user:  748s     OK
Starting work on to_bviProgTheory
to_bviProgTheory                                                                                                                                             real:  651s  user:  632s     OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                                            real:  363s  user:  352s     OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                                              real:  553s  user:  536s     OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                                             real: 1008s  user:  980s     OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                                                                          real: 1804s  user: 1757s     OK
Starting work on inferProgTheory
inferProgTheory                                                                                                                                              real: 1758s  user: 1715sFAIL<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 /root/regression/cakeml-1184/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 /root/regression/cakeml-1184/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"}