Job 2949

CakeML:192db9b6873cf02b6dd740dd9669f0aa5184a4d4
  Fix lingering export_theory [Aug 22 06:00:05]
#1221 (halogentlepersuasion:pan_shape_check)
Merging into:e0f8aef6bb083e4d8737c69213c12f838358039b
  Merge pull request #1210 from CakeML/revisedFloats [Aug 23 13:52:27]
HOL:466a40abe43a384327cf9fd1ada840fa176b961d
  Change bossLib.oneline to preserve input hypotheses as hypotheses [Aug 02 07:09:04]
Machine:timtam

Aug 23 23:29:42 Claimed job
Aug 23 23:29:46 Reusing HOL
Aug 23 23:29:54 Starting developers
Aug 23 23:29:58 Finished developers                                               3s 227MB
Aug 23 23:29:59 Starting developers/bin
Aug 23 23:30:04 Finished developers/bin                                           3s 594MB
Aug 23 23:30:05 Starting misc
Aug 23 23:30:47 Finished misc                                                    41s   1GB
Aug 23 23:30:48 Starting compiler/proofs
Aug 24 00:50:07 Finished compiler/proofs                                    1h19m17s  28GB
Aug 24 00:50:07 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 24 07:08:52 Finished compiler/bootstrap/compilation/x64/64/proofs       6h18m44s  79GB
Aug 24 07:08:53 Starting semantics/ffi
Aug 24 07:09:02 Finished semantics/ffi                                            8s 544MB
Aug 24 07:09:03 Starting semantics
Aug 24 07:09:05 Finished semantics                                                0s  59MB
Aug 24 07:09:05 Starting semantics/proofs
Aug 24 07:09:29 Finished semantics/proofs                                        23s   1GB
Aug 24 07:09:30 Starting semantics/alt_semantics
Aug 24 07:09:48 Finished semantics/alt_semantics                                 16s 640MB
Aug 24 07:09:49 Starting semantics/alt_semantics/proofs
Aug 24 07:13:02 Finished semantics/alt_semantics/proofs                        3m12s   2GB
Aug 24 07:13:03 Starting basis/pure
Aug 24 07:13:05 Finished basis/pure                                               0s  94MB
Aug 24 07:13:06 Starting translator
Aug 24 07:14:30 Finished translator                                            1m22s   2GB
Aug 24 07:14:31 Starting compiler/parsing
Aug 24 07:14:32 Finished compiler/parsing                                         0s  64MB
Aug 24 07:14:33 Starting characteristic
Aug 24 07:14:35 Finished characteristic                                           1s 128MB
Aug 24 07:14:36 Starting translator/monadic
Aug 24 07:14:38 Finished translator/monadic                                       1s 125MB
Aug 24 07:14:39 Starting translator/monadic/monad_base
Aug 24 07:14:40 Finished translator/monadic/monad_base                            0s  61MB
Aug 24 07:14:41 Starting basis
Aug 24 07:16:51 Finished basis                                                 2m09s   4GB
Aug 24 07:16:52 Starting compiler
Aug 24 07:16:55 Finished compiler                                                 2s 214MB
Aug 24 07:16:56 Starting compiler/inference
Aug 24 07:16:58 Finished compiler/inference                                       1s 117MB
Aug 24 07:16:59 Starting compiler/backend/reg_alloc
Aug 24 07:17:01 Finished compiler/backend/reg_alloc                               0s 103MB
Aug 24 07:17:02 Starting compiler/backend/gc
Aug 24 07:17:04 Finished compiler/backend/gc                                      1s 146MB
Aug 24 07:17:05 Starting compiler/backend
Aug 24 07:17:10 Finished compiler/backend                                         4s 272MB
Aug 24 07:17:11 Starting compiler/encoders/asm
Aug 24 07:17:12 Finished compiler/encoders/asm                                    0s  86MB
Aug 24 07:17:13 Starting compiler/encoders/x64
Aug 24 07:17:15 Finished compiler/encoders/x64                                    0s  96MB
Aug 24 07:17:16 Starting compiler/encoders/arm7
Aug 24 07:17:17 Finished compiler/encoders/arm7                                   0s  91MB
Aug 24 07:17:18 Starting compiler/encoders/arm8
Aug 24 07:17:20 Finished compiler/encoders/arm8                                   0s  93MB
Aug 24 07:17:21 Starting compiler/encoders/arm8_asl
Aug 24 07:17:34 Finished compiler/encoders/arm8_asl                              12s   1GB
Aug 24 07:17:35 Starting compiler/encoders/mips
Aug 24 07:17:36 Finished compiler/encoders/mips                                   0s  98MB
Aug 24 07:17:37 Starting compiler/encoders/riscv
Aug 24 07:17:39 Finished compiler/encoders/riscv                                  0s  91MB
Aug 24 07:17:40 Starting compiler/encoders/ag32
Aug 24 07:17:41 Finished compiler/encoders/ag32                                   0s  89MB
Aug 24 07:17:42 Starting compiler/encoders/tests
Aug 24 07:17:44 Finished compiler/encoders/tests                                  0s 108MB
Aug 24 07:17:45 Starting compiler/encoders/monadic_enc
Aug 24 07:18:07 Finished compiler/encoders/monadic_enc                           20s   1GB
Aug 24 07:18:08 Starting compiler/backend/x64
Aug 24 07:18:10 Finished compiler/backend/x64                                     1s 148MB
Aug 24 07:18:11 Starting compiler/backend/arm7
Aug 24 07:18:13 Finished compiler/backend/arm7                                    1s 149MB
Aug 24 07:18:14 Starting compiler/backend/arm8
Aug 24 07:18:16 Finished compiler/backend/arm8                                    1s 148MB
Aug 24 07:18:17 Starting compiler/backend/mips
Aug 24 07:18:19 Finished compiler/backend/mips                                    1s 148MB
Aug 24 07:18:20 Starting compiler/backend/riscv
Aug 24 07:18:22 Finished compiler/backend/riscv                                   1s 149MB
Aug 24 07:18:23 Starting compiler/backend/ag32
Aug 24 07:19:29 Finished compiler/backend/ag32                                 1m05s   3GB
Aug 24 07:19:30 Starting compiler/backend/pattern_matching
Aug 24 07:19:31 Finished compiler/backend/pattern_matching                        0s  62MB
Aug 24 07:19:32 Starting compiler/parsing/ocaml
Aug 24 07:21:15 Finished compiler/parsing/ocaml                                1m41s   1GB
Aug 24 07:21:16 Starting compiler/printing
Aug 24 07:21:18 Finished compiler/printing                                        1s 121MB
Aug 24 07:21:18 Starting compiler/parsing/proofs
Aug 24 07:21:20 Finished compiler/parsing/proofs                                  0s  68MB
Aug 24 07:21:21 Starting compiler/inference/proofs
Aug 24 07:21:23 Finished compiler/inference/proofs                                1s 117MB
Aug 24 07:21:24 Starting compiler/backend/semantics
Aug 24 07:24:13 Finished compiler/backend/semantics                            2m49s   3GB
Aug 24 07:24:14 Starting compiler/backend/reg_alloc/proofs
Aug 24 07:24:16 Finished compiler/backend/reg_alloc/proofs                        1s 120MB
Aug 24 07:24:17 Starting compiler/backend/proofs
Aug 24 07:25:07 Finished compiler/backend/proofs                                 48s   3GB
Aug 24 07:25:07 Starting compiler/backend/serialiser
Aug 24 07:25:10 Finished compiler/backend/serialiser                              1s 161MB
Aug 24 07:25:11 Starting compiler/encoders/x64/proofs
Aug 24 07:25:12 Finished compiler/encoders/x64/proofs                             0s  92MB
Aug 24 07:25:13 Starting compiler/encoders/arm7/proofs
Aug 24 07:38:23 Finished compiler/encoders/arm7/proofs                        13m09s   8GB
Aug 24 07:38:24 Starting compiler/encoders/arm8/proofs
Aug 24 07:45:33 Finished compiler/encoders/arm8/proofs                         7m07s   4GB
Aug 24 07:45:33 Starting compiler/encoders/arm8_asl/proofs
Aug 24 08:01:26 Finished compiler/encoders/arm8_asl/proofs                    15m51s   3GB
Aug 24 08:01:27 Starting compiler/encoders/mips/proofs
Aug 24 08:11:22 Finished compiler/encoders/mips/proofs                         9m54s   6GB
Aug 24 08:11:23 Starting compiler/encoders/riscv/proofs
Aug 24 08:19:35 Finished compiler/encoders/riscv/proofs                        8m10s   4GB
Aug 24 08:19:36 Starting compiler/encoders/ag32/proofs
Aug 24 08:22:28 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Aug 24 08:22:29 Starting compiler/backend/x64/proofs
Aug 24 08:22:32 Finished compiler/backend/x64/proofs                              2s 221MB
Aug 24 08:22:33 Starting compiler/backend/arm7/proofs
Aug 24 08:23:07 Finished compiler/backend/arm7/proofs                            33s   2GB
Aug 24 08:23:08 Starting compiler/backend/arm8/proofs
Aug 24 08:23:43 Finished compiler/backend/arm8/proofs                            33s   2GB
Aug 24 08:23:43 Starting compiler/backend/arm8_asl
Aug 24 08:24:07 Finished compiler/backend/arm8_asl                               22s   2GB
Aug 24 08:24:08 Starting compiler/backend/mips/proofs
Aug 24 08:24:40 Finished compiler/backend/mips/proofs                            31s   2GB
Aug 24 08:24:41 Starting compiler/backend/riscv/proofs
Aug 24 08:25:15 Finished compiler/backend/riscv/proofs                           33s   2GB
Aug 24 08:25:16 Starting compiler/backend/ag32/proofs
Aug 24 08:38:17 Finished compiler/backend/ag32/proofs                         13m00s   4GB
Aug 24 08:38:18 Starting compiler/backend/cv_compute
Aug 24 08:38:43 Finished compiler/backend/cv_compute                             24s   2GB
Aug 24 08:38:44 Starting cv_translator
Aug 24 08:44:02 Finished cv_translator                                         5m17s   5GB
Aug 24 08:44:03 Starting candle
Aug 24 08:44:04 Finished candle                                                   0s  14MB
Aug 24 08:44:04 Starting candle/set-theory
Aug 24 08:44:31 Finished candle/set-theory                                       25s 975MB
Aug 24 08:44:32 Starting candle/syntax-lib
Aug 24 08:44:34 Finished candle/syntax-lib                                        0s 105MB
Aug 24 08:44:35 Starting candle/standard
Aug 24 08:44:36 Finished candle/standard                                          0s  13MB
Aug 24 08:44:36 Starting candle/standard/syntax
Aug 24 08:44:49 Finished candle/standard/syntax                                  11s 774MB
Aug 24 08:44:49 Starting candle/standard/semantics
Aug 24 08:46:48 Finished candle/standard/semantics                             1m57s   1GB
Aug 24 08:46:49 Starting candle/standard/monadic
Aug 24 08:46:51 Finished candle/standard/monadic                                  1s 130MB
Aug 24 08:46:52 Starting candle/standard/ml_kernel
Aug 24 08:48:38 Finished candle/standard/ml_kernel                             1m45s   4GB
Aug 24 08:48:39 Starting candle/standard/ml_kernel/lisp
Aug 24 08:48:40 Finished candle/standard/ml_kernel/lisp                           0s  55MB
Aug 24 08:48:41 Starting candle/overloading
Aug 24 08:48:42 Finished candle/overloading                                       0s  16MB
Aug 24 08:48:43 Starting candle/overloading/syntax
Aug 24 08:51:46 Finished candle/overloading/syntax                             3m02s   2GB
Aug 24 08:51:47 Starting candle/overloading/semantics
Aug 24 09:02:45 Finished candle/overloading/semantics                         10m57s   6GB
Aug 24 09:02:46 Starting candle/overloading/monadic
Aug 24 09:05:02 Finished candle/overloading/monadic                            2m15s   2GB
Aug 24 09:05:03 Starting candle/overloading/ml_kernel
Aug 24 09:11:58 Finished candle/overloading/ml_kernel                          6m54s   6GB
Aug 24 09:11:59 Starting candle/overloading/ml_checker
Aug 24 09:14:09 Finished candle/overloading/ml_checker                         2m08s   6GB
Aug 24 09:14:09 Starting candle/prover
Aug 24 09:14:12 Finished candle/prover                                            1s 160MB
Aug 24 09:14:13 Starting candle/prover/compute
Aug 24 09:14:15 Finished candle/prover/compute                                    1s 158MB
Aug 24 09:14:16 Starting pancake
Aug 24 09:14:18 Finished pancake                                                  1s 151MB
Aug 24 09:14:19 Starting pancake/semantics
Aug 24 09:17:00 Finished pancake/semantics                                     2m39s   2GB
Aug 24 09:17:01 Starting pancake/parser
Aug 24 09:17:29 Finished pancake/parser                                          27s 468MB
Aug 24 09:17:30 Starting pancake/static_checker
Aug 24 09:18:32 Finished pancake/static_checker                                1m01s   1GB
Aug 24 09:18:33 Starting pancake/proofs
Aug 24 09:35:42 Finished pancake/proofs                                       17m07s   6GB
Aug 24 09:35:43 Starting compiler/dafny
Aug 24 09:36:42 Finished compiler/dafny                                          58s   1GB
Aug 24 09:36:42 Starting compiler/dafny/translation
Aug 24 09:42:48 Finished compiler/dafny/translation                            6m04s   2GB
Aug 24 09:42:49 Starting compiler/dafny/compilation
Aug 24 09:44:28 Finished compiler/dafny/compilation                            1m38s   6GB
Aug 24 09:44:28 Starting compiler/dafny/semantics
Aug 24 09:46:40 Finished compiler/dafny/semantics                              2m11s   2GB
Aug 24 09:46:41 Starting compiler/dafny/vcg
Aug 24 09:46:47 Finished compiler/dafny/vcg                                       4s 269MB
Aug 24 09:46:48 Starting compiler/scheme
Aug 24 09:47:14 Finished compiler/scheme                                         25s   1GB
Aug 24 09:47:15 Starting compiler/scheme/translation
Aug 24 09:54:22 Finished compiler/scheme/translation                           7m06s   7GB
Aug 24 09:54:23 Starting compiler/scheme/compilation
Aug 24 09:55:36 Finished compiler/scheme/compilation                           1m12s   5GB
Aug 24 09:55:37 Starting compiler/scheme/proofs
Aug 24 10:11:47 Finished compiler/scheme/proofs                               16m09s  42GB
Aug 24 10:11:48 Starting characteristic/examples
Aug 24 10:13:12 Finished characteristic/examples                               1m23s   4GB
Aug 24 10:13:13 Starting tutorial/solutions
Aug 24 10:15:38 Finished tutorial/solutions                                    2m23s   3GB
Aug 24 10:15:38 Starting translator/monadic/examples
Aug 24 10:18:37 Finished translator/monadic/examples                           2m57s   3GB
Aug 24 10:18:38 Starting examples
Aug 24 10:24:05 Finished examples                                              5m26s   4GB
Aug 24 10:24:06 Starting examples/compilation
Aug 24 10:24:07 Finished examples/compilation                                     0s  13MB
Aug 24 10:24:07 Starting examples/compilation/x64
Aug 24 10:30:55 Finished examples/compilation/x64                              6m46s   4GB
Aug 24 10:30:56 Starting examples/compilation/x64/proofs
Aug 24 10:33:30 Finished examples/compilation/x64/proofs                       2m33s   4GB
Aug 24 10:33:31 Starting examples/compilation/ag32
Aug 24 10:35:26 Finished examples/compilation/ag32                             1m54s   3GB
Aug 24 10:35:27 Starting examples/compilation/ag32/proofs
Aug 24 10:36:32 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Aug 24 10:36:33 Starting examples/lpr_checker
Aug 24 10:37:07 Finished examples/lpr_checker                                    33s   1GB
Aug 24 10:37:07 Starting examples/lpr_checker/array
Aug 24 11:00:05 Finished examples/lpr_checker/array                           22m56s  22GB
Aug 24 11:00:05 Starting examples/lpr_checker/array/compilation
Aug 24 11:02:18 Finished examples/lpr_checker/array/compilation                2m11s   6GB
Aug 24 11:02:19 Starting examples/lpr_checker/array/compilation/proofs
Aug 24 11:03:34 Finished examples/lpr_checker/array/compilation/proofs         1m13s   6GB
Aug 24 11:03:34 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 24 11:04:47 Finished examples/lpr_checker/array/compilation/proofsARM8     1m11s   6GB
Aug 24 11:04:48 Starting .
Aug 24 11:04:52 Finished .                                                        3s 361MB
Aug 24 11:04:53 Starting examples/xlrup_checker
Aug 24 11:05:41 Finished examples/xlrup_checker                                  46s   1GB
Aug 24 11:05:41 Starting examples/xlrup_checker/array
Aug 24 11:20:58 Finished examples/xlrup_checker/array                         15m15s  15GB
Aug 24 11:20:58 Starting examples/xlrup_checker/array/compilation
Aug 24 11:22:07 Finished examples/xlrup_checker/array/compilation              1m08s   4GB
Aug 24 11:22:08 Starting examples/xlrup_checker/array/compilation/proofs
Aug 24 11:23:13 Finished examples/xlrup_checker/array/compilation/proofs       1m04s   5GB
Aug 24 11:23:14 Starting examples/scpog_checker
Aug 24 11:23:58 Finished examples/scpog_checker                                  42s   2GB
Aug 24 11:23:59 Starting examples/scpog_checker/array
Aug 24 11:32:39 Finished examples/scpog_checker/array                          8m39s   6GB
Aug 24 11:32:40 Starting examples/scpog_checker/array/compilation
Aug 24 11:34:33 Finished examples/scpog_checker/array/compilation              1m52s   7GB
Aug 24 11:34:34 Starting examples/scpog_checker/array/compilation/proofs
Aug 24 11:35:50 Finished examples/scpog_checker/array/compilation/proofs       1m15s   6GB
Aug 24 11:35:51 Starting examples/pseudo_bool
Aug 24 11:37:49 Finished examples/pseudo_bool                                  1m57s   1GB
Aug 24 11:37:50 Starting examples/pseudo_bool/cnf_encoding
Aug 24 11:38:19 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Aug 24 11:38:20 Starting examples/pseudo_bool/graph_encoding
Aug 24 11:39:03 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Aug 24 11:39:04 Starting examples/pseudo_bool/array
Aug 24 12:57:48 Finished examples/pseudo_bool/array                         1h18m43s  33GB
Aug 24 12:57:49 Starting examples/pseudo_bool/array/compilation
Aug 24 13:08:03 Finished examples/pseudo_bool/array/compilation               10m12s  17GB
Aug 24 13:08:04 Starting examples/pseudo_bool/array/compilation/proofs
Aug 24 13:10:54 Finished examples/pseudo_bool/array/compilation/proofs         2m49s   7GB
Aug 24 13:10:55 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 24 13:12:17 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m21s   7GB
Aug 24 13:12:18 Starting examples/opentheory
Aug 24 13:20:29 Finished examples/opentheory                                   8m09s   7GB
Aug 24 13:20:30 Starting examples/opentheory/compilation
Aug 24 13:21:58 Finished examples/opentheory/compilation                       1m27s   6GB
Aug 24 13:21:59 Starting examples/opentheory/compilation/proofs
Aug 24 13:23:05 Finished examples/opentheory/compilation/proofs                1m05s   4GB
Aug 24 13:23:06 Starting examples/opentheory/compilation/ag32
Aug 24 13:24:39 Finished examples/opentheory/compilation/ag32                  1m32s   6GB
Aug 24 13:24:40 Starting examples/opentheory/compilation/ag32/proofs
Aug 24 13:26:23 FAILED: examples/opentheory/compilation/ag32/proofs
Scanning $(HOLDIR)/src/TeX
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)/src/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/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/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
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
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
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)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(CAKEMLDIR)/compiler/backend/gc
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 $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
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 $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code
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/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
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/ag32
Scanned 105 directories
Starting work on README.md
Starting work on readerProgProofTheory
README.md                                                           (0s)     OK
readerProgProofTheory                                              (88s)FAIL<1>
 <<HOL message: Created theory "readerProgProof">>
 Saved theorem _______ "extcalls_ffi_names"
 Saved theorem _______ "target_state_rel_reader_start_asm_state"
 Saved theorem _______ "reader_installed"
 Saved theorem _______ "reader_machine_sem"
 Proved triviality ___ "all_lines_stdin_fs"
 Saved theorem _______ "reader_extract_writes"
 Saved theorem _______ "reader_ag32_next"
 
 Failure while writing theory!
 error in quse /scratch/cakeml/regression2/cakeml-2949/examples/opentheory/compilation/ag32/proofs/readerProgProofScript.sml : Io "No space left on device"
 error in load /scratch/cakeml/regression2/cakeml-2949/examples/opentheory/compilation/ag32/proofs/readerProgProofScript : Io "No space left on device"
 Uncaught exception at /scratch/cakeml/regression2/HOL-466a40abe43a384327cf9fd1ada840fa176b961d/src/postkernel/Theory.sml:951: Io "No space left on device"
 Full log: /scratch/cakeml/regression2/cakeml-2949/examples/opentheory/compilation/ag32/proofs/.hol/logs/readerProgProofTheory