Job 3606

CakeML:1c4645fdc1f5f9bc746766109e2d8cbed9cb4ca4
  Added minimal socket I/O examples [Oct 12 21:20:59]
#1541 (didriklundberg:socketio)
Merging into:f73189499bb295f0859dec7ee38c169c48da682c
  Merge pull request #1539 from CakeML/names-via-metadata [Oct 12 11:47:28]
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
  Merge remote-tracking branch 'origin/master' into develop [Sep 27 02:14:15]
Machine:spagbol

Oct 13 00:27:59 Claimed job
Oct 13 00:28:04 Reusing HOL
Oct 13 00:28:13 Starting developers
Oct 13 00:29:10 Finished developers                                              55s   1GB
Oct 13 00:29:11 Starting developers/bin
Oct 13 00:29:20 Finished developers/bin                                           8s   1GB
Oct 13 00:29:21 Starting misc
Oct 13 00:30:10 Finished misc                                                    47s   1GB
Oct 13 00:30:11 Starting compiler/proofs
Oct 13 01:49:42 Finished compiler/proofs                                    1h19m30s  16GB
Oct 13 01:49:43 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 13 07:54:06 Finished compiler/bootstrap/compilation/x64/64/proofs       6h04m21s  79GB
Oct 13 07:54:07 Starting semantics/ffi
Oct 13 07:54:30 Finished semantics/ffi                                           21s   1GB
Oct 13 07:54:31 Starting semantics
Oct 13 07:54:38 Finished semantics                                                6s   1GB
Oct 13 07:54:39 Starting semantics/proofs
Oct 13 07:55:11 Finished semantics/proofs                                        30s   1GB
Oct 13 07:55:12 Starting semantics/alt_semantics
Oct 13 07:55:35 Finished semantics/alt_semantics                                 22s   1GB
Oct 13 07:55:36 Starting semantics/alt_semantics/proofs
Oct 13 07:59:43 Finished semantics/alt_semantics/proofs                        4m06s   2GB
Oct 13 07:59:44 Starting basis/pure
Oct 13 07:59:52 Finished basis/pure                                               6s   1GB
Oct 13 07:59:53 Starting translator
Oct 13 08:01:11 Finished translator                                            1m17s   2GB
Oct 13 08:01:12 Starting compiler/parsing
Oct 13 08:02:08 Finished compiler/parsing                                        55s   1GB
Oct 13 08:02:09 Starting characteristic
Oct 13 08:02:17 Finished characteristic                                           6s   1GB
Oct 13 08:02:17 Starting translator/monadic
Oct 13 08:02:25 Finished translator/monadic                                       6s   1GB
Oct 13 08:02:26 Starting translator/monadic/monad_base
Oct 13 08:02:33 Finished translator/monadic/monad_base                            6s   1GB
Oct 13 08:02:34 Starting profiler
Oct 13 08:03:09 Finished profiler                                                33s   1GB
Oct 13 08:03:10 Starting basis
Oct 13 08:05:04 Finished basis                                                 1m53s   4GB
Oct 13 08:05:05 Starting compiler
Oct 13 08:05:12 Finished compiler                                                 6s   1GB
Oct 13 08:05:13 Starting compiler/inference
Oct 13 08:05:20 Finished compiler/inference                                       6s   1GB
Oct 13 08:05:21 Starting compiler/backend/reg_alloc
Oct 13 08:05:29 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 13 08:05:30 Starting compiler/backend/gc
Oct 13 08:05:37 Finished compiler/backend/gc                                      6s   1GB
Oct 13 08:05:38 Starting compiler/backend
Oct 13 08:05:48 Finished compiler/backend                                         9s   1GB
Oct 13 08:05:49 Starting compiler/encoders/asm
Oct 13 08:05:57 Finished compiler/encoders/asm                                    6s   1GB
Oct 13 08:05:58 Starting compiler/encoders/x64
Oct 13 08:06:05 Finished compiler/encoders/x64                                    6s   1GB
Oct 13 08:06:06 Starting compiler/encoders/arm7
Oct 13 08:06:13 Finished compiler/encoders/arm7                                   6s   1GB
Oct 13 08:06:14 Starting compiler/encoders/arm8
Oct 13 08:06:22 Finished compiler/encoders/arm8                                   6s   1GB
Oct 13 08:06:23 Starting compiler/encoders/arm8_asl
Oct 13 08:06:47 Finished compiler/encoders/arm8_asl                              23s   1GB
Oct 13 08:06:48 Starting compiler/encoders/mips
Oct 13 08:06:55 Finished compiler/encoders/mips                                   6s   1GB
Oct 13 08:06:56 Starting compiler/encoders/riscv
Oct 13 08:07:04 Finished compiler/encoders/riscv                                  6s   1GB
Oct 13 08:07:05 Starting compiler/encoders/ag32
Oct 13 08:07:12 Finished compiler/encoders/ag32                                   6s   1GB
Oct 13 08:07:13 Starting compiler/encoders/tests
Oct 13 08:07:52 Finished compiler/encoders/tests                                 37s   1GB
Oct 13 08:07:53 Starting compiler/encoders/monadic_enc
Oct 13 08:08:19 Finished compiler/encoders/monadic_enc                           25s   1GB
Oct 13 08:08:20 Starting compiler/backend/x64
Oct 13 08:08:27 Finished compiler/backend/x64                                     6s   1GB
Oct 13 08:08:28 Starting compiler/backend/arm7
Oct 13 08:08:35 Finished compiler/backend/arm7                                    6s   1GB
Oct 13 08:08:36 Starting compiler/backend/arm8
Oct 13 08:08:44 Finished compiler/backend/arm8                                    6s   1GB
Oct 13 08:08:45 Starting compiler/backend/mips
Oct 13 08:08:52 Finished compiler/backend/mips                                    6s   1GB
Oct 13 08:08:53 Starting compiler/backend/riscv
Oct 13 08:09:01 Finished compiler/backend/riscv                                   6s   1GB
Oct 13 08:09:02 Starting compiler/backend/ag32
Oct 13 08:10:10 Finished compiler/backend/ag32                                 1m07s   1GB
Oct 13 08:10:11 Starting compiler/backend/pattern_matching
Oct 13 08:10:33 Finished compiler/backend/pattern_matching                       20s   1GB
Oct 13 08:10:34 Starting compiler/printing
Oct 13 08:11:35 Finished compiler/printing                                     1m00s   1GB
Oct 13 08:11:36 Starting compiler/parsing/proofs
Oct 13 08:11:44 Finished compiler/parsing/proofs                                  6s   1GB
Oct 13 08:11:45 Starting compiler/inference/proofs
Oct 13 08:11:53 Finished compiler/inference/proofs                                7s   1GB
Oct 13 08:11:54 Starting compiler/backend/semantics
Oct 13 08:15:21 Finished compiler/backend/semantics                            3m25s   3GB
Oct 13 08:15:22 Starting compiler/backend/reg_alloc/proofs
Oct 13 08:15:30 Finished compiler/backend/reg_alloc/proofs                        7s   1GB
Oct 13 08:15:31 Starting compiler/backend/proofs
Oct 13 08:16:21 Finished compiler/backend/proofs                                 49s   2GB
Oct 13 08:16:22 Starting compiler/backend/serialiser
Oct 13 08:16:29 Finished compiler/backend/serialiser                              6s   1GB
Oct 13 08:16:30 Starting compiler/encoders/x64/proofs
Oct 13 08:16:37 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 13 08:16:38 Starting compiler/encoders/arm7/proofs
Oct 13 08:29:38 Finished compiler/encoders/arm7/proofs                        12m58s   6GB
Oct 13 08:29:39 Starting compiler/encoders/arm8/proofs
Oct 13 08:42:04 Finished compiler/encoders/arm8/proofs                        12m24s  17GB
Oct 13 08:42:05 Starting compiler/encoders/arm8_asl/proofs
Oct 13 13:00:08 Resuming compiler/encoders/arm8_asl/proofs
Oct 13 13:00:15 Finished compiler/encoders/arm8_asl/proofs                        6s   1GB
Oct 13 13:00:16 Starting compiler/encoders/mips/proofs
Oct 13 13:12:06 Finished compiler/encoders/mips/proofs                        11m49s  11GB
Oct 13 13:12:07 Starting compiler/encoders/riscv/proofs
Oct 13 13:22:09 Finished compiler/encoders/riscv/proofs                       10m00s   3GB
Oct 13 13:22:10 Starting compiler/encoders/ag32/proofs
Oct 13 13:25:33 Finished compiler/encoders/ag32/proofs                         3m22s   2GB
Oct 13 13:25:34 Starting compiler/backend/x64/proofs
Oct 13 13:25:42 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 13 13:25:42 Starting compiler/backend/arm7/proofs
Oct 13 13:26:25 Finished compiler/backend/arm7/proofs                            41s   2GB
Oct 13 13:26:26 Starting compiler/backend/arm8/proofs
Oct 13 13:27:11 Finished compiler/backend/arm8/proofs                            44s   2GB
Oct 13 13:27:12 Starting compiler/backend/arm8_asl
Oct 13 13:27:55 Finished compiler/backend/arm8_asl                               42s   2GB
Oct 13 13:27:56 Starting compiler/backend/mips/proofs
Oct 13 13:28:47 Finished compiler/backend/mips/proofs                            49s   2GB
Oct 13 13:28:48 Starting compiler/backend/riscv/proofs
Oct 13 13:29:36 Finished compiler/backend/riscv/proofs                           47s   2GB
Oct 13 13:29:37 Starting compiler/backend/San
Oct 13 13:30:50 Finished compiler/backend/San                                  1m12s   4GB
Oct 13 13:30:51 Starting compiler/backend/ag32/proofs
Oct 13 13:40:32 Finished compiler/backend/ag32/proofs                          9m39s   4GB
Oct 13 13:40:33 Starting compiler/backend/cv_compute
Oct 13 13:41:08 Finished compiler/backend/cv_compute                             34s   1GB
Oct 13 13:41:09 Starting cv_translator
Oct 13 13:47:39 Finished cv_translator                                         6m28s   3GB
Oct 13 13:47:40 Starting candle
Oct 13 13:47:47 Finished candle                                                   6s   1GB
Oct 13 13:47:48 Starting candle/set-theory
Oct 13 13:48:10 Finished candle/set-theory                                       21s   1GB
Oct 13 13:48:11 Starting candle/syntax-lib
Oct 13 13:48:19 Finished candle/syntax-lib                                        6s   1GB
Oct 13 13:48:20 Starting candle/standard
Oct 13 13:48:27 Finished candle/standard                                          6s   1GB
Oct 13 13:48:28 Starting candle/standard/syntax
Oct 13 13:48:49 Finished candle/standard/syntax                                  20s   1GB
Oct 13 13:48:50 Starting candle/standard/syntax/little_theories
Oct 13 13:50:58 Finished candle/standard/syntax/little_theories                2m07s   1GB
Oct 13 13:50:59 Starting candle/standard/semantics
Oct 13 13:51:07 Finished candle/standard/semantics                                6s   1GB
Oct 13 13:51:08 Starting candle/standard/monadic
Oct 13 13:51:15 Finished candle/standard/monadic                                  6s   1GB
Oct 13 13:51:16 Starting candle/standard/ml_kernel
Oct 13 13:53:35 Finished candle/standard/ml_kernel                             2m17s   5GB
Oct 13 13:53:36 Starting candle/overloading
Oct 13 13:53:43 Finished candle/overloading                                       6s   1GB
Oct 13 13:53:44 Starting candle/overloading/syntax
Oct 13 13:57:06 Finished candle/overloading/syntax                             3m20s   2GB
Oct 13 13:57:07 Starting candle/overloading/semantics
Oct 13 14:05:35 Finished candle/overloading/semantics                          8m26s   3GB
Oct 13 14:05:36 Starting candle/overloading/monadic
Oct 13 14:07:44 Finished candle/overloading/monadic                            2m07s   1GB
Oct 13 14:07:45 Starting candle/overloading/ml_kernel
Oct 13 14:15:18 Finished candle/overloading/ml_kernel                          7m31s   5GB
Oct 13 14:15:18 Starting candle/overloading/ml_checker
Oct 13 14:17:25 Finished candle/overloading/ml_checker                         2m05s   6GB
Oct 13 14:17:26 Starting candle/prover
Oct 13 14:17:34 Finished candle/prover                                            6s   1GB
Oct 13 14:17:35 Starting candle/prover/compute
Oct 13 14:17:42 Finished candle/prover/compute                                    6s   1GB
Oct 13 14:17:43 Starting candle/parser
Oct 13 14:17:51 Finished candle/parser                                            6s   1GB
Oct 13 14:17:51 Starting pancake
Oct 13 14:17:59 Finished pancake                                                  6s   1GB
Oct 13 14:18:00 Starting pancake/semantics
Oct 13 14:21:22 Finished pancake/semantics                                     3m21s   2GB
Oct 13 14:21:23 Starting pancake/parser
Oct 13 14:22:11 Finished pancake/parser                                          46s   1GB
Oct 13 14:22:12 Starting pancake/static_checker
Oct 13 14:25:00 Finished pancake/static_checker                                2m46s   1GB
Oct 13 14:25:01 Starting pancake/proofs
Oct 13 14:42:09 Finished pancake/proofs                                       17m07s   5GB
Oct 13 14:42:10 Starting pancake/decompiler
Oct 13 14:43:05 Finished pancake/decompiler                                      54s   1GB
Oct 13 14:43:06 Starting pancake/decompiler/examples
Oct 13 14:43:53 Finished pancake/decompiler/examples                             45s   2GB
Oct 13 14:43:54 Starting compiler/dafny
Oct 13 14:44:23 Finished compiler/dafny                                          28s   1GB
Oct 13 14:44:24 Starting compiler/dafny/translation
Oct 13 14:56:27 Finished compiler/dafny/translation                           12m02s   7GB
Oct 13 14:56:28 Starting compiler/dafny/compilation
Oct 13 14:58:53 Finished compiler/dafny/compilation                            2m23s   6GB
Oct 13 14:58:54 Starting compiler/dafny/semantics
Oct 13 14:59:37 Finished compiler/dafny/semantics                                41s   1GB
Oct 13 14:59:38 Starting compiler/dafny/proofs
Oct 13 15:01:24 Finished compiler/dafny/proofs                                 1m45s   1GB
Oct 13 15:01:25 Starting compiler/dafny/vcg
Oct 13 15:01:33 Finished compiler/dafny/vcg                                       6s   1GB
Oct 13 15:01:34 Starting compiler/dafny/vcg/examples
Oct 13 15:02:09 Finished compiler/dafny/vcg/examples                             34s   1GB
Oct 13 15:02:10 Starting compiler/scheme
Oct 13 15:02:43 Finished compiler/scheme                                         32s   1GB
Oct 13 15:02:44 Starting compiler/scheme/translation
Oct 13 15:09:49 Finished compiler/scheme/translation                           7m04s   6GB
Oct 13 15:09:50 Starting compiler/scheme/compilation
Oct 13 15:11:43 Finished compiler/scheme/compilation                           1m51s   5GB
Oct 13 15:11:44 Starting compiler/scheme/proofs
Oct 13 15:18:47 Finished compiler/scheme/proofs                                7m01s   3GB
Oct 13 15:18:48 Starting characteristic/examples
Oct 13 15:20:07 FAILED: characteristic/examples
  HOLORIG=/scratch/regbox/regression/cakeml-3606/characteristic/examples [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
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/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/parser
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64/64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/32
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
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)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/decompiler
Scanning $(CAKEMLDIR)/pancake/decompiler/examples
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanning $(xlrup_checker)/array
Scanning $(xlrup_checker)/array/compilation
Scanning $(xlrup_checker)/array/compilation/proofs
Scanned 311 directories
Building 2 theory files
Starting work on README.md
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
README.md                                                   (0s)             OK
cf_tutorialTheory                                          (53s)   [1/2]     OK
cf_examplesTheory                                          (63s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** cf_examplesTheory (status 1)
 Saved theorem _______ "nsLookup_cf_examples_env_0_pfun_eqs"
 Proved triviality ___ "example_let1_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_1_pfun_eqs"
 Proved triviality ___ "example_let2_spec"
 Saved theorem _______ "nsLookup_cf_examples_env_2_pfun_eqs"
 Adding nsLookup representation thms for 612 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 9)) []))
 
 failed.
 Tactic failure proving "example_raise_spec"; heap saved to cf_examples.example_raise_spec.dumpedheap.
 Resume with: bin/hol --holstate=cf_examples.example_raise_spec.dumpedheap
 Full log: /scratch/regbox/regression/cakeml-3606/characteristic/examples/.hol/logs/cf_examplesTheory