CakeML Regression Test

Job 584

CakeML:485b0e0ae1abc90b190d3ff4a2d0f85ee8a1b560
  Remove manual EqualityType from parserProgScript. [Nov 25 15:12:00]
#564 (EqualityType)
Merging into:59886cd0205c1d5d943ef10a26890f79b515b68f
  Merge pull request #561 from CakeML/print-types [Nov 26 04:25:18]
HOL:9038f10089a8ec0f452de53da02a270ef646a3e2
  Move holpathdb test to be earlier in build sequence [Nov 26 01:19:14]
Machine:demi

Nov 26 11:43:57 Claimed job
Nov 26 11:44:06 Building HOL
Nov 26 11:57:04 Starting developers/bin
Nov 26 11:57:11 Finished developers/bin                                           6s 923MB
Nov 26 11:57:11 Starting semantics/ffi
Nov 26 11:58:10 Finished semantics/ffi                                           57s 431MB
Nov 26 11:58:10 Starting semantics
Nov 26 12:00:17 Finished semantics                                             2m06s 918MB
Nov 26 12:00:17 Starting semantics/proofs
Nov 26 12:04:22 Finished semantics/proofs                                      4m03s   1GB
Nov 26 12:04:22 Starting basis/pure
Nov 26 12:09:27 Finished basis/pure                                            5m04s 765MB
Nov 26 12:09:27 Starting translator
Nov 26 12:13:52 Finished translator                                            4m23s 949MB
Nov 26 12:13:52 Starting compiler/parsing
Nov 26 12:15:39 Finished compiler/parsing                                      1m45s   1GB
Nov 26 12:15:39 Starting characteristic
Nov 26 12:19:15 Finished characteristic                                        3m34s   1GB
Nov 26 12:19:15 Starting translator/monadic
Nov 26 12:21:24 Finished translator/monadic                                    2m07s   1GB
Nov 26 12:21:24 Starting basis
Nov 26 12:44:11 Finished basis                                                22m46s   2GB
Nov 26 12:44:12 Starting compiler/inference
Nov 26 12:46:36 Finished compiler/inference                                    2m24s   1GB
Nov 26 12:46:37 Starting compiler/backend/reg_alloc
Nov 26 12:47:40 Finished compiler/backend/reg_alloc                            1m03s 955MB
Nov 26 12:47:41 Starting compiler/backend/gc
Nov 26 12:57:44 Finished compiler/backend/gc                                  10m02s   1GB
Nov 26 12:57:45 Starting compiler/backend
Nov 26 12:57:48 Finished compiler/backend                                         2s  49MB
Nov 26 12:57:48 Starting compiler/encoders/asm
Nov 26 12:57:50 Finished compiler/encoders/asm                                    1s  36MB
Nov 26 12:57:50 Starting compiler/encoders/x64
Nov 26 12:59:06 Finished compiler/encoders/x64                                 1m14s 611MB
Nov 26 12:59:06 Starting compiler/encoders/arm6
Nov 26 13:01:34 Finished compiler/encoders/arm6                                2m27s   1GB
Nov 26 13:01:35 Starting compiler/encoders/arm8
Nov 26 13:02:13 Finished compiler/encoders/arm8                                  37s 496MB
Nov 26 13:02:14 Starting compiler/encoders/mips
Nov 26 13:03:41 Finished compiler/encoders/mips                                1m26s 885MB
Nov 26 13:03:41 Starting compiler/encoders/riscv
Nov 26 13:05:10 Finished compiler/encoders/riscv                               1m28s 901MB
Nov 26 13:05:11 Starting compiler/encoders/ag32
Nov 26 13:05:35 Finished compiler/encoders/ag32                                  24s 616MB
Nov 26 13:05:36 Starting compiler/backend/x64
Nov 26 13:06:02 Finished compiler/backend/x64                                    25s   1GB
Nov 26 13:06:02 Starting compiler/backend/arm6
Nov 26 13:06:30 Finished compiler/backend/arm6                                   27s   1GB
Nov 26 13:06:30 Starting compiler/backend/arm8
Nov 26 13:06:55 Finished compiler/backend/arm8                                   24s 916MB
Nov 26 13:06:56 Starting compiler/backend/mips
Nov 26 13:07:22 Finished compiler/backend/mips                                   25s   1GB
Nov 26 13:07:22 Starting compiler/backend/riscv
Nov 26 13:07:48 Finished compiler/backend/riscv                                  25s   1GB
Nov 26 13:07:48 Starting compiler/backend/ag32
Nov 26 13:09:26 Finished compiler/backend/ag32                                 1m36s   1GB
Nov 26 13:09:26 Starting compiler/parsing/proofs
Nov 26 13:18:53 Finished compiler/parsing/proofs                               9m26s 914MB
Nov 26 13:18:54 Starting compiler/inference/proofs
Nov 26 13:22:52 Finished compiler/inference/proofs                             3m57s   1GB
Nov 26 13:22:53 Starting compiler/backend/semantics
Nov 26 13:34:52 Finished compiler/backend/semantics                           11m58s   2GB
Nov 26 13:34:52 Starting compiler/backend/reg_alloc/proofs
Nov 26 13:38:35 Finished compiler/backend/reg_alloc/proofs                     3m42s 856MB
Nov 26 13:38:35 Starting compiler/backend/proofs
Nov 26 14:35:15 Finished compiler/backend/proofs                              56m39s   3GB
Nov 26 14:35:16 Starting compiler/encoders/x64/proofs
Nov 26 14:48:55 Finished compiler/encoders/x64/proofs                         13m38s   5GB
Nov 26 14:48:55 Starting compiler/encoders/arm6/proofs
Nov 26 15:09:40 Finished compiler/encoders/arm6/proofs                        20m44s   2GB
Nov 26 15:09:40 Starting compiler/encoders/arm8/proofs
Nov 26 15:17:53 Finished compiler/encoders/arm8/proofs                         8m12s   1GB
Nov 26 15:17:54 Starting compiler/encoders/mips/proofs
Nov 26 15:32:15 Finished compiler/encoders/mips/proofs                        14m20s   2GB
Nov 26 15:32:16 Starting compiler/encoders/riscv/proofs
Nov 26 15:43:09 Finished compiler/encoders/riscv/proofs                       10m53s   1GB
Nov 26 15:43:10 Starting compiler/encoders/ag32/proofs
Nov 26 15:46:46 Finished compiler/encoders/ag32/proofs                         3m35s 990MB
Nov 26 15:46:47 Starting compiler/backend/x64/proofs
Nov 26 15:47:17 Finished compiler/backend/x64/proofs                             29s   1GB
Nov 26 15:47:17 Starting compiler/backend/arm6/proofs
Nov 26 15:47:48 Finished compiler/backend/arm6/proofs                            30s   1GB
Nov 26 15:47:49 Starting compiler/backend/arm8/proofs
Nov 26 15:48:16 Finished compiler/backend/arm8/proofs                            26s 847MB
Nov 26 15:48:17 Starting compiler/backend/mips/proofs
Nov 26 15:48:48 Finished compiler/backend/mips/proofs                            30s   1GB
Nov 26 15:48:48 Starting compiler/backend/riscv/proofs
Nov 26 15:49:17 Finished compiler/backend/riscv/proofs                           28s   1GB
Nov 26 15:49:18 Starting compiler/backend/ag32/proofs
Nov 26 16:02:15 Finished compiler/backend/ag32/proofs                         12m56s   2GB
Nov 26 16:02:15 Starting compiler/proofs
Nov 26 16:04:02 Finished compiler/proofs                                       1m46s   2GB
Nov 26 16:04:03 Starting candle/set-theory
Nov 26 16:04:48 Finished candle/set-theory                                       44s 614MB
Nov 26 16:04:48 Starting candle/syntax-lib
Nov 26 16:05:03 Finished candle/syntax-lib                                       14s 620MB
Nov 26 16:05:03 Starting candle/standard/syntax
Nov 26 16:07:12 Finished candle/standard/syntax                                2m08s 805MB
Nov 26 16:07:13 Starting candle/standard/semantics
Nov 26 16:09:05 Finished candle/standard/semantics                             1m52s 870MB
Nov 26 16:09:06 Starting candle/standard/monadic
Nov 26 16:11:14 Finished candle/standard/monadic                               2m07s   1GB
Nov 26 16:11:15 Starting candle/standard/ml_kernel
Nov 26 16:30:48 Finished candle/standard/ml_kernel                            19m32s   4GB
Nov 26 16:30:49 Starting candle/standard/opentheory
Nov 26 16:41:14 Finished candle/standard/opentheory                           10m24s   3GB
Nov 26 16:41:14 Starting candle/standard/opentheory/compilation
Nov 26 17:17:35 Finished candle/standard/opentheory/compilation               36m19s  22GB
Nov 26 17:17:35 Starting candle/standard/opentheory/compilation/proofs
Nov 26 17:18:27 Finished candle/standard/opentheory/compilation/proofs           51s   5GB
Nov 26 17:18:28 Starting characteristic/examples
Nov 26 17:20:25 Finished characteristic/examples                               1m56s   1GB
Nov 26 17:20:25 Starting tutorial/solutions
Nov 26 17:38:18 Finished tutorial/solutions                                   17m52s   7GB
Nov 26 17:38:18 Starting translator/monadic/examples
Nov 26 17:39:21 FAILED: translator/monadic/examples
]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/machine-code/hoare-triple]0;Holmake: ~/cakeml/regression-worker/HOL-9038f10089a8ec0f452de53da02a270ef646a3e2/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../../../basis]0;Holmake: ../../../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/translator/monadic/examples
Starting work on arrayGlobalStateProgTheory
Starting work on arrayLocalStateProgTheory
Starting work on exceptionArityTestProgTheory
Starting work on exceptionProgTheory
exceptionProgTheory                                                                                                                                                                                                                                                                    OK
Starting work on fibProgTheory
exceptionArityTestProgTheory                                                                                                                                                                                                                                                           OK
Starting work on floyd_warshallProgTheory
arrayGlobalStateProgTheory                                                                                                                                                                                                                                                             OK
Starting work on helloProgTheory
arrayLocalStateProgTheory                                                                                                                                                                                                                                                              OK
Starting work on refStateProgTheory
fibProgTheory                                                                                                                                                                                                                                                                 FAILED! <1>
 Doing proof of: EqualityType STATE_EXN_TYPE
 Doing EqualityType proof via ONTO thm:error in quse /usr/local/google/home/ramanakumar/cakeml/regression-worker/cakeml-584/translator/monadic/examples/fibProgScript.sml : HOL_ERR {message = "not a comb", origin_function = "rand", origin_structure = "Term"}
 error in load fibProgScript : HOL_ERR {message = "not a comb", origin_function = "rand", origin_structure = "Term"}
  a. r. (a = num2state_exn r)  r < 1
 Proof of 
 
 EqualityType STATE_EXN_TYPE
 
 failed.
 Uncaught exception: HOL_ERR {message = "not a comb", origin_function = "rand", origin_structure = "Term"}
floyd_warshallProgTheory                                                                                                                                                                                                                                                         M-KILLED
helloProgTheory                                                                                                                                                                                                                                                                  M-KILLED
refStateProgTheory                                                                                                                                                                                                                                                               M-KILLED