CakeML Regression Test

Job 1681

CakeML:fed59d356e45c8e9b580f79aaa6e510391dc9305
  Remove code that breaks now some real theories are not ancestors [Dec 08 23:53:02]
HOL:c51de550191d516cb9dfe47c6a1e866b232f2c96
  Remove another use of .. that causes grammar precedence problems [Dec 09 23:13:20]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 10 07:25:15 Claimed job
Dec 10 07:25:24 Building HOL
Dec 10 07:35:27 Starting developers
Dec 10 07:35:32 Finished developers                                               4s 147MB
Dec 10 07:35:32 Starting developers/bin
Dec 10 07:35:39 Finished developers/bin                                           6s   1GB
Dec 10 07:35:39 Starting semantics/ffi
Dec 10 07:35:48 Finished semantics/ffi                                            8s 213MB
Dec 10 07:35:48 Starting semantics
Dec 10 07:37:25 Finished semantics                                             1m36s   1GB
Dec 10 07:37:25 Starting semantics/proofs
Dec 10 07:41:16 Finished semantics/proofs                                      3m50s   1GB
Dec 10 07:41:16 Starting semantics/alt_semantics
Dec 10 07:41:28 Finished semantics/alt_semantics                                 11s 357MB
Dec 10 07:41:28 Starting semantics/alt_semantics/proofs
Dec 10 07:44:06 Finished semantics/alt_semantics/proofs                        2m36s 827MB
Dec 10 07:44:06 Starting basis/pure
Dec 10 07:47:15 Finished basis/pure                                            3m09s 976MB
Dec 10 07:47:16 Starting translator
Dec 10 07:50:15 Finished translator                                            2m58s   1GB
Dec 10 07:50:15 Starting compiler/parsing
Dec 10 07:51:34 Finished compiler/parsing                                      1m19s   1GB
Dec 10 07:51:35 Starting characteristic
Dec 10 07:57:27 Finished characteristic                                        5m52s   1GB
Dec 10 07:57:27 Starting translator/monadic
Dec 10 07:59:09 Finished translator/monadic                                    1m41s   1GB
Dec 10 07:59:09 Starting basis
Dec 10 08:47:59 Finished basis                                                48m48s  15GB
Dec 10 08:47:59 Starting compiler/inference
Dec 10 08:49:16 Finished compiler/inference                                    1m17s   1GB
Dec 10 08:49:16 Starting compiler/backend/reg_alloc
Dec 10 08:50:25 Finished compiler/backend/reg_alloc                            1m08s   1GB
Dec 10 08:50:25 Starting compiler/backend/gc
Dec 10 08:54:11 Finished compiler/backend/gc                                   3m46s   2GB
Dec 10 08:54:11 Starting compiler/backend
Dec 10 08:58:57 Finished compiler/backend                                      4m45s   1GB
Dec 10 08:58:58 Starting compiler/encoders/asm
Dec 10 08:59:21 Finished compiler/encoders/asm                                   23s 678MB
Dec 10 08:59:22 Starting compiler/encoders/x64
Dec 10 09:00:27 Finished compiler/encoders/x64                                 1m04s   1GB
Dec 10 09:00:27 Starting compiler/encoders/arm7
Dec 10 09:02:40 Finished compiler/encoders/arm7                                2m12s   1GB
Dec 10 09:02:40 Starting compiler/encoders/arm8
Dec 10 09:03:19 Finished compiler/encoders/arm8                                  39s 914MB
Dec 10 09:03:19 Starting compiler/encoders/mips
Dec 10 09:04:56 Finished compiler/encoders/mips                                1m36s   1GB
Dec 10 09:04:56 Starting compiler/encoders/riscv
Dec 10 09:06:51 Finished compiler/encoders/riscv                               1m54s   1GB
Dec 10 09:06:51 Starting compiler/encoders/ag32
Dec 10 09:07:10 Finished compiler/encoders/ag32                                  18s 809MB
Dec 10 09:07:10 Starting compiler/backend/x64
Dec 10 09:07:31 Finished compiler/backend/x64                                    20s   1GB
Dec 10 09:07:31 Starting compiler/backend/arm7
Dec 10 09:07:52 Finished compiler/backend/arm7                                   21s   1GB
Dec 10 09:07:53 Starting compiler/backend/arm8
Dec 10 09:08:13 Finished compiler/backend/arm8                                   20s   1GB
Dec 10 09:08:13 Starting compiler/backend/mips
Dec 10 09:08:33 Finished compiler/backend/mips                                   19s   1GB
Dec 10 09:08:33 Starting compiler/backend/riscv
Dec 10 09:08:54 Finished compiler/backend/riscv                                  20s   1GB
Dec 10 09:08:54 Starting compiler/backend/ag32
Dec 10 09:10:06 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 10 09:10:06 Starting compiler/parsing/proofs
Dec 10 09:14:05 Finished compiler/parsing/proofs                               3m58s   1GB
Dec 10 09:14:06 Starting compiler/inference/proofs
Dec 10 09:16:37 Finished compiler/inference/proofs                             2m31s   1GB
Dec 10 09:16:38 Starting compiler/backend/semantics
Dec 10 09:49:28 Finished compiler/backend/semantics                           32m50s   2GB
Dec 10 09:49:29 Starting compiler/backend/reg_alloc/proofs
Dec 10 09:53:14 Finished compiler/backend/reg_alloc/proofs                     3m45s 872MB
Dec 10 09:53:15 Starting compiler/backend/proofs
Dec 10 10:04:22 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)/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)/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/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
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  (0s)     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                       compiler/backend/proofs (14s)     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                      compiler/backend/proofs (26s)     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                         compiler/backend/proofs (18s)     OK
Starting work on clos_annotateProofTheory
clos_annotateProofTheory                   compiler/backend/proofs (27s)     OK
Starting work on clos_callProofTheory
data_liveProofTheory                       compiler/backend/proofs (76s)     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                       compiler/backend/proofs(109s)     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                      compiler/backend/proofs (19s)     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                      compiler/backend/proofs (32s)     OK
Starting work on clos_fvsProofTheory
bvi_tailrecProofTheory                     compiler/backend/proofs(193s)     OK
Starting work on bvl_to_bviProofTheory
clos_fvsProofTheory                        compiler/backend/proofs (16s)     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                      compiler/backend/proofs (10s)     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                     compiler/backend/proofs(139s)     OK
Starting work on clos_opProofTheory
clos_letopProofTheory                      compiler/backend/proofs (17s)     OK
Starting work on clos_ticksProofTheory
clos_opProofTheory                         compiler/backend/proofs (22s)     OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory                      compiler/backend/proofs (23s)     OK
Starting work on clos_knownProofTheory
clos_callProofTheory                       compiler/backend/proofs(175s)     OK
Starting work on clos_numberProofTheory
clos_mtiProofTheory                        compiler/backend/proofs (33s)     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                     compiler/backend/proofs (26s)     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                        compiler/backend/proofs  (9s)     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                       compiler/backend/proofs (55s)     OK
Starting work on word_gcFunctionsTheory
word_gcFunctionsTheory                     compiler/backend/proofs (31s)     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                      compiler/backend/proofs(198s)     OK
Starting work on word_allocProofTheory
clos_knownProofTheory                      compiler/backend/proofs(140s)     OK
Starting work on clos_to_bvlProofTheory
word_bignumProofTheory                     compiler/backend/proofs(212s)     OK
Starting work on word_instProofTheory
word_instProofTheory                       compiler/backend/proofs (54s)     OK
Starting work on word_removeProofTheory
word_removeProofTheory                     compiler/backend/proofs (30s)     OK
Starting work on word_depthProofTheory
clos_to_bvlProofTheory                     compiler/backend/proofs(210s)     OK
Starting work on flat_patternProofTheory
flat_patternProofTheory                    compiler/backend/proofs (42s)     OK
Starting work on flat_to_closProofTheory
word_depthProofTheory                      compiler/backend/proofs (66s)FAIL<1>
 res  SOME Error  subspt funs s.code 
 option_le s1.stack_max
   (OPTION_MAP2 MAX s.stack_max
      (OPTION_MAP2 $+ s.locals_size
         (OPTION_MAP2 $+ (stack_size s.stack)
            (max_depth s.stack_size (full_call_graph dest funs)))))
 
 failed.
 Failed to prove theorem max_depth_Call_SOME.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 851)", origin_function = "THEN1", origin_structure = "Tactical"}
data_to_word_memoryProofTheory             compiler/backend/proofs(285s)MKILLED
word_allocProofTheory                      compiler/backend/proofs(261s)MKILLED
flat_to_closProofTheory                    compiler/backend/proofs  (7s)MKILLED