Job 3066

CakeML:a3a3dd8b528ba125b8830579645d4256ac1eb6de
  check_thm should not fail with --fast [Dec 04 12:52:25]
#1276 (checkthm_fastbuild)
Merging into:fa305e33ff056f1bdd43a4f42ef65a883f86b854
  Merge pull request #1273 from CakeML/scheme_redex [Dec 04 08:22:10]
HOL:f02a261b181e0408a16745877f3feb8f1b8c1cb6
  Modernise syntax in milawa_proofp [Nov 27 06:20:54]
Machine:lammmington

Dec 04 13:35:01 Claimed job
Dec 04 13:35:04 Reusing HOL
Dec 04 13:35:11 Starting developers
Dec 04 13:35:16 Finished developers                                               4s 215MB
Dec 04 13:35:17 Starting developers/bin
Dec 04 13:35:21 Finished developers/bin                                           3s  91MB
Dec 04 13:35:22 Starting misc
Dec 04 13:36:01 Finished misc                                                    37s   1GB
Dec 04 13:36:02 Starting compiler/proofs
Dec 04 14:34:07 Finished compiler/proofs                                      58m04s  10GB
Dec 04 14:34:08 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 04 20:03:59 Finished compiler/bootstrap/compilation/x64/64/proofs       5h29m50s  59GB
Dec 04 20:03:59 Starting semantics/ffi
Dec 04 20:04:09 Finished semantics/ffi                                            8s 515MB
Dec 04 20:04:10 Starting semantics
Dec 04 20:04:11 Finished semantics                                                0s  62MB
Dec 04 20:04:12 Starting semantics/proofs
Dec 04 20:04:33 Finished semantics/proofs                                        20s 724MB
Dec 04 20:04:34 Starting semantics/alt_semantics
Dec 04 20:04:51 Finished semantics/alt_semantics                                 16s 714MB
Dec 04 20:04:52 Starting semantics/alt_semantics/proofs
Dec 04 20:08:39 Finished semantics/alt_semantics/proofs                        3m45s   2GB
Dec 04 20:08:40 Starting basis/pure
Dec 04 20:08:41 Finished basis/pure                                               0s  93MB
Dec 04 20:08:42 Starting translator
Dec 04 20:09:41 Finished translator                                              57s   2GB
Dec 04 20:09:42 Starting compiler/parsing
Dec 04 20:09:43 Finished compiler/parsing                                         0s  69MB
Dec 04 20:09:44 Starting characteristic
Dec 04 20:09:46 Finished characteristic                                           1s 109MB
Dec 04 20:09:47 Starting translator/monadic
Dec 04 20:09:49 Finished translator/monadic                                       1s 119MB
Dec 04 20:09:50 Starting translator/monadic/monad_base
Dec 04 20:09:51 Finished translator/monadic/monad_base                            0s  63MB
Dec 04 20:09:52 Starting profiler
Dec 04 20:10:18 Finished profiler                                                24s   1GB
Dec 04 20:10:19 Starting basis
Dec 04 20:11:39 Finished basis                                                 1m19s   3GB
Dec 04 20:11:40 Starting compiler
Dec 04 20:11:43 Finished compiler                                                 2s 218MB
Dec 04 20:11:44 Starting compiler/inference
Dec 04 20:11:46 Finished compiler/inference                                       1s 109MB
Dec 04 20:11:47 Starting compiler/backend/reg_alloc
Dec 04 20:11:49 Finished compiler/backend/reg_alloc                               0s  93MB
Dec 04 20:11:50 Starting compiler/backend/gc
Dec 04 20:11:52 Finished compiler/backend/gc                                      1s 138MB
Dec 04 20:11:53 Starting compiler/backend
Dec 04 20:11:58 Finished compiler/backend                                         4s 283MB
Dec 04 20:11:59 Starting compiler/encoders/asm
Dec 04 20:12:01 Finished compiler/encoders/asm                                    0s  95MB
Dec 04 20:12:02 Starting compiler/encoders/x64
Dec 04 20:12:03 Finished compiler/encoders/x64                                    0s  94MB
Dec 04 20:12:04 Starting compiler/encoders/arm7
Dec 04 20:12:06 Finished compiler/encoders/arm7                                   0s  91MB
Dec 04 20:12:07 Starting compiler/encoders/arm8
Dec 04 20:12:09 Finished compiler/encoders/arm8                                   0s  94MB
Dec 04 20:12:09 Starting compiler/encoders/arm8_asl
Dec 04 20:12:23 Finished compiler/encoders/arm8_asl                              12s   1GB
Dec 04 20:12:24 Starting compiler/encoders/mips
Dec 04 20:12:25 Finished compiler/encoders/mips                                   0s  90MB
Dec 04 20:12:26 Starting compiler/encoders/riscv
Dec 04 20:12:28 Finished compiler/encoders/riscv                                  0s  91MB
Dec 04 20:12:29 Starting compiler/encoders/ag32
Dec 04 20:12:30 Finished compiler/encoders/ag32                                   0s  89MB
Dec 04 20:12:31 Starting compiler/encoders/tests
Dec 04 20:12:33 Finished compiler/encoders/tests                                  1s 106MB
Dec 04 20:12:34 Starting compiler/encoders/monadic_enc
Dec 04 20:12:55 Finished compiler/encoders/monadic_enc                           19s   1GB
Dec 04 20:12:56 Starting compiler/backend/x64
Dec 04 20:12:58 Finished compiler/backend/x64                                     1s 136MB
Dec 04 20:12:59 Starting compiler/backend/arm7
Dec 04 20:13:01 Finished compiler/backend/arm7                                    1s 140MB
Dec 04 20:13:02 Starting compiler/backend/arm8
Dec 04 20:13:04 Finished compiler/backend/arm8                                    1s 140MB
Dec 04 20:13:05 Starting compiler/backend/mips
Dec 04 20:13:07 Finished compiler/backend/mips                                    1s 136MB
Dec 04 20:13:08 Starting compiler/backend/riscv
Dec 04 20:13:10 Finished compiler/backend/riscv                                   1s 139MB
Dec 04 20:13:11 Starting compiler/backend/ag32
Dec 04 20:14:08 Finished compiler/backend/ag32                                   55s   1GB
Dec 04 20:14:08 Starting compiler/backend/pattern_matching
Dec 04 20:14:10 Finished compiler/backend/pattern_matching                        0s  64MB
Dec 04 20:14:11 Starting compiler/parsing/ocaml
Dec 04 20:15:52 Finished compiler/parsing/ocaml                                1m40s   1GB
Dec 04 20:15:53 Starting compiler/printing
Dec 04 20:15:55 Finished compiler/printing                                        1s 112MB
Dec 04 20:15:56 Starting compiler/parsing/proofs
Dec 04 20:15:57 Finished compiler/parsing/proofs                                  0s  69MB
Dec 04 20:15:58 Starting compiler/inference/proofs
Dec 04 20:16:00 Finished compiler/inference/proofs                                1s 110MB
Dec 04 20:16:01 Starting compiler/backend/semantics
Dec 04 20:18:02 Finished compiler/backend/semantics                            1m59s   2GB
Dec 04 20:18:03 Starting compiler/backend/reg_alloc/proofs
Dec 04 20:18:05 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Dec 04 20:18:06 Starting compiler/backend/proofs
Dec 04 20:18:44 Finished compiler/backend/proofs                                 37s   1GB
Dec 04 20:18:45 Starting compiler/backend/serialiser
Dec 04 20:18:47 Finished compiler/backend/serialiser                              1s 143MB
Dec 04 20:18:48 Starting compiler/encoders/x64/proofs
Dec 04 20:18:50 Finished compiler/encoders/x64/proofs                             0s  90MB
Dec 04 20:18:51 Starting compiler/encoders/arm7/proofs
Dec 04 20:30:07 Finished compiler/encoders/arm7/proofs                        11m15s  13GB
Dec 04 20:30:08 Starting compiler/encoders/arm8/proofs
Dec 04 20:36:33 Finished compiler/encoders/arm8/proofs                         6m23s   4GB
Dec 04 20:36:33 Starting compiler/encoders/arm8_asl/proofs
Dec 04 20:51:01 Finished compiler/encoders/arm8_asl/proofs                    14m26s   4GB
Dec 04 20:51:02 Starting compiler/encoders/mips/proofs
Dec 04 20:59:47 Finished compiler/encoders/mips/proofs                         8m44s   7GB
Dec 04 20:59:48 Starting compiler/encoders/riscv/proofs
Dec 04 21:07:23 Finished compiler/encoders/riscv/proofs                        7m34s   3GB
Dec 04 21:07:24 Starting compiler/encoders/ag32/proofs
Dec 04 21:09:56 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Dec 04 21:09:57 Starting compiler/backend/x64/proofs
Dec 04 21:10:00 Finished compiler/backend/x64/proofs                              2s 206MB
Dec 04 21:10:01 Starting compiler/backend/arm7/proofs
Dec 04 21:10:36 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 04 21:10:37 Starting compiler/backend/arm8/proofs
Dec 04 21:11:08 Finished compiler/backend/arm8/proofs                            30s   2GB
Dec 04 21:11:09 Starting compiler/backend/arm8_asl
Dec 04 21:11:31 Finished compiler/backend/arm8_asl                               22s   2GB
Dec 04 21:11:32 Starting compiler/backend/mips/proofs
Dec 04 21:12:03 Finished compiler/backend/mips/proofs                            30s   1GB
Dec 04 21:12:04 Starting compiler/backend/riscv/proofs
Dec 04 21:12:39 Finished compiler/backend/riscv/proofs                           33s   2GB
Dec 04 21:12:40 Starting compiler/backend/ag32/proofs
Dec 04 21:23:16 Finished compiler/backend/ag32/proofs                         10m34s   5GB
Dec 04 21:23:16 Starting compiler/backend/cv_compute
Dec 04 21:23:41 Finished compiler/backend/cv_compute                             23s   1GB
Dec 04 21:23:42 Starting cv_translator
Dec 04 21:28:36 Finished cv_translator                                         4m53s   4GB
Dec 04 21:28:37 Starting candle
Dec 04 21:28:38 Finished candle                                                   0s  14MB
Dec 04 21:28:39 Starting candle/set-theory
Dec 04 21:29:05 Finished candle/set-theory                                       25s 930MB
Dec 04 21:29:06 Starting candle/syntax-lib
Dec 04 21:29:08 Finished candle/syntax-lib                                        0s  88MB
Dec 04 21:29:08 Starting candle/standard
Dec 04 21:29:09 Finished candle/standard                                          0s  15MB
Dec 04 21:29:10 Starting candle/standard/syntax
Dec 04 21:29:23 Finished candle/standard/syntax                                  11s 768MB
Dec 04 21:29:23 Starting candle/standard/semantics
Dec 04 21:31:17 Finished candle/standard/semantics                             1m52s   2GB
Dec 04 21:31:18 Starting candle/standard/monadic
Dec 04 21:31:20 Finished candle/standard/monadic                                  1s 115MB
Dec 04 21:31:21 Starting candle/standard/ml_kernel
Dec 04 21:33:15 Finished candle/standard/ml_kernel                             1m53s   3GB
Dec 04 21:33:16 Starting candle/standard/ml_kernel/lisp
Dec 04 21:33:17 Finished candle/standard/ml_kernel/lisp                           0s  56MB
Dec 04 21:33:18 Starting candle/overloading
Dec 04 21:33:19 Finished candle/overloading                                       0s  15MB
Dec 04 21:33:20 Starting candle/overloading/syntax
Dec 04 21:36:07 Finished candle/overloading/syntax                             2m46s   1GB
Dec 04 21:36:08 Starting candle/overloading/semantics
Dec 04 21:45:51 Finished candle/overloading/semantics                          9m41s   4GB
Dec 04 21:45:52 Starting candle/overloading/monadic
Dec 04 21:47:46 Finished candle/overloading/monadic                            1m53s   2GB
Dec 04 21:47:47 Starting candle/overloading/ml_kernel
Dec 04 21:53:34 Finished candle/overloading/ml_kernel                          5m46s   6GB
Dec 04 21:53:35 Starting candle/overloading/ml_checker
Dec 04 21:55:43 Finished candle/overloading/ml_checker                         2m07s   6GB
Dec 04 21:55:44 Starting candle/prover
Dec 04 21:55:46 Finished candle/prover                                            1s 165MB
Dec 04 21:55:47 Starting candle/prover/compute
Dec 04 21:55:50 Finished candle/prover/compute                                    1s 144MB
Dec 04 21:55:51 Starting pancake
Dec 04 21:55:53 Finished pancake                                                  1s 139MB
Dec 04 21:55:54 Starting pancake/semantics
Dec 04 21:58:21 Finished pancake/semantics                                     2m26s   1GB
Dec 04 21:58:22 Starting pancake/parser
Dec 04 21:58:51 Finished pancake/parser                                          27s 468MB
Dec 04 21:58:52 Starting pancake/static_checker
Dec 04 21:59:54 Finished pancake/static_checker                                1m01s   1GB
Dec 04 21:59:55 Starting pancake/proofs
Dec 04 22:12:58 Finished pancake/proofs                                       13m02s   4GB
Dec 04 22:12:59 Starting compiler/dafny
Dec 04 22:13:23 Finished compiler/dafny                                          23s 734MB
Dec 04 22:13:24 Starting compiler/dafny/translation
Dec 04 22:22:18 Finished compiler/dafny/translation                            8m53s   5GB
Dec 04 22:22:19 Starting compiler/dafny/compilation
Dec 04 22:24:03 Finished compiler/dafny/compilation                            1m43s   6GB
Dec 04 22:24:04 Starting compiler/dafny/semantics
Dec 04 22:24:36 Finished compiler/dafny/semantics                                30s 556MB
Dec 04 22:24:37 Starting compiler/dafny/proofs
Dec 04 22:25:55 Finished compiler/dafny/proofs                                 1m17s   1GB
Dec 04 22:25:56 Starting compiler/dafny/vcg
Dec 04 22:26:58 Finished compiler/dafny/vcg                                    1m01s   1GB
Dec 04 22:26:59 Starting compiler/scheme
Dec 04 22:27:25 Finished compiler/scheme                                         24s   1GB
Dec 04 22:27:26 Starting compiler/scheme/translation
Dec 04 22:34:00 Finished compiler/scheme/translation                           6m33s   8GB
Dec 04 22:34:01 Starting compiler/scheme/compilation
Dec 04 22:35:13 Finished compiler/scheme/compilation                           1m11s   4GB
Dec 04 22:35:14 Starting compiler/scheme/proofs
Dec 04 22:41:26 Finished compiler/scheme/proofs                                6m10s   2GB
Dec 04 22:41:27 Starting characteristic/examples
Dec 04 22:42:48 Finished characteristic/examples                               1m20s   5GB
Dec 04 22:42:49 Starting tutorial/solutions
Dec 04 22:45:09 Finished tutorial/solutions                                    2m18s   3GB
Dec 04 22:45:09 Starting translator/monadic/examples
Dec 04 22:47:53 Finished translator/monadic/examples                           2m42s   4GB
Dec 04 22:47:54 Starting examples
Dec 04 22:52:19 Finished examples                                              4m24s   7GB
Dec 04 22:52:20 Starting examples/compilation
Dec 04 22:52:20 Finished examples/compilation                                     0s  15MB
Dec 04 22:52:21 Starting examples/compilation/x64
Dec 04 22:59:00 Finished examples/compilation/x64                              6m37s   4GB
Dec 04 22:59:01 Starting examples/compilation/x64/proofs
Dec 04 23:01:31 Finished examples/compilation/x64/proofs                       2m29s   4GB
Dec 04 23:01:32 Starting examples/compilation/ag32
Dec 04 23:03:23 Finished examples/compilation/ag32                             1m50s   3GB
Dec 04 23:03:24 Starting examples/compilation/ag32/proofs
Dec 04 23:04:28 Finished examples/compilation/ag32/proofs                      1m03s   4GB
Dec 04 23:04:29 Starting examples/lpr_checker
Dec 04 23:05:00 Finished examples/lpr_checker                                    30s   1GB
Dec 04 23:05:01 Starting examples/lpr_checker/array
Dec 04 23:16:59 Finished examples/lpr_checker/array                           11m57s   8GB
Dec 04 23:17:00 Starting examples/lpr_checker/array/compilation
Dec 04 23:19:17 Finished examples/lpr_checker/array/compilation                2m16s   6GB
Dec 04 23:19:18 Starting examples/lpr_checker/array/compilation/proofs
Dec 04 23:20:26 Finished examples/lpr_checker/array/compilation/proofs         1m07s   5GB
Dec 04 23:20:27 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 04 23:21:38 Finished examples/lpr_checker/array/compilation/proofsARM8     1m09s   6GB
Dec 04 23:21:39 Starting .
Dec 04 23:21:43 Finished .                                                        3s 327MB
Dec 04 23:21:44 Starting examples/xlrup_checker
Dec 04 23:22:29 Finished examples/xlrup_checker                                  43s   1GB
Dec 04 23:22:29 Starting examples/xlrup_checker/array
Dec 04 23:31:36 Finished examples/xlrup_checker/array                          9m06s   4GB
Dec 04 23:31:37 Starting examples/xlrup_checker/array/compilation
Dec 04 23:32:45 Finished examples/xlrup_checker/array/compilation              1m07s   4GB
Dec 04 23:32:46 Starting examples/xlrup_checker/array/compilation/proofs
Dec 04 23:33:46 Finished examples/xlrup_checker/array/compilation/proofs         58s   5GB
Dec 04 23:33:47 Starting examples/scpog_checker
Dec 04 23:34:28 Finished examples/scpog_checker                                  40s   1GB
Dec 04 23:34:28 Starting examples/scpog_checker/array
Dec 04 23:40:06 Finished examples/scpog_checker/array                          5m36s   4GB
Dec 04 23:40:07 Starting examples/scpog_checker/array/compilation
Dec 04 23:41:55 Finished examples/scpog_checker/array/compilation              1m46s   7GB
Dec 04 23:41:55 Starting examples/scpog_checker/array/compilation/proofs
Dec 04 23:43:05 Finished examples/scpog_checker/array/compilation/proofs       1m09s   6GB
Dec 04 23:43:06 Starting examples/pseudo_bool
Dec 04 23:44:54 Finished examples/pseudo_bool                                  1m46s   1GB
Dec 04 23:44:55 Starting examples/pseudo_bool/cnf_encoding
Dec 04 23:45:22 Finished examples/pseudo_bool/cnf_encoding                       25s   1GB
Dec 04 23:45:23 Starting examples/pseudo_bool/graph_encoding
Dec 04 23:46:01 Finished examples/pseudo_bool/graph_encoding                     37s   1GB
Dec 04 23:46:02 Starting examples/pseudo_bool/array
Dec 05 00:21:07 Finished examples/pseudo_bool/array                           35m04s  19GB
Dec 05 00:21:08 Starting examples/pseudo_bool/array/compilation
Dec 05 00:31:00 Finished examples/pseudo_bool/array/compilation                9m50s  17GB
Dec 05 00:31:00 Starting examples/pseudo_bool/array/compilation/proofs
Dec 05 00:33:43 Finished examples/pseudo_bool/array/compilation/proofs         2m42s   7GB
Dec 05 00:33:44 Starting examples/pseudo_bool/array/compilation/proofsARM8
Dec 05 00:35:03 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m18s   6GB
Dec 05 00:35:04 Starting examples/opentheory
Dec 05 00:41:52 Finished examples/opentheory                                   6m47s   5GB
Dec 05 00:41:53 Starting examples/opentheory/compilation
Dec 05 00:43:21 Finished examples/opentheory/compilation                       1m26s   5GB
Dec 05 00:43:22 Starting examples/opentheory/compilation/proofs
Dec 05 00:44:27 FAILED: examples/opentheory/compilation/proofs
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)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/examples/opentheory
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
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)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/examples/opentheory/compilation
Scanned 104 directories
Starting work on README.md
Starting work on readerProgProofTheory
README.md                                                           (0s)     OK
readerProgProofTheory                                              (53s)FAIL<1>
 <<HOL message: Created theory "readerProgProof">>
 Saved theorem _______ "reader_compiled_thm"
 Saved definition ____ "installed_x64_def"
 Saved definition ____ "reader_code_def"
 Proof of 
 
 input_exists fs cl  wfcl cl  wfFS fs  STD_streams fs 
 (installed_x64 reader_code mc ms 
  machine_sem mc (basis_ffi cl fs) ms 
  extend_with_resource_limit {Terminate Success (reader_io_events cl fs)}) 
 fs_out hol_refs s.
   extract_fs fs (reader_io_events cl fs) = SOME fs_out 
   (no_errors fs fs_out 
    reader_main fs init_refs (TL cl) = (fs_out,hol_refs,SOME s) 
    hol_refs.the_context extends init_ctxt 
    fs_out =
    add_stdout (flush_stdin (TL cl) fs)
      (concat (append (msg_success s hol_refs.the_context))) 
    asl c.
      MEM (Sequent asl c) s.thms  is_set_theory mem 
      (thyof hol_refs.the_context,asl) |= c)
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at folTools.FOL_FIND:
   Failed to prove theorem "machine_code_sound":
 no solution found
 Full log: /scratch/cakeml/regression3/cakeml-3066/examples/opentheory/compilation/proofs/.hol/logs/readerProgProofTheory