Job 41

CakeML:f5e728ebd637e3c6bfc94d4f336998ab1214a49e
  Fix backend proofs broken by automatic rewrites [Nov 25 02:10:27]
HOL:5a30cd803ef0c285a4edf698778113ac21ce5509
  Prove more about RATN & RATD; define RAT_SGN; prove results about it [Nov 24 04:53:00]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Nov 25 02:20:44 Claimed job
Nov 25 02:20:51 Building HOL
Nov 25 02:21:04 Starting semantics/ffi
Nov 25 02:21:26 Finished semantics/ffi                                           19s 258MB
Nov 25 02:21:27 Starting semantics
Nov 25 02:23:49 Finished semantics                                             2m18s   1GB
Nov 25 02:23:51 Starting semantics/proofs
Nov 25 02:27:26 Finished semantics/proofs                                      3m33s 994MB
Nov 25 02:27:28 Starting basis/pure
Nov 25 02:28:38 Finished basis/pure                                            1m08s 618MB
Nov 25 02:28:40 Starting translator
Nov 25 02:36:04 Finished translator                                            7m21s   1GB
Nov 25 02:36:06 Starting compiler/parsing
Nov 25 02:38:40 Finished compiler/parsing                                      2m32s   2GB
Nov 25 02:38:42 Starting characteristic
Nov 25 02:43:36 Finished characteristic                                        4m51s   2GB
Nov 25 02:43:38 Starting basis
Nov 25 03:12:22 Finished basis                                                28m41s   2GB
Nov 25 03:12:24 Starting translator/monadic
Nov 25 03:16:16 Finished translator/monadic                                    3m50s   1GB
Nov 25 03:16:18 Starting compiler/inference
Nov 25 03:18:39 Finished compiler/inference                                    2m18s 911MB
Nov 25 03:18:41 Starting compiler/backend/reg_alloc
Nov 25 03:19:30 Finished compiler/backend/reg_alloc                              47s 887MB
Nov 25 03:19:32 Starting compiler/backend/gc
Nov 25 03:34:25 Finished compiler/backend/gc                                  14m51s   3GB
Nov 25 03:34:27 Starting compiler/backend
Nov 25 03:34:31 Finished compiler/backend                                         1s  14MB
Nov 25 03:34:33 Starting compiler/encoders/asm
Nov 25 03:34:36 Finished compiler/encoders/asm                                    0s  25MB
Nov 25 03:34:37 Starting compiler/encoders/x64
Nov 25 03:35:08 Finished compiler/encoders/x64                                   28s 411MB
Nov 25 03:35:09 Starting compiler/encoders/arm6
Nov 25 03:36:43 Finished compiler/encoders/arm6                                1m31s 463MB
Nov 25 03:36:45 Starting compiler/encoders/arm8
Nov 25 03:37:02 Finished compiler/encoders/arm8                                  15s 419MB
Nov 25 03:37:04 Starting compiler/encoders/mips
Nov 25 03:37:24 Finished compiler/encoders/mips                                  18s 459MB
Nov 25 03:37:26 Starting compiler/encoders/riscv
Nov 25 03:37:44 Finished compiler/encoders/riscv                                 15s 414MB
Nov 25 03:37:46 Starting compiler/backend/x64
Nov 25 03:38:31 Finished compiler/backend/x64                                    43s   1GB
Nov 25 03:38:33 Starting compiler/backend/arm6
Nov 25 03:39:22 Finished compiler/backend/arm6                                   46s   1GB
Nov 25 03:39:24 Starting compiler/backend/arm8
Nov 25 03:40:09 Finished compiler/backend/arm8                                   42s   1GB
Nov 25 03:40:11 Starting compiler/backend/mips
Nov 25 03:40:57 Finished compiler/backend/mips                                   44s   1GB
Nov 25 03:40:59 Starting compiler/backend/riscv
Nov 25 03:41:43 Finished compiler/backend/riscv                                  41s 937MB
Nov 25 03:41:45 Starting compiler/parsing/proofs
Nov 25 03:46:37 Finished compiler/parsing/proofs                               4m50s 748MB
Nov 25 03:46:39 Starting compiler/inference/proofs
Nov 25 03:51:03 Finished compiler/inference/proofs                             4m21s   1GB
Nov 25 03:51:05 Starting compiler/backend/semantics
Nov 25 04:11:02 Finished compiler/backend/semantics                           19m55s   2GB
Nov 25 04:11:04 Starting compiler/backend/reg_alloc/proofs
Nov 25 04:12:16 Finished compiler/backend/reg_alloc/proofs                     1m10s 509MB
Nov 25 04:12:18 Starting compiler/backend/proofs
Nov 25 05:25:27 Finished compiler/backend/proofs                            1h13m06s   5GB
Nov 25 05:25:29 Starting compiler/encoders/x64/proofs
Nov 25 05:36:55 Finished compiler/encoders/x64/proofs                         11m23s   1GB
Nov 25 05:36:57 Starting compiler/encoders/arm6/proofs
Nov 25 05:50:51 Finished compiler/encoders/arm6/proofs                        13m52s   2GB
Nov 25 05:50:53 Starting compiler/encoders/arm8/proofs
Nov 25 06:00:34 Finished compiler/encoders/arm8/proofs                         9m38s 895MB
Nov 25 06:00:36 Starting compiler/encoders/mips/proofs
Nov 25 06:13:57 Finished compiler/encoders/mips/proofs                        13m19s   2GB
Nov 25 06:13:59 Starting compiler/encoders/riscv/proofs
Nov 25 06:28:01 Finished compiler/encoders/riscv/proofs                       14m00s   1GB
Nov 25 06:28:03 Starting compiler/backend/x64/proofs
Nov 25 06:28:58 Finished compiler/backend/x64/proofs                             53s   1GB
Nov 25 06:29:00 Starting compiler/backend/arm6/proofs
Nov 25 06:30:04 Finished compiler/backend/arm6/proofs                          1m01s   1GB
Nov 25 06:30:06 Starting compiler/backend/arm8/proofs
Nov 25 06:31:03 Finished compiler/backend/arm8/proofs                            54s   1GB
Nov 25 06:31:05 Starting compiler/backend/mips/proofs
Nov 25 06:32:00 Finished compiler/backend/mips/proofs                            53s   1GB
Nov 25 06:32:02 Starting compiler/backend/riscv/proofs
Nov 25 06:32:57 Finished compiler/backend/riscv/proofs                           53s   1GB
Nov 25 06:32:59 Starting compiler/proofs
Nov 25 06:34:50 Finished compiler/proofs                                       1m49s   1GB
Nov 25 06:34:52 Starting candle/set-theory
Nov 25 06:36:39 Finished candle/set-theory                                     1m44s 560MB
Nov 25 06:36:41 Starting candle/syntax-lib
Nov 25 06:37:03 Finished candle/syntax-lib                                       20s 557MB
Nov 25 06:37:05 Starting candle/standard/syntax
Nov 25 06:40:13 Finished candle/standard/syntax                                3m06s 629MB
Nov 25 06:40:16 Starting candle/standard/semantics
Nov 25 06:42:50 Finished candle/standard/semantics                             2m32s 682MB
Nov 25 06:42:52 Starting candle/standard/monadic
Nov 25 06:45:47 Finished candle/standard/monadic                               2m53s 949MB
Nov 25 06:45:49 Starting candle/standard/ml_kernel
Nov 25 06:57:36 Finished candle/standard/ml_kernel                            11m44s   2GB
Nov 25 06:57:38 Starting candle/standard/opentheory
Nov 25 06:58:11 Finished candle/standard/opentheory                              31s 593MB
Nov 25 06:58:13 Starting characteristic/examples
Nov 25 07:00:26 Finished characteristic/examples                               2m11s   1GB
Nov 25 07:00:28 Starting tutorial/solutions
Nov 25 07:33:54 Finished tutorial/solutions                                   33m24s   8GB
Nov 25 07:33:56 Starting examples
Nov 25 07:35:09 FAILED: examples
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/regular
]0;Holmake: .Recursively calling Holmake in ../basis
]0;Holmake: ../basisRecursively calling Holmake in ../basis/pure
]0;Holmake: ../basis/pureRecursively calling Holmake in ../misc
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: ../miscRecursively calling Holmake in ../developers
]0;Holmake: ../developers]0;Holmake: ../developersFinished recursive invocation in ../developers
]0;Holmake: ../miscRecursively calling Holmake in ../misc/lem_lib_stub
]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stubFinished recursive invocation in ../misc/lem_lib_stub
]0;Holmake: ../misc]0;Holmake: ../miscFinished recursive invocation in ../misc
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pureFinished recursive invocation in ../basis/pure
]0;Holmake: ../basisRecursively calling Holmake in ../characteristic
]0;Holmake: ../characteristicRecursively calling Holmake in ../compiler/parsing
]0;Holmake: ../compiler/parsingRecursively calling Holmake in ../semantics
]0;Holmake: ../semanticsRecursively calling Holmake in ../semantics/ffi
]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffiFinished recursive invocation in ../semantics/ffi
]0;Holmake: ../semantics]0;Holmake: ../semanticsFinished recursive invocation in ../semantics
]0;Holmake: ../compiler/parsing]0;Holmake: ../compiler/parsingFinished recursive invocation in ../compiler/parsing
]0;Holmake: ../characteristicRecursively calling Holmake in ../semantics/alt_semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsFinished recursive invocation in ../semantics/alt_semantics
]0;Holmake: ../semantics/alt_semantics/proofsRecursively calling Holmake in ../semantics/proofs
]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsFinished recursive invocation in ../semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsFinished recursive invocation in ../semantics/alt_semantics/proofs
]0;Holmake: ../characteristicRecursively calling Holmake in ../translator
]0;Holmake: ../translator]0;Holmake: ../translatorFinished recursive invocation in ../translator
]0;Holmake: ../characteristic]0;Holmake: ../characteristicFinished recursive invocation in ../characteristic
]0;Holmake: ../basis]0;Holmake: ../basisFinished recursive invocation in ../basis
]0;Holmake: .]0;Holmake: .Starting work on heap
Starting work on README.md
README.md                                                                    OK
heap                                                                         OK
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on echoProgTheory
Starting work on grepProgTheory
lcsTheory                                                                    OK
Starting work on diffTheory
diffTheory                                                          FAILED! <1>
      TOKENS (x. x = #"a"  x = #"d"  x = #"c"  x = #"\n") (TL r)
    else l::TOKENS (x. x = #"a"  x = #"d"  x = #"c"  x = #"\n") r)
   (if
      CHR (Num (ABS n) + 55) = #"a"  CHR (Num (ABS n) + 55) = #"d" 
      CHR (Num (ABS n) + 55) = #"c"  CHR (Num (ABS n) + 55) = #"\n"
    then
      ("",STRING (CHR (Num (ABS n) + 55)) "")
    else (STRING (CHR (Num (ABS n) + 55)) "","")) =
 [STRING (CHR (Num (ABS n) + 55)) ""]
 
catProgTheory                                                          M-KILLED
echoProgTheory                                                         M-KILLED
grepProgTheory                                                         M-KILLED