CakeML Regression Test

Job 3648

CakeML:f2063c9bd97a25993921da7d370ed5714ddba24a
  Merge pull request #1561 from CakeML/ptr-eq-wordlang [Oct 26 19:43:41]
HOL:9783a49979c94c401ff8c0e51b2eefae7ea95ae3
  RecordType: name the variables of the record cases proof [Oct 26 22:48:32]
Machine:fairybread

Oct 27 02:08:42 Claimed job
Oct 27 02:08:48 Building HOL
Oct 27 02:20:32 Starting developers
Oct 27 02:21:32 Finished developers                                              58s   1GB
Oct 27 02:21:33 Starting developers/bin
Oct 27 02:21:42 Finished developers/bin                                           8s   1GB
Oct 27 02:21:43 Starting misc
Oct 27 02:22:37 Finished misc                                                    52s   1GB
Oct 27 02:22:38 Starting compiler/proofs
Oct 27 02:25:26 FAILED: compiler/proofs
  HOLORIG=/scratch/regbox/regression2/cakeml-3648/compiler/proofs [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/parser
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/tests
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64/64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/32
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/decompiler
Scanning $(CAKEMLDIR)/pancake/decompiler/examples
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(hwmcc_checker)/compilation
Scanning $(hwmcc_checker)/compilation/proofs
Scanning $(hwmcc_checker)/examples
Scanning $(hwmcc_checker)/translation
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanned 313 directories
Building 363 theory files
Starting work on spt_closureTheory
Starting work on balanced_mapTheory
Starting work on NTpropertiesTheory
Starting work on FormalLangTheory
spt_closureTheory            $(HOLDIR)/examples/algorithms  (1s)  [362]     OK
Starting work on charsetTheory
Finished $(HOLDIR)/examples/algorithms [#theories: 1]                  (1.960s) 
FormalLangTheory       $(HOLDIR)/examples/formal-languages  (3s)  [361]     OK
Starting work on vec_mapTheory
Finished $(HOLDIR)/examples/formal-languages [#theories: 1]            (3.660s) 
NTpropertiesTheory              $(HOLDIR)/.../context-free  (4s)  [360]     OK
Starting work on temporalTheory
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1] (4.930s) 
vec_mapTheory  $(HOLDIR)/examples/formal-languages/regular  (1s)  [359]     OK
Starting work on utilsLibSupportTheory
temporalTheory     $(HOLDIR)/.../machine-code/hoare-triple  (2s)  [358]     OK
Starting work on armTheory
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]   (2.380s) 
Finished $(HOLDIR)/examples/l3-machine-code/lib                        (0.000s) 
utilsLibSupportTheory $(HOLDIR)/.../l3-machine-code/common  (2s)  [357]     OK
Starting work on arm8Theory
Finished $(HOLDIR)/examples/l3-machine-code/common [#theories: 1]      (2.190s) 
charsetTheory  $(HOLDIR)/examples/formal-languages/regular  (9s)  [356]     OK
Starting work on regexpTheory
arm8Theory   $(HOLDIR)/examples/l3-machine-code/arm8/model (13s)  [355]     OK
Starting work on decompilerLibSupportTheory
Finished $(HOLDIR)/examples/l3-machine-code/arm8/model [#theories: 1] (13.450s) 
regexpTheory   $(HOLDIR)/examples/formal-languages/regular (12s)  [354]     OK
Starting work on mipsTheory
decompilerLibSupportTheory        $(HOLDIR)/.../decompiler  (1s)  [353]     OK
Starting work on l3-heap
Finished $(HOLDIR)/examples/machine-code/decompiler [#theories: 1]     (1.860s) 
l3-heap                 $(HOLDIR)/examples/l3-machine-code (20s)             OK
Finished $(HOLDIR)/examples/l3-machine-code                           (20.720s) 
Starting work on arm8-heap
armTheory     $(HOLDIR)/examples/l3-machine-code/arm/model (30s)  [352]     OK
Starting work on riscvTheory
Finished $(HOLDIR)/examples/l3-machine-code/arm/model [#theories: 1]  (30.830s) 
arm8-heap     $(HOLDIR)/examples/l3-machine-code/arm8/step (20s)             OK
Starting work on arm8_stepTheory
arm8_stepTheory    $(HOLDIR)/.../l3-machine-code/arm8/step  (4s)  [351]     OK
Starting work on x64Theory
Finished $(HOLDIR)/examples/l3-machine-code/arm8/step [#theories: 1]  (25.120s) 
mipsTheory   $(HOLDIR)/examples/l3-machine-code/mips/model (26s)  [350]     OK
Starting work on multiwordTheory
Finished $(HOLDIR)/examples/l3-machine-code/mips/model [#theories: 1] (26.610s) 
x64Theory     $(HOLDIR)/examples/l3-machine-code/x64/model (17s)  [349]     OK
Starting work on MarshallingTheory
Finished $(HOLDIR)/examples/l3-machine-code/x64/model [#theories: 1]  (17.620s) 
MarshallingTheory                       $(CAKEMLDIR)/basis  (3s)  [348]     OK
Starting work on mllistTheory
multiwordTheory  $(HOLDIR)/examples/machine-code/multiword (18s)  [347]     OK
Starting work on mc_multiwordTheory
mllistTheory                       $(CAKEMLDIR)/basis/pure  (3s)  [346]     OK
Starting work on mlstringTheory
balanced_mapTheory              $(HOLDIR)/.../balanced_bst (78s)  [345]     OK
Starting work on osetTheory
riscvTheory $(HOLDIR)/examples/l3-machine-code/riscv/model (36s)  [344]     OK
Starting work on mlmapTheory
Finished $(HOLDIR)/examples/l3-machine-code/riscv/model [#theories: 1] (36.340s) 
mlstringTheory                     $(CAKEMLDIR)/basis/pure  (6s)  [343]     OK
Starting work on mlsexpTheory
osetTheory $(HOLDIR)/examples/data-structures/balanced_bst  (4s)  [342]     OK
Starting work on regexp_mapTheory
Finished $(HOLDIR)/examples/data-structures/balanced_bst [#theories: 2] (82.590s) 
mlmapTheory                        $(CAKEMLDIR)/basis/pure  (3s)  [341]     OK
Starting work on mloptionTheory
mloptionTheory                     $(CAKEMLDIR)/basis/pure  (1s)  [340]     OK
Starting work on mlsetTheory
regexp_mapTheory    $(HOLDIR)/.../formal-languages/regular  (4s)  [339]     OK
Starting work on regexp_compilerTheory
mlsetTheory                        $(CAKEMLDIR)/basis/pure  (2s)  [338]     OK
Starting work on cfFFITypeTheory
cfFFITypeTheory                $(CAKEMLDIR)/characteristic  (2s)  [337]     OK
Starting work on db_varsTheory
db_varsTheory                $(CAKEMLDIR)/compiler/backend  (2s)  [336]     OK
Starting work on parmoveTheory
regexp_compilerTheory                $(HOLDIR)/.../regular (12s)  [335]     OK
Starting work on mlvectorTheory
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 5]   (39.540s) 
mc_multiwordTheory    $(HOLDIR)/.../machine-code/multiword (29s)  [334]     OK
Starting work on riscv-heap
Finished $(HOLDIR)/examples/machine-code/multiword [#theories: 2]     (47.670s) 
mlvectorTheory                     $(CAKEMLDIR)/basis/pure  (3s)  [333]     OK
Starting work on mlintTheory
riscv-heap   $(HOLDIR)/examples/l3-machine-code/riscv/step (19s)             OK
Starting work on riscv_stepTheory
mlintTheory                        $(CAKEMLDIR)/basis/pure  (6s)  [332]     OK
Starting work on mlprettyprinterTheory
mlprettyprinterTheory              $(CAKEMLDIR)/basis/pure  (3s)  [331]     OK
Starting work on mlratTheory
parmoveTheory      $(CAKEMLDIR)/compiler/backend/reg_alloc (21s)  [330]     OK
Starting work on jsonLangTheory
mlratTheory                        $(CAKEMLDIR)/basis/pure  (4s)  [329]     OK
Starting work on exportTheory
jsonLangTheory               $(CAKEMLDIR)/compiler/backend  (2s)  [328]     OK
Starting work on namespaceTheory
namespaceTheory                     $(CAKEMLDIR)/semantics  (0s)  [327]     OK
Starting work on astTheory
exportTheory                 $(CAKEMLDIR)/compiler/backend  (3s)  [326]     OK
Starting work on tokensTheory
astTheory                           $(CAKEMLDIR)/semantics  (5s)  [325]     OK
Starting work on source_dceTheory
tokensTheory                        $(CAKEMLDIR)/semantics  (4s)  [324]     OK
Starting work on source_letTheory
source_letTheory             $(CAKEMLDIR)/compiler/backend  (2s)  [323]     OK
Starting work on asmTheory
source_dceTheory             $(CAKEMLDIR)/compiler/backend  (4s)  [322]     OK
Starting work on source_lift_constsTheory
riscv_stepTheory  $(HOLDIR)/.../l3-machine-code/riscv/step (27s)  [321]     OK
Starting work on fpSemTheory
Finished $(HOLDIR)/examples/l3-machine-code/riscv/step [#theories: 1] (47.010s) 
fpSemTheory                         $(CAKEMLDIR)/semantics  (1s)  [320]     OK
Starting work on lexer_funTheory
source_lift_constsTheory     $(CAKEMLDIR)/compiler/backend  (8s)  [319]     OK
Starting work on source_to_sourceTheory
asmTheory               $(CAKEMLDIR)/compiler/encoders/asm  (9s)  [318]     OK
Starting work on backend_commonTheory
source_to_sourceTheory       $(CAKEMLDIR)/compiler/backend  (2s)  [317]     OK
Starting work on asmSemTheory
backend_commonTheory         $(CAKEMLDIR)/compiler/backend  (4s)  [316]     OK
Starting work on closLangTheory
lexer_funTheory                     $(CAKEMLDIR)/semantics  (8s)  [315]     OK
Starting work on stackLangTheory
closLangTheory               $(CAKEMLDIR)/compiler/backend  (4s)        FAIL<1>
mlsexpTheory                       $(CAKEMLDIR)/basis/pure (67s)         killed
asmSemTheory            $(CAKEMLDIR)/compiler/encoders/asm  (7s)         killed
stackLangTheory              $(CAKEMLDIR)/compiler/backend  (4s)         killed
*** Holmake aborted - 1 target failed:
*** closLangTheory in $(CAKEMLDIR)/compiler/backend (status 1)
 Saved theorem _______ "glob_op_size_def"
 Saved theorem _______ "datatype_glob_op"
 Saved theorem _______ "glob_op_11"
 Saved theorem _______ "glob_op_distinct"
 Saved theorem _______ "glob_op_nchotomy"
 Saved theorem _______ "glob_op_Axiom"
 Saved theorem _______ "glob_op_induction"
 Saved theorem _______ "glob_op_case_cong"
 Saved theorem _______ "glob_op_case_eq"
 <<HOL message: Defined type: "glob_op">>
 Saved theorem _______ "mem_op_size_def"
 Saved theorem _______ "datatype_mem_op"
 Saved theorem _______ "mem_op_11"
 Saved theorem _______ "mem_op_distinct"
 Saved theorem _______ "mem_op_nchotomy"
 Saved theorem _______ "mem_op_Axiom"
 Saved theorem _______ "mem_op_induction"
 Saved theorem _______ "mem_op_case_cong"
 Saved theorem _______ "mem_op_case_eq"
 <<HOL message: Defined type: "mem_op">>
 Saved theorem _______ "op_size_def"
 Saved theorem _______ "datatype_op"
 Saved theorem _______ "op_11"
 Saved theorem _______ "op_distinct"
 Saved theorem _______ "op_nchotomy"
 Saved theorem _______ "op_Axiom"
 Saved theorem _______ "op_induction"
 Saved theorem _______ "op_case_cong"
 Saved theorem _______ "op_case_eq"
 <<HOL message: Defined type: "op">>
 Saved theorem _______ "exp_size_def"
 Saved theorem _______ "datatype_exp"
 Saved theorem _______ "exp_11"
 Saved theorem _______ "exp_distinct"
 Saved theorem _______ "exp_nchotomy"
 Saved theorem _______ "exp_Axiom"
 Saved theorem _______ "exp_induction"
 Saved theorem _______ "exp_case_cong"
 Saved theorem _______ "exp_case_eq"
 <<HOL message: Defined type: "exp">>
 <<HOL warning: Context.snapshot: ambient context read while a proof was running (in closLang)>>
 Saved definition ____ "has_install_def"
 Saved induction _____ "has_install_ind"
 Proof of 
 
 fns n x. MEM (n,x) fns  exp_size x < exp1_size fns
 
 failed.
 Tactic failure proving "exp1_size_lemma"; heap saved to closLang.exp1_size_lemma.dumpedheap.
 Resume with: bin/hol --holstate=closLang.exp1_size_lemma.dumpedheap
 Full log: /scratch/regbox/regression2/cakeml-3648/compiler/backend/.hol/logs/closLangTheory