Job 1637

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:7e1cdab63fa78a67a3fabc28a9f2a909e65b6921
  Make RPROD (and PAIR_REL and ###) more polymorphic [Nov 12 10:36:34]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 15 12:00:03 Claimed job
Nov 15 12:00:17 Building HOL
Nov 15 12:10:20 Starting developers
Nov 15 12:10:25 Finished developers                                               4s 120MB
Nov 15 12:10:25 Starting developers/bin
Nov 15 12:10:32 Finished developers/bin                                           6s   1GB
Nov 15 12:10:32 Starting semantics/ffi
Nov 15 12:10:44 Finished semantics/ffi                                           11s 227MB
Nov 15 12:10:45 Starting semantics
Nov 15 12:12:24 Finished semantics                                             1m39s   1GB
Nov 15 12:12:24 Starting semantics/proofs
Nov 15 12:16:15 Finished semantics/proofs                                      3m51s   1GB
Nov 15 12:16:16 Starting semantics/alt_semantics
Nov 15 12:16:27 Finished semantics/alt_semantics                                 11s 359MB
Nov 15 12:16:28 Starting semantics/alt_semantics/proofs
Nov 15 12:19:07 Finished semantics/alt_semantics/proofs                        2m39s 975MB
Nov 15 12:19:08 Starting basis/pure
Nov 15 12:22:09 Finished basis/pure                                            3m00s 748MB
Nov 15 12:22:09 Starting translator
Nov 15 12:25:46 Finished translator                                            3m36s   1GB
Nov 15 12:25:46 Starting compiler/parsing
Nov 15 12:27:04 Finished compiler/parsing                                      1m18s   2GB
Nov 15 12:27:05 Starting characteristic
Nov 15 12:33:04 Finished characteristic                                        5m59s   1GB
Nov 15 12:33:04 Starting translator/monadic
Nov 15 12:34:53 Finished translator/monadic                                    1m48s   1GB
Nov 15 12:34:54 Starting basis
Nov 15 13:24:07 Finished basis                                                49m12s  17GB
Nov 15 13:24:07 Starting compiler/inference
Nov 15 13:25:26 Finished compiler/inference                                    1m18s   1GB
Nov 15 13:25:26 Starting compiler/backend/reg_alloc
Nov 15 13:26:37 Finished compiler/backend/reg_alloc                            1m10s   1GB
Nov 15 13:26:37 Starting compiler/backend/gc
Nov 15 13:30:30 Finished compiler/backend/gc                                   3m52s   2GB
Nov 15 13:30:30 Starting compiler/backend
Nov 15 13:35:47 Finished compiler/backend                                      5m17s   3GB
Nov 15 13:35:48 Starting compiler/encoders/asm
Nov 15 13:36:12 Finished compiler/encoders/asm                                   24s 781MB
Nov 15 13:36:12 Starting compiler/encoders/x64
Nov 15 13:37:20 Finished compiler/encoders/x64                                 1m07s 833MB
Nov 15 13:37:20 Starting compiler/encoders/arm7
Nov 15 13:39:32 Finished compiler/encoders/arm7                                2m11s   1GB
Nov 15 13:39:33 Starting compiler/encoders/arm8
Nov 15 13:40:12 Finished compiler/encoders/arm8                                  39s 574MB
Nov 15 13:40:13 Starting compiler/encoders/mips
Nov 15 13:41:51 Finished compiler/encoders/mips                                1m37s   1GB
Nov 15 13:41:51 Starting compiler/encoders/riscv
Nov 15 13:43:47 Finished compiler/encoders/riscv                               1m56s 877MB
Nov 15 13:43:48 Starting compiler/encoders/ag32
Nov 15 13:44:07 Finished compiler/encoders/ag32                                  18s 614MB
Nov 15 13:44:07 Starting compiler/backend/x64
Nov 15 13:44:27 Finished compiler/backend/x64                                    20s   1GB
Nov 15 13:44:28 Starting compiler/backend/arm7
Nov 15 13:44:50 Finished compiler/backend/arm7                                   22s   1GB
Nov 15 13:44:50 Starting compiler/backend/arm8
Nov 15 13:45:11 Finished compiler/backend/arm8                                   20s   1GB
Nov 15 13:45:11 Starting compiler/backend/mips
Nov 15 13:45:31 Finished compiler/backend/mips                                   19s   1GB
Nov 15 13:45:31 Starting compiler/backend/riscv
Nov 15 13:45:52 Finished compiler/backend/riscv                                  20s   1GB
Nov 15 13:45:52 Starting compiler/backend/ag32
Nov 15 13:47:06 Finished compiler/backend/ag32                                 1m13s   1GB
Nov 15 13:47:06 Starting compiler/parsing/proofs
Nov 15 13:54:09 Finished compiler/parsing/proofs                               7m03s 967MB
Nov 15 13:54:09 Starting compiler/inference/proofs
Nov 15 13:56:50 Finished compiler/inference/proofs                             2m39s   1GB
Nov 15 13:56:50 Starting compiler/backend/semantics
Nov 15 14:29:55 Finished compiler/backend/semantics                           33m04s   2GB
Nov 15 14:29:55 Starting compiler/backend/reg_alloc/proofs
Nov 15 14:33:45 Finished compiler/backend/reg_alloc/proofs                     3m50s   1GB
Nov 15 14:33:45 Starting compiler/backend/proofs
Nov 15 15:32:10 Finished compiler/backend/proofs                              58m23s  11GB
Nov 15 15:32:10 Starting compiler/backend/serialiser
Nov 15 15:33:25 Finished compiler/backend/serialiser                           1m14s   1GB
Nov 15 15:33:25 Starting compiler/encoders/x64/proofs
Nov 15 15:43:44 Finished compiler/encoders/x64/proofs                         10m19s   4GB
Nov 15 15:43:44 Starting compiler/encoders/arm7/proofs
Nov 15 15:57:42 Finished compiler/encoders/arm7/proofs                        13m57s   6GB
Nov 15 15:57:42 Starting compiler/encoders/arm8/proofs
Nov 15 16:04:54 Finished compiler/encoders/arm8/proofs                         7m11s   1GB
Nov 15 16:04:54 Starting compiler/encoders/mips/proofs
Nov 15 16:15:32 Finished compiler/encoders/mips/proofs                        10m38s   2GB
Nov 15 16:15:33 Starting compiler/encoders/riscv/proofs
Nov 15 16:24:58 Finished compiler/encoders/riscv/proofs                        9m24s   1GB
Nov 15 16:24:58 Starting compiler/encoders/ag32/proofs
Nov 15 16:27:44 Finished compiler/encoders/ag32/proofs                         2m46s 648MB
Nov 15 16:27:44 Starting compiler/backend/x64/proofs
Nov 15 16:28:08 Finished compiler/backend/x64/proofs                             23s   1GB
Nov 15 16:28:09 Starting compiler/backend/arm7/proofs
Nov 15 16:28:33 Finished compiler/backend/arm7/proofs                            24s   1GB
Nov 15 16:28:33 Starting compiler/backend/arm8/proofs
Nov 15 16:28:58 Finished compiler/backend/arm8/proofs                            24s   1GB
Nov 15 16:28:58 Starting compiler/backend/mips/proofs
Nov 15 16:29:21 Finished compiler/backend/mips/proofs                            22s   1GB
Nov 15 16:29:21 Starting compiler/backend/riscv/proofs
Nov 15 16:29:45 Finished compiler/backend/riscv/proofs                           23s   1GB
Nov 15 16:29:45 Starting compiler/backend/ag32/proofs
Nov 15 16:43:35 Finished compiler/backend/ag32/proofs                         13m49s   2GB
Nov 15 16:43:36 Starting compiler/proofs
Nov 15 16:45:46 Finished compiler/proofs                                       2m09s   4GB
Nov 15 16:45:46 Starting candle/set-theory
Nov 15 16:46:17 Finished candle/set-theory                                       30s 793MB
Nov 15 16:46:17 Starting candle/syntax-lib
Nov 15 16:46:28 Finished candle/syntax-lib                                       11s 722MB
Nov 15 16:46:29 Starting candle/standard/syntax
Nov 15 16:48:25 Finished candle/standard/syntax                                1m56s   1GB
Nov 15 16:48:25 Starting candle/standard/semantics
Nov 15 16:50:14 Finished candle/standard/semantics                             1m48s   1GB
Nov 15 16:50:14 Starting candle/standard/monadic
Nov 15 16:52:05 Finished candle/standard/monadic                               1m50s   1GB
Nov 15 16:52:05 Starting candle/standard/ml_kernel
Nov 15 16:58:14 Finished candle/standard/ml_kernel                             6m08s   5GB
Nov 15 16:58:14 Starting candle/overloading/syntax
Nov 15 17:01:36 Finished candle/overloading/syntax                             3m21s   1GB
Nov 15 17:01:37 Starting candle/overloading/semantics
Nov 15 17:14:26 Finished candle/overloading/semantics                         12m48s   2GB
Nov 15 17:14:26 Starting pancake
Nov 15 17:16:23 Finished pancake                                               1m56s   2GB
Nov 15 17:16:23 Starting pancake/ffi
Nov 15 17:16:24 Finished pancake/ffi                                              0s   5MB
Nov 15 17:16:24 Starting pancake/semantics
Nov 15 17:18:52 Finished pancake/semantics                                     2m27s   1GB
Nov 15 17:18:52 Starting pancake/proofs
Nov 15 17:32:19 Finished pancake/proofs                                       13m26s   6GB
Nov 15 17:32:20 Starting characteristic/examples
Nov 15 17:33:44 Finished characteristic/examples                               1m24s   2GB
Nov 15 17:33:44 Starting tutorial/solutions
Nov 15 17:49:51 Finished tutorial/solutions                                   16m04s  11GB
Nov 15 17:49:51 Starting translator/monadic/examples
Nov 15 17:53:18 Finished translator/monadic/examples                           3m26s   2GB
Nov 15 17:53:18 Starting examples
Nov 15 18:03:24 Finished examples                                             10m05s   4GB
Nov 15 18:03:24 Starting examples/compilation/x64
Nov 15 20:35:56 Finished examples/compilation/x64                           2h32m30s  18GB
Nov 15 20:35:56 Starting examples/compilation/x64/proofs
Nov 15 20:37:48 Finished examples/compilation/x64/proofs                       1m51s   3GB
Nov 15 20:37:48 Starting examples/compilation/ag32
Nov 15 21:13:24 Finished examples/compilation/ag32                            35m35s   9GB
Nov 15 21:13:24 Starting examples/compilation/ag32/proofs
Nov 15 21:14:17 Finished examples/compilation/ag32/proofs                        53s   4GB
Nov 15 21:14:18 Starting examples/cost
Nov 15 22:12:50 Finished examples/cost                                        58m31s   7GB
Nov 15 22:12:50 Starting examples/lpr_checker
Nov 15 22:13:41 Finished examples/lpr_checker                                    50s   1GB
Nov 15 22:13:41 Starting examples/lpr_checker/array
Nov 15 22:44:29 Finished examples/lpr_checker/array                           30m47s   5GB
Nov 15 22:44:29 Starting examples/lpr_checker/array/compilation
Nov 16 00:15:13 Finished examples/lpr_checker/array/compilation             1h30m42s  38GB
Nov 16 00:15:14 Starting examples/lpr_checker/array/compilation/proofs
Nov 16 00:16:06 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_arrayRamseyProofTheory                                         (45s)     OK
lpr_arrayProofTheory                                               (46s)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"