Job 2460

CakeML:561f8adc336449adea9eb250a3bc9436c0f390de
  Fix source_let [Jul 16 14:32:49]
#1014 (source_let-fix)
Merging into:1791142331ecadf0de62e3834aa2785ffbd51f8b
  Make a theorem name unambiguous [Jul 17 09:29:17]
HOL:c37de731916a5fe5fdc6218d4b2e19234435e4ce
  Add lots of regexp matching regression tests for DBSearchParser [Jul 15 06:13:45]
Machine:lammmington

Jul 18 03:41:20 Claimed job
Jul 18 03:41:29 Building HOL
Jul 18 03:55:53 Starting developers
Jul 18 03:55:56 Finished developers                                               2s 212MB
Jul 18 03:55:57 Starting developers/bin
Jul 18 03:56:07 Finished developers/bin                                           9s   1GB
Jul 18 03:56:08 Starting compiler/proofs
Jul 18 05:52:09 Finished compiler/proofs                                    1h55m59s  25GB
Jul 18 05:52:10 Starting compiler/bootstrap/translation
Jul 18 14:04:54 Finished compiler/bootstrap/translation                     8h12m43s  50GB
Jul 18 14:04:55 Starting semantics/ffi
Jul 18 14:05:03 Finished semantics/ffi                                            7s 617MB
Jul 18 14:05:04 Starting semantics
Jul 18 14:05:06 Finished semantics                                                0s  69MB
Jul 18 14:05:07 Starting semantics/proofs
Jul 18 14:05:45 Finished semantics/proofs                                        37s   2GB
Jul 18 14:05:46 Starting semantics/alt_semantics
Jul 18 14:06:27 Finished semantics/alt_semantics                                 40s   1GB
Jul 18 14:06:28 Starting semantics/alt_semantics/proofs
Jul 18 14:17:32 Finished semantics/alt_semantics/proofs                       11m02s   3GB
Jul 18 14:17:32 Starting basis/pure
Jul 18 14:17:34 Finished basis/pure                                               0s  70MB
Jul 18 14:17:35 Starting translator
Jul 18 14:19:24 Finished translator                                            1m48s   4GB
Jul 18 14:19:25 Starting compiler/parsing
Jul 18 14:19:26 Finished compiler/parsing                                         0s  74MB
Jul 18 14:19:27 Starting characteristic
Jul 18 14:19:29 Finished characteristic                                           0s  89MB
Jul 18 14:19:30 Starting translator/monadic
Jul 18 14:19:31 Finished translator/monadic                                       0s  97MB
Jul 18 14:19:32 Starting basis
Jul 18 14:23:07 Finished basis                                                 3m33s   5GB
Jul 18 14:23:08 Starting compiler/inference
Jul 18 14:23:09 Finished compiler/inference                                       0s 101MB
Jul 18 14:23:10 Starting compiler/backend/reg_alloc
Jul 18 14:23:11 Finished compiler/backend/reg_alloc                               0s  70MB
Jul 18 14:23:12 Starting compiler/backend/gc
Jul 18 14:23:14 Finished compiler/backend/gc                                      0s 139MB
Jul 18 14:23:15 Starting compiler/backend
Jul 18 14:23:35 Finished compiler/backend                                        19s   1GB
Jul 18 14:23:36 Starting compiler/encoders/asm
Jul 18 14:23:37 Finished compiler/encoders/asm                                    0s  89MB
Jul 18 14:23:38 Starting compiler/encoders/x64
Jul 18 14:23:40 Finished compiler/encoders/x64                                    0s 101MB
Jul 18 14:23:41 Starting compiler/encoders/arm7
Jul 18 14:23:42 Finished compiler/encoders/arm7                                   0s 101MB
Jul 18 14:23:43 Starting compiler/encoders/arm8
Jul 18 14:23:44 Finished compiler/encoders/arm8                                   0s 101MB
Jul 18 14:23:45 Starting compiler/encoders/arm8_asl
Jul 18 16:47:42 Finished compiler/encoders/arm8_asl                         2h23m55s  37GB
Jul 18 16:47:42 Starting compiler/encoders/mips
Jul 18 16:47:44 Finished compiler/encoders/mips                                   0s 100MB
Jul 18 16:47:45 Starting compiler/encoders/riscv
Jul 18 16:47:46 Finished compiler/encoders/riscv                                  0s 102MB
Jul 18 16:47:47 Starting compiler/encoders/ag32
Jul 18 16:47:49 Finished compiler/encoders/ag32                                   0s  99MB
Jul 18 16:47:49 Starting compiler/backend/x64
Jul 18 16:47:51 Finished compiler/backend/x64                                     0s 142MB
Jul 18 16:47:52 Starting compiler/backend/arm7
Jul 18 16:47:54 Finished compiler/backend/arm7                                    0s 142MB
Jul 18 16:47:55 Starting compiler/backend/arm8
Jul 18 16:47:57 Finished compiler/backend/arm8                                    0s 142MB
Jul 18 16:47:57 Starting compiler/backend/mips
Jul 18 16:47:59 Finished compiler/backend/mips                                    0s 142MB
Jul 18 16:48:00 Starting compiler/backend/riscv
Jul 18 16:48:02 Finished compiler/backend/riscv                                   0s 142MB
Jul 18 16:48:03 Starting compiler/backend/ag32
Jul 18 16:49:22 Finished compiler/backend/ag32                                 1m18s   2GB
Jul 18 16:49:23 Starting compiler/parsing/proofs
Jul 18 16:49:24 Finished compiler/parsing/proofs                                  0s  73MB
Jul 18 16:49:25 Starting compiler/inference/proofs
Jul 18 16:49:27 Finished compiler/inference/proofs                                0s  99MB
Jul 18 16:49:28 Starting compiler/backend/semantics
Jul 18 16:53:11 Finished compiler/backend/semantics                            3m42s   3GB
Jul 18 16:53:12 Starting compiler/backend/reg_alloc/proofs
Jul 18 16:53:14 Finished compiler/backend/reg_alloc/proofs                        0s  92MB
Jul 18 16:53:15 Starting compiler/backend/proofs
Jul 18 16:54:19 Finished compiler/backend/proofs                               1m03s   3GB
Jul 18 16:54:20 Starting compiler/backend/serialiser
Jul 18 16:54:22 Finished compiler/backend/serialiser                              0s 145MB
Jul 18 16:54:22 Starting compiler/encoders/x64/proofs
Jul 18 17:03:54 Finished compiler/encoders/x64/proofs                          9m30s   5GB
Jul 18 17:03:55 Starting compiler/encoders/arm7/proofs
Jul 18 17:16:39 Finished compiler/encoders/arm7/proofs                        12m43s   8GB
Jul 18 17:16:40 Starting compiler/encoders/arm8/proofs
Jul 18 17:23:13 Finished compiler/encoders/arm8/proofs                         6m31s   4GB
Jul 18 17:23:13 Starting compiler/encoders/arm8_asl/proofs
Jul 18 18:11:00 Finished compiler/encoders/arm8_asl/proofs                    47m45s  12GB
Jul 18 18:11:01 Starting compiler/encoders/mips/proofs
Jul 18 18:21:10 Finished compiler/encoders/mips/proofs                        10m07s   7GB
Jul 18 18:21:11 Starting compiler/encoders/riscv/proofs
Jul 18 18:29:35 Finished compiler/encoders/riscv/proofs                        8m23s   5GB
Jul 18 18:29:36 Starting compiler/encoders/ag32/proofs
Jul 18 18:31:58 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Jul 18 18:31:59 Starting compiler/backend/x64/proofs
Jul 18 18:32:41 Finished compiler/backend/x64/proofs                             41s   3GB
Jul 18 18:32:42 Starting compiler/backend/arm7/proofs
Jul 18 18:33:33 Finished compiler/backend/arm7/proofs                            49s   3GB
Jul 18 18:33:34 Starting compiler/backend/arm8/proofs
Jul 18 18:34:16 Finished compiler/backend/arm8/proofs                            41s   3GB
Jul 18 18:34:17 Starting compiler/backend/arm8_asl
Jul 18 18:34:46 Finished compiler/backend/arm8_asl                               28s   2GB
Jul 18 18:34:47 Starting compiler/backend/mips/proofs
Jul 18 18:35:32 Finished compiler/backend/mips/proofs                            44s   3GB
Jul 18 18:35:33 Starting compiler/backend/riscv/proofs
Jul 18 18:36:25 Finished compiler/backend/riscv/proofs                           50s   4GB
Jul 18 18:36:26 Starting compiler/backend/ag32/proofs
Jul 18 18:50:31 Finished compiler/backend/ag32/proofs                         14m04s   6GB
Jul 18 18:50:32 Starting compiler/backend/cv_compute
Jul 18 18:52:17 Finished compiler/backend/cv_compute                           1m44s   3GB
Jul 18 18:52:18 Starting cv_translator
Jul 18 18:52:52 FAILED: cv_translator
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/num/theories/cv_compute/automation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/algebra/base[0m
Scanning [1m$(HOLDIR)/src/algebra/construction[0m
Scanning [1m$(HOLDIR)/src/algebra[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[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$(CAKEMLDIR)/compiler/backend/serialiser[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[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$(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$(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/cv_compute[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanned 79 directories
Starting work on README.md
Starting work on to_data_cvTheory
README.md                                                           (0s)     OK
to_data_cvTheory                                                   (27s)FAIL<1>
                 v0.
                   v = SOME v0 
                   v0' v1'. v0 = (... ,... )  source_let_compile_decs_pre v1) 
          source_let_compile_decs_pre v) 
     v. source_let_compile_decs_pre v
 
 Stopping. Use cv_trans_pre instead (or one of its variants).
 error in quse /scratch/cakeml/regression2/cakeml-2460/cv_translator/to_data_cvScript.sml : HOL_ERR {message = "Could not prove a precondition.", origin_function = "failwith", origin_structure = "??"}
 error in load /scratch/cakeml/regression2/cakeml-2460/cv_translator/to_data_cvScript : HOL_ERR {message = "Could not prove a precondition.", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "Could not prove a precondition.", origin_function = "failwith", origin_structure = "??"}