Job 3080

CakeML:caaa9089584b24c2dd30a5324421141b33ee5b18
  Remove a now dated example [Dec 17 12:09:54]
#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 21:22:25 Claimed job
Dec 17 21:22:29 Reusing HOL
Dec 17 21:22:36 Starting developers
Dec 17 21:22:41 Finished developers                                               3s 201MB
Dec 17 21:22:41 Starting developers/bin
Dec 17 21:22:46 Finished developers/bin                                           3s  91MB
Dec 17 21:22:46 Starting misc
Dec 17 21:23:24 Finished misc                                                    36s   1GB
Dec 17 21:23:25 Starting compiler/proofs
Dec 17 22:21:42 Finished compiler/proofs                                      58m14s  13GB
Dec 17 22:21:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 18 04:00:14 Finished compiler/bootstrap/compilation/x64/64/proofs       5h38m28s  84GB
Dec 18 04:00:15 Starting semantics/ffi
Dec 18 04:00:24 Finished semantics/ffi                                            8s 539MB
Dec 18 04:00:25 Starting semantics
Dec 18 04:00:27 Finished semantics                                                0s  59MB
Dec 18 04:00:28 Starting semantics/proofs
Dec 18 04:00:48 Finished semantics/proofs                                        19s 909MB
Dec 18 04:00:49 Starting semantics/alt_semantics
Dec 18 04:01:06 Finished semantics/alt_semantics                                 15s 539MB
Dec 18 04:01:07 Starting semantics/alt_semantics/proofs
Dec 18 04:04:51 Finished semantics/alt_semantics/proofs                        3m43s   2GB
Dec 18 04:04:52 Starting basis/pure
Dec 18 04:04:54 Finished basis/pure                                               0s  97MB
Dec 18 04:04:55 Starting translator
Dec 18 04:05:54 Finished translator                                              58s   3GB
Dec 18 04:05:55 Starting compiler/parsing
Dec 18 04:05:57 Finished compiler/parsing                                         0s  70MB
Dec 18 04:05:58 Starting characteristic
Dec 18 04:06:00 Finished characteristic                                           1s 115MB
Dec 18 04:06:00 Starting translator/monadic
Dec 18 04:06:02 Finished translator/monadic                                       1s 124MB
Dec 18 04:06:03 Starting translator/monadic/monad_base
Dec 18 04:06:05 Finished translator/monadic/monad_base                            0s  63MB
Dec 18 04:06:06 Starting profiler
Dec 18 04:06:28 Finished profiler                                                21s   1GB
Dec 18 04:06:29 Starting basis
Dec 18 04:07:55 Finished basis                                                 1m25s   4GB
Dec 18 04:07:56 Starting compiler
Dec 18 04:07:59 Finished compiler                                                 2s 218MB
Dec 18 04:08:00 Starting compiler/inference
Dec 18 04:08:02 Finished compiler/inference                                       1s 110MB
Dec 18 04:08:03 Starting compiler/backend/reg_alloc
Dec 18 04:08:05 Finished compiler/backend/reg_alloc                               0s  94MB
Dec 18 04:08:05 Starting compiler/backend/gc
Dec 18 04:08:08 Finished compiler/backend/gc                                      1s 144MB
Dec 18 04:08:09 Starting compiler/backend
Dec 18 04:08:14 Finished compiler/backend                                         4s 268MB
Dec 18 04:08:15 Starting compiler/encoders/asm
Dec 18 04:08:16 Finished compiler/encoders/asm                                    0s  95MB
Dec 18 04:08:17 Starting compiler/encoders/x64
Dec 18 04:08:19 Finished compiler/encoders/x64                                    0s  94MB
Dec 18 04:08:20 Starting compiler/encoders/arm7
Dec 18 04:08:22 Finished compiler/encoders/arm7                                   0s  90MB
Dec 18 04:08:22 Starting compiler/encoders/arm8
Dec 18 04:08:24 Finished compiler/encoders/arm8                                   0s  94MB
Dec 18 04:08:25 Starting compiler/encoders/arm8_asl
Dec 18 04:08:38 Finished compiler/encoders/arm8_asl                              12s   1GB
Dec 18 04:08:39 Starting compiler/encoders/mips
Dec 18 04:08:41 Finished compiler/encoders/mips                                   0s  94MB
Dec 18 04:08:41 Starting compiler/encoders/riscv
Dec 18 04:08:43 Finished compiler/encoders/riscv                                  0s  95MB
Dec 18 04:08:44 Starting compiler/encoders/ag32
Dec 18 04:08:46 Finished compiler/encoders/ag32                                   0s  93MB
Dec 18 04:08:47 Starting compiler/encoders/tests
Dec 18 04:08:49 Finished compiler/encoders/tests                                  1s 106MB
Dec 18 04:08:49 Starting compiler/encoders/monadic_enc
Dec 18 04:09:10 Finished compiler/encoders/monadic_enc                           19s   1GB
Dec 18 04:09:11 Starting compiler/backend/x64
Dec 18 04:09:13 Finished compiler/backend/x64                                     1s 139MB
Dec 18 04:09:14 Starting compiler/backend/arm7
Dec 18 04:09:16 Finished compiler/backend/arm7                                    1s 139MB
Dec 18 04:09:17 Starting compiler/backend/arm8
Dec 18 04:09:19 Finished compiler/backend/arm8                                    1s 139MB
Dec 18 04:09:20 Starting compiler/backend/mips
Dec 18 04:09:22 Finished compiler/backend/mips                                    1s 139MB
Dec 18 04:09:23 Starting compiler/backend/riscv
Dec 18 04:09:25 Finished compiler/backend/riscv                                   1s 139MB
Dec 18 04:09:26 Starting compiler/backend/ag32
Dec 18 04:10:22 Finished compiler/backend/ag32                                   55s   2GB
Dec 18 04:10:23 Starting compiler/backend/pattern_matching
Dec 18 04:10:24 Finished compiler/backend/pattern_matching                        0s  65MB
Dec 18 04:10:25 Starting compiler/parsing/ocaml
Dec 18 04:12:06 Finished compiler/parsing/ocaml                                1m40s   1GB
Dec 18 04:12:07 Starting compiler/printing
Dec 18 04:12:09 Finished compiler/printing                                        1s 120MB
Dec 18 04:12:10 Starting compiler/parsing/proofs
Dec 18 04:12:12 Finished compiler/parsing/proofs                                  0s  70MB
Dec 18 04:12:12 Starting compiler/inference/proofs
Dec 18 04:12:15 Finished compiler/inference/proofs                                1s 111MB
Dec 18 04:12:15 Starting compiler/backend/semantics
Dec 18 04:14:14 Finished compiler/backend/semantics                            1m58s   2GB
Dec 18 04:14:15 Starting compiler/backend/reg_alloc/proofs
Dec 18 04:14:17 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Dec 18 04:14:18 Starting compiler/backend/proofs
Dec 18 04:14:58 Finished compiler/backend/proofs                                 38s   3GB
Dec 18 04:14:59 Starting compiler/backend/serialiser
Dec 18 04:15:01 Finished compiler/backend/serialiser                              1s 153MB
Dec 18 04:15:02 Starting compiler/encoders/x64/proofs
Dec 18 04:15:04 Finished compiler/encoders/x64/proofs                             0s  94MB
Dec 18 04:15:04 Starting compiler/encoders/arm7/proofs
Dec 18 04:25:32 Finished compiler/encoders/arm7/proofs                        10m26s   8GB
Dec 18 04:25:33 Starting compiler/encoders/arm8/proofs
Dec 18 04:32:09 Finished compiler/encoders/arm8/proofs                         6m35s   4GB
Dec 18 04:32:10 Starting compiler/encoders/arm8_asl/proofs
Dec 18 04:46:26 Finished compiler/encoders/arm8_asl/proofs                    14m14s   3GB
Dec 18 04:46:27 Starting compiler/encoders/mips/proofs
Dec 18 04:55:03 Finished compiler/encoders/mips/proofs                         8m35s   8GB
Dec 18 04:55:04 Starting compiler/encoders/riscv/proofs
Dec 18 05:02:37 Finished compiler/encoders/riscv/proofs                        7m31s   5GB
Dec 18 05:02:38 Starting compiler/encoders/ag32/proofs
Dec 18 05:05:10 Finished compiler/encoders/ag32/proofs                         2m31s   2GB
Dec 18 05:05:11 Starting compiler/backend/x64/proofs
Dec 18 05:05:14 Finished compiler/backend/x64/proofs                              2s 219MB
Dec 18 05:05:15 Starting compiler/backend/arm7/proofs
Dec 18 05:05:48 Finished compiler/backend/arm7/proofs                            32s   2GB
Dec 18 05:05:49 Starting compiler/backend/arm8/proofs
Dec 18 05:06:22 Finished compiler/backend/arm8/proofs                            31s   2GB
Dec 18 05:06:23 Starting compiler/backend/arm8_asl
Dec 18 05:06:46 Finished compiler/backend/arm8_asl                               22s   2GB
Dec 18 05:06:47 Starting compiler/backend/mips/proofs
Dec 18 05:07:18 Finished compiler/backend/mips/proofs                            30s   1GB
Dec 18 05:07:19 Starting compiler/backend/riscv/proofs
Dec 18 05:07:54 Finished compiler/backend/riscv/proofs                           33s   2GB
Dec 18 05:07:54 Starting compiler/backend/ag32/proofs
Dec 18 05:18:31 Finished compiler/backend/ag32/proofs                         10m35s   5GB
Dec 18 05:18:32 Starting compiler/backend/cv_compute
Dec 18 05:18:57 Finished compiler/backend/cv_compute                             23s   1GB
Dec 18 05:18:57 Starting cv_translator
Dec 18 05:23:52 Finished cv_translator                                         4m53s   3GB
Dec 18 05:23:53 Starting candle
Dec 18 05:23:54 Finished candle                                                   0s  18MB
Dec 18 05:23:55 Starting candle/set-theory
Dec 18 05:24:20 Finished candle/set-theory                                       24s 929MB
Dec 18 05:24:21 Starting candle/syntax-lib
Dec 18 05:24:23 Finished candle/syntax-lib                                        0s  97MB
Dec 18 05:24:24 Starting candle/standard
Dec 18 05:24:25 Finished candle/standard                                          0s  18MB
Dec 18 05:24:25 Starting candle/standard/syntax
Dec 18 05:24:37 Finished candle/standard/syntax                                  11s 754MB
Dec 18 05:24:38 Starting candle/standard/semantics
Dec 18 05:26:34 Finished candle/standard/semantics                             1m54s   2GB
Dec 18 05:26:35 Starting candle/standard/monadic
Dec 18 05:26:37 Finished candle/standard/monadic                                  1s 121MB
Dec 18 05:26:38 Starting candle/standard/ml_kernel
Dec 18 05:28:18 Finished candle/standard/ml_kernel                             1m39s   4GB
Dec 18 05:28:19 Starting candle/overloading
Dec 18 05:28:20 Finished candle/overloading                                       0s  18MB
Dec 18 05:28:21 Starting candle/overloading/syntax
Dec 18 05:31:09 Finished candle/overloading/syntax                             2m48s   1GB
Dec 18 05:31:10 Starting candle/overloading/semantics
Dec 18 05:41:01 Finished candle/overloading/semantics                          9m49s   5GB
Dec 18 05:41:02 Starting candle/overloading/monadic
Dec 18 05:42:58 Finished candle/overloading/monadic                            1m55s   1GB
Dec 18 05:42:59 Starting candle/overloading/ml_kernel
Dec 18 05:48:54 Finished candle/overloading/ml_kernel                          5m53s   5GB
Dec 18 05:48:55 Starting candle/overloading/ml_checker
Dec 18 05:51:07 Finished candle/overloading/ml_checker                         2m11s   6GB
Dec 18 05:51:08 Starting candle/prover
Dec 18 05:51:11 Finished candle/prover                                            1s 161MB
Dec 18 05:51:12 Starting candle/prover/compute
Dec 18 05:51:14 Finished candle/prover/compute                                    1s 144MB
Dec 18 05:51:15 Starting pancake
Dec 18 05:51:17 Finished pancake                                                  1s 139MB
Dec 18 05:51:18 Starting pancake/semantics
Dec 18 05:54:00 Finished pancake/semantics                                     2m39s   1GB
Dec 18 05:54:01 Starting pancake/parser
Dec 18 05:54:29 Finished pancake/parser                                          26s 511MB
Dec 18 05:54:29 Starting pancake/static_checker
Dec 18 05:55:32 Finished pancake/static_checker                                1m02s   1GB
Dec 18 05:55:33 Starting pancake/proofs
Dec 18 06:08:27 Finished pancake/proofs                                       12m53s   5GB
Dec 18 06:08:28 Starting compiler/dafny
Dec 18 06:08:51 Finished compiler/dafny                                          21s 720MB
Dec 18 06:08:51 Starting compiler/dafny/translation
Dec 18 06:18:28 Finished compiler/dafny/translation                            9m35s   5GB
Dec 18 06:18:29 Starting compiler/dafny/compilation
Dec 18 06:20:12 Finished compiler/dafny/compilation                            1m41s   5GB
Dec 18 06:20:13 Starting compiler/dafny/semantics
Dec 18 06:20:45 Finished compiler/dafny/semantics                                31s 544MB
Dec 18 06:20:46 Starting compiler/dafny/proofs
Dec 18 06:22:10 Finished compiler/dafny/proofs                                 1m23s   1GB
Dec 18 06:22:11 Starting compiler/dafny/vcg
Dec 18 06:22:13 Finished compiler/dafny/vcg                                       1s 104MB
Dec 18 06:22:14 Starting compiler/dafny/vcg/examples
Dec 18 06:22:38 Finished compiler/dafny/vcg/examples                             23s   1GB
Dec 18 06:22:39 Starting compiler/scheme
Dec 18 06:23:04 Finished compiler/scheme                                         24s   1GB
Dec 18 06:23:04 Starting compiler/scheme/translation
Dec 18 06:29:45 Finished compiler/scheme/translation                           6m39s   9GB
Dec 18 06:29:46 Starting compiler/scheme/compilation
Dec 18 06:31:00 Finished compiler/scheme/compilation                           1m12s   4GB
Dec 18 06:31:01 Starting compiler/scheme/proofs
Dec 18 06:36:59 Finished compiler/scheme/proofs                                5m57s   2GB
Dec 18 06:37:00 Starting characteristic/examples
Dec 18 06:38:05 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                                                  (45s)     OK
cf_examplesTheory                                                  (54s)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-3080/characteristic/examples/.hol/logs/cf_examplesTheory