Job 3317

CakeML:51d26ddf3668987f306a2dc2e0182c0b6b846bbe
  Mention Dlet flatLang simplification in release notes [Apr 28 20:22:17]
#1380 (remove-flatlang-decs)
Merging into:53fd5640a5e851cff67e9703a5d5eae800469dc4
  Merge pull request #1378 from CakeML/source-dlet-var [Apr 27 19:18:32]
HOL:77fad203c275899bfee21faf6d2d3a66e749d7e1
  patch no_sig_docs for asl-equiv [Apr 21 06:34:06]
Machine:pavlova

Apr 28 20:29:05 Claimed job
Apr 28 20:29:09 Reusing HOL
Apr 28 20:29:21 Starting developers
Apr 28 20:29:27 Finished developers                                               4s 137MB
Apr 28 20:29:27 Starting developers/bin
Apr 28 20:29:32 Finished developers/bin                                           3s  93MB
Apr 28 20:29:33 Starting misc
Apr 28 20:30:16 Finished misc                                                    41s   1GB
Apr 28 20:30:16 Starting compiler/proofs
Apr 28 21:30:59 Finished compiler/proofs                                    1h00m41s  10GB
Apr 28 21:31:00 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 29 03:25:52 Finished compiler/bootstrap/compilation/x64/64/proofs       5h54m51s  95GB
Apr 29 03:25:53 Starting semantics/ffi
Apr 29 03:26:05 Finished semantics/ffi                                           10s 564MB
Apr 29 03:26:06 Starting semantics
Apr 29 03:26:08 Finished semantics                                                1s  83MB
Apr 29 03:26:09 Starting semantics/proofs
Apr 29 03:26:30 Finished semantics/proofs                                        20s 732MB
Apr 29 03:26:31 Starting semantics/alt_semantics
Apr 29 03:26:48 Finished semantics/alt_semantics                                 16s 614MB
Apr 29 03:26:49 Starting semantics/alt_semantics/proofs
Apr 29 03:30:06 Finished semantics/alt_semantics/proofs                        3m16s   2GB
Apr 29 03:30:07 Starting basis/pure
Apr 29 03:30:09 Finished basis/pure                                               0s  76MB
Apr 29 03:30:10 Starting translator
Apr 29 03:31:17 Finished translator                                            1m06s   3GB
Apr 29 03:31:18 Starting compiler/parsing
Apr 29 03:31:20 Finished compiler/parsing                                         1s  88MB
Apr 29 03:31:20 Starting characteristic
Apr 29 03:31:23 Finished characteristic                                           1s 111MB
Apr 29 03:31:24 Starting translator/monadic
Apr 29 03:31:26 Finished translator/monadic                                       1s 106MB
Apr 29 03:31:30 Starting translator/monadic/monad_base
Apr 29 03:31:32 Finished translator/monadic/monad_base                            1s  78MB
Apr 29 03:31:32 Starting profiler
Apr 29 03:32:04 Finished profiler                                                30s   1GB
Apr 29 03:32:05 Starting basis
Apr 29 03:33:43 Finished basis                                                 1m37s   4GB
Apr 29 03:33:44 Starting compiler
Apr 29 03:33:47 Finished compiler                                                 2s 194MB
Apr 29 03:33:48 Starting compiler/inference
Apr 29 03:33:50 Finished compiler/inference                                       1s 105MB
Apr 29 03:33:51 Starting compiler/backend/reg_alloc
Apr 29 03:33:53 Finished compiler/backend/reg_alloc                               1s  83MB
Apr 29 03:33:54 Starting compiler/backend/gc
Apr 29 03:33:56 Finished compiler/backend/gc                                      1s 130MB
Apr 29 03:33:57 Starting compiler/backend
Apr 29 03:34:03 FAILED: compiler/backend
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)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/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/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 42 directories
Starting work on README.md
Starting work on flat_uncheck_ctorsTheory
README.md                                                           (0s)     OK
flat_uncheck_ctorsTheory                                            (2s)FAIL<1>
 <<HOL message: Created theory "flat_uncheck_ctors">>
 Saved definition ____ "compile_pat_def"
 Saved induction _____ "compile_pat_ind"
 Saved definition ____ "compile_def"
 Saved induction _____ "compile_ind"
 Saved theorem _______ "compile_length"
 Saved theorem _______ "compile_sing"
 Saved theorem _______ "compile_nil"
 Saved theorem _______ "compile_not_nil"
 Saved theorem _______ "compile_cons"
 Saved theorem _______ "compile_append"
 Saved theorem _______ "compile_reverse"
 Saved theorem _______ "compile_HD_sing"
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn: between line 106, character 2 and line 108, character 41:
 at Defn.parse_quote:
 at Term.prim_mk_const: "Dlet" not found in theory "flatLang"
 Full log: /scratch/cakeml/regression/cakeml-3317/compiler/backend/.hol/logs/flat_uncheck_ctorsTheory