Overview

Job 1760

CakeML:874bb72cf49d4a806eb88215b31da518ea5352f8
  Delay building of L3 equivalence proofs until needed
#858 (asl-equiv)
Merging into:5525b2dc1da264a4ad4d5b5dd23599b8fe8bafe3
  Use Definition.new_definition
HOL:1cb031bd28388f55c032c31177684989f80eda10
  emacs-mode: cope with deletion of copy-region-as-hol-definition-quietly
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               4s 151MB
 Starting developers/bin
 Finished developers/bin                                           5s 670MB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 234MB
 Starting semantics
 Finished semantics                                             1m30s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m52s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 13s 364MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m40s 777MB
 Starting basis/pure
 Finished basis/pure                                              54s 983MB
 Starting translator
 Finished translator                                            3m03s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m20s   2GB
 Starting characteristic
 Finished characteristic                                        6m11s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m50s   1GB
 Starting basis
 Finished basis                                                50m24s  13GB
 Starting compiler/inference
 Finished compiler/inference                                    1m13s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m10s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m47s   1GB
 Starting compiler/backend
 FAILED: compiler/backend
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)/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/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
Scanned 38 directories
Starting work on pattern_commonTheory
Starting work on README.md
Starting work on bviTheory
Starting work on data_liveTheory
README.md                                         compiler/backend  (0s)     OK
Starting work on data_simpTheory
pattern_commonTheory             compiler/backend/pattern_matching  (8s)     OK
Starting work on pattern_semanticsTheory
bviTheory                                         compiler/backend (11s)     OK
Starting work on data_spaceTheory
data_simpTheory                                   compiler/backend (11s)     OK
Starting work on bvi_letTheory
data_liveTheory                                   compiler/backend (15s)     OK
Starting work on bvi_tailrecTheory
pattern_semanticsTheory          compiler/backend/pattern_matching (13s)     OK
Starting work on pattern_compTheory
bvi_letTheory                                     compiler/backend (11s)     OK
Starting work on bvlTheory
data_spaceTheory                                  compiler/backend (16s)     OK
Starting work on bvi_to_dataTheory
bvlTheory                                         compiler/backend (11s)     OK
Starting work on bvl_constTheory
pattern_compTheory               compiler/backend/pattern_matching (15s)     OK
Finished $(CAKEMLDIR)/compiler/backend/pattern_matching [#theories: 3] (37.011s) 
Starting work on db_varsTheory
bvi_to_dataTheory                                 compiler/backend (18s)     OK
Starting work on bvl_jumpTheory
db_varsTheory                                     compiler/backend (11s)     OK
Starting work on clos_annotateTheory
bvl_jumpTheory                                    compiler/backend (11s)     OK
Starting work on clos_callTheory
bvi_tailrecTheory                                 compiler/backend (46s)     OK
Starting work on clos_fvsTheory
clos_annotateTheory                               compiler/backend (14s)     OK
Starting work on clos_letopTheory
clos_fvsTheory                                    compiler/backend (11s)     OK
Starting work on clos_opTheory
clos_callTheory                                   compiler/backend (15s)     OK
Starting work on clos_ticksTheory
clos_letopTheory                                  compiler/backend (12s)     OK
Starting work on clos_mtiTheory
clos_ticksTheory                                  compiler/backend (10s)     OK
Starting work on clos_numberTheory
clos_mtiTheory                                    compiler/backend (14s)     OK
Starting work on flatLangTheory
clos_numberTheory                                 compiler/backend (11s)     OK
Starting work on jsonLangTheory
bvl_constTheory                                   compiler/backend (73s)     OK
Starting work on bvl_handleTheory
flatLangTheory                                    compiler/backend (18s)     OK
Starting work on flat_to_closTheory
jsonLangTheory                                    compiler/backend (13s)     OK
Starting work on labLangTheory
clos_opTheory                                     compiler/backend (40s)     OK
Starting work on clos_knownTheory
bvl_handleTheory                                  compiler/backend (15s)     OK
Starting work on bvl_inlineTheory
labLangTheory                                     compiler/backend (12s)     OK
Starting work on lab_filterTheory
flat_to_closTheory                                compiler/backend (17s)     OK
Starting work on displayLangTheory
clos_knownTheory                                  compiler/backend (15s)FAIL<1>
 Exception raised at Tactical.FIRST_ASSUM:
 
 
 Exception raised at TotalDefn.tDefine:
 at Defn.tprove:
 at Tactical.FIRST_ASSUM:
 
 error in quse /home/cake/oven/regression/cakeml-1760/compiler/backend/clos_knownScript.sml : HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
 error in load /home/cake/oven/regression/cakeml-1760/compiler/backend/clos_knownScript : HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.tprove:\nat Tactical.FIRST_ASSUM:\n", origin_function = "tDefine", origin_structure = "TotalDefn"}
bvl_inlineTheory                                  compiler/backend  (5s)MKILLED
lab_filterTheory                                  compiler/backend  (2s)MKILLED
displayLangTheory                                 compiler/backend  (0s)MKILLED