CakeML Regression Test

Job 1979

CakeML:c6c9b176da407ad8178a26a707df2df6df991f80
  Rename a couple of example scripts away from doubleProg name [Sep 12 04:41:05]
HOL:6d032bf33d3633d210f8817c9e769ae66be444aa
  Fix sttVariants given ancestry change in stt example [Sep 09 06:53:04]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Sep 12 04:54:12 Claimed job
Sep 12 04:54:15 Building HOL
Sep 12 05:06:35 Starting developers
Sep 12 05:06:40 Finished developers                                               5s  95MB
Sep 12 05:06:40 Starting developers/bin
Sep 12 05:08:20 Finished developers/bin                                        1m39s   1GB
Sep 12 05:08:20 Starting semantics/ffi
Sep 12 05:08:29 Finished semantics/ffi                                            9s 199MB
Sep 12 05:08:30 Starting semantics
Sep 12 05:11:13 Finished semantics                                             2m43s   1GB
Sep 12 05:11:13 Starting semantics/proofs
Sep 12 05:20:16 Finished semantics/proofs                                      9m01s   1GB
Sep 12 05:20:16 Starting semantics/alt_semantics
Sep 12 05:20:44 Finished semantics/alt_semantics                                 27s 653MB
Sep 12 05:20:44 Starting semantics/alt_semantics/proofs
Sep 12 05:36:51 Finished semantics/alt_semantics/proofs                       16m06s   2GB
Sep 12 05:36:52 Starting basis/pure
Sep 12 05:40:47 Finished basis/pure                                            3m54s 832MB
Sep 12 05:40:47 Starting translator
Sep 12 05:48:39 Finished translator                                            7m51s   3GB
Sep 12 05:48:39 Starting compiler/parsing
Sep 12 05:50:16 Finished compiler/parsing                                      1m36s   4GB
Sep 12 05:50:16 Starting characteristic
Sep 12 05:57:40 Finished characteristic                                        7m23s   2GB
Sep 12 05:57:40 Starting translator/monadic
Sep 12 05:59:41 Finished translator/monadic                                    2m01s   1GB
Sep 12 05:59:42 Starting basis
Sep 12 06:55:04 Finished basis                                                55m21s  15GB
Sep 12 06:55:04 Starting compiler/inference
Sep 12 06:56:46 Finished compiler/inference                                    1m42s   1GB
Sep 12 06:56:47 Starting compiler/backend/reg_alloc
Sep 12 06:58:33 Finished compiler/backend/reg_alloc                            1m46s   1GB
Sep 12 06:58:34 Starting compiler/backend/gc
Sep 12 07:03:13 Finished compiler/backend/gc                                   4m38s   1GB
Sep 12 07:03:13 Starting compiler/backend
Sep 12 07:09:13 Finished compiler/backend                                      6m00s   2GB
Sep 12 07:09:13 Starting compiler/encoders/asm
Sep 12 07:09:44 Finished compiler/encoders/asm                                   30s 893MB
Sep 12 07:09:44 Starting compiler/encoders/x64
Sep 12 07:10:54 Finished compiler/encoders/x64                                 1m09s 710MB
Sep 12 07:10:55 Starting compiler/encoders/arm7
Sep 12 07:13:13 Finished compiler/encoders/arm7                                2m18s   1GB
Sep 12 07:13:14 Starting compiler/encoders/arm8
Sep 12 07:13:58 Finished compiler/encoders/arm8                                  43s 785MB
Sep 12 07:13:58 Starting compiler/encoders/arm8_asl
Sep 12 09:43:10 Finished compiler/encoders/arm8_asl                         2h29m10s  30GB
Sep 12 09:43:11 Starting compiler/encoders/mips
Sep 12 09:44:54 Finished compiler/encoders/mips                                1m42s   1GB
Sep 12 09:44:54 Starting compiler/encoders/riscv
Sep 12 09:46:55 Finished compiler/encoders/riscv                               2m00s 974MB
Sep 12 09:46:55 Starting compiler/encoders/ag32
Sep 12 09:47:16 Finished compiler/encoders/ag32                                  21s 903MB
Sep 12 09:47:17 Starting compiler/backend/x64
Sep 12 09:47:38 Finished compiler/backend/x64                                    21s   1GB
Sep 12 09:47:38 Starting compiler/backend/arm7
Sep 12 09:48:02 Finished compiler/backend/arm7                                   23s   1GB
Sep 12 09:48:02 Starting compiler/backend/arm8
Sep 12 09:48:24 Finished compiler/backend/arm8                                   20s   1GB
Sep 12 09:48:24 Starting compiler/backend/mips
Sep 12 09:48:46 Finished compiler/backend/mips                                   22s   1GB
Sep 12 09:48:47 Starting compiler/backend/riscv
Sep 12 09:49:09 Finished compiler/backend/riscv                                  21s   1GB
Sep 12 09:49:09 Starting compiler/backend/ag32
Sep 12 09:50:40 Finished compiler/backend/ag32                                 1m30s   1GB
Sep 12 09:50:40 Starting compiler/parsing/proofs
Sep 12 09:55:02 Finished compiler/parsing/proofs                               4m21s   1GB
Sep 12 09:55:02 Starting compiler/inference/proofs
Sep 12 09:58:01 Finished compiler/inference/proofs                             2m58s   1GB
Sep 12 09:58:01 Starting compiler/backend/semantics
Sep 12 10:28:47 Finished compiler/backend/semantics                           30m46s   2GB
Sep 12 10:28:47 Starting compiler/backend/reg_alloc/proofs
Sep 12 10:32:50 Finished compiler/backend/reg_alloc/proofs                     4m02s   1GB
Sep 12 10:32:50 Starting compiler/backend/proofs
Sep 12 10:44:26 FAILED: compiler/backend/proofs
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
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/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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/hol88
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)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanned 48 directories
Finished $(CAKEMLDIR)/misc                                             (0.000s) 
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
README.md                                  compiler/backend/proofs  (1s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                       compiler/backend/proofs (14s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                      compiler/backend/proofs (30s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                         compiler/backend/proofs (22s)     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                       compiler/backend/proofs (91s)     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                       compiler/backend/proofs(117s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                      compiler/backend/proofs (21s)     OK
Starting work on bvl_inlineProofTheory
clos_annotateProofTheory                   compiler/backend/proofs(102s)     OK
Starting work on clos_callProofTheory
bvl_inlineProofTheory                      compiler/backend/proofs (38s)     OK
Starting work on clos_fvsProofTheory
bvi_tailrecProofTheory                     compiler/backend/proofs(205s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                        compiler/backend/proofs (18s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                      compiler/backend/proofs (11s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                     compiler/backend/proofs(151s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                      compiler/backend/proofs (19s)     OK
Starting work on clos_ticksProofTheory
clos_ticksProofTheory                      compiler/backend/proofs (27s)     OK
Starting work on clos_mtiProofTheory
clos_opProofTheory                         compiler/backend/proofs (46s)     OK
Starting work on clos_knownProofTheory
clos_mtiProofTheory                        compiler/backend/proofs (36s)     OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                     compiler/backend/proofs (28s)     OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                        compiler/backend/proofs  (9s)     OK
Starting work on clos_constantProofTheory
clos_constantProofTheory                   compiler/backend/proofs (30s)     OK
Starting work on word_simpProofTheory
clos_callProofTheory                       compiler/backend/proofs(244s)     OK
Starting work on word_bignumProofTheory
bvl_to_bviProofTheory                      compiler/backend/proofs(214s)     OK
Starting work on word_allocProofTheory
word_simpProofTheory                       compiler/backend/proofs (62s)     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                      compiler/backend/proofs(192s)     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                     compiler/backend/proofs (42s)     OK
Starting work on data_to_word_memoryProofTheory
word_bignumProofTheory                     compiler/backend/proofs(233s)     OK
Starting work on word_instProofTheory
word_allocProofTheory                      compiler/backend/proofs(258s)FAIL<1>
 Saved definition ____ "ssa_map_ok_def"
 /home/cake/oven/regression/cakeml-1979/compiler/backend/proofs/word_allocProofScript.sml:3778: warning: Pattern is not exhaustive. Found near val (_, [al, ...]) = strip_comb tm
 error in quse /home/cake/oven/regression/cakeml-1979/compiler/backend/proofs/word_allocProofScript.sml : HOL_ERR {message = "not a \"!\"", origin_function = "dest_forall", origin_structure = "boolSyntax"}
 error in load /home/cake/oven/regression/cakeml-1979/compiler/backend/proofs/word_allocProofScript : HOL_ERR {message = "not a \"!\"", origin_function = "dest_forall", origin_structure = "boolSyntax"}
 Proof of 
 
 is_alloc_var na  is_stack_var (na + 2)
 
 failed.
 Uncaught exception: HOL_ERR {message = "not a \"!\"", origin_function = "dest_forall", origin_structure = "boolSyntax"}
clos_to_bvlProofTheory                     compiler/backend/proofs(193s)MKILLED
data_to_word_memoryProofTheory             compiler/backend/proofs(185s)MKILLED
word_instProofTheory                       compiler/backend/proofs (37s)MKILLED