Job 3079

CakeML:27abb4bf32ff72cd5f024c6ec124f67b3b69e044
  Remove mention of str_treeTheory [Dec 17 11:15:32]
#1280 (mlsexp)
Merging into:3c7122a14a373c06ab0fd744837c8be8069a5bfc
  Merge pull request #1276 from CakeML/checkthm_fastbuild [Dec 10 08:15:00]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:timtam

Dec 17 12:08:52 Claimed job
Dec 17 12:08:56 Reusing HOL
Dec 17 12:09:03 Starting developers
Dec 17 12:09:08 Finished developers                                               3s 223MB
Dec 17 12:09:09 Starting developers/bin
Dec 17 12:09:13 Finished developers/bin                                           3s  91MB
Dec 17 12:09:14 Starting misc
Dec 17 12:09:53 Finished misc                                                    38s   1GB
Dec 17 12:09:54 Starting compiler/proofs
Dec 17 13:08:05 Finished compiler/proofs                                      58m09s  12GB
Dec 17 13:08:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 17 18:45:46 Finished compiler/bootstrap/compilation/x64/64/proofs       5h37m38s 101GB
Dec 17 18:45:47 Starting semantics/ffi
Dec 17 18:45:56 Finished semantics/ffi                                            8s 518MB
Dec 17 18:45:57 Starting semantics
Dec 17 18:45:59 Finished semantics                                                0s  63MB
Dec 17 18:46:00 Starting semantics/proofs
Dec 17 18:46:21 Finished semantics/proofs                                        20s 722MB
Dec 17 18:46:22 Starting semantics/alt_semantics
Dec 17 18:46:39 Finished semantics/alt_semantics                                 16s 714MB
Dec 17 18:46:40 Starting semantics/alt_semantics/proofs
Dec 17 18:50:25 Finished semantics/alt_semantics/proofs                        3m45s   1GB
Dec 17 18:50:26 Starting basis/pure
Dec 17 18:50:28 Finished basis/pure                                               0s  93MB
Dec 17 18:50:29 Starting translator
Dec 17 18:51:28 Finished translator                                              58s   2GB
Dec 17 18:51:29 Starting compiler/parsing
Dec 17 18:51:30 Finished compiler/parsing                                         0s  70MB
Dec 17 18:51:31 Starting characteristic
Dec 17 18:51:33 Finished characteristic                                           1s 110MB
Dec 17 18:51:34 Starting translator/monadic
Dec 17 18:51:36 Finished translator/monadic                                       1s 120MB
Dec 17 18:51:37 Starting translator/monadic/monad_base
Dec 17 18:51:39 Finished translator/monadic/monad_base                            0s  64MB
Dec 17 18:51:39 Starting profiler
Dec 17 18:52:03 Finished profiler                                                23s   1GB
Dec 17 18:52:04 Starting basis
Dec 17 18:53:30 Finished basis                                                 1m24s   4GB
Dec 17 18:53:30 Starting compiler
Dec 17 18:53:33 Finished compiler                                                 2s 215MB
Dec 17 18:53:34 Starting compiler/inference
Dec 17 18:53:36 Finished compiler/inference                                       1s 110MB
Dec 17 18:53:37 Starting compiler/backend/reg_alloc
Dec 17 18:53:39 Finished compiler/backend/reg_alloc                               0s  92MB
Dec 17 18:53:40 Starting compiler/backend/gc
Dec 17 18:53:42 Finished compiler/backend/gc                                      1s 143MB
Dec 17 18:53:43 Starting compiler/backend
Dec 17 18:53:48 Finished compiler/backend                                         4s 269MB
Dec 17 18:53:49 Starting compiler/encoders/asm
Dec 17 18:53:51 Finished compiler/encoders/asm                                    0s  95MB
Dec 17 18:53:52 Starting compiler/encoders/x64
Dec 17 18:53:53 Finished compiler/encoders/x64                                    0s  94MB
Dec 17 18:53:54 Starting compiler/encoders/arm7
Dec 17 18:53:56 Finished compiler/encoders/arm7                                   0s  90MB
Dec 17 18:53:57 Starting compiler/encoders/arm8
Dec 17 18:53:58 Finished compiler/encoders/arm8                                   0s  94MB
Dec 17 18:53:59 Starting compiler/encoders/arm8_asl
Dec 17 18:54:12 Finished compiler/encoders/arm8_asl                              12s   1GB
Dec 17 18:54:13 Starting compiler/encoders/mips
Dec 17 18:54:15 Finished compiler/encoders/mips                                   0s  95MB
Dec 17 18:54:16 Starting compiler/encoders/riscv
Dec 17 18:54:17 Finished compiler/encoders/riscv                                  0s  95MB
Dec 17 18:54:18 Starting compiler/encoders/ag32
Dec 17 18:54:20 Finished compiler/encoders/ag32                                   0s  90MB
Dec 17 18:54:21 Starting compiler/encoders/tests
Dec 17 18:54:23 Finished compiler/encoders/tests                                  1s 106MB
Dec 17 18:54:24 Starting compiler/encoders/monadic_enc
Dec 17 18:54:42 Finished compiler/encoders/monadic_enc                           17s   1GB
Dec 17 18:54:43 Starting compiler/backend/x64
Dec 17 18:54:45 Finished compiler/backend/x64                                     1s 140MB
Dec 17 18:54:46 Starting compiler/backend/arm7
Dec 17 18:54:48 Finished compiler/backend/arm7                                    1s 140MB
Dec 17 18:54:49 Starting compiler/backend/arm8
Dec 17 18:54:51 Finished compiler/backend/arm8                                    1s 140MB
Dec 17 18:54:52 Starting compiler/backend/mips
Dec 17 18:54:55 Finished compiler/backend/mips                                    1s 140MB
Dec 17 18:54:55 Starting compiler/backend/riscv
Dec 17 18:54:58 Finished compiler/backend/riscv                                   1s 140MB
Dec 17 18:54:58 Starting compiler/backend/ag32
Dec 17 18:55:54 Finished compiler/backend/ag32                                   54s   2GB
Dec 17 18:55:55 Starting compiler/backend/pattern_matching
Dec 17 18:55:56 Finished compiler/backend/pattern_matching                        0s  65MB
Dec 17 18:55:57 Starting compiler/parsing/ocaml
Dec 17 18:57:38 Finished compiler/parsing/ocaml                                1m40s   1GB
Dec 17 18:57:39 Starting compiler/printing
Dec 17 18:57:41 Finished compiler/printing                                        1s 112MB
Dec 17 18:57:42 Starting compiler/parsing/proofs
Dec 17 18:57:43 Finished compiler/parsing/proofs                                  0s  71MB
Dec 17 18:57:44 Starting compiler/inference/proofs
Dec 17 18:57:46 Finished compiler/inference/proofs                                1s 111MB
Dec 17 18:57:47 Starting compiler/backend/semantics
Dec 17 18:59:48 Finished compiler/backend/semantics                            2m00s   1GB
Dec 17 18:59:49 Starting compiler/backend/reg_alloc/proofs
Dec 17 18:59:51 Finished compiler/backend/reg_alloc/proofs                        1s 124MB
Dec 17 18:59:52 Starting compiler/backend/proofs
Dec 17 19:00:29 Finished compiler/backend/proofs                                 36s   2GB
Dec 17 19:00:30 Starting compiler/backend/serialiser
Dec 17 19:00:32 Finished compiler/backend/serialiser                              1s 152MB
Dec 17 19:00:33 Starting compiler/encoders/x64/proofs
Dec 17 19:00:35 Finished compiler/encoders/x64/proofs                             0s  94MB
Dec 17 19:00:36 Starting compiler/encoders/arm7/proofs
Dec 17 19:11:09 Finished compiler/encoders/arm7/proofs                        10m32s   8GB
Dec 17 19:11:10 Starting compiler/encoders/arm8/proofs
Dec 17 19:17:40 Finished compiler/encoders/arm8/proofs                         6m28s   4GB
Dec 17 19:17:41 Starting compiler/encoders/arm8_asl/proofs
Dec 17 19:31:59 Finished compiler/encoders/arm8_asl/proofs                    14m17s   3GB
Dec 17 19:32:00 Starting compiler/encoders/mips/proofs
Dec 17 19:40:36 Finished compiler/encoders/mips/proofs                         8m35s   8GB
Dec 17 19:40:37 Starting compiler/encoders/riscv/proofs
Dec 17 19:48:05 Finished compiler/encoders/riscv/proofs                        7m27s   4GB
Dec 17 19:48:06 Starting compiler/encoders/ag32/proofs
Dec 17 19:50:38 Finished compiler/encoders/ag32/proofs                         2m30s   1GB
Dec 17 19:50:39 Starting compiler/backend/x64/proofs
Dec 17 19:50:42 Finished compiler/backend/x64/proofs                              2s 226MB
Dec 17 19:50:43 Starting compiler/backend/arm7/proofs
Dec 17 19:51:14 Finished compiler/backend/arm7/proofs                            30s   2GB
Dec 17 19:51:15 Starting compiler/backend/arm8/proofs
Dec 17 19:51:49 Finished compiler/backend/arm8/proofs                            32s   2GB
Dec 17 19:51:50 Starting compiler/backend/arm8_asl
Dec 17 19:52:13 Finished compiler/backend/arm8_asl                               22s   2GB
Dec 17 19:52:14 Starting compiler/backend/mips/proofs
Dec 17 19:52:47 Finished compiler/backend/mips/proofs                            31s   2GB
Dec 17 19:52:47 Starting compiler/backend/riscv/proofs
Dec 17 19:53:23 Finished compiler/backend/riscv/proofs                           35s   2GB
Dec 17 19:53:24 Starting compiler/backend/ag32/proofs
Dec 17 20:03:59 Finished compiler/backend/ag32/proofs                         10m34s   5GB
Dec 17 20:04:00 Starting compiler/backend/cv_compute
Dec 17 20:04:25 Finished compiler/backend/cv_compute                             24s   1GB
Dec 17 20:04:26 Starting cv_translator
Dec 17 20:09:22 Finished cv_translator                                         4m54s   4GB
Dec 17 20:09:23 Starting candle
Dec 17 20:09:24 Finished candle                                                   0s  18MB
Dec 17 20:09:25 Starting candle/set-theory
Dec 17 20:09:50 Finished candle/set-theory                                       24s 932MB
Dec 17 20:09:51 Starting candle/syntax-lib
Dec 17 20:09:52 Finished candle/syntax-lib                                        0s  93MB
Dec 17 20:09:53 Starting candle/standard
Dec 17 20:09:54 Finished candle/standard                                          0s  18MB
Dec 17 20:09:55 Starting candle/standard/syntax
Dec 17 20:10:07 Finished candle/standard/syntax                                  10s 810MB
Dec 17 20:10:08 Starting candle/standard/semantics
Dec 17 20:12:01 Finished candle/standard/semantics                             1m52s   2GB
Dec 17 20:12:02 Starting candle/standard/monadic
Dec 17 20:12:04 Finished candle/standard/monadic                                  1s 121MB
Dec 17 20:12:05 Starting candle/standard/ml_kernel
Dec 17 20:13:46 Finished candle/standard/ml_kernel                             1m40s   4GB
Dec 17 20:13:47 Starting candle/overloading
Dec 17 20:13:48 Finished candle/overloading                                       0s  18MB
Dec 17 20:13:49 Starting candle/overloading/syntax
Dec 17 20:16:39 Finished candle/overloading/syntax                             2m49s   2GB
Dec 17 20:16:40 Starting candle/overloading/semantics
Dec 17 20:26:21 Finished candle/overloading/semantics                          9m39s   5GB
Dec 17 20:26:22 Starting candle/overloading/monadic
Dec 17 20:28:13 Finished candle/overloading/monadic                            1m50s   2GB
Dec 17 20:28:14 Starting candle/overloading/ml_kernel
Dec 17 20:34:05 Finished candle/overloading/ml_kernel                          5m49s   6GB
Dec 17 20:34:06 Starting candle/overloading/ml_checker
Dec 17 20:36:16 Finished candle/overloading/ml_checker                         2m08s   6GB
Dec 17 20:36:17 Starting candle/prover
Dec 17 20:36:19 Finished candle/prover                                            1s 164MB
Dec 17 20:36:20 Starting candle/prover/compute
Dec 17 20:36:22 Finished candle/prover/compute                                    1s 146MB
Dec 17 20:36:23 Starting pancake
Dec 17 20:36:26 Finished pancake                                                  1s 138MB
Dec 17 20:36:26 Starting pancake/semantics
Dec 17 20:39:04 Finished pancake/semantics                                     2m36s   1GB
Dec 17 20:39:05 Starting pancake/parser
Dec 17 20:39:34 Finished pancake/parser                                          27s 639MB
Dec 17 20:39:35 Starting pancake/static_checker
Dec 17 20:40:37 Finished pancake/static_checker                                1m01s   1GB
Dec 17 20:40:38 Starting pancake/proofs
Dec 17 20:53:26 Finished pancake/proofs                                       12m47s   5GB
Dec 17 20:53:27 Starting compiler/dafny
Dec 17 20:53:48 Finished compiler/dafny                                          20s 725MB
Dec 17 20:53:49 Starting compiler/dafny/translation
Dec 17 21:02:49 Finished compiler/dafny/translation                            8m59s   5GB
Dec 17 21:02:50 Starting compiler/dafny/compilation
Dec 17 21:04:33 Finished compiler/dafny/compilation                            1m42s   5GB
Dec 17 21:04:34 Starting compiler/dafny/semantics
Dec 17 21:05:06 Finished compiler/dafny/semantics                                30s 551MB
Dec 17 21:05:07 Starting compiler/dafny/proofs
Dec 17 21:06:30 Finished compiler/dafny/proofs                                 1m22s   1GB
Dec 17 21:06:31 Starting compiler/dafny/vcg
Dec 17 21:06:33 Finished compiler/dafny/vcg                                       1s 104MB
Dec 17 21:06:34 Starting compiler/dafny/vcg/examples
Dec 17 21:06:59 Finished compiler/dafny/vcg/examples                             24s   1GB
Dec 17 21:07:00 Starting compiler/scheme
Dec 17 21:07:25 Finished compiler/scheme                                         24s   1GB
Dec 17 21:07:26 Starting compiler/scheme/translation
Dec 17 21:14:01 Finished compiler/scheme/translation                           6m33s   7GB
Dec 17 21:14:02 Starting compiler/scheme/compilation
Dec 17 21:15:16 Finished compiler/scheme/compilation                           1m13s   4GB
Dec 17 21:15:17 Starting compiler/scheme/proofs
Dec 17 21:21:18 Finished compiler/scheme/proofs                                5m59s   3GB
Dec 17 21:21:19 Starting characteristic/examples
Dec 17 21:22:20 FAILED: characteristic/examples
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/integer
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)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 37 directories
Starting work on README.md
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
README.md                                                           (0s)     OK
cf_tutorialTheory                                                  (44s)     OK
cf_examplesTheory                                                  (51s)FAIL<1>
 Proved triviality ___ "example_let2_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_2_pfun_eqs"
 Adding nsLookup representation thms for 574 consts [cf_examples_env_1, cf_examples_env_0, ..., SexpProg_env]
 Using translator specification plus_v_thm from theory mlbasicsProg
 Using translator specification minus_v_thm from theory mlbasicsProg
 Using translator specification plus_v_thm from theory mlbasicsProg
 Proved triviality ___ "example_let_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_3_pfun_eqs"
 Proved triviality ___ "alloc_ref2_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_4_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_3, cf_examples_env_2]
 Using CF specification deref_spec from theory mlbasicsProg
 Using CF specification deref_spec from theory mlbasicsProg
 Using CF specification assign_spec from theory mlbasicsProg
 Using CF specification assign_spec from theory mlbasicsProg
 Proved triviality ___ "swap_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_5_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_4]
 Using translator specification gt_v_thm from theory mlbasicsProg
 Proved triviality ___ "example_if_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_6_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_5]
 Adding nsLookup representation thms for [init_env]
 Proved triviality ___ "is_nil_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_7_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_6]
 Proved triviality ___ "is_none_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_8_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_7]
 Using translator specification eq_v_thm from theory mlbasicsProg
 Proved triviality ___ "example_eq_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_9_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_8]
 Proved triviality ___ "example_and_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_10_pfun_eqs"
 Saved theorem _______ "nsLookup_cf_examples_env_11_pfun_eqs"
 Adding nsLookup representation thms for [cf_examples_env_10, cf_examples_env_9]
 Proof of 
 
 uv.
   UNIT_TYPE () uv 
   app p example_raise_v [uv] emp
     (POSTe v. &(v = Conv (SOME (ExnStamp 8)) []))
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.THEN1:
   Failed to prove theorem "example_raise_spec":
 first subgoal not solved by second tactic
 Full log: /scratch/cakeml/regression2/cakeml-3079/characteristic/examples/.hol/logs/cf_examplesTheory