Job 1639

CakeML:13eb6f5aa6a5bb9c159b02dfa1cc8c1d7bfc4d3a
  Fix a mistake [Nov 09 13:44:27]
#842 (ramsey)
Merging into:6b1184f731754a44e6368258d6c1b1cc729aa0f5
  Merge pull request #843 from CakeML/newline-fix [Nov 13 19:24:32]
HOL:6ad5e919416a5bf9dbe3bf35248a3cee706d8be5
  Disable unicode_version of `Borel` (Manual building broken), also nee [Nov 15 07:48:55]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 16 10:50:17 Claimed job
Nov 16 10:50:28 Building HOL
Nov 16 11:00:34 Starting developers
Nov 16 11:00:38 Finished developers                                               4s 119MB
Nov 16 11:00:39 Starting developers/bin
Nov 16 11:00:46 Finished developers/bin                                           6s   1GB
Nov 16 11:00:46 Starting semantics/ffi
Nov 16 11:00:58 Finished semantics/ffi                                           11s 244MB
Nov 16 11:00:58 Starting semantics
Nov 16 11:02:37 Finished semantics                                             1m39s 999MB
Nov 16 11:02:37 Starting semantics/proofs
Nov 16 11:06:30 Finished semantics/proofs                                      3m51s   1GB
Nov 16 11:06:30 Starting semantics/alt_semantics
Nov 16 11:06:42 Finished semantics/alt_semantics                                 11s 458MB
Nov 16 11:06:42 Starting semantics/alt_semantics/proofs
Nov 16 11:09:23 Finished semantics/alt_semantics/proofs                        2m40s 735MB
Nov 16 11:09:23 Starting basis/pure
Nov 16 11:12:34 Finished basis/pure                                            3m10s 799MB
Nov 16 11:12:34 Starting translator
Nov 16 11:16:13 Finished translator                                            3m39s   1GB
Nov 16 11:16:14 Starting compiler/parsing
Nov 16 11:17:31 Finished compiler/parsing                                      1m17s   3GB
Nov 16 11:17:31 Starting characteristic
Nov 16 11:23:30 Finished characteristic                                        5m57s   1GB
Nov 16 11:23:30 Starting translator/monadic
Nov 16 11:25:16 Finished translator/monadic                                    1m45s   1GB
Nov 16 11:25:16 Starting basis
Nov 16 12:14:22 Finished basis                                                49m04s  11GB
Nov 16 12:14:22 Starting compiler/inference
Nov 16 12:15:42 Finished compiler/inference                                    1m19s   1GB
Nov 16 12:15:42 Starting compiler/backend/reg_alloc
Nov 16 12:16:52 Finished compiler/backend/reg_alloc                            1m09s   1GB
Nov 16 12:16:52 Starting compiler/backend/gc
Nov 16 12:20:46 Finished compiler/backend/gc                                   3m53s   2GB
Nov 16 12:20:46 Starting compiler/backend
Nov 16 12:26:05 Finished compiler/backend                                      5m18s   4GB
Nov 16 12:26:06 Starting compiler/encoders/asm
Nov 16 12:26:30 Finished compiler/encoders/asm                                   24s 718MB
Nov 16 12:26:31 Starting compiler/encoders/x64
Nov 16 12:27:37 Finished compiler/encoders/x64                                 1m06s   1GB
Nov 16 12:27:37 Starting compiler/encoders/arm7
Nov 16 12:29:51 Finished compiler/encoders/arm7                                2m13s   1GB
Nov 16 12:29:51 Starting compiler/encoders/arm8
Nov 16 12:30:32 Finished compiler/encoders/arm8                                  40s 931MB
Nov 16 12:30:32 Starting compiler/encoders/mips
Nov 16 12:32:09 Finished compiler/encoders/mips                                1m36s 880MB
Nov 16 12:32:09 Starting compiler/encoders/riscv
Nov 16 12:34:04 Finished compiler/encoders/riscv                               1m54s   1GB
Nov 16 12:34:05 Starting compiler/encoders/ag32
Nov 16 12:34:24 Finished compiler/encoders/ag32                                  19s 655MB
Nov 16 12:34:24 Starting compiler/backend/x64
Nov 16 12:34:44 Finished compiler/backend/x64                                    19s   1GB
Nov 16 12:34:45 Starting compiler/backend/arm7
Nov 16 12:35:08 Finished compiler/backend/arm7                                   22s   1GB
Nov 16 12:35:08 Starting compiler/backend/arm8
Nov 16 12:35:28 Finished compiler/backend/arm8                                   20s   1GB
Nov 16 12:35:29 Starting compiler/backend/mips
Nov 16 12:35:48 Finished compiler/backend/mips                                   19s   1GB
Nov 16 12:35:49 Starting compiler/backend/riscv
Nov 16 12:36:10 Finished compiler/backend/riscv                                  20s   1GB
Nov 16 12:36:10 Starting compiler/backend/ag32
Nov 16 12:37:24 Finished compiler/backend/ag32                                 1m13s   1GB
Nov 16 12:37:24 Starting compiler/parsing/proofs
Nov 16 12:44:25 Finished compiler/parsing/proofs                               7m00s   1GB
Nov 16 12:44:25 Starting compiler/inference/proofs
Nov 16 12:47:06 Finished compiler/inference/proofs                             2m40s   1GB
Nov 16 12:47:06 Starting compiler/backend/semantics
Nov 16 13:20:28 Finished compiler/backend/semantics                           33m20s   2GB
Nov 16 13:20:28 Starting compiler/backend/reg_alloc/proofs
Nov 16 13:24:15 Finished compiler/backend/reg_alloc/proofs                     3m46s 877MB
Nov 16 13:24:15 Starting compiler/backend/proofs
Nov 16 14:23:04 Finished compiler/backend/proofs                              58m48s  14GB
Nov 16 14:23:04 Starting compiler/backend/serialiser
Nov 16 14:24:18 Finished compiler/backend/serialiser                           1m14s   1GB
Nov 16 14:24:19 Starting compiler/encoders/x64/proofs
Nov 16 14:34:36 Finished compiler/encoders/x64/proofs                         10m16s   4GB
Nov 16 14:34:36 Starting compiler/encoders/arm7/proofs
Nov 16 14:48:41 Finished compiler/encoders/arm7/proofs                        14m04s   3GB
Nov 16 14:48:41 Starting compiler/encoders/arm8/proofs
Nov 16 14:55:58 Finished compiler/encoders/arm8/proofs                         7m17s   1GB
Nov 16 14:55:59 Starting compiler/encoders/mips/proofs
Nov 16 15:06:38 Finished compiler/encoders/mips/proofs                        10m39s   2GB
Nov 16 15:06:39 Starting compiler/encoders/riscv/proofs
Nov 16 15:16:18 Finished compiler/encoders/riscv/proofs                        9m38s   1GB
Nov 16 15:16:18 Starting compiler/encoders/ag32/proofs
Nov 16 15:19:04 Finished compiler/encoders/ag32/proofs                         2m45s 672MB
Nov 16 15:19:04 Starting compiler/backend/x64/proofs
Nov 16 15:19:27 Finished compiler/backend/x64/proofs                             22s   1GB
Nov 16 15:19:27 Starting compiler/backend/arm7/proofs
Nov 16 15:19:51 Finished compiler/backend/arm7/proofs                            24s   1GB
Nov 16 15:19:52 Starting compiler/backend/arm8/proofs
Nov 16 15:20:16 Finished compiler/backend/arm8/proofs                            24s   1GB
Nov 16 15:20:16 Starting compiler/backend/mips/proofs
Nov 16 15:20:41 Finished compiler/backend/mips/proofs                            24s   1GB
Nov 16 15:20:41 Starting compiler/backend/riscv/proofs
Nov 16 15:21:05 Finished compiler/backend/riscv/proofs                           23s   1GB
Nov 16 15:21:05 Starting compiler/backend/ag32/proofs
Nov 16 15:34:55 Finished compiler/backend/ag32/proofs                         13m49s   2GB
Nov 16 15:34:55 Starting compiler/proofs
Nov 16 15:37:01 Finished compiler/proofs                                       2m06s   2GB
Nov 16 15:37:01 Starting candle/set-theory
Nov 16 15:37:31 Finished candle/set-theory                                       29s 714MB
Nov 16 15:37:32 Starting candle/syntax-lib
Nov 16 15:37:43 Finished candle/syntax-lib                                       11s 647MB
Nov 16 15:37:43 Starting candle/standard/syntax
Nov 16 15:39:41 Finished candle/standard/syntax                                1m57s   1GB
Nov 16 15:39:42 Starting candle/standard/semantics
Nov 16 15:41:29 Finished candle/standard/semantics                             1m47s   1GB
Nov 16 15:41:30 Starting candle/standard/monadic
Nov 16 15:43:20 Finished candle/standard/monadic                               1m50s   1GB
Nov 16 15:43:21 Starting candle/standard/ml_kernel
Nov 16 15:49:28 Finished candle/standard/ml_kernel                             6m06s   5GB
Nov 16 15:49:28 Starting candle/overloading/syntax
Nov 16 15:52:48 Finished candle/overloading/syntax                             3m19s   1GB
Nov 16 15:52:48 Starting candle/overloading/semantics
Nov 16 16:05:55 Finished candle/overloading/semantics                         13m06s   2GB
Nov 16 16:05:55 Starting pancake
Nov 16 16:07:51 Finished pancake                                               1m56s   2GB
Nov 16 16:07:51 Starting pancake/ffi
Nov 16 16:07:52 Finished pancake/ffi                                              0s   4MB
Nov 16 16:07:52 Starting pancake/semantics
Nov 16 16:10:22 Finished pancake/semantics                                     2m29s 987MB
Nov 16 16:10:22 Starting pancake/proofs
Nov 16 16:23:53 Finished pancake/proofs                                       13m30s   7GB
Nov 16 16:23:53 Starting characteristic/examples
Nov 16 16:25:27 Finished characteristic/examples                               1m33s   3GB
Nov 16 16:25:27 Starting tutorial/solutions
Nov 16 16:41:42 Finished tutorial/solutions                                   16m14s   9GB
Nov 16 16:41:42 Starting translator/monadic/examples
Nov 16 16:45:12 Finished translator/monadic/examples                           3m29s   2GB
Nov 16 16:45:12 Starting examples
Nov 16 16:55:17 Finished examples                                             10m04s   4GB
Nov 16 16:55:17 Starting examples/compilation/x64
Nov 16 19:28:14 Finished examples/compilation/x64                           2h32m56s  17GB
Nov 16 19:28:14 Starting examples/compilation/x64/proofs
Nov 16 19:30:08 Finished examples/compilation/x64/proofs                       1m53s   3GB
Nov 16 19:30:08 Starting examples/compilation/ag32
Nov 16 20:05:59 Finished examples/compilation/ag32                            35m49s   9GB
Nov 16 20:05:59 Starting examples/compilation/ag32/proofs
Nov 16 20:06:53 Finished examples/compilation/ag32/proofs                        53s   4GB
Nov 16 20:06:53 Starting examples/cost
Nov 16 21:06:31 Finished examples/cost                                        59m37s   7GB
Nov 16 21:06:31 Starting examples/lpr_checker
Nov 16 21:07:21 Finished examples/lpr_checker                                    50s   1GB
Nov 16 21:07:22 Starting examples/lpr_checker/array
Nov 16 21:38:48 Finished examples/lpr_checker/array                           31m25s   5GB
Nov 16 21:38:48 Starting examples/lpr_checker/array/compilation
Nov 16 23:09:32 Finished examples/lpr_checker/array/compilation             1h30m42s  36GB
Nov 16 23:09:32 Starting examples/lpr_checker/array/compilation/proofs
Nov 16 23:10:41 FAILED: examples/lpr_checker/array/compilation/proofs
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/topology
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/lpr_checker
Scanning $(CAKEMLDIR)/examples/lpr_checker/array
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/examples/lpr_checker/array/compilation
Starting work on README.md
Starting work on lpr_arrayProofTheory
Starting work on lpr_arrayRamseyProofTheory
README.md                                                           (0s)     OK
lpr_arrayProofTheory                                               (59s)FAIL<1>
   Q.store_thm
   (
      "machine_code_sound",
      [
         QUOTE
         " (*#loc 85 28*)\n  cake_lpr_run cl fs mc ms \226\135\146\n  machine_sem mc (basis_ffi cl fs) ms \226\138\134\n    extend_with_resource_limit\n      {Terminate Success (check_unsat_io_events cl fs)} \226\136\167\n  \226\136\131out err.\n    extract_fs fs (check_unsat_io_events cl fs) =\n      SOME (add_stdout (add_stderr fs err) out) \226\136\167\n  if LENGTH cl = 2 then\n    if inFS_fname fs (EL 1 cl)\n    then\n      case parse_dimacs (all_lines fs (EL 1 cl)) of\n        NONE => out = strlit \"\"\n      | SOME fml => out = concat (print_dimacs fml)\n    else out = strlit \"\"\n  else if LENGTH cl = 3 then\n    if out = strlit \"s VERIFIED UNSAT\\n\" then\n      inFS_fname fs (EL 1 cl) \226\136\167\n      \226\136\131fml.\n        parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml \226\136\167\n        unsatisfiable (interp fml)\n    else out = strlit \"\"\n  else if LENGTH cl = 4 then\n    if out = strlit \"s VERIFIED TRANSFORMATION\\n\" then\n    inFS_fname fs (EL 1 cl) \226\136\167 inFS_fname fs (EL 3 cl) \226\136\167\n    \226\136\131fml fml2.\n      parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml \226\136\167\n      parse_dimacs (all_lines fs (EL 3 cl)) = SOME fml2 \226\136\167\n      (satisfiable (interp fml) \226\135\146 satisfiable (interp fml2))\n    else out = strlit \"\"\n  else if LENGTH cl = 5 then\n    if \226\136\131cnf_md5 proof_md5 rng. out = success_str cnf_md5 proof_md5 rng then\n    inFS_fname fs (EL 1 cl) \226\136\167 inFS_fname fs (EL 2 cl) \226\136\167\n    inFS_fname fs (EL 4 cl) \226\136\167\n    \226\136\131i j fml pf.\n      out = success_str\n        (implode (md5 (THE (file_content fs (EL 1 cl)))))\n        (implode (md5 (THE (file_content fs (EL 2 cl)))))\n        (print_rng i j) \226\136\167\n      parse_rng (EL 3 cl) = SOME (i,j) \226\136\167\n      parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml \226\136\167\n      parse_proof (all_lines fs (EL 2 cl)) = SOME pf \226\136\167\n      i \226\137\164 j \226\136\167 j \226\137\164 LENGTH pf \226\136\167\n      (satisfiable (interp (run_proof fml (TAKE i pf))) \226\135\146\n       satisfiable (interp (run_proof fml (TAKE j pf))))\n    else if ?n:num. out = concat [strlit \"s VERIFIED INTERVALS COVER 0-\"; toString n; strlit \"\\n\"] then\n    inFS_fname fs (EL 1 cl) \226\136\167 inFS_fname fs (EL 2 cl) \226\136\167 inFS_fname fs (EL 4 cl) \226\136\167\n    EL 3 cl = strlit \"-check\" \226\136\167\n    check_lines (implode (md5 (THE (file_content fs (EL 1 cl)))))\n                (implode (md5 (THE (file_content fs (EL 2 cl)))))\n                (all_lines fs (EL 4 cl)) (LENGTH (all_lines fs (EL 2 cl))) = INR out\n    else out = strlit \"\"\n  else\n    out = strlit \"\""
         ],
      ... >> ... >> ... ...
      )
 Uncaught exception: Fail "Static Errors"
lpr_arrayRamseyProofTheory                                         (63s)MKILLED