Job 1496

CakeML:f7df7312a404dff6f94d3f4f510eec5b63d08646
  Fix sum example and make progress on lcg [Feb 08 17:58:50]
#811 (eval)
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:oven3 4.19.67.1.amd64-smp

Mar 22 20:47:20 Claimed job
Mar 22 20:47:31 Building HOL
Mar 22 21:20:51 Starting developers
Mar 22 21:20:59 Finished developers                                               7s  92MB
Mar 22 21:20:59 Starting developers/bin
Mar 22 21:21:12 Finished developers/bin                                          12s   1GB
Mar 22 21:21:13 Starting semantics/ffi
Mar 22 21:21:37 Finished semantics/ffi                                           24s 275MB
Mar 22 21:21:38 Starting semantics
Mar 22 21:24:47 Finished semantics                                             3m09s   1GB
Mar 22 21:24:48 Starting semantics/proofs
Mar 22 21:32:53 Finished semantics/proofs                                      8m05s   1GB
Mar 22 21:32:54 Starting basis/pure
Mar 22 21:38:53 Finished basis/pure                                            5m59s 776MB
Mar 22 21:38:53 Starting translator
Mar 22 21:45:37 Finished translator                                            6m43s   1GB
Mar 22 21:45:37 Starting compiler/parsing
Mar 22 21:48:08 Finished compiler/parsing                                      2m30s   2GB
Mar 22 21:48:08 Starting characteristic
Mar 22 22:00:11 Finished characteristic                                       12m02s   2GB
Mar 22 22:00:12 Starting translator/monadic
Mar 22 22:03:41 Finished translator/monadic                                    3m29s   1GB
Mar 22 22:03:41 Starting basis
Mar 22 23:38:20 Finished basis                                              1h34m37s  19GB
Mar 22 23:38:20 Starting compiler/inference
Mar 22 23:41:04 Finished compiler/inference                                    2m43s   1GB
Mar 22 23:41:05 Starting compiler/backend/reg_alloc
Mar 22 23:43:13 Finished compiler/backend/reg_alloc                            2m07s   1GB
Mar 22 23:43:13 Starting compiler/backend/gc
Mar 22 23:50:03 Finished compiler/backend/gc                                   6m49s   2GB
Mar 22 23:50:03 Starting compiler/backend
Mar 22 23:59:39 Finished compiler/backend                                      9m35s   4GB
Mar 22 23:59:39 Starting compiler/encoders/asm
Mar 23 00:00:27 Finished compiler/encoders/asm                                   47s 729MB
Mar 23 00:00:27 Starting compiler/encoders/x64
Mar 23 00:02:48 Finished compiler/encoders/x64                                 2m20s 753MB
Mar 23 00:02:49 Starting compiler/encoders/arm7
Mar 23 00:07:18 Finished compiler/encoders/arm7                                4m28s   1GB
Mar 23 00:07:18 Starting compiler/encoders/arm8
Mar 23 00:08:45 Finished compiler/encoders/arm8                                1m27s 943MB
Mar 23 00:08:46 Starting compiler/encoders/mips
Mar 23 00:12:00 Finished compiler/encoders/mips                                3m13s 880MB
Mar 23 00:12:00 Starting compiler/encoders/riscv
Mar 23 00:15:34 Finished compiler/encoders/riscv                               3m33s   1GB
Mar 23 00:15:34 Starting compiler/encoders/ag32
Mar 23 00:16:13 Finished compiler/encoders/ag32                                  38s 783MB
Mar 23 00:16:13 Starting compiler/backend/x64
Mar 23 00:16:55 Finished compiler/backend/x64                                    41s   1GB
Mar 23 00:16:55 Starting compiler/backend/arm7
Mar 23 00:17:39 Finished compiler/backend/arm7                                   43s   1GB
Mar 23 00:17:40 Starting compiler/backend/arm8
Mar 23 00:18:22 Finished compiler/backend/arm8                                   42s   1GB
Mar 23 00:18:22 Starting compiler/backend/mips
Mar 23 00:19:05 Finished compiler/backend/mips                                   42s   1GB
Mar 23 00:19:06 Starting compiler/backend/riscv
Mar 23 00:19:51 Finished compiler/backend/riscv                                  45s   1GB
Mar 23 00:19:52 Starting compiler/backend/ag32
Mar 23 00:22:16 Finished compiler/backend/ag32                                 2m24s   1GB
Mar 23 00:22:17 Starting compiler/parsing/proofs
Mar 23 00:35:02 Finished compiler/parsing/proofs                              12m45s   1GB
Mar 23 00:35:02 Starting compiler/inference/proofs
Mar 23 00:40:30 Finished compiler/inference/proofs                             5m25s   1GB
Mar 23 00:40:30 Starting compiler/backend/semantics
Mar 23 01:40:08 Finished compiler/backend/semantics                           59m37s   2GB
Mar 23 01:40:08 Starting compiler/backend/reg_alloc/proofs
Mar 23 01:47:48 Finished compiler/backend/reg_alloc/proofs                     7m38s 971MB
Mar 23 01:47:48 Starting compiler/backend/proofs
Mar 23 03:30:05 Finished compiler/backend/proofs                            1h42m16s  24GB
Mar 23 03:30:05 Starting compiler/encoders/x64/proofs
Mar 23 03:51:40 Finished compiler/encoders/x64/proofs                         21m34s   4GB
Mar 23 03:51:40 Starting compiler/encoders/arm7/proofs
Mar 23 04:22:36 Finished compiler/encoders/arm7/proofs                        30m55s   3GB
Mar 23 04:22:37 Starting compiler/encoders/arm8/proofs
Mar 23 04:37:39 Finished compiler/encoders/arm8/proofs                        15m02s   1GB
Mar 23 04:37:40 Starting compiler/encoders/mips/proofs
Mar 23 05:00:16 Finished compiler/encoders/mips/proofs                        22m35s   2GB
Mar 23 05:00:16 Starting compiler/encoders/riscv/proofs
Mar 23 05:20:19 Finished compiler/encoders/riscv/proofs                       20m02s   1GB
Mar 23 05:20:19 Starting compiler/encoders/ag32/proofs
Mar 23 05:26:04 Finished compiler/encoders/ag32/proofs                         5m45s 882MB
Mar 23 05:26:04 Starting compiler/backend/x64/proofs
Mar 23 05:26:52 Finished compiler/backend/x64/proofs                             46s   1GB
Mar 23 05:26:52 Starting compiler/backend/arm7/proofs
Mar 23 05:27:45 Finished compiler/backend/arm7/proofs                            53s   1GB
Mar 23 05:27:45 Starting compiler/backend/arm8/proofs
Mar 23 05:28:32 Finished compiler/backend/arm8/proofs                            46s   1GB
Mar 23 05:28:33 Starting compiler/backend/mips/proofs
Mar 23 05:29:22 Finished compiler/backend/mips/proofs                            49s   1GB
Mar 23 05:29:22 Starting compiler/backend/riscv/proofs
Mar 23 05:30:13 Finished compiler/backend/riscv/proofs                           50s   1GB
Mar 23 05:30:13 Starting compiler/backend/ag32/proofs
Mar 23 05:58:08 Finished compiler/backend/ag32/proofs                         27m54s   2GB
Mar 23 05:58:08 Starting compiler/proofs
Mar 23 06:02:14 Finished compiler/proofs                                       4m05s   5GB
Mar 23 06:02:14 Starting candle/set-theory
Mar 23 06:03:14 Finished candle/set-theory                                       59s 762MB
Mar 23 06:03:14 Starting candle/syntax-lib
Mar 23 06:03:37 Finished candle/syntax-lib                                       23s 732MB
Mar 23 06:03:37 Starting candle/standard/syntax
Mar 23 06:07:40 Finished candle/standard/syntax                                4m01s   1GB
Mar 23 06:07:40 Starting candle/standard/semantics
Mar 23 06:11:38 Finished candle/standard/semantics                             3m57s   1GB
Mar 23 06:11:38 Starting candle/standard/monadic
Mar 23 06:15:17 Finished candle/standard/monadic                               3m38s   1GB
Mar 23 06:15:17 Starting candle/standard/ml_kernel
Mar 23 06:27:30 Finished candle/standard/ml_kernel                            12m11s   4GB
Mar 23 06:27:30 Starting candle/overloading/syntax
Mar 23 06:34:12 Finished candle/overloading/syntax                             6m41s   1GB
Mar 23 06:34:12 Starting candle/overloading/semantics
Mar 23 07:01:04 Finished candle/overloading/semantics                         26m51s   3GB
Mar 23 07:01:04 Starting characteristic/examples
Mar 23 07:03:54 Finished characteristic/examples                               2m49s   2GB
Mar 23 07:03:54 Starting tutorial/solutions
Mar 23 07:39:22 Finished tutorial/solutions                                   35m28s   7GB
Mar 23 07:39:23 Starting translator/monadic/examples
Mar 23 07:45:02 Finished translator/monadic/examples                           5m39s   2GB
Mar 23 07:45:02 Starting examples
Mar 23 08:00:31 Finished examples                                             15m28s   3GB
Mar 23 08:00:31 Starting examples/compilation/x64
Mar 23 13:24:21 Finished examples/compilation/x64                           5h23m49s  17GB
Mar 23 13:24:21 Starting examples/compilation/x64/proofs
Mar 23 13:27:53 Finished examples/compilation/x64/proofs                       3m31s   3GB
Mar 23 13:27:53 Starting examples/compilation/ag32
Mar 23 14:44:18 Finished examples/compilation/ag32                          1h16m24s   7GB
Mar 23 14:44:19 Starting examples/compilation/ag32/proofs
Mar 23 14:45:58 Finished examples/compilation/ag32/proofs                      1m39s   4GB
Mar 23 14:45:58 Starting examples/cost
Mar 23 15:12:02 FAILED: examples/cost
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/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/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/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)/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$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Starting work on README.md
Starting work on costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
README.md                                                                                                                                                    real:    0s  user:    0s     OK
miniBasisProgTheory                                                                                                                                          real:   55s  user:   52s     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                                                                                                                                           real:   56s  user:   54s     OK
costPropsTheory                                                                                                                                              real:  181s  user:  174s     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                                                                                                            real: 1160s  user: 1235s     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                                                                                                                                           real: 1117s  user: 1174s     OK
Starting work on pureLoopProofTheory
allProgTheory                                                                                                                                                real: 1145s  user: 1201s     OK
Starting work on allProofTheory
pureLoopProofTheory                                                                                                                                          real:  258s  user:  249sFAIL<1>
           <|row := 1; col := 41; offset := 0|>)
        [("pureLoop","x",App Opapp [Var (Short "pureLoop"); Var (Short "x")])];
      Dlet
        (Locs <|row := 2; col := 4; offset := 0|>
           <|row := 2; col := 21; offset := 0|>) Pany
        (App Opapp [Var (Short "pureLoop"); Lit (IntLit 1)])] (1000,1000)
 
 failed.
 Failed to prove theorem data_safe_pureLoop.
 Uncaught exception: HOL_ERR {message = "No matching sub-term found", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
cyesProgTheory                                                                                                                                                                       M-KILLED
lcgLoopProofTheory                                                                                                                                                                   M-KILLED
allProofTheory                                                                                                                                                                       M-KILLED